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

Refactored lock predicates to improve readability.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-29 09:37:23 -05:00
parent b310efa029
commit 014acb9a00
6 changed files with 56 additions and 68 deletions
Download patch file Download diff file Expand all files Collapse all files

14
include/stack_macros.h
View file

@ -96,22 +96,22 @@
#define taskCHECK_FOR_STACK_OVERFLOW() VF__taskCHECK_FOR_STACK_OVERFLOW() #define taskCHECK_FOR_STACK_OVERFLOW() VF__taskCHECK_FOR_STACK_OVERFLOW()
void VF__taskCHECK_FOR_STACK_OVERFLOW() void VF__taskCHECK_FOR_STACK_OVERFLOW()
/*@ requires prvTCB_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*& /*@ requires prvSeg_TCB_p(?gCurrentTCB, ?ulFreeBytesOnStack) &*&
pubTCB_p(gCurrentTCB, ?uxCriticalNesting) &*& coreLocalSeg_TCB_p(gCurrentTCB, ?uxCriticalNesting) &*&
// chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()` // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
interruptState_p(coreID_f(), ?state) &*& interruptState_p(coreID_f(), ?state) &*&
interruptsDisabled_f(state) == true &*& interruptsDisabled_f(state) == true &*&
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB);
@*/ @*/
/*@ ensures prvTCB_p(gCurrentTCB, ulFreeBytesOnStack) &*& /*@ ensures prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack) &*&
pubTCB_p(gCurrentTCB, uxCriticalNesting) &*& coreLocalSeg_TCB_p(gCurrentTCB, uxCriticalNesting) &*&
// chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()` // chunks required by `pxCurrentTCB` aka `xTaskGetCurrentTaskHandle()`
interruptState_p(coreID_f(), state) &*& interruptState_p(coreID_f(), state) &*&
interruptsDisabled_f(state) == true &*& interruptsDisabled_f(state) == true &*&
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); \ pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB); \
@*/ \ @*/ \
{ \ { \
/*@ open prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ /*@ open prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \
/*@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack, \ /*@ assert( stack_p_2(?pxStack, ?ulStackDepth, ?pxTopOfStack, \
?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) ); \ ?ulFreeBytes, ?ulUsedCells, ?ulUnalignedBytes) ); \
@*/ \ @*/ \
@ -139,7 +139,7 @@
/*@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \ /*@ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \
ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ ulFreeBytes, ulUsedCells, ulUnalignedBytes); \
@*/ \ @*/ \
/*@ close prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \ /*@ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); @*/ \
TCB_t* tcb1 = pxCurrentTCB; \ TCB_t* tcb1 = pxCurrentTCB; \
TCB_t* tcb2 = pxCurrentTCB; \ TCB_t* tcb2 = pxCurrentTCB; \
vApplicationStackOverflowHook( ( TaskHandle_t ) tcb1, tcb2->pcTaskName ); \ vApplicationStackOverflowHook( ( TaskHandle_t ) tcb1, tcb2->pcTaskName ); \
@ -151,7 +151,7 @@
chars_split((char*) pxStack, ulFreeBytesOnStack); \ chars_split((char*) pxStack, ulFreeBytesOnStack); \
close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \ close stack_p_2(pxStack, ulStackDepth, pxTopOfStack, \
ulFreeBytes, ulUsedCells, ulUnalignedBytes); \ ulFreeBytes, ulUsedCells, ulUnalignedBytes); \
close prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); \ close prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack); \
} \ } \
@*/ \ @*/ \
} }

8
include/task.h
View file

@ -1863,11 +1863,11 @@ configSTACK_DEPTH_TYPE uxTaskGetStackHighWaterMark2( TaskHandle_t xTask ) PRIVIL
*/ */
void vApplicationStackOverflowHook( TaskHandle_t xTask, void vApplicationStackOverflowHook( TaskHandle_t xTask,
char * pcTaskName ); char * pcTaskName );
/*@ requires prvTCB_p(xTask, ?ulFreeBytesOnStack) &*& /*@ requires prvSeg_TCB_p(xTask, ?ulFreeBytesOnStack) &*&
pubTCB_p(xTask, ?uxCriticalNesting); coreLocalSeg_TCB_p(xTask, ?uxCriticalNesting);
@*/ @*/
/*@ ensures prvTCB_p(xTask, ulFreeBytesOnStack) &*& /*@ ensures prvSeg_TCB_p(xTask, ulFreeBytesOnStack) &*&
pubTCB_p(xTask, uxCriticalNesting); coreLocalSeg_TCB_p(xTask, uxCriticalNesting);
@*/ @*/
#endif #endif

