len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-12 06:35:19 -05:00
Code Issues Projects Releases Packages Wiki Activity

Added proof idea and TODOs. Need to refactor single-core list predicates.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-29 13:53:53 -05:00
parent e8b8234416
commit 22dc5c1287
3 changed files with 61 additions and 10 deletions
Download patch file Download diff file Expand all files Collapse all files

11
tasks.c
View file

@ -1033,10 +1033,15 @@ static void prvYieldForTask( TCB_t * pxTCB,
* must not be decremented any further */
xDecrementTopPriority = pdFALSE;
//@ mem_nth(uxCurrentPriority, gCellLists);
//@ assert( mem(gCells, gCellLists) == true);
//@ open_collection_of_sharedSeg_TCB(gCellLists, gCells);
do
/*@ invariant
mem(pxTaskItem, gCells) == true &*&
xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals);
xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals) &*&
foreach(gCells, sharedSeg_TCB_of_itemOwner);
@*/
{
TCB_t * pxTCB;
@ -1072,6 +1077,10 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ close xLIST_ITEM(gTaskItem_3, _, _, _, gReadyList);
//@ DLS_close_2(gTaskItem_3, gCells, gVals);
// Get access to sharedSeg_TCB_p(pxTCB).
//@ foreach_remove(gTaskItem_3, gCells);
//@ open sharedSeg_TCB_of_itemOwner(gTaskItem_3);
/*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */

15
verification/verifast/proof/ready_list_predicates.h
View file

@ -3,7 +3,15 @@
#include "single_core_proofs/scp_list_predicates.h"
/*@
// TODO: We know that the list of priority 0 is never empty.
// It contains the idle task and nothing else.
predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists) =
configMAX_PRIORITIES == length(gCellLists) &*&
List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, gCellLists);
predicate List_array_p(List_t* array, int size,
list<list<struct xLIST_ITEM*> > cellLists) =
size >= 0 &*&
@ -74,12 +82,7 @@ ensures
@*/
/*@
// TODO: We know that the list of priority 0 is never empty.
// It contains the idle task and nothing else.
predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists) =
List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, gCellLists);
@*/
/*@

45
verification/verifast/proof/verifast_lock_predicates.h
View file

@ -92,9 +92,11 @@ predicate taskISRLockInv_p() =
integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&
0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
&*&
readyLists_p(?gCellLists) &*&
true;
readyLists_p(?gCellLists)
&*&
// ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner)
//foreach(gCellLists, foreach_sharedSeg_TCB_of_itemOwner);
collection_of_sharedSeg_TCB_p(gCellLists);
lemma void produce_taskISRLockInv();
@ -110,6 +112,43 @@ lemma void consume_taskISRLockInv();
requires locked_p( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*&
taskISRLockInv_p();
ensures locked_p(otherLocks);
// ∀items ∈ itemLists. ∀it ∈ items. sharedSeg_TCB_p(it->pvOwner)
predicate collection_of_sharedSeg_TCB_p(list<list<struct xLIST_ITEM*> > itemLists) =
foreach(itemLists, foreach_sharedSeg_TCB_of_itemOwner);
// Auxiliary prediactes to express nested quantification
// ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner)
// TODO: Can we refactor this to make easier to understand?
// We cannot acces `item->pvOwner` without the necessary points-to chunk.
// TODO: Expose list of owners in ITEM and DLS predicates.
predicate sharedSeg_TCB_of_itemOwner(struct xLIST_ITEM* item) =
sharedSeg_TCB_p(item->pvOwner);
predicate foreach_sharedSeg_TCB_of_itemOwner(list<struct xLIST_ITEM*> items) =
foreach(items, sharedSeg_TCB_of_itemOwner);
lemma void open_collection_of_sharedSeg_TCB(list<list<struct xLIST_ITEM*> > itemLists,
list<struct xLIST_ITEM*> items)
requires
collection_of_sharedSeg_TCB_p(itemLists) &*&
mem(items, itemLists) == true;
ensures
collection_of_sharedSeg_TCB_p(remove(items, itemLists)) &*&
foreach(items, sharedSeg_TCB_of_itemOwner);
{
open collection_of_sharedSeg_TCB_p(itemLists);
foreach_remove(items, itemLists);
open foreach_sharedSeg_TCB_of_itemOwner(items);
close collection_of_sharedSeg_TCB_p(remove(items, itemLists));
}
// TODO: Add closing lemma
@*/