diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h b/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h index 539a22e88..e0162f57a 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h @@ -96,14 +96,14 @@ #define taskCHECK_FOR_STACK_OVERFLOW() VF__taskCHECK_FOR_STACK_OVERFLOW() void VF__taskCHECK_FOR_STACK_OVERFLOW() - /*@ requires prvSeg_TCB_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*& + /*@ requires TCB_stack_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*& coreLocalSeg_TCB_p(gCurrentTCB, ?uxCriticalNesting) &*& // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()` interruptState_p(coreID_f(), ?state) &*& interruptsDisabled_f(state) == true &*& pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); @*/ - /*@ ensures prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack) &*& + /*@ ensures TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack) &*& coreLocalSeg_TCB_p(gCurrentTCB, uxCriticalNesting) &*& // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()` interruptState_p(coreID_f(), state) &*& @@ -111,7 +111,7 @@ pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); \ @*/ \ { \ - /*@ open prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ + /*@ open TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ /*@ assert( stack_p(?pxStack, ?ulStackDepth, ?pxTopOfStack, \ ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) ); \ @*/ \ @@ -139,7 +139,7 @@ /*@ close stack_p(pxStack, ulStackDepth, pxTopOfStack, \ ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ @*/ \ - /*@ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ + /*@ close TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ TCB_t* tcb1 = pxCurrentTCB; \ TCB_t* tcb2 = pxCurrentTCB; \ vApplicationStackOverflowHook( ( TaskHandle_t ) tcb1, tcb2->pcTaskName ); \ @@ -151,7 +151,7 @@ chars_split((char*) pxStack, ulFreeBytesOnStack); \ close stack_p(pxStack, ulStackDepth, pxTopOfStack, \ ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ - close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); \ + close TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack); \ } \ @*/ \ } diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/include/task.h b/Test/VeriFast/tasks/vTaskSwitchContext/include/task.h index 56e054299..0b48e3f58 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/include/task.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/include/task.h @@ -1863,10 +1863,10 @@ configSTACK_DEPTH_TYPE uxTaskGetStackHighWaterMark2( TaskHandle_t xTask ) PRIVIL */ void vApplicationStackOverflowHook( TaskHandle_t xTask, char * pcTaskName ); - /*@ requires prvSeg_TCB_p(xTask, ?ulFreeBytesOnStack) &*& + /*@ requires TCB_stack_p(xTask, ?ulFreeBytesOnStack) &*& coreLocalSeg_TCB_p(xTask, ?uxCriticalNesting); @*/ - /*@ ensures prvSeg_TCB_p(xTask, ulFreeBytesOnStack) &*& + /*@ ensures TCB_stack_p(xTask, ulFreeBytesOnStack) &*& coreLocalSeg_TCB_p(xTask, uxCriticalNesting); @*/ diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h index f34ed7a1d..5687a735f 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h @@ -49,30 +49,20 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) = @*/ /*@ -// We have to segment TCBs into: -// (i) public parts that can be accessed by anyone after -// following the appropriote synchronization steps and -// (ii) private parts that may only be used by the task itself -// which the TCB represents -// -// The predicates below will be expanded iteratively. - -// This predicate captures the private part of a TCB that should only be -// accessed by the TCB represents or under specific circumstances where -// we are certain that the task is not running. -predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) = +// This predicate represents write access to a TCB's stack. +predicate TCB_stack_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) = tcb->pxStack |-> ?stackPtr &*& tcb->pxTopOfStack |-> ?topPtr &*& stack_p(stackPtr, ?ulStackDepth, topPtr, ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes); -// This predicate represents a shared part of a TCB that can be accessed by -// anyone. Note that this predicate only contains the minimal access rights -// required by the `vTaskSwitchContext` proof. It can be extended in the future -// as needed. -predicate sharedSeg_TCB_p(TCB_t* tcb, TaskRunning_t state;) = +// This predicate represents write access to the run state of a TCB. +predicate TCB_runState_p(TCB_t* tcb, TaskRunning_t state;) = tcb->xTaskRunState |-> state; +// This predicate represents write access to the nesting level of a TCB. +// Entering a critical section increases the nesting level. Leaving it, +// decreases it. predicate coreLocalSeg_TCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) = tcb->uxCriticalNesting |-> uxCriticalNesting; @*/ diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h index 615c7451c..3c9b50f08 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h +++ b/Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h @@ -106,14 +106,14 @@ predicate _taskISRLockInv_p(UBaseType_t gTopReadyPriority) = // (RP-All) Read permissions for every task // and recording of task states in state list // (∀t ∈ gTasks. - // [1/2]sharedSeg_TCB_p(t, _)) + // [1/2]TCB_runState_p(t, _)) // ∧ // ∀i. ∀t. gTasks[i] == t -> gStates[i] == t->xTaskRunState - foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) + foreach(gTasks, readOnly_TCB_runState_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, ?gCurrentTCB_state) &*& + [1/2]TCB_runState_p(gCurrentTCB, ?gCurrentTCB_state) &*& // gCurrentTCB_state != taskTASK_NOT_RUNNING &*& (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*& nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state @@ -122,7 +122,7 @@ predicate _taskISRLockInv_p(UBaseType_t gTopReadyPriority) = // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks // ∀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)) + foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates)) &*& readyLists_p(?gCellLists, ?gOwnerLists) &*& @@ -172,18 +172,18 @@ fixpoint bool mem_list_elem(list xs, t x) { // Auxiliary predicate to allow foreach-quantification about fraction // and reflection of `t->xTaskRunState` in state list. -predicate_ctor readOnly_sharedSeg_TCB_p +predicate_ctor readOnly_TCB_runState_p (list tasks, list states) (TCB_t* t;) = mem(t, tasks) == true &*& - [1/2]sharedSeg_TCB_p(t, nth(index_of(t, tasks), states)); + [1/2]TCB_runState_p(t, nth(index_of(t, tasks), states)); -predicate_ctor readOnly_sharedSeg_TCB_IF_not_running_p +predicate_ctor readOnly_TCB_runState_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) + ? [1/2]TCB_runState_p(t, taskTASK_NOT_RUNNING) : true; @*/ @@ -201,16 +201,16 @@ lemma void nonauto_nth_update(int i, int j, t y, list xs); // TODO: Move lemmas below to separate header file. /*@ -lemma void update_readOnly_sharedSeg_TCB(TCB_t* t, +lemma void update_readOnly_TCB_runState(TCB_t* t, list tasks, list states, int updatedIndex, TaskRunning_t s) -requires readOnly_sharedSeg_TCB_p(tasks, states)(t) &*& +requires readOnly_TCB_runState_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); +ensures readOnly_TCB_runState_p(tasks, update(updatedIndex, s, states))(t); { list states2 = update(updatedIndex, s, states); int t_index = index_of(t, tasks); @@ -218,20 +218,20 @@ ensures readOnly_sharedSeg_TCB_p(tasks, update(updatedIndex, s, states))(t); 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)); + open readOnly_TCB_runState_p(tasks, states)(t); + open [1/2]TCB_runState_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); + close [1/2]TCB_runState_p(t, nth(t_index, states2)); + close readOnly_TCB_runState_p(tasks, states2)(t); } } -lemma void update_foreach_readOnly_sharedSeg_TCB(TCB_t* updatedTask, +lemma void update_foreach_readOnly_TCB_runState(TCB_t* updatedTask, list tasks, list subTasks, list states, @@ -240,37 +240,37 @@ lemma void update_foreach_readOnly_sharedSeg_TCB(TCB_t* updatedTask, requires mem(updatedTask, tasks) == true &*& length(tasks) == length(states) &*& - foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states)) &*& + foreach(subTasks, readOnly_TCB_runState_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)); + foreach(subTasks, readOnly_TCB_runState_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)); + open foreach(nil, readOnly_TCB_runState_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_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)); + open foreach(subTasks, readOnly_TCB_runState_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); + update_readOnly_TCB_runState(h, tasks, states, index, s); assert( mem(updatedTask, rest) == false ); - update_foreach_readOnly_sharedSeg_TCB(updatedTask, tasks, rest, + update_foreach_readOnly_TCB_runState(updatedTask, tasks, rest, states, states2, s); - close foreach(subTasks, readOnly_sharedSeg_TCB_p(tasks, states2)); + close foreach(subTasks, readOnly_TCB_runState_p(tasks, states2)); } } -lemma void close_updated_foreach_readOnly_sharedSeg_TCB(TCB_t* updatedTask, +lemma void close_updated_foreach_readOnly_TCB_runState(TCB_t* updatedTask, list tasks, list states, list states2, @@ -279,45 +279,45 @@ requires mem(updatedTask, tasks) == true &*& length(states) == length(tasks) &*& distinct(tasks) == true &*& - foreach(remove(updatedTask, tasks), readOnly_sharedSeg_TCB_p(tasks, states)) &*& + foreach(remove(updatedTask, tasks), readOnly_TCB_runState_p(tasks, states)) &*& states2 == update(index_of(updatedTask, tasks), s, states) &*& - [1/2]sharedSeg_TCB_p(updatedTask, s); + [1/2]TCB_runState_p(updatedTask, s); ensures - foreach(tasks, readOnly_sharedSeg_TCB_p(tasks, states2)); + foreach(tasks, readOnly_TCB_runState_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, + close readOnly_TCB_runState_p(tasks, states2)(updatedTask); + update_foreach_readOnly_TCB_runState(updatedTask, tasks, remove(updatedTask, tasks), states, states2, s); foreach_unremove(updatedTask, tasks); } -lemma void stopUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running +lemma void stopUpdate_foreach_readOnly_TCB_runState_IF_not_running (TCB_t* stoppedTask, list tasks, list subTasks, list states, list states2) requires distinct(tasks) == true &*& distinct(subTasks) == true &*& length(tasks) == length(states) &*& - foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)) &*& + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& states2 == update(index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states) &*& nth(index_of(stoppedTask, tasks), states) != taskTASK_NOT_RUNNING &*& subset(subTasks, tasks) == true &*& mem(stoppedTask, tasks) == true &*& mem(stoppedTask, subTasks) - ? [1/2]sharedSeg_TCB_p(stoppedTask, taskTASK_NOT_RUNNING) + ? [1/2]TCB_runState_p(stoppedTask, taskTASK_NOT_RUNNING) : true; ensures - foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)); + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states2)); { switch(subTasks) { case nil: - open foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)); - close foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)); + open foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states2)); case cons(h, t): if( h == stoppedTask ) { assert( remove(stoppedTask, subTasks) == t ); @@ -333,17 +333,17 @@ ensures } nth_update(index_of(stoppedTask, tasks), index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states); - open foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)); - open readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)(h); + open foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + open readOnly_TCB_runState_IF_not_running_p(tasks, states)(h); assert( nth(index_of(stoppedTask, tasks), states2) == taskTASK_NOT_RUNNING ); - close readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)(h); - stopUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running + close readOnly_TCB_runState_IF_not_running_p(tasks, states2)(h); + stopUpdate_foreach_readOnly_TCB_runState_IF_not_running (stoppedTask, tasks, t, states, states2); - close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)); + close foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states2)); } } -lemma void updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running +lemma void updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running (TCB_t* updatedTask, list tasks, list subTasks, list states, list updatedStates, TaskRunning_t s) @@ -354,32 +354,32 @@ requires mem(updatedTask, tasks) == true &*& mem(updatedTask, subTasks) == false &*& subset(subTasks, tasks) == true &*& - foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)) &*& + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& updatedStates == update(index_of(updatedTask, tasks), s, states); ensures - foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)); + foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); { switch(subTasks) { case nil: - open foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)); - close foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)); + open foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); case cons(h, t): - open foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)); + open foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)); // Prove that update preserves state of `h`. index_of_different(h, updatedTask, tasks); nth_update(index_of(h, tasks), index_of(updatedTask, tasks), s, states); assert( nth(index_of(h, tasks), states) == nth(index_of(h, tasks), updatedStates) ); - open readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)(h); - close readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)(h); - updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running + open readOnly_TCB_runState_IF_not_running_p(tasks, states)(h); + close readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)(h); + updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running (updatedTask, tasks, t, states, updatedStates, s); - close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)); + close foreach(subTasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); } } -lemma void startUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running +lemma void startUpdate_foreach_readOnly_TCB_runState_IF_not_running (TCB_t* startedTask, list tasks, list states, list updatedStates, int coreID) @@ -387,25 +387,25 @@ requires distinct(tasks) == true &*& length(tasks) == length(states) &*& mem(startedTask, tasks) == true &*& - foreach(remove(startedTask, tasks), readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)) &*& + foreach(remove(startedTask, tasks), readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& updatedStates == update(index_of(startedTask, tasks), coreID, states) &*& 0 <= coreID &*& coreID < configNUM_CORES; ensures - foreach(tasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)); + foreach(tasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); { distinct_remove(startedTask, tasks); distinct_mem_remove(startedTask, tasks); remove_result_subset(startedTask, tasks); - updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running + updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running (startedTask, tasks, remove(startedTask, tasks), states, updatedStates, coreID); - assert( foreach(remove(startedTask, tasks), readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)) ); - close readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)(startedTask); + assert( foreach(remove(startedTask, tasks), readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)) ); + close readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)(startedTask); foreach_unremove(startedTask, tasks); } -lemma void scheduleRunning_in_foreach_readOnly_sharedSeg_TCB_IF_not_running +lemma void scheduleRunning_in_foreach_readOnly_TCB_runState_IF_not_running (TCB_t* runningTask, list tasks, list states, list updatedStates, int coreID) @@ -416,29 +416,29 @@ requires (nth(index_of(runningTask, tasks), states) == coreID || nth(index_of(runningTask, tasks), states) == taskTASK_YIELDING) &*& - foreach(tasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)) &*& + foreach(tasks, readOnly_TCB_runState_IF_not_running_p(tasks, states)) &*& updatedStates == update(index_of(runningTask, tasks), coreID, states) &*& 0 <= coreID &*& coreID < configNUM_CORES; ensures - foreach(tasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)) &*& + foreach(tasks, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)) &*& nth(index_of(runningTask, tasks), updatedStates) == coreID; { switch(tasks) { case nil: - open foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)); - close foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)); + open foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, states)); + close foreach(nil, readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)); case cons(h, t): foreach_remove(runningTask, tasks); distinct_remove(runningTask, tasks); distinct_mem_remove(runningTask, tasks); remove_result_subset(runningTask, tasks); - updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running + updateUnaffectedStates_in_foreach_readOnly_TCB_runState_IF_not_running (runningTask, tasks, remove(runningTask, tasks), states, updatedStates, coreID); - open readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)(runningTask); - close readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates)(runningTask); + open readOnly_TCB_runState_IF_not_running_p(tasks, states)(runningTask); + close readOnly_TCB_runState_IF_not_running_p(tasks, updatedStates)(runningTask); foreach_unremove(runningTask, tasks); } diff --git a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c index c68514334..c92cc7cfc 100644 --- a/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c +++ b/Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c @@ -909,7 +909,7 @@ static void prvYieldForTask( TCB_t * pxTCB, // coreLocalSeg_TCB_p(gCurrentTCB0, 0) &*& // read access to current task's stack pointer, etc -// prvSeg_TCB_p(gCurrentTCB0, ?ulFreeBytesOnStack); +// TCB_stack_p(gCurrentTCB0, ?ulFreeBytesOnStack); true; @*/ /*@ ensures 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& @@ -927,7 +927,7 @@ static void prvYieldForTask( TCB_t * pxTCB, // coreLocalSeg_TCB_p(gCurrentTCB, 0) &*& // read access to current task's stack pointer, etc -// prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); +// TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack); true; @*/ { @@ -1059,15 +1059,15 @@ static void prvYieldForTask( TCB_t * pxTCB, exists_in_taskISRLockInv_p(gTasks, ?gStates) &*& // Read permissions for every task - foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) + foreach(gTasks, readOnly_TCB_runState_p(gTasks, gStates)) &*& // Write permission for task scheduled on this core - [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*& + [1/2]TCB_runState_p(gCurrentTCB, ?gCurrentTCB_state) &*& (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*& nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state &*& // Write permissions for unscheduled tasks - foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) + foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates)) &*& subset(gOwners, gTasks) == true &*& List_array_p(&pxReadyTasksLists, uxCurrentPriority, gPrefCellLists, @@ -1126,7 +1126,7 @@ static void prvYieldForTask( TCB_t * pxTCB, //@ 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)) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_TCB_runState_p(gTasks, gStates)) ); /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ @@ -1156,9 +1156,9 @@ static void prvYieldForTask( TCB_t * pxTCB, { //@ open exists_in_taskISRLockInv_p(gTasks, gStates); //@ assert( nth(index_of(pxTCB, gTasks), gStates) == taskTASK_NOT_RUNNING); - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_TCB_runState_p(gTasks, gStates)) ); //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_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 @@ -1166,70 +1166,70 @@ static void prvYieldForTask( TCB_t * pxTCB, */ // Put read permission for `pxTCB` back - //@ close [1/2]sharedSeg_TCB_p(pxTCB, _); - //@ close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB); + //@ close [1/2]TCB_runState_p(pxTCB, _); + //@ close readOnly_TCB_runState_p(gTasks, gStates)(pxTCB); //@ foreach_unremove(pxTCB, gTasks); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_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)) ); + //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_TCB_runState_p(gTasks, 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)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_TCB_runState_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates)) ); // New states list reflects state update above. //@ list gStates1 = def_state1(gTasks, gStates, gCurrentTCB, pxTCB); //@ assert( nth(index_of(pxTCB, gTasks), gStates1) == taskTASK_NOT_RUNNING); - /*@ close_updated_foreach_readOnly_sharedSeg_TCB(gCurrentTCB, gTasks, gStates, + /*@ close_updated_foreach_readOnly_TCB_runState(gCurrentTCB, gTasks, gStates, gStates1, taskTASK_NOT_RUNNING); @*/ - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates1)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); - /*@ stopUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running + //@ assert( foreach(gTasks, readOnly_TCB_runState_p(gTasks, gStates1)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates)) ); + /*@ stopUpdate_foreach_readOnly_TCB_runState_IF_not_running (gCurrentTCB, gTasks, gTasks, gStates, gStates1); @*/ - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates1)) ); // Get write permission for `pxTCB` //@ foreach_remove(pxTCB, gTasks); //@ foreach_remove(pxTCB, gTasks); - //@ open readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)(pxTCB); + //@ open readOnly_TCB_runState_IF_not_running_p(gTasks, gStates1)(pxTCB); #if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) ) pxPreviousTCB = pxCurrentTCBs[ xCoreID ]; #endif pxTCB->xTaskRunState = ( TaskRunning_t ) xCoreID; - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates1)) ); - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_TCB_runState_p(gTasks, gStates1)) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_TCB_runState_IF_not_running_p(gTasks, gStates1)) ); /*@ list gStates2 = def_state2(gTasks, gStates, gCurrentTCB, pxTCB, xCoreID); @*/ - /*@ close_updated_foreach_readOnly_sharedSeg_TCB(pxTCB, gTasks, gStates1, + /*@ close_updated_foreach_readOnly_TCB_runState(pxTCB, gTasks, gStates1, gStates2, xCoreID); @*/ - /*@ startUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running + /*@ startUpdate_foreach_readOnly_TCB_runState_IF_not_running (pxTCB, gTasks, gStates1, gStates2, xCoreID); @*/ - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates2)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates2)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_p(gTasks, gStates2)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates2)) ); pxCurrentTCBs[ xCoreID ] = pxTCB; xTaskScheduled = pdTRUE; - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates2)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates2)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_p(gTasks, gStates2)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates2)) ); //@ close exists_in_taskISRLockInv_p(gTasks, gStates2); // Putting back first have of write permission to `pxTCB` - //@ close [1/2]sharedSeg_TCB_p(pxTCB, _); + //@ close [1/2]TCB_runState_p(pxTCB, _); } } else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) @@ -1242,9 +1242,9 @@ static void prvYieldForTask( TCB_t * pxTCB, #endif { //@ assert( pxTCB->xTaskRunState != taskTASK_NOT_RUNNING ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStates)) ); //@ assert( nth(index_of(pxTCB, gTasks), gStates) != taskTASK_NOT_RUNNING); - //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_TCB_runState_p(gTasks, gStates)) ); /* The task is already running on this core, mark it as scheduled */ pxTCB->xTaskRunState = ( TaskRunning_t ) xCoreID; @@ -1254,13 +1254,13 @@ static void prvYieldForTask( TCB_t * pxTCB, = update(index_of(pxTCB, gTasks), xCoreID, gStates); @*/ //@ open exists_in_taskISRLockInv_p(gTasks, gStates); - /*@ scheduleRunning_in_foreach_readOnly_sharedSeg_TCB_IF_not_running + /*@ scheduleRunning_in_foreach_readOnly_TCB_runState_IF_not_running (pxTCB, gTasks, gStates, gEquivStates, xCoreID); @*/ //@ distinct_mem_remove(pxTCB, gTasks); //@ remove_result_subset(pxTCB, gTasks); - /*@ update_foreach_readOnly_sharedSeg_TCB + /*@ update_foreach_readOnly_TCB_runState (pxTCB, gTasks, remove(pxTCB, gTasks), gStates, gEquivStates, xCoreID); @*/ @@ -1270,16 +1270,16 @@ static void prvYieldForTask( TCB_t * pxTCB, // Put read permission for `pxTCB` back //@ foreach_unremove(pxTCB, gTasks); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gEquivStates)) ); - //@ close [1/2]sharedSeg_TCB_p(pxTCB, _); + //@ assert( foreach(gTasks, readOnly_TCB_runState_p(gTasks, gEquivStates)) ); + //@ close [1/2]TCB_runState_p(pxTCB, _); } } /*@ if( !gPxTCB_not_running && pxTCB != gCurrentTCB ) { assert( exists_in_taskISRLockInv_p(gTasks, gStates) ); // Put read permission for `pxTCB` back - close [1/2]sharedSeg_TCB_p(pxTCB, _); - close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB); + close [1/2]TCB_runState_p(pxTCB, _); + close readOnly_TCB_runState_p(gTasks, gStates)(pxTCB); foreach_unremove(pxTCB, gTasks); } @*/ @@ -1325,8 +1325,8 @@ static void prvYieldForTask( TCB_t * pxTCB, } //@ assert( exists_in_taskISRLockInv_p(gTasks, ?gStatesEnd) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStatesEnd)) ); - //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStatesEnd)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_p(gTasks, gStatesEnd)) ); + //@ assert( foreach(gTasks, readOnly_TCB_runState_IF_not_running_p(gTasks, gStatesEnd)) ); } while( pxTaskItem != pxLastTaskItem ); /* - If the loop above terminated via the break-branch, @@ -4388,7 +4388,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) coreLocalSeg_TCB_p(gCurrentTCB, 0) &*& // read access to current task's stack pointer, etc - prvSeg_TCB_p(gCurrentTCB, ?ulFreeBytesOnStack); + TCB_stack_p(gCurrentTCB, ?ulFreeBytesOnStack); @*/ /*@ ensures // all locks are released and interrupts remain disabled @@ -4403,7 +4403,7 @@ void vTaskSwitchContext( BaseType_t xCoreID ) coreLocalSeg_TCB_p(gCurrentTCB, 0) &*& // read access to current task's stack pointer, etc - prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); + TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack); // Remark: the part of the post condition relating to TCBs will have to change. @*/ {