70
tasks.c
View file

@ -908,11 +908,11 @@ static void prvYieldForTask( TCB_t * pxTCB,
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) coreLocalSeg_TCB_p(gCurrentTCB, 0)
&*& &*&
// read access to current task's stack pointer, etc // read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ?ulFreeBytesOnStack); prvSeg_TCB_p(gCurrentTCB, ?ulFreeBytesOnStack);
@*/ @*/
/*@ ensures 0 <= xCoreID &*& xCoreID < configNUM_CORES &*& /*@ ensures 0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
xCoreID == coreID_f() &*& xCoreID == coreID_f() &*&
@ -925,11 +925,11 @@ static void prvYieldForTask( TCB_t * pxTCB,
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) coreLocalSeg_TCB_p(gCurrentTCB, 0)
&*& &*&
// read access to current task's stack pointer, etc // read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack);
@*/ @*/
{ {
//@ open taskISRLockInv(); //@ open taskISRLockInv();
@ -961,11 +961,12 @@ static void prvYieldForTask( TCB_t * pxTCB,
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*& // pubTCB_p(gCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*&
coreLocalSeg_TCB_p(gCurrentTCB, 0)
&*& &*&
// read access to current task's stack pointer, etc // read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ulFreeBytesOnStack) prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack)
&*& &*&
// additional knowledge // additional knowledge
0 <= uxCurrentPriority &*& uxCurrentPriority <= gTopReadyPriority &*& 0 <= uxCurrentPriority &*& uxCurrentPriority <= gTopReadyPriority &*&
@ -986,19 +987,19 @@ static void prvYieldForTask( TCB_t * pxTCB,
#endif #endif
//@ open taskISRLockInv(); //@ open taskISRLockInv();
//@ open readyLists_p(); //@ open readyLists_p(?gCellLists);
//@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
//@ List_array_get_l(pxReadyTasksLists, uxCurrentPriority); //@ List_array_split(pxReadyTasksLists, uxCurrentPriority);
//@ List_t* gReadyList = &pxReadyTasksLists[uxCurrentPriority]; //@ List_t* gReadyList = &pxReadyTasksLists[uxCurrentPriority];
/*@ assert( xLIST(gReadyList, ?gNumberOfItems, ?gIndex, ?gListEnd,
?gCells, ?gVals) ); //@ assert( xLIST(gReadyList, ?gSize, ?gIndex, ?gEnd, ?gCells, ?gVals) );
@*/
//@ open xLIST(gReadyList, _, _, _, _, _); //@ open xLIST(gReadyList, _, _, _, _, _);
if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE ) if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE )
{ {
List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] ); List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] );
//@ assert( pxReadyList->pxIndex |-> gIndex ); //@ assert( pxReadyList->pxIndex |-> gIndex );
/*@ assert( DLS(gListEnd, ?gEndPrev, gListEnd, gEndPrev, /*@ assert( DLS(gEnd, ?gEndPrev, gEnd, gEndPrev,
gCells, gVals, gReadyList) ); gCells, gVals, gReadyList) );
@*/ @*/
@ -1012,7 +1013,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ assert( mem(pxTaskItem, gCells) == true); //@ assert( mem(pxTaskItem, gCells) == true);
//@ open DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, gReadyList); //@ open DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gReadyList);
//@ assert( xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList) ); //@ assert( xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList) );
//@ open xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList); //@ open xLIST_ITEM(&pxReadyList->xListEnd, _, _, _, gReadyList);
// opening required to prove validity of `&( pxReadyList->xListEnd )` // opening required to prove validity of `&( pxReadyList->xListEnd )`
@ -1025,10 +1026,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxLastTaskItem = pxLastTaskItem->pxPrevious; pxLastTaskItem = pxLastTaskItem->pxPrevious;
//@ close xLIST_ITEM(gOldLastTaskItem, gV, gO, gEndPrev, gReadyList); //@ close xLIST_ITEM(gOldLastTaskItem, gV, gO, gEndPrev, gReadyList);
} }
//@ close DLS(gListEnd, gEndPrev, gListEnd, gEndPrev, gCells, gVals, gReadyList); //@ close DLS(gEnd, gEndPrev, gEnd, gEndPrev, gCells, gVals, gReadyList);
/*@ close xLIST(gReadyList, gNumberOfItems, gIndex, gListEnd, //@ close xLIST(gReadyList, _, gIndex, gEnd, gCells, gVals);
gCells, gVals);
@*/
/* The ready task list for uxCurrentPriority is not empty, so uxTopReadyPriority /* The ready task list for uxCurrentPriority is not empty, so uxTopReadyPriority
* must not be decremented any further */ * must not be decremented any further */
@ -1036,16 +1035,14 @@ static void prvYieldForTask( TCB_t * pxTCB,
do do
/*@ invariant /*@ invariant
xLIST(gReadyList, gNumberOfItems, gIndex, gListEnd, mem(pxTaskItem, gCells) == true &*&
gCells, gVals) xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals);
&*&
mem(pxTaskItem, gCells) == true;
@*/ @*/
{ {
TCB_t * pxTCB; TCB_t * pxTCB;
//@ open xLIST(gReadyList, gNumberOfItems, gIndex, gListEnd, gCells, gVals); //@ open xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals);
//@ assert( DLS(gListEnd, ?gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) ); //@ assert( DLS(gEnd, ?gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gReadyList) );
// Building an SSA for important variables helps us to // Building an SSA for important variables helps us to
// refer to the right instances. // refer to the right instances.
@ -1075,10 +1072,6 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ close xLIST_ITEM(gTaskItem_3, _, _, _, gReadyList); //@ close xLIST_ITEM(gTaskItem_3, _, _, _, gReadyList);
//@ DLS_close_2(gTaskItem_3, gCells, gVals); //@ DLS_close_2(gTaskItem_3, gCells, gVals);
//@ assume(false);
// Make sure that we covered all cases so far
//@ assume(false);
#ifdef IGNORED
/*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */ /*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */
@ -1138,7 +1131,6 @@ static void prvYieldForTask( TCB_t * pxTCB,
vListInsertEnd( pxReadyList, pxTaskItem ); vListInsertEnd( pxReadyList, pxTaskItem );
break; break;
} }
#endif /* IGNORED */
} while( pxTaskItem != pxLastTaskItem ); } while( pxTaskItem != pxLastTaskItem );
} }
else else
@ -4297,11 +4289,11 @@ void vTaskSwitchContext( BaseType_t xCoreID )
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) coreLocalSeg_TCB_p(gCurrentTCB, 0)
&*& &*&
// read access to current task's stack pointer, etc // read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ?ulFreeBytesOnStack); prvSeg_TCB_p(gCurrentTCB, ?ulFreeBytesOnStack);
@*/ @*/
/*@ ensures // all locks are released and interrupts remain disabled /*@ ensures // all locks are released and interrupts remain disabled
@ -4312,11 +4304,11 @@ void vTaskSwitchContext( BaseType_t xCoreID )
&*& &*&
// opened predicate `coreLocalInterruptInv_p()` // opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gNewCurrentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?gNewCurrentTCB) &*&
pubTCB_p(gNewCurrentTCB, 0) &*& integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) coreLocalSeg_TCB_p(gCurrentTCB, 0)
&*& &*&
// read access to current task's stack pointer, etc // read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ulFreeBytesOnStack); prvSeg_TCB_p(gCurrentTCB, ulFreeBytesOnStack);
// Remark: the part of the post condition relating to TCBs will have to change. // Remark: the part of the post condition relating to TCBs will have to change.
@*/ @*/
{ {
@ -4346,10 +4338,10 @@ void vTaskSwitchContext( BaseType_t xCoreID )
// TODO: Inspect reason. // TODO: Inspect reason.
TaskHandle_t currentHandle = pxCurrentTCB; TaskHandle_t currentHandle = pxCurrentTCB;
//@ assert( currentHandle == gCurrentTCB ); //@ assert( currentHandle == gCurrentTCB );
//@ open pubTCB_p(gCurrentTCB, 0); //@ open coreLocalSeg_TCB_p(gCurrentTCB, 0);
UBaseType_t nesting = currentHandle->uxCriticalNesting; UBaseType_t nesting = currentHandle->uxCriticalNesting;
configASSERT( nesting == 0 ); configASSERT( nesting == 0 );
//@ close pubTCB_p(gCurrentTCB, 0); //@ close coreLocalSeg_TCB_p(gCurrentTCB, 0);
} }
#else #else
configASSERT( pxCurrentTCB->uxCriticalNesting == 0 ); configASSERT( pxCurrentTCB->uxCriticalNesting == 0 );

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

