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

Added lemma to update the read permissions for unscheduled tasks after a task has been stopped.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-03 18:05:15 -05:00
parent 0df45b465e
commit e403e8bc74
2 changed files with 83 additions and 34 deletions
Download patch file Download diff file Expand all files Collapse all files

64
tasks.c
View file

@ -1057,7 +1057,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates))
&*&
// Write permission for task scheduled on this core
[1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state)
[1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*&
gCurrentTCB_state != taskTASK_NOT_RUNNING &*&
nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state
&*&
// TODO:
// Write permissions for unscheduled tasks
@ -1155,56 +1157,54 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ close readOnly_sharedSeg_TCB_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)) );
// 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<TaskRunning_t> 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)) );
//@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) );
/*@ list<TaskRunning_t> gStates1 =
update(index_of(gCurrentTCB, gTasks), taskTASK_NOT_RUNNING, gStates);
@*/
//@ open exists_in_taskISRLockInv_p(gTasks, gStates);
/*@ close_updated_foreach_readOnly_sharedSeg_TCB
(gCurrentTCB, gTasks, gStates,
gStates1, taskTASK_NOT_RUNNING);
/*@ close_updated_foreach_readOnly_sharedSeg_TCB(gCurrentTCB, gTasks, gStates,
gStates1, taskTASK_NOT_RUNNING);
@*/
//@ assume(false);
/*@ list<TaskRunning_t> gStates2 =
update(gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates);
//@ 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
(gCurrentTCB, gTasks, gTasks, gStates, gStates1);
@*/
//@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)) );
// 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));
}
@*/
// Get write permission for `pxTCB`
//@ foreach_remove(pxTCB, gTasks);
//@ foreach_remove(pxTCB, gTasks);
#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, gStates)) );
/*@ list<TaskRunning_t> gStates2 =
update(index_of(pxTCB, gTasks), xCoreID, gStates1);
@*/
/*@ close_updated_foreach_readOnly_sharedSeg_TCB(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)) );
pxCurrentTCBs[ xCoreID ] = pxTCB;
xTaskScheduled = pdTRUE;

53
verification/verifast/proof/verifast_lock_predicates.h
View file

@ -107,9 +107,10 @@ predicate taskISRLockInv_p() =
&*&
// (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]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*&
gCurrentTCB_state != taskTASK_NOT_RUNNING &*&
nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state
&*&
// TODO:
// (RP-Unsched) Read permissions for unscheduled tasks
// (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks
// ∀t ∈ tasks. t->xTaskState == taskTASK_NOT_RUNNING
@ -283,6 +284,54 @@ ensures
states, states2, s);
foreach_unremove(updatedTask, tasks);
}
lemma void stopUpdate_foreach_readOnly_sharedSeg_TCB_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)) &*&
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)
: true;
ensures
foreach(subTasks, readOnly_sharedSeg_TCB_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));
case cons(h, t):
if( h == stoppedTask ) {
assert( remove(stoppedTask, subTasks) == t );
distinct_mem_remove(stoppedTask, subTasks);
assert( mem(stoppedTask, t) == false );
mem_index_of(stoppedTask, tasks);
} else {
mem_index_of(stoppedTask, tasks);
nth_update(index_of(h, tasks), index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states);
index_of_different(h, stoppedTask, tasks);
assert( index_of(h, tasks) != index_of(stoppedTask, tasks) );
assert( nth(index_of(h, tasks), states) == nth(index_of(h, tasks), states2) );
}
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);
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
(stoppedTask, tasks, t, states, states2);
close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2));
}
}
@*/