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

Updated ready list invariant from requiring exactly 1 idle task to configNUM_CORES idle tasks.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-07 07:34:46 -05:00
parent 9a81e7b860
commit 136b1d69b2
2 changed files with 6 additions and 6 deletions
Download patch file Download diff file Expand all files Collapse all files

2
tasks.c
View file

@ -1079,7 +1079,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
&*& &*&
subset(gOwners, gTasks) == true &*& subset(gOwners, gTasks) == true &*&
(uxCurrentPriority == 0 (uxCurrentPriority == 0
? length(gCells) == 2 ? length(gCells) == configNUM_CORES
: true : true
) &*& ) &*&
List_array_p(&pxReadyTasksLists, uxCurrentPriority, gPrefCellLists, List_array_p(&pxReadyTasksLists, uxCurrentPriority, gPrefCellLists,

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

@ -18,7 +18,7 @@ predicate readyLists_p(list<list<struct xLIST_ITEM*> > gCellLists,
length(gCellLists) == length(gOwnerLists) &*& length(gCellLists) == length(gOwnerLists) &*&
// List of priority 0 always contains the idle task and the end marker // List of priority 0 always contains the idle task and the end marker
// nothing else // nothing else
length( nth(0, gCellLists) ) == 2; length( nth(0, gCellLists) ) == configNUM_CORES;
predicate List_array_p(List_t* array, int size, predicate List_array_p(List_t* array, int size,
@ -139,7 +139,7 @@ lemma void closeUnchanged_readyLists(list<list<struct xLIST_ITEM*> > cellLists,
requires requires
configMAX_PRIORITIES == length(cellLists) &*& configMAX_PRIORITIES == length(cellLists) &*&
configMAX_PRIORITIES == length(ownerLists) &*& configMAX_PRIORITIES == length(ownerLists) &*&
length( nth(0, cellLists) ) == 2 &*& length( nth(0, cellLists) ) == configNUM_CORES &*&
List_array_p(&pxReadyTasksLists, ?gIndex, ?gPrefCellLists, ?gPrefOwnerLists) &*& List_array_p(&pxReadyTasksLists, ?gIndex, ?gPrefCellLists, ?gPrefOwnerLists) &*&
gIndex < length(cellLists) &*& gIndex < length(cellLists) &*&
xLIST(&pxReadyTasksLists + gIndex, ?gLen, _, _, ?gCells, ?gVals, ?gOwners) &*& xLIST(&pxReadyTasksLists + gIndex, ?gLen, _, _, ?gCells, ?gVals, ?gOwners) &*&
@ -181,7 +181,7 @@ lemma void closeReordered_readyLists(list<list<struct xLIST_ITEM*> > cellLists,
requires requires
configMAX_PRIORITIES == length(cellLists) &*& configMAX_PRIORITIES == length(cellLists) &*&
configMAX_PRIORITIES == length(ownerLists) &*& configMAX_PRIORITIES == length(ownerLists) &*&
length( nth(0, cellLists) ) == 2 &*& length( nth(0, cellLists) ) == configNUM_CORES &*&
List_array_p(&pxReadyTasksLists, ?gIndex, ?gPrefCellLists, ?gPrefOwnerLists) &*& List_array_p(&pxReadyTasksLists, ?gIndex, ?gPrefCellLists, ?gPrefOwnerLists) &*&
gIndex < length(cellLists) &*& gIndex < length(cellLists) &*&
xLIST(&pxReadyTasksLists + gIndex, ?gLen, _, _, reorderedCells, _, reorderedOwners) &*& xLIST(&pxReadyTasksLists + gIndex, ?gLen, _, _, reorderedCells, _, reorderedOwners) &*&
@ -220,7 +220,7 @@ ensures
assert( nth(0, gPrefCellLists) == nth(0, cellLists) ); assert( nth(0, gPrefCellLists) == nth(0, cellLists) );
} }
assert( length(nth(0, gReorderedCellLists)) == length(nth(0, cellLists)) ); assert( length(nth(0, gReorderedCellLists)) == length(nth(0, cellLists)) );
assert( length(nth(0, gReorderedCellLists)) == 2 ); assert( length(nth(0, gReorderedCellLists)) == configNUM_CORES );
close readyLists_p(gReorderedCellLists, gReorderedOwnerLists); close readyLists_p(gReorderedCellLists, gReorderedOwnerLists);
@ -256,7 +256,7 @@ void VF_reordeReadyList(List_t* pxReadyList, ListItem_t * pxTaskItem)
&*& &*&
length(gCellLists) == configMAX_PRIORITIES &*& length(gCellLists) == configMAX_PRIORITIES &*&
length(gOwnerLists) == configMAX_PRIORITIES &*& length(gOwnerLists) == configMAX_PRIORITIES &*&
length(nth(0, gCellLists)) == 2 &*& length(nth(0, gCellLists)) == configNUM_CORES &*&
0 <= gOffset &*& gOffset < length(gCellLists) 0 <= gOffset &*& gOffset < length(gCellLists)
&*& &*&
// current ready list // current ready list