From 78de786d89809706ce63bf955c6f4449b408872e Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 30 Nov 2022 11:05:06 -0500 Subject: [PATCH] Expanded lock invariant to give us access to shared segments of all ready TCBs. --- tasks.c | 27 ++++++----- .../verifast/proof/ready_list_predicates.h | 1 + .../verifast/proof/verifast_lock_predicates.h | 46 ++++++++++++++++--- 3 files changed, 57 insertions(+), 17 deletions(-) diff --git a/tasks.c b/tasks.c index fd6f74a94..f30596c92 100644 --- a/tasks.c +++ b/tasks.c @@ -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 { diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h index 8a0da795a..2c0f2a952 100644 --- a/verification/verifast/proof/ready_list_predicates.h +++ b/verification/verifast/proof/ready_list_predicates.h @@ -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); diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index 87bfba9af..68f6a6148 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -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 > itemLists) = - true; +// ∀owners ∈ gOwnerLists. ∀ow ∈ owners. sharedSeg_TCB_p(owner) +predicate owned_sharedSeg_TCBs_p(list > ownerLists) = + foreach(ownerLists, foreach_sharedSeg_TCB_p); + +// ∀ow ∈ owners. sharedSeg_TCB_p(owner) +predicate foreach_sharedSeg_TCB_p(list owners) = + foreach(owners, sharedSeg_TCB_p); + +lemma void open_owned_sharedSeg_TCBs(list > ownerLists, + list 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 > ownerLists, + list 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);