From 0df45b465e3c1e80f02a95e3083cf0b6843f8dd2 Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Sat, 3 Dec 2022 14:54:26 -0500 Subject: [PATCH] Added lemmas that allow updating the lock invariant after a state update. --- tasks.c | 92 ++++++++++--- .../verifast/proof/verifast_lists_extended.h | 55 ++++++++ .../verifast/proof/verifast_lock_predicates.h | 126 +++++++++++++++++- 3 files changed, 247 insertions(+), 26 deletions(-) diff --git a/tasks.c b/tasks.c index ea8bbeb26..577afa43a 100644 --- a/tasks.c +++ b/tasks.c @@ -1051,6 +1051,8 @@ static void prvYieldForTask( TCB_t * pxTCB, mem(pxTaskItem, gCells) == true &*& xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& gSize > 0 &*& + exists_in_taskISRLockInv_p(gTasks, gStates) + &*& // Read permissions for every task foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) &*& @@ -1059,7 +1061,7 @@ static void prvYieldForTask( TCB_t * pxTCB, &*& // TODO: // Write permissions for unscheduled tasks - true + foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) &*& subset(gOwners, gTasks) == true; @@ -1107,10 +1109,12 @@ static void prvYieldForTask( TCB_t * pxTCB, @*/ //@ DLS_close_2(gTaskItem_final, gCells, gVals, gOwners); - // Getting access to fields of `pxTCB` + // Getting read access to fields of `pxTCB` + // aka first half of write permission //@ assert( subset(gOwners, gTasks) == true ); //@ mem_subset(pxTCB, gOwners, gTasks); //@ foreach_remove(pxTCB, gTasks); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ @@ -1139,17 +1143,64 @@ static void prvYieldForTask( TCB_t * pxTCB, { //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] ); - /*@ - if( gCurrentTCB == pxTCB ) { - // We can use the opened `sharedSeg_TCB_p` chunk - // for `pxTCB`. - } else { - neq_mem_remove(gCurrentTCB, pxTCB, gTasks); - foreach_remove(gCurrentTCB, remove(pxTCB, gTasks)); - } - @*/ + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + + /* We could reuse the read permission to `pxTCB` we extracted before the if statement. + * But putting permissions back as soon as we no longer need them simplifies the + * proof state and elimintates case-splits in the proof. + */ + + // Put read permission for `pxTCB` back + //@ close [1/2]sharedSeg_TCB_p(pxTCB, _); + //@ close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB); + //@ foreach_unremove(pxTCB, gTasks); + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + + // Get 2nd half of write permission for `gCurrentTCB` + //@ foreach_remove(gCurrentTCB, gTasks); + //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + + //@ int gCurrentTCB_index = index_of(gCurrentTCB, gTasks); + /*@ list gStates1 = + update(gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates); + @*/ + /* If the task is not being executed by any core swap it in */ pxCurrentTCBs[ xCoreID ]->xTaskRunState = taskTASK_NOT_RUNNING; + + //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + + //@ open exists_in_taskISRLockInv_p(gTasks, gStates); + + /*@ close_updated_foreach_readOnly_sharedSeg_TCB + (gCurrentTCB, gTasks, gStates, + gStates1, taskTASK_NOT_RUNNING); + @*/ + +//@ assume(false); + /*@ list gStates2 = + update(gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates); + @*/ + + // If we acquired an additional second half of a + // write permission for `gCurrentTCB`, release it. + /*@ + if( gCurrentTCB == pxTCB ) { + // We used the opened `sharedSeg_TCB_p` chunk + // for `pxTCB`. + // => We don't have to close anything. + } else { + close sharedSeg_TCB_p(gCurrentTCB, taskTASK_NOT_RUNNING); + assert( gCurrentTCB_index < length(gTasks) ); + assert( gCurrentTCB_index < length(gStates) ); + // nonauto_nth_update(gCurrentTCB_index, gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates); + // assert( taskTASK_NOT_RUNNING == nth(gCurrentTCB_index, gStates2) ); + assume( taskTASK_NOT_RUNNING == nth(gCurrentTCB_index, gStates2) ); + close readOnly_sharedSeg_TCB_p(gTasks, gStates2)(gCurrentTCB); + foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks)); + } + @*/ + #if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) ) pxPreviousTCB = pxCurrentTCBs[ xCoreID ]; #endif @@ -1157,21 +1208,18 @@ static void prvYieldForTask( TCB_t * pxTCB, pxCurrentTCBs[ xCoreID ] = pxTCB; xTaskScheduled = pdTRUE; - /*@ - if( gCurrentTCB == pxTCB ) { - // We used the opened `sharedSeg_TCB_p` chunk - // for `pxTCB`. - // => We don't have to close anything. - } else { - close sharedSeg_TCB_p(gCurrentTCB); - close readOnly_sharedSeg_TCB_p(gCurrentTCB); - foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks)); - } - @*/ + + + + + + // Release second half of write permission for `pxTCB` + //@ foreach_unremove(pxTCB, gTasks); // Ensure we restored the collection as it was // at the beginning of the block. //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); } } else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) diff --git a/verification/verifast/proof/verifast_lists_extended.h b/verification/verifast/proof/verifast_lists_extended.h index 0c5450ad1..23080910c 100644 --- a/verification/verifast/proof/verifast_lists_extended.h +++ b/verification/verifast/proof/verifast_lists_extended.h @@ -121,6 +121,61 @@ ensures mem(x, remove(r, xs)) == (mem(x, xs) && x != r); fixpoint bool superset(list super, list sub) { return subset(sub, super); } + + +// TODO: Can we prove this in VeriFast or do we have to axiomatise? +lemma void update_out_of_bounds(int index, t x, list xs) +requires (index < 0 || index >= length(xs)); +ensures update(index, x, xs) == xs; +{ + switch(xs) { + case nil: // nothing to do + case cons(h, rest): { + update_out_of_bounds(index-1, x, rest); + } + } +} + + +lemma void index_of_different(t x1, t x2, list xs) +requires x1 != x2 &*& mem(x1, xs) == true &*& mem(x2, xs) == true; +ensures index_of(x1, xs) != index_of(x2, xs); +{ + switch(xs) { + case nil: + case cons(h, rest): + if(h != x1 && h != x2) { + index_of_different(x1, x2, rest); + } + } +} + +// TODO: Can we prove this in VeriFast or do we have to axiomatise? +lemma void subset_cons_tail(list xs); +requires xs == cons(?h, ?t); +ensures subset(t, xs) == true; + +// TODO: Can we prove this in VeriFast or do we have to axiomatise? +lemma void remove_result_subset(t x, list xs); +requires true; +ensures subset(remove(x, xs), xs) == true; +// TODO: Revisit this lemma +// { +// switch(xs) { +// case nil: +// case cons(h, t): +// remove_result_subset(x, t); +// if(h == x) { +// assert( remove(x, xs) == t ); +// subset_cons_tail(xs); +// assert( subset(t, cons(x, t) ) == true ); +// } else { +// ; +// } +// } +// } + + @*/ diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index e66dc0096..27f4b2388 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -1,7 +1,7 @@ #ifndef VERIFAST_LOCK_PREDICATES_H #define VERIFAST_LOCK_PREDICATES_H - +#include "verifast_task_running_states.h" /* We follow a minimalistic approach during the definition of the @@ -11,7 +11,7 @@ * other parts of FRTOS. */ - +#include "verifast_lists_extended.h" @@ -112,7 +112,9 @@ predicate taskISRLockInv_p() = // TODO: // (RP-Unsched) Read permissions for unscheduled tasks // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks - true + // ∀t ∈ tasks. t->xTaskState == taskTASK_NOT_RUNNING + // -> [1/2]shared_TCB_p(t, taskTASK_NOT_RUNNING) + foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) &*& readyLists_p(?gCellLists, ?gOwnerLists) &*& @@ -146,7 +148,8 @@ predicate exists_in_taskISRLockInv_p(list gTasks, list gStates) = exists(gTasks) &*& exists(gStates) &*& - length(gTasks) == length(gStates); + length(gTasks) == length(gStates) &*& + distinct(gTasks) == true; // Auxiliary function that allows us to partially apply the list argument. // @@ -166,10 +169,125 @@ predicate_ctor readOnly_sharedSeg_TCB_p (TCB_t* t;) = mem(t, tasks) == true &*& [1/2]sharedSeg_TCB_p(t, nth(index_of(t, tasks), states)); + +predicate_ctor readOnly_sharedSeg_TCB_IF_not_running_p + (list tasks, list states) + (TCB_t* t;) = + mem(t, tasks) == true &*& + nth(index_of(t, tasks), states) == taskTASK_NOT_RUNNING + ? [1/2]sharedSeg_TCB_p(t, taskTASK_NOT_RUNNING) + : true; +@*/ + + + +/*@ +lemma void nonauto_nth_update(int i, int j, t y, list xs); + requires 0 <= i && i < length(xs) && 0 <= j && j < length(xs); + ensures nth(i, update(j, y, xs)) == (i == j ? y : nth(i, xs)); +@*/ + + + +/*@ +lemma void update_readOnly_sharedSeg_TCB(TCB_t* t, + list tasks, + list states, + int updatedIndex, + TaskRunning_t s) +requires readOnly_sharedSeg_TCB_p(tasks, states)(t) &*& + updatedIndex != index_of(t, tasks) &*& + mem(t, tasks) == true &*& + length(tasks) == length(states); +ensures readOnly_sharedSeg_TCB_p(tasks, update(updatedIndex, s, states))(t); +{ + list states2 = update(updatedIndex, s, states); + int t_index = index_of(t, tasks); + + if( updatedIndex < 0 || updatedIndex >= length(states) ) { + update_out_of_bounds(updatedIndex, s, states); + } else { + open readOnly_sharedSeg_TCB_p(tasks, states)(t); + open [1/2]sharedSeg_TCB_p(t, nth(t_index, states)); + + mem_index_of(t, tasks); + nth_update(t_index, updatedIndex, s, states); + assert( nth(t_index, states) == nth(t_index, states2) ); + + close [1/2]sharedSeg_TCB_p(t, nth(t_index, states2)); + close readOnly_sharedSeg_TCB_p(tasks, states2)(t); + } +} + + +lemma void update_foreach_readOnly_sharedSeg_TCB(TCB_t* updatedTask, + list tasks, + list subTasks, + list states, + list states2, + TaskRunning_t s) +requires + mem(updatedTask, tasks) == true &*& + length(tasks) == length(states) &*& + foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states)) &*& + states2 == update(index_of(updatedTask, tasks), s, states) &*& + distinct(tasks) == true &*& + mem(updatedTask, subTasks) == false &*& + subset(subTasks, tasks) == true; +ensures + foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states2)); +{ + switch(subTasks) { + case nil: + open foreach(nil, readOnly_sharedSeg_TCB_p(tasks, states)); + close foreach(nil, readOnly_sharedSeg_TCB_p(tasks, states2)); + case cons(h, rest): + int index = index_of(updatedTask, tasks); +// distinct_mem_remove(t, tasks); +// neq_mem_remove(h, t, tasks); +// index_of_different(h, t, tasks); + open foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states)); + assert( updatedTask != h ); + index_of_different(updatedTask, h, tasks); + assert( index != index_of(h, tasks) ); + update_readOnly_sharedSeg_TCB(h, tasks, states, index, s); + assert( mem(updatedTask, rest) == false ); + update_foreach_readOnly_sharedSeg_TCB(updatedTask, tasks, rest, + states, states2, s); + close foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states2)); + } +} + + +lemma void close_updated_foreach_readOnly_sharedSeg_TCB(TCB_t* updatedTask, + list tasks, + list states, + list states2, + TaskRunning_t s) +requires + mem(updatedTask, tasks) == true &*& + length(states) == length(tasks) &*& + distinct(tasks) == true &*& + foreach(remove(updatedTask, tasks), readOnly_sharedSeg_TCB_p(tasks, states)) &*& + states2 == update(index_of(updatedTask, tasks), s, states) &*& + [1/2]sharedSeg_TCB_p(updatedTask, s); +ensures + foreach(tasks, readOnly_sharedSeg_TCB_p(tasks, states2)); +{ + distinct_mem_remove(updatedTask, tasks); + remove_result_subset(updatedTask, tasks); + + close readOnly_sharedSeg_TCB_p(tasks, states2)(updatedTask); + update_foreach_readOnly_sharedSeg_TCB(updatedTask, tasks, + remove(updatedTask, tasks), + states, states2, s); + foreach_unremove(updatedTask, tasks); +} @*/ + #endif /* VERIFAST_LOCK_PREDICATES_H */ \ No newline at end of file