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

Added lemmas to update read permissions for unscheduled tasks after new task has been started.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-04 10:19:48 -05:00
parent 6a0b2116fe
commit fbf4ba981f
2 changed files with 66 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

3
tasks.c
View file

@ -1203,6 +1203,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
/*@ close_updated_foreach_readOnly_sharedSeg_TCB(pxTCB, gTasks, gStates1,
gStates2, xCoreID);
@*/
/*@ startUpdate_foreach_readOnly_sharedSeg_TCB_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)) );

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

@ -335,8 +335,71 @@ ensures
close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2));
}
}
lemma void updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_IF_not_running
(TCB_t* updatedTask, list<void*> tasks, list<void*> subTasks,
list<TaskRunning_t> states, list<TaskRunning_t> updatedStates,
TaskRunning_t s)
requires
distinct(tasks) == true &*&
distinct(subTasks) == true &*&
length(tasks) == length(states) &*&
mem(updatedTask, tasks) == true &*&
mem(updatedTask, subTasks) == false &*&
subset(subTasks, tasks) == true &*&
foreach(subTasks, readOnly_sharedSeg_TCB_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));
{
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));
case cons(h, t):
open foreach(subTasks, readOnly_sharedSeg_TCB_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
(updatedTask, tasks, t, states, updatedStates, s);
close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, updatedStates));
}
}
lemma void startUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running
(TCB_t* startedTask, list<void*> tasks,
list<TaskRunning_t> states, list<TaskRunning_t> updatedStates,
int coreID)
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)) &*&
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));
{
distinct_remove(startedTask, tasks);
distinct_mem_remove(startedTask, tasks);
remove_result_subset(startedTask, tasks);
updateUnaffectedStates_in_foreach_readOnly_sharedSeg_TCB_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);
foreach_unremove(startedTask, tasks);
}
@*/
/*@
lemma list<TaskRunning_t> def_state1(list<void*> tasks,
list<TaskRunning_t> states,