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 loop invariant to main search loop in prvSelectHighestPriorityTask.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-17 14:24:44 -05:00
parent 9b2871bc92
commit 6dcaef48d6
2 changed files with 34 additions and 1 deletions
Download patch file Download diff file Expand all files Collapse all files

28
tasks.c
View file

@ -929,6 +929,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); prvTCB_p(gCurrentTCB, ulFreeBytesOnStack);
@*/ @*/
{ {
//@ open taskISRLockInv();
//@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) );
//@ assert( gTopReadyPriority == uxTopReadyPriority);
UBaseType_t uxCurrentPriority = uxTopReadyPriority; UBaseType_t uxCurrentPriority = uxTopReadyPriority;
BaseType_t xTaskScheduled = pdFALSE; BaseType_t xTaskScheduled = pdFALSE;
BaseType_t xDecrementTopPriority = pdTRUE; BaseType_t xDecrementTopPriority = pdTRUE;
@ -939,8 +942,33 @@ static void prvYieldForTask( TCB_t * pxTCB,
#if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
BaseType_t xPriorityDropped = pdFALSE; BaseType_t xPriorityDropped = pdFALSE;
#endif #endif
//@ close taskISRLockInv();
while( xTaskScheduled == pdFALSE ) while( xTaskScheduled == pdFALSE )
/*@ invariant
// requires clause
0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
xCoreID == coreID_f() &*&
// interrupts are disabled and locks acquired
interruptState_p(xCoreID, state) &*&
interruptsDisabled_f(state) == true &*&
taskLockInv() &*&
isrLockInv() &*&
taskISRLockInv()
&*&
// opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
&*&
// read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ulFreeBytesOnStack)
&*&
// additional knowledge
0 <= uxCurrentPriority &*& uxCurrentPriority <= gTopReadyPriority &*&
gTopReadyPriority < configMAX_PRIORITIES
;
@*/
{ {
#if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
{ {

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

@ -88,7 +88,12 @@ predicate isrLockInv() =
fixpoint int taskISRLockID_f(); fixpoint int taskISRLockID_f();
predicate taskISRLockInv() = predicate taskISRLockInv() =
integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*& integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _)
&*&
// top ready priority must be in range
integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&
0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
&*&
readyLists_p() &*& readyLists_p() &*&
// Update: The current task on this core is interrupt protected. // Update: The current task on this core is interrupt protected.
// TODO: Exclude from `allTasks`. // TODO: Exclude from `allTasks`.