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

Partial proof justifying that updates of pxTaskItem in inner search loop in prvSelectHighestPriorityTask are safe.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-22 07:18:45 -05:00
parent 2fd6bcc2d7
commit 49643b6f5e
1 changed files with 84 additions and 0 deletions
Download patch file Download diff file Expand all files Collapse all files

84
tasks.c
View file

@ -1073,14 +1073,98 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ List_t* gReadyList = &pxReadyTasksLists[ uxCurrentPriority ];
//@ open xLIST(gReadyList, gNumberOfItems, gIndex, gListEnd, gCells, gVals);
//@ assert( DLS(gListEnd, ?gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) );
//@ int gTaskItemIndex0 = index_of(pxTaskItem, gCells);
//@ struct xLIST_ITEM* gTaskItem0 = pxTaskItem;
// Open DLS predicate to get access to `pxTaskItem`
/*@
if( gTaskItem0 == gListEnd) {
open DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
} else {
split(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gTaskItem0, gTaskItemIndex0);
assert( DLS( gListEnd, gEndPrev2, gTaskItem0, ?gTaskItemPrev, take(gTaskItemIndex0, gCells), take(gTaskItemIndex0, gVals), gReadyList) );
assert( DLS( gTaskItem0, gTaskItemPrev, gListEnd, gEndPrev2, drop(gTaskItemIndex0, gCells), drop(gTaskItemIndex0, gVals), gReadyList) );
open DLS(gTaskItem0, gTaskItemPrev, gListEnd, gEndPrev2, drop(gTaskItemIndex0, gCells), _, gReadyList);
}
@*/
pxTaskItem = pxTaskItem->pxNext;
//@ int gTaskItemIndex1 = index_of(pxTaskItem, gCells);
//@ struct xLIST_ITEM* gTaskItem1 = pxTaskItem;
// We have to prove ethat `gTaskItem1` points to a valid list item.
/*@
if( gTaskItem0 == gEndPrev2) {
;
} else {
open DLS(gTaskItem1, ?a, ?b, ?c, ?gCellsSuffix, ?e, gReadyList);
assert( mem(gTaskItem1, gCellsSuffix) == true );
assert( mem(gTaskItem1, gCells) == true );
close DLS(gTaskItem1, a, b, c, gCellsSuffix, e, gReadyList);
}
@*/
// close DLS predicate again
/*@
if( gTaskItem0 == gListEnd) {
close xLIST_ITEM(gListEnd, _, _, gEndPrev2, gReadyList);
close DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
} else {
assert( DLS( gListEnd, gEndPrev2, gTaskItem0, ?gTaskItemPrev, take(gTaskItemIndex0, gCells), take(gTaskItemIndex0, gVals), gReadyList) );
close xLIST_ITEM(gTaskItem0, _, _, gTaskItemPrev, gReadyList);
close DLS( gTaskItem0, gTaskItemPrev, gListEnd, gEndPrev2, drop(gTaskItemIndex0, gCells), drop(gTaskItemIndex0, gVals), gReadyList);
join(gListEnd, gEndPrev2, gTaskItem0, gTaskItemPrev, take(gTaskItemIndex0, gCells), take(gTaskItemIndex0, gVals),
gTaskItem0, gTaskItemPrev, gListEnd, gEndPrev2, drop(gTaskItemIndex0, gCells), drop(gTaskItemIndex0, gVals));
}
@*/
// unifying ghost branches
//@ assert( DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) );
// We have to prove ethat `gTaskItem1` points to a valid list item.
/*@
if( gTaskItem0 == gEndPrev2) {
dls_first_mem(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells);
assert( mem(gTaskItem1, gCells) == true );
} else {
;
}
@*/
// Open DLS predicate to get access to `pxTaskItem`
/*@
if( gTaskItem1 == gListEnd) {
open DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
} else {
split(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gTaskItem1, gTaskItemIndex1);
assert( DLS( gListEnd, gEndPrev2, gTaskItem1, ?gTaskItemPrev, take(gTaskItemIndex1, gCells), take(gTaskItemIndex1, gVals), gReadyList) );
assert( DLS( gTaskItem1, gTaskItemPrev, gListEnd, gEndPrev2, drop(gTaskItemIndex1, gCells), drop(gTaskItemIndex1, gVals), gReadyList) );
open DLS(gTaskItem1, gTaskItemPrev, gListEnd, gEndPrev2, _, _, gReadyList);
}
@*/
if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) )
{
pxTaskItem = pxTaskItem->pxNext;
}
/*@
if( gTaskItem1 == gListEnd) {
close xLIST_ITEM(gListEnd, _, _, gEndPrev2, gReadyList);
close DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
} else {
assert( DLS( gListEnd, gEndPrev2, gTaskItem1, ?gTaskItemPrev, take(gTaskItemIndex1, gCells), take(gTaskItemIndex1, gVals), gReadyList) );
close xLIST_ITEM(gTaskItem1, _, _, gTaskItemPrev, gReadyList);
close DLS( gTaskItem1, gTaskItemPrev, gListEnd, gEndPrev2, drop(gTaskItemIndex1, gCells), drop(gTaskItemIndex1, gVals), gReadyList);
join(gListEnd, gEndPrev2, gTaskItem1, gTaskItemPrev, take(gTaskItemIndex1, gCells), take(gTaskItemIndex1, gVals),
gTaskItem1, gTaskItemPrev, gListEnd, gEndPrev2, drop(gTaskItemIndex1, gCells), drop(gTaskItemIndex1, gVals));
}
@*/
// unifying ghost branches
//@ assert( DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) );
pxTCB = pxTaskItem->pvOwner;
/*debug_printf("Attempting to schedule %s on core %d\n", pxTCB->pcTaskName, portGET_CORE_ID() ); */