From fe5612cf4fcce0ac34e24187c014e778acafc995 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Wed, 30 Nov 2022 15:52:00 -0500 Subject: [PATCH] Extended lock invariants to justify safe access to ready tasks as well as scheduled task. --- tasks.c | 93 ++++++++++++++-- .../verifast/proof/verifast_lists_extended.h | 24 +++-- .../verifast/proof/verifast_lock_predicates.h | 100 +++++++++++------- 3 files changed, 166 insertions(+), 51 deletions(-) diff --git a/tasks.c b/tasks.c index f30596c92..553e4d9e4 100644 --- a/tasks.c +++ b/tasks.c @@ -907,7 +907,7 @@ static void prvYieldForTask( TCB_t * pxTCB, taskISRLockInv_p() &*& // opened predicate `coreLocalInterruptInv_p()` - pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& + [0.5]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& coreLocalSeg_TCB_p(gCurrentTCB, 0) &*& @@ -960,7 +960,7 @@ static void prvYieldForTask( TCB_t * pxTCB, taskISRLockInv_p() &*& // opened predicate `coreLocalInterruptInv_p()` - pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& + [0.5]pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& // pubTCB_p(gCurrentTCB, 0) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& coreLocalSeg_TCB_p(gCurrentTCB, 0) @@ -987,6 +987,16 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif //@ open taskISRLockInv_p(); + //@ assert( valid_sharedSeg_TCBs_p(?gTaskLists) ); + + // Eliminates exists predicate to avoid pattern matching conflicts + //@ open exists(gTaskLists); + + // Get list containing currentTCB and ensure we matched the right variable + //@ assert( exists(?gCurrentTCB_category) ); + //@ assert( mem(gCurrentTCB, gCurrentTCB_category) == true ); + + //@ open readyLists_p(?gCellLists, ?gOwnerLists); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_split(pxReadyTasksLists, uxCurrentPriority); @@ -1037,14 +1047,27 @@ static void prvYieldForTask( TCB_t * pxTCB, //@ mem_nth(uxCurrentPriority, gCellLists); //@ assert( mem(gCells, gCellLists) == true); - // Get access to `sharedSeg_TCB_p` predicates of current ready list. - //@ open_owned_sharedSeg_TCBs(gOwnerLists, gOwners); + // Prove that `mem(gOwners, gTaskLists) == true` + // Necessary to get access to `sharedSeg_TCB_p` predicates of + // current ready list in the loop + //@ assert( mem(gOwners, gOwnerLists) == true ); + //@ assert( forall(gOwnerLists, (mem_list_elem)(gTaskLists) ) == true ); + //@ forall_instantiate(gOwners, gOwnerLists, (mem_list_elem)(gTaskLists)); + //@ assert( mem(gOwners, gTaskLists) == true ); + ///@ open_valid_sharedSeg_TCBs(gTaskLists, gOwners); do /*@ invariant + 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& + xCoreID == coreID_f() &*& + pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& mem(pxTaskItem, gCells) == true &*& xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& - foreach(gOwners, sharedSeg_TCB_p); +// foreach(gOwners, sharedSeg_TCB_p); + valid_sharedSeg_TCBs_p(gTaskLists) &*& + mem(gOwners, gTaskLists) == true &*& + mem(gCurrentTCB, gCurrentTCB_category) == true &*& + mem(gCurrentTCB_category, gTaskLists) == true; @*/ { TCB_t * pxTCB; @@ -1083,6 +1106,7 @@ static void prvYieldForTask( TCB_t * pxTCB, //@ DLS_close_2(gTaskItem_final, gCells, gVals, gOwners); // Getting access to fields of `pxTCB` + //@ open_valid_sharedSeg_TCBs(gTaskLists, gOwners); //@ foreach_remove(pxTCB, gOwners); //@ open sharedSeg_TCB_p(pxTCB); @@ -1111,6 +1135,33 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif #endif { + //@ assert( foreach(remove(pxTCB, gOwners), sharedSeg_TCB_p) ); + //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] ); + /*@ + if( gCurrentTCB == pxTCB ) { + // We can use the opened `sharedSeg_TCB_p` chunk + // for `pxTCB`. + } else { + if( gCurrentTCB_category == gOwners ) { + // `gCurrentTCB` is different from `pxTCB` but + // they belong to the same ready list. + + assert( mem(gCurrentTCB, gOwners) == true ); + mem_after_remove(gCurrentTCB, gOwners, pxTCB); + assert( mem(gCurrentTCB, remove(pxTCB, gOwners)) == true ); + foreach_remove(gCurrentTCB, remove(pxTCB, gOwners)); + } else { + assert( mem(gCurrentTCB_category, gTaskLists) == true ); + mem_after_remove(gCurrentTCB_category, gTaskLists, gOwners); + assert( mem(gCurrentTCB_category, remove(gOwners, gTaskLists)) == true ); + open_valid_sharedSeg_TCBs(remove(gOwners, gTaskLists), + gCurrentTCB_category); + foreach_remove(gCurrentTCB, gCurrentTCB_category); + } + + open sharedSeg_TCB_p(gCurrentTCB); + } + @*/ /* If the task is not being executed by any core swap it in */ pxCurrentTCBs[ xCoreID ]->xTaskRunState = taskTASK_NOT_RUNNING; #if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) ) @@ -1119,6 +1170,36 @@ static void prvYieldForTask( TCB_t * pxTCB, pxTCB->xTaskRunState = ( TaskRunning_t ) xCoreID; pxCurrentTCBs[ xCoreID ] = pxTCB; xTaskScheduled = pdTRUE; + + /*@ + if( gCurrentTCB == pxTCB ) { + // We can used the opened `sharedSeg_TCB_p` chunk + // for `pxTCB`. + // => We don't have to close anything. + } else { + // Above, we extracted `sharedSeg_TCB_p(gCurrentTCB)` + // from the collection of all remaining shared TCB + // segments and opened it. + // => Close predicate and restore collection. + + close sharedSeg_TCB_p(gCurrentTCB); + + if( gCurrentTCB_category == gOwners ) { + // `gCurrentTCB` is different from `pxTCB` but + // they belong to the same ready list. + + foreach_unremove(gCurrentTCB, remove(pxTCB, gOwners)); + } else { + foreach_unremove(gCurrentTCB, gCurrentTCB_category); + close_valid_sharedSeg_TCBs(remove(gOwners, gTaskLists), + gCurrentTCB_category); + } + } + @*/ + + // Ensure we restored the collection as it was + // at the beginning of the block. + //@ assert( foreach(remove(pxTCB, gOwners), sharedSeg_TCB_p) ); } } else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) @@ -1146,7 +1227,7 @@ static void prvYieldForTask( TCB_t * pxTCB, } } while( pxTaskItem != pxLastTaskItem ); - //@ close_owned_sharedSeg_TCBs(gOwnerLists, gOwners); + //@ close_valid_sharedSeg_TCBs(gOwnerLists, gOwners); } else { diff --git a/verification/verifast/proof/verifast_lists_extended.h b/verification/verifast/proof/verifast_lists_extended.h index e2879c352..70bd5d6f4 100644 --- a/verification/verifast/proof/verifast_lists_extended.h +++ b/verification/verifast/proof/verifast_lists_extended.h @@ -8,7 +8,7 @@ -// TODO: prove +// TODO: Can we prove this in VeriFast or do we have to axiomatise? /*@ lemma void head_drop_n_equals_nths(list xs, int n) requires n >= 0; @@ -32,7 +32,7 @@ ensures head(drop(n, xs)) == nth(n, xs); assume(false); } -// TODO: prove +// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void drop_index_equals_singleton_implies_last_element(list xs, t x) requires drop(index_of(x, xs), xs) == cons(x, nil); ensures index_of(x, xs) == length(xs) - 1; @@ -50,7 +50,7 @@ ensures index_of(x, xs) == length(xs) - 1; assume(false); } -// TODO: prove +// TODO: Can we prove this in VeriFast or do we have to axiomatise? // Can we replace this by standard lemma `drop_n_plus_one`? lemma void drop_cons(list xs, int n) requires n < length(xs); @@ -70,7 +70,7 @@ ensures drop(n, xs) == cons(nth(n, xs), drop(n+1, xs)); assume(false); } -// TODO: prove +// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void nth_index(list xs, t x) requires mem(x, xs) == true; ensures nth(index_of(x, xs), xs) == x; @@ -88,12 +88,12 @@ ensures nth(index_of(x, xs), xs) == x; assume(false); } -// TODO: prove +// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void mem_prefix_implies_mem(t x, list xs, int n); requires mem(x, take(n, xs)) == true; ensures mem(x, xs) == true; -// TODO: prove +// TODO: Can we prove this in VeriFast or do we have to axiomatise? lemma void mem_suffix_implies_mem(t x, list xs, int n); requires mem(x, drop(n, xs)) == true; ensures mem(x, xs) == true; @@ -102,6 +102,18 @@ ensures mem(x, xs) == true; lemma void drop_n_plus_m(list xs, int n, int m); requires true; ensures drop(n, drop(m, xs)) == drop(n + m, xs); + + +// TODO: Can we prove this in VeriFast or do we have to axiomatise? +lemma void forall_instantiate(t x, list xs, fixpoint(t, bool) f); +requires forall(xs, f) == true &*& mem(x, xs) == true; +ensures forall(xs, f) == true &*& f(x) == true; + + +// TODO: Can we prove this in VeriFast or do we have to axiomatise? +lemma void mem_after_remove(t x, list xs, t r); +requires true; +ensures mem(x, remove(r, xs)) == (mem(x, xs) && x != r); @*/ diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index 68f6a6148..9372b2b5f 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -28,7 +28,7 @@ predicate interruptState_p(uint32_t coreID, uint32_t state); fixpoint bool interruptsDisabled_f(uint32_t); predicate coreLocalInterruptInv_p() = - pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*& + [0.5]pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*& //pubTCB_p(currentTCB, 0) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*& coreLocalSeg_TCB_p(currentTCB, ?gCriticalNesting); @@ -85,17 +85,29 @@ predicate isrLockInv_p(); fixpoint int taskISRLockID_f(); predicate taskISRLockInv_p() = - integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*& - integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _) + // Access to global variables + [0.5]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& + integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*& + integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _) &*& // top ready priority must be in range integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*& 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES &*& - readyLists_p(?gCellLists, ?gOwnerLists) - &*& - // ∀owners ∈ gOwnerLists. ∀ow ∈ owners. sharedSeg_TCB_p(owner) - owned_sharedSeg_TCBs_p(gOwnerLists); + // tasks / TCBs + exists > >(?gTaskLists) + &*& + // ∀l ∈ gTaskLists. ∀t ∈ l. sharedSeg_TCB_p(l) + valid_sharedSeg_TCBs_p(gTaskLists) + &*& + readyLists_p(?gCellLists, ?gOwnerLists) + &*& + // gOwnerLists ⊆ gTaskLists + forall(gOwnerLists, (mem_list_elem)(gTaskLists)) == true + &*& + exists >(?gCurrentTCB_category) &*& + mem(gCurrentTCB_category, gTaskLists) == true &*& + mem(gCurrentTCB, gCurrentTCB_category) == true; lemma void produce_taskISRLockInv(); @@ -113,43 +125,53 @@ requires locked_p( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*& ensures locked_p(otherLocks); - -// ∀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); +// Auxiliary function that allows us to partially apply the list argument. +// +// Notes: +// - Partial application of fixpoint functions in VeriFast is not documented. +// The syntax for partially application is `()()` +// - VeriFast only supports partially applying the first argument, e.g., +// `(mem)(0)` is allowed but `(mem)(_)(nil)` is not. +fixpoint bool mem_list_elem(list xs, t x) { + return mem(x, xs); } -lemma void close_owned_sharedSeg_TCBs(list > ownerLists, - list owners) +// l ∈ taskLists. ∀t ∈ tasks. sharedSeg_TCB_p(t) +predicate valid_sharedSeg_TCBs_p(list > taskLists) = + foreach(taskLists, foreach_sharedSeg_TCB_p); + +// ∀t ∈ tasks. sharedSeg_TCB_p(t) +predicate foreach_sharedSeg_TCB_p(list tasks) = + foreach(tasks, sharedSeg_TCB_p); + +lemma void open_valid_sharedSeg_TCBs(list > taskLists, + list tasks) requires - owned_sharedSeg_TCBs_p(remove(owners, ownerLists)) &*& - foreach(owners, sharedSeg_TCB_p) &*& - mem(owners, ownerLists) == true; + valid_sharedSeg_TCBs_p(taskLists) &*& + mem(tasks, taskLists) == true; ensures - owned_sharedSeg_TCBs_p(ownerLists); + valid_sharedSeg_TCBs_p(remove(tasks, taskLists)) &*& + foreach(tasks, sharedSeg_TCB_p); { - close foreach_sharedSeg_TCB_p(owners); - open owned_sharedSeg_TCBs_p(remove(owners, ownerLists)); - foreach_unremove(owners, ownerLists); - close owned_sharedSeg_TCBs_p(ownerLists); + open valid_sharedSeg_TCBs_p(taskLists); + foreach_remove(tasks, taskLists); + close valid_sharedSeg_TCBs_p(remove(tasks, taskLists)); + open foreach_sharedSeg_TCB_p(tasks); +} + +lemma void close_valid_sharedSeg_TCBs(list > taskLists, + list tasks) +requires + valid_sharedSeg_TCBs_p(remove(tasks, taskLists)) &*& + foreach(tasks, sharedSeg_TCB_p) &*& + mem(tasks, taskLists) == true; +ensures + valid_sharedSeg_TCBs_p(taskLists); +{ + close foreach_sharedSeg_TCB_p(tasks); + open valid_sharedSeg_TCBs_p(remove(tasks, taskLists)); + foreach_unremove(tasks, taskLists); + close valid_sharedSeg_TCBs_p(taskLists); } @*/