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

Expanded lock invariant to give us access to shared segments of all ready TCBs.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-30 11:05:06 -05:00
parent e800ebd293
commit 78de786d89
3 changed files with 57 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

27
tasks.c
View file

@ -993,6 +993,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ List_t* gReadyList = &pxReadyTasksLists[uxCurrentPriority];
//@ assert( xLIST(gReadyList, ?gSize, ?gIndex, ?gEnd, ?gCells, ?gVals, ?gOwners) );
//@ assert( mem(gOwners, gOwnerLists) == true );
//@ open xLIST(gReadyList, _, _, _, _, _, _);
if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
@ -1035,14 +1036,15 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ mem_nth(uxCurrentPriority, gCellLists);
//@ assert( mem(gCells, gCellLists) == true);
// //@ open_collection_of_sharedSeg_TCB(gCellLists, gCells);
// Get access to `sharedSeg_TCB_p` predicates of current ready list.
//@ open_owned_sharedSeg_TCBs(gOwnerLists, gOwners);
do
/*@ invariant
mem(pxTaskItem, gCells) == true &*&
xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
// foreach(gCells, sharedSeg_TCB_of_itemOwner);
true;
foreach(gOwners, sharedSeg_TCB_p);
@*/
{
TCB_t * pxTCB;
@ -1071,17 +1073,18 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ DLS_close_2(gTaskItem_1, gCells, gVals, gOwners);
}
//@ struct xLIST_ITEM* gTaskItem_3 = pxTaskItem;
//@ struct xLIST_ITEM* gTaskItem_final = pxTaskItem;
//@ DLS_open_2(gTaskItem_3);
//@ DLS_open_2(gTaskItem_final);
pxTCB = pxTaskItem->pvOwner;
//@ close xLIST_ITEM(gTaskItem_3, _, _, _, _, gReadyList);
//@ DLS_close_2(gTaskItem_3, gCells, gVals, gOwners);
// Get access to sharedSeg_TCB_p(pxTCB).
// //@ foreach_remove(gTaskItem_3, gCells);
// //@ open sharedSeg_TCB_of_itemOwner(gTaskItem_3);
/*@ close xLIST_ITEM(gTaskItem_final, _, _, _,
pxTCB, gReadyList);
@*/
//@ DLS_close_2(gTaskItem_final, gCells, gVals, gOwners);
// Getting access to fields of `pxTCB`
//@ foreach_remove(pxTCB, gOwners);
//@ open sharedSeg_TCB_p(pxTCB);
/*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */
@ -1142,6 +1145,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
break;
}
} while( pxTaskItem != pxLastTaskItem );
//@ close_owned_sharedSeg_TCBs(gOwnerLists, gOwners);
}
else
{

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

@ -59,6 +59,7 @@ ensures
xLIST(array + index, _, _, _, ?gCells, ?gVals, ?gOwners) &*&
gCells == nth(index, gCellLists) &*&
gOwners == nth(index, gOwnerLists) &*&
mem(gOwners, gOwnerLists) == true &*&
List_array_p(array + index + 1, gSize-index-1, ?gSufCellLists, ?gSufOwnerLists) &*&
gSufCellLists == drop(index+1, gCellLists) &*&
gSufOwnerLists == drop(index+1, gOwnerLists);

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

@ -94,9 +94,8 @@ predicate taskISRLockInv_p() =
&*&
readyLists_p(?gCellLists, ?gOwnerLists)
&*&
// ∀gCells ∈ gCellLists. ∀item ∈ gCells. sharedSeg_TCB_p(item->pvOwner)
//foreach(gCellLists, foreach_sharedSeg_TCB_of_itemOwner);
collection_of_sharedSeg_TCB_p(gCellLists);
// ∀owners ∈ gOwnerLists. ∀ow ∈ owners. sharedSeg_TCB_p(owner)
owned_sharedSeg_TCBs_p(gOwnerLists);
lemma void produce_taskISRLockInv();
@ -115,10 +114,45 @@ 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) =
true;
// ∀owners ∈ gOwnerLists. ∀ow ∈ owners. sharedSeg_TCB_p(owner)
predicate owned_sharedSeg_TCBs_p(list<list<void*> > ownerLists) =
foreach(ownerLists, foreach_sharedSeg_TCB_p);
// ∀ow ∈ owners. sharedSeg_TCB_p(owner)
predicate foreach_sharedSeg_TCB_p(list<void*> owners) =
foreach(owners, sharedSeg_TCB_p);
lemma void open_owned_sharedSeg_TCBs(list<list<void*> > ownerLists,
list<void*> owners)
requires
owned_sharedSeg_TCBs_p(ownerLists) &*&
mem(owners, ownerLists) == true;
ensures
owned_sharedSeg_TCBs_p(remove(owners, ownerLists)) &*&
foreach(owners, sharedSeg_TCB_p);
{
open owned_sharedSeg_TCBs_p(ownerLists);
foreach_remove(owners, ownerLists);
close owned_sharedSeg_TCBs_p(remove(owners, ownerLists));
open foreach_sharedSeg_TCB_p(owners);
}
lemma void close_owned_sharedSeg_TCBs(list<list<void*> > ownerLists,
list<void*> owners)
requires
owned_sharedSeg_TCBs_p(remove(owners, ownerLists)) &*&
foreach(owners, sharedSeg_TCB_p) &*&
mem(owners, ownerLists) == true;
ensures
owned_sharedSeg_TCBs_p(ownerLists);
{
close foreach_sharedSeg_TCB_p(owners);
open owned_sharedSeg_TCBs_p(remove(owners, ownerLists));
foreach_unremove(owners, ownerLists);
close owned_sharedSeg_TCBs_p(ownerLists);
}
@*/
/*
foreach(itemLists, foreach_sharedSeg_TCB_of_itemOwner);