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

Refined lock invariant to only give read permission to all tasks and write permission to locally scheduled task

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-03 08:58:19 -05:00
parent 1919f8142f
commit e4db1f8aba
3 changed files with 22 additions and 9 deletions
Download patch file Download diff file Expand all files Collapse all files

14
tasks.c
View file

@ -1051,7 +1051,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
gSize > 0 &*& gSize > 0 &*&
foreach(gTasks, sharedSeg_TCB_p) &*& // Read permissions for every task
foreach(gTasks, readOnly_sharedSeg_TCB_p)
&*&
// Write permission for task scheduled on this core
[1/2]sharedSeg_TCB_p(gCurrentTCB)
&*&
subset(gOwners, gTasks) == true; subset(gOwners, gTasks) == true;
@*/ @*/
@ -1129,7 +1134,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
#endif #endif
#endif #endif
{ {
//@ assert( foreach(remove(pxTCB, gTasks), sharedSeg_TCB_p) ); //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p) );
//@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] ); //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] );
/*@ /*@
if( gCurrentTCB == pxTCB ) { if( gCurrentTCB == pxTCB ) {
@ -1138,7 +1143,6 @@ static void prvYieldForTask( TCB_t * pxTCB,
} else { } else {
neq_mem_remove(gCurrentTCB, pxTCB, gTasks); neq_mem_remove(gCurrentTCB, pxTCB, gTasks);
foreach_remove(gCurrentTCB, remove(pxTCB, gTasks)); foreach_remove(gCurrentTCB, remove(pxTCB, gTasks));
open sharedSeg_TCB_p(gCurrentTCB);
} }
@*/ @*/
/* If the task is not being executed by any core swap it in */ /* If the task is not being executed by any core swap it in */
@ -1157,13 +1161,14 @@ static void prvYieldForTask( TCB_t * pxTCB,
// => We don't have to close anything. // => We don't have to close anything.
} else { } else {
close sharedSeg_TCB_p(gCurrentTCB); close sharedSeg_TCB_p(gCurrentTCB);
close readOnly_sharedSeg_TCB_p(gCurrentTCB);
foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks)); foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks));
} }
@*/ @*/
// Ensure we restored the collection as it was // Ensure we restored the collection as it was
// at the beginning of the block. // at the beginning of the block.
//@ assert( foreach(remove(pxTCB, gTasks), sharedSeg_TCB_p) ); //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p) );
} }
} }
else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) else if( pxTCB == pxCurrentTCBs[ xCoreID ] )
@ -1196,6 +1201,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
} }
//@ close sharedSeg_TCB_p(pxTCB); //@ close sharedSeg_TCB_p(pxTCB);
//@ close readOnly_sharedSeg_TCB(pxTCB);
//@ foreach_unremove(pxTCB, gTasks); //@ foreach_unremove(pxTCB, gTasks);
} while( pxTaskItem != pxLastTaskItem ); } while( pxTaskItem != pxLastTaskItem );

4
verification/verifast/proof/task_predicates.h
View file

@ -111,6 +111,10 @@ predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) =
predicate sharedSeg_TCB_p(TCB_t* tcb;) = predicate sharedSeg_TCB_p(TCB_t* tcb;) =
tcb->xTaskRunState |-> ?gTaskRunState; tcb->xTaskRunState |-> ?gTaskRunState;
// Auxiliary predicate to allow foreach-quantification about fraction
predicate readOnly_sharedSeg_TCB_p(TCB_t* tcb;) =
[1/2]sharedSeg_TCB_p(tcb);
predicate coreLocalSeg_TCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) = predicate coreLocalSeg_TCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) =
tcb->uxCriticalNesting |-> uxCriticalNesting; tcb->uxCriticalNesting |-> uxCriticalNesting;
@*/ @*/

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

@ -97,10 +97,13 @@ predicate taskISRLockInv_p() =
// tasks / TCBs // tasks / TCBs
exists_in_taskISRLockInv_p(?gTasks) exists_in_taskISRLockInv_p(?gTasks)
&*& &*&
// Access permissions for every task // (RP-All) Read permissions for every task
// TODO: Convert to read permissions // ∀t ∈ gTasks. [1/2]sharedSeg_TCB_p(t)
// ∀t ∈ gTasks. sharedSeg_TCB_p(t) foreach(gTasks, readOnly_sharedSeg_TCB_p)
foreach(gTasks, sharedSeg_TCB_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)
&*& &*&
readyLists_p(?gCellLists, ?gOwnerLists) readyLists_p(?gCellLists, ?gOwnerLists)
&*& &*&