From dda2dbda6f020a22f699b8eba8c8381e4be01163 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Sat, 3 Dec 2022 10:04:04 -0500 Subject: [PATCH] Added states list to lock invariant. --- tasks.c | 15 +++++---- verification/verifast/proof/task_predicates.h | 8 ++--- .../verifast/proof/verifast_lock_predicates.h | 32 +++++++++++++++---- 3 files changed, 37 insertions(+), 18 deletions(-) diff --git a/tasks.c b/tasks.c index 067c66460..ea8bbeb26 100644 --- a/tasks.c +++ b/tasks.c @@ -988,7 +988,7 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif //@ open taskISRLockInv_p(); - //@ assert( exists_in_taskISRLockInv_p(?gTasks) ); + //@ assert( exists_in_taskISRLockInv_p(?gTasks, ?gStates) ); //@ open readyLists_p(?gCellLists, ?gOwnerLists); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); @@ -1052,10 +1052,14 @@ static void prvYieldForTask( TCB_t * pxTCB, xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& gSize > 0 &*& // Read permissions for every task - foreach(gTasks, readOnly_sharedSeg_TCB_p) + foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) &*& // Write permission for task scheduled on this core - [1/2]sharedSeg_TCB_p(gCurrentTCB) + [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) + &*& + // TODO: + // Write permissions for unscheduled tasks + true &*& subset(gOwners, gTasks) == true; @@ -1107,7 +1111,6 @@ static void prvYieldForTask( TCB_t * pxTCB, //@ assert( subset(gOwners, gTasks) == true ); //@ mem_subset(pxTCB, gOwners, gTasks); //@ foreach_remove(pxTCB, gTasks); - //@ open sharedSeg_TCB_p(pxTCB); /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ @@ -1134,7 +1137,7 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif #endif { - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] ); /*@ if( gCurrentTCB == pxTCB ) { @@ -1168,7 +1171,7 @@ static void prvYieldForTask( TCB_t * pxTCB, // Ensure we restored the collection as it was // at the beginning of the block. - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); } } else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) diff --git a/verification/verifast/proof/task_predicates.h b/verification/verifast/proof/task_predicates.h index ee17bad1f..ebd37d71c 100644 --- a/verification/verifast/proof/task_predicates.h +++ b/verification/verifast/proof/task_predicates.h @@ -108,12 +108,8 @@ predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) = stack_p_2(stackPtr, ?ulStackDepth, topPtr, ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes); -predicate sharedSeg_TCB_p(TCB_t* tcb;) = - tcb->xTaskRunState |-> ?gTaskRunState; - -// Auxiliary predicate to allow foreach-quantification about fraction -predicate readOnly_sharedSeg_TCB_p(TCB_t* tcb;) = - [1/2]sharedSeg_TCB_p(tcb); +predicate sharedSeg_TCB_p(TCB_t* tcb, TaskRunning_t state;) = + tcb->xTaskRunState |-> state; predicate coreLocalSeg_TCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) = tcb->uxCriticalNesting |-> uxCriticalNesting; diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index 88017fa40..e66dc0096 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -95,15 +95,24 @@ predicate taskISRLockInv_p() = 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES &*& // tasks / TCBs - exists_in_taskISRLockInv_p(?gTasks) + exists_in_taskISRLockInv_p(?gTasks, ?gStates) &*& // (RP-All) Read permissions for every task - // ∀t ∈ gTasks. [1/2]sharedSeg_TCB_p(t) - foreach(gTasks, readOnly_sharedSeg_TCB_p) + // and recording of task states in state list + // (∀t ∈ gTasks. + // [1/2]sharedSeg_TCB_p(t, _)) + // ∧ + // ∀i. ∀t. gTasks[i] == t -> gStates[i] == t->xTaskRunState + foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) &*& // (RP-Current) Read permission for task currently scheduled on this core // (RP-All) + (RP-Current) => Write permission for scheduled task - [1/2]sharedSeg_TCB_p(gCurrentTCB) + [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) + &*& + // TODO: + // (RP-Unsched) Read permissions for unscheduled tasks + // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks + true &*& readyLists_p(?gCellLists, ?gOwnerLists) &*& @@ -133,8 +142,11 @@ ensures locked_p(otherLocks); // Auxiliary predicate to assing names to existentially quantified variables. // Having multiple `exists` chunks on the heap makes matching against their // arguments ambiguous in most cases. -predicate exists_in_taskISRLockInv_p(list gTasks) = - exists(gTasks); +predicate exists_in_taskISRLockInv_p(list gTasks, + list gStates) = + exists(gTasks) &*& + exists(gStates) &*& + length(gTasks) == length(gStates); // Auxiliary function that allows us to partially apply the list argument. // @@ -146,6 +158,14 @@ predicate exists_in_taskISRLockInv_p(list gTasks) = fixpoint bool mem_list_elem(list xs, t x) { return mem(x, xs); } + +// Auxiliary predicate to allow foreach-quantification about fraction +// and reflection of `t->xTaskRunState` in state list. +predicate_ctor readOnly_sharedSeg_TCB_p + (list tasks, list states) + (TCB_t* t;) = + mem(t, tasks) == true &*& + [1/2]sharedSeg_TCB_p(t, nth(index_of(t, tasks), states)); @*/