len0rd/FreeRTOS-Kernel
1
0
Fork 0
mirror of https://github.com/FreeRTOS/FreeRTOS-Kernel.git synced 2025-12-11 14:15:12 -05:00
Code Issues Projects Releases Packages Wiki Activity

Renamed TCB predicates to convey access rights expressed by each predicate. Updated lemmas accordinly.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-28 09:51:40 -05:00
parent 63154a4add
commit 6dc6c5dbbe
5 changed files with 121 additions and 131 deletions
Download patch file Download diff file Expand all files Collapse all files

10
Test/VeriFast/tasks/vTaskSwitchContext/include/stack_macros.h
View file

@ -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); \
} \
@*/ \
}

4
Test/VeriFast/tasks/vTaskSwitchContext/include/task.h
View file

@ -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);
@*/

24
Test/VeriFast/tasks/vTaskSwitchContext/proof/task_predicates.h
View file

@ -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;
@*/

130
Test/VeriFast/tasks/vTaskSwitchContext/proof/verifast_lock_predicates.h
View file

@ -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<t>(list<t> 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<void*> tasks, list<TaskRunning_t> 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<void*> tasks, list<TaskRunning_t> 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<t>(int i, int j, t y, list<t> 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<void*> tasks,
list<TaskRunning_t> 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<TaskRunning_t> 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<void*> tasks,
list<void*> subTasks,
list<TaskRunning_t> 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<void*> tasks,
list<TaskRunning_t> states,
list<TaskRunning_t> 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<void*> tasks, list<void*> subTasks,
list<TaskRunning_t> states, list<TaskRunning_t> 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<void*> tasks, list<void*> subTasks,
list<TaskRunning_t> states, list<TaskRunning_t> 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<void*> tasks,
list<TaskRunning_t> states, list<TaskRunning_t> 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<void*> tasks,
list<TaskRunning_t> states, list<TaskRunning_t> 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);
}

84
Test/VeriFast/tasks/vTaskSwitchContext/src/tasks.c
View file

@ -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<TaskRunning_t> 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<TaskRunning_t> 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.
@*/
{