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

Deleted comments.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-29 15:00:42 -05:00
parent 5cbf66ca63
commit 53d3062e2c
4 changed files with 6 additions and 22 deletions
Download patch file Download diff file Expand all files Collapse all files

3
Test/VeriFast/tasks/vTaskSwitchContext/proof/README.md
View file

@ -1,9 +1,6 @@
This directory contains the bulk of VeriFast formalizations and proofs. This directory contains the bulk of VeriFast formalizations and proofs.
# Directory Structure # Directory Structure
``` ```
├── lock_predicates.h ├── lock_predicates.h

1
Test/VeriFast/tasks/vTaskSwitchContext/proof/lock_predicates.h
View file

@ -150,7 +150,6 @@ predicate _taskISRLockInv_p(UBaseType_t gTopReadyPriority) =
// (RP-Current) Read permission for task currently scheduled on this core // (RP-Current) Read permission for task currently scheduled on this core
// (RP-All) + (RP-Current) => Write permission for scheduled task // (RP-All) + (RP-Current) => Write permission for scheduled task
[1/2]TCB_runState_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) &*& (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*&
nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state
&*& &*&

4
Test/VeriFast/tasks/vTaskSwitchContext/proof/ready_list_predicates.h
View file

@ -8,6 +8,10 @@
/*@ /*@
// This predicate represents the global ready lists, i.e., the global array
// `pxReadyTasksLists` in `tasks.c`.
// Each index `p` stores a cyclic doubly linked list containing all tasks
// of priority `p` that are ready to run.
predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists, predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists,
list<list<void*> > gOwnerLists) = list<list<void*> > gOwnerLists) =
configMAX_PRIORITIES == length(gCellLists) &*& configMAX_PRIORITIES == length(gCellLists) &*&

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

@ -904,12 +904,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
[1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB0) &*& [1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
// TCB_criticalNesting_p(gCurrentTCB0, 0)
&*&
// read access to current task's stack pointer, etc
// TCB_stack_p(gCurrentTCB0, ?ulFreeBytesOnStack);
true;
@*/ @*/
/*@ ensures 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& /*@ ensures 0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
xCoreID == coreID_f() &*& xCoreID == coreID_f() &*&
@ -922,12 +917,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
[1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& [1/2]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
// TCB_criticalNesting_p(gCurrentTCB, 0)
&*&
// read access to current task's stack pointer, etc
// TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack);
true;
@*/ @*/
{ {
//@ open taskISRLockInv_p(); //@ open taskISRLockInv_p();
@ -1422,12 +1412,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
// @ append_take_nth_drop(uxCurrentPriority, gCellLists); // @ append_take_nth_drop(uxCurrentPriority, gCellLists);
// @ append_take_nth_drop(uxCurrentPriority, gOwnerLists); // @ append_take_nth_drop(uxCurrentPriority, gOwnerLists);
// //@ assert( List_array_p(&pxReadyTasksLists, ?gSize2, ?gCellLists2, ?gOwnerLists2) );
//@ assert( exists_in_taskISRLockInv_p(gTasks, ?gStates) ); //@ assert( exists_in_taskISRLockInv_p(gTasks, ?gStates) );
// //@ close readyLists_p(gCellLists2, gOwnerLists2);
//@ close _taskISRLockInv_p(uxTopReadyPriority); //@ close _taskISRLockInv_p(uxTopReadyPriority);
} // outer loop end } // outer loop end
@ -4403,7 +4388,6 @@ void vTaskSwitchContext( BaseType_t xCoreID )
&*& &*&
// read access to current task's stack pointer, etc // read access to current task's stack pointer, etc
TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack); TCB_stack_p(gCurrentTCB, ulFreeBytesOnStack);
// Remark: the part of the post condition relating to TCBs will have to change.
@*/ @*/
{ {
/* Acquire both locks: /* Acquire both locks: