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

Finished verification of iteration updates in prvSelectHighestPriorityTask.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-23 15:18:11 -05:00
parent 9d1b47c5e5
commit 49af8fd30f
2 changed files with 46 additions and 3 deletions
Download patch file Download diff file Expand all files Collapse all files

44
tasks.c
View file

@ -1130,11 +1130,48 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ assert( mem(gTaskItem_3, gCells) == true ); //@ assert( mem(gTaskItem_3, gCells) == true );
// TODO: Remove /*@
// Ensure that we covered all cases until this point if( gTaskItem_3 == gListEnd ) {
//@ assume(false); open DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
} else{
split(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gTaskItem_3, gTaskItemIndex_3);
open DLS(gTaskItem_3, _, gListEnd, gEndPrev2, _, _, gReadyList);
}
@*/
pxTCB = pxTaskItem->pvOwner; pxTCB = pxTaskItem->pvOwner;
//@ close xLIST_ITEM(gTaskItem_3, ?gTaskItem_3_val, ?gTaskItem_3_next, _, gReadyList);
/*@
if( gTaskItem_3 == gListEnd ) {
close DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList);
} else{
assert( DLS(gListEnd, gEndPrev2, gTaskItem_3, ?gTaskItem_3_prev, ?gCellsPrefix, ?gValsPrefix, gReadyList) );
if( gTaskItem_3 == gEndPrev2 ) {
close DLS(gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2,
cons(gTaskItem_3, nil), cons(gTaskItem_3_val, nil),
gReadyList);
} else {
assert( DLS(gTaskItem_3_next, gTaskItem_3, gListEnd, gEndPrev2,
?gCellsSuffix2, ?gValsSuffix2, gReadyList));
close DLS(gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2,
cons(gTaskItem_3, gCellsSuffix2),
cons(gTaskItem_3_val, gValsSuffix2),
gReadyList);
}
assert( DLS(gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2, ?gCellsSuffix, ?gValsSuffix, gReadyList) );
join(gListEnd, gEndPrev2, gTaskItem_3, gTaskItem_3_prev, gCellsPrefix, gValsPrefix,
gTaskItem_3, gTaskItem_3_prev, gListEnd, gEndPrev2, gCellsSuffix, gValsSuffix);
}
@*/
//@ assert( DLS(gListEnd, gEndPrev2, gListEnd, gEndPrev2, gCells, gVals, gReadyList) );
// 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() ); */
#if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) )
@ -1193,6 +1230,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
vListInsertEnd( pxReadyList, pxTaskItem ); vListInsertEnd( pxReadyList, pxTaskItem );
break; break;
} }
#endif /* IGNORED */
} while( pxTaskItem != pxLastTaskItem ); } while( pxTaskItem != pxLastTaskItem );
} }
else else

5
verification/verifast/proof/single_core_proofs_extended/scp_list_predicates_extended.h
View file

@ -3,6 +3,11 @@
#include "single_core_proofs/scp_list_predicates.h" #include "single_core_proofs/scp_list_predicates.h"
/* =============================================================================
* The lemmas below assist in opening and closing DLS predicates in a way that
* allows accesses to `pxItem->pxNext`.
*/
/*@ /*@
lemma void DLS_end_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem) lemma void DLS_end_next_open(struct xLIST* pxList, struct xLIST_ITEM* pxItem)
requires requires