@ -77,8 +77,8 @@ ensures
/*@ /*@
// TODO: We know that the list of priority 0 is never empty. // TODO: We know that the list of priority 0 is never empty.
// It contains the idle task and nothing else. // It contains the idle task and nothing else.
predicate readyLists_p() = predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists) =
List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, ?gCellLists); List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, gCellLists);
@*/ @*/

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

@ -66,7 +66,7 @@ predicate TCB_p(TCB_t * tcb, uint32_t ulFreeBytesOnStack) =
tcb->uxPriority |-> _ &*& tcb->uxPriority |-> _ &*&
tcb->xTaskRunState |-> _ &*& tcb->xTaskRunState |-> ?gTaskRunState &*&
tcb->xIsIdle |-> _ &*& tcb->xIsIdle |-> _ &*&
// Assumes macro `configMAX_TASK_NAME_LEN` evaluates to 16. // Assumes macro `configMAX_TASK_NAME_LEN` evaluates to 16.
@ -102,13 +102,17 @@ predicate absTCB_p(TCB_t* tcb) =
// //
// The predicates below will be expanded iteratively. // The predicates below will be expanded iteratively.
predicate prvTCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) = predicate prvSeg_TCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack) =
tcb->pxStack |-> ?stackPtr &*& tcb->pxStack |-> ?stackPtr &*&
tcb->pxTopOfStack |-> ?topPtr &*& tcb->pxTopOfStack |-> ?topPtr &*&
stack_p_2(stackPtr, ?ulStackDepth, topPtr, stack_p_2(stackPtr, ?ulStackDepth, topPtr,
ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes); ulFreeBytesOnStack, ?ulUsedCells, ?ulUnalignedBytes);
predicate pubTCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) = predicate sharedSeg_TCB_p(TCB_t* tcb) =
tcb->xTaskRunState |-> ?gTaskRunState &*&
true;
predicate coreLocalSeg_TCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) =
tcb->uxCriticalNesting |-> uxCriticalNesting; tcb->uxCriticalNesting |-> uxCriticalNesting;
@*/ @*/

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

@ -29,8 +29,9 @@ fixpoint bool interruptsDisabled_f(uint32_t);
predicate coreLocalInterruptInv_p() = predicate coreLocalInterruptInv_p() =
pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*& pointer(&pxCurrentTCBs[coreID_f], ?currentTCB) &*&
pubTCB_p(currentTCB, 0) &*& //pubTCB_p(currentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _); integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _) &*&
coreLocalSeg_TCB_p(currentTCB, ?gCriticalNesting);
predicate coreLocalLocked(uint32_t coreID); predicate coreLocalLocked(uint32_t coreID);
@ -94,20 +95,11 @@ predicate taskISRLockInv() =
integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*& integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, ?gTopReadyPriority) &*&
0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
&*& &*&
readyLists_p() &*& readyLists_p(?gCellLists) &*&
// Update: The current task on this core is interrupt protected.
// TODO: Exclude from `allTasks`.
// `allTasks` stores pointers to all currently valid tasks (i.e. TCB_t instances)
//foreach(?tasks, absTCB_p) &*&
// If a task is scheduled, it must be valid
//[0.5]pointer(&pxCurrentTCBs[coreID_f()], ?scheduledTask) &*&
//scheduledTask != NULL
// ? mem(scheduledTask, tasks) == true
// : true
//&*&
true; true;
lemma void produce_taskISRLockInv(); lemma void produce_taskISRLockInv();
requires locked(?heldLocks) &*& requires locked(?heldLocks) &*&
heldLocks == cons(?i, cons(?t, nil)) &*& heldLocks == cons(?i, cons(?t, nil)) &*&