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

Introduced list of flat list of tasks in lock invariant. Simplifies access to sharedSeg_TCB_p chunks.

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-02 14:59:06 -05:00
parent eb1cfa53d3
commit df780a1823
4 changed files with 51 additions and 78 deletions
Download patch file Download diff file Expand all files Collapse all files

85
tasks.c
View file

@ -988,15 +988,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
#endif #endif
//@ open taskISRLockInv_p(); //@ open taskISRLockInv_p();
//@ assert( valid_sharedSeg_TCBs_p(?gTaskLists) ); //@ assert( exists_in_taskISRLockInv_p(?gTasks) );
// Eliminates exists predicate to avoid pattern matching conflicts
//@ open exists(gTaskLists);
// Get list containing currentTCB and ensure we matched the right variable
//@ assert( exists(?gCurrentTCB_category) );
//@ assert( mem(gCurrentTCB, gCurrentTCB_category) == true );
//@ open readyLists_p(?gCellLists, ?gOwnerLists); //@ open readyLists_p(?gCellLists, ?gOwnerLists);
//@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority);
@ -1048,14 +1040,8 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ mem_nth(uxCurrentPriority, gCellLists); //@ mem_nth(uxCurrentPriority, gCellLists);
//@ assert( mem(gCells, gCellLists) == true); //@ assert( mem(gCells, gCellLists) == true);
// Prove that `mem(gOwners, gTaskLists) == true` // Prove that `gTasks` contains all tasks in current ready
// Necessary to get access to `sharedSeg_TCB_p` predicates of //@ forall_mem(gOwners, gOwnerLists, (superset)(gTasks));
// current ready list in the loop
//@ assert( mem(gOwners, gOwnerLists) == true );
//@ assert( forall(gOwnerLists, (mem_list_elem)(gTaskLists) ) == true );
//@ forall_instantiate(gOwners, gOwnerLists, (mem_list_elem)(gTaskLists));
//@ assert( mem(gOwners, gTaskLists) == true );
///@ open_valid_sharedSeg_TCBs(gTaskLists, gOwners);
do do
/*@ invariant /*@ invariant
@ -1065,10 +1051,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
mem(pxTaskItem, gCells) == true &*& mem(pxTaskItem, gCells) == true &*&
xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*& xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners) &*&
gSize > 0 &*& gSize > 0 &*&
valid_sharedSeg_TCBs_p(gTaskLists) &*& foreach(gTasks, sharedSeg_TCB_p) &*&
mem(gOwners, gTaskLists) == true &*& subset(gOwners, gTasks) == true;
mem(gCurrentTCB, gCurrentTCB_category) == true &*&
mem(gCurrentTCB_category, gTaskLists) == true;
@*/ @*/
{ {
TCB_t * pxTCB; TCB_t * pxTCB;
@ -1089,9 +1074,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) ) if( ( void * ) pxTaskItem == ( void * ) &( pxReadyList->xListEnd ) )
{ {
//@ open DLS(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList);
// Prove that `gTaskItem_1->pxNext != gEnd` // Prove that `gTaskItem_1->pxNext != gEnd`
//@ dls_distinct(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells);
//@ open DLS(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList);
//@ open DLS(?gTaskItem_1_next, _, gEnd, gEndPrev2, _, _, _, gReadyList); //@ open DLS(?gTaskItem_1_next, _, gEnd, gEndPrev2, _, _, _, gReadyList);
//@ assert( gTaskItem_1_next != gEnd ); //@ assert( gTaskItem_1_next != gEnd );
/*@ close DLS(gTaskItem_1_next, _, gEnd, gEndPrev2, /*@ close DLS(gTaskItem_1_next, _, gEnd, gEndPrev2,
@ -1104,7 +1089,6 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ close xLIST_ITEM(gTaskItem_1, _, _, _, _, gReadyList); //@ close xLIST_ITEM(gTaskItem_1, _, _, _, _, gReadyList);
//@ close DLS(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList); //@ close DLS(gEnd, gEndPrev2, gEnd, gEndPrev2, gCells, gVals, gOwners, gReadyList);
} }
//@ struct xLIST_ITEM* gTaskItem_final = pxTaskItem; //@ struct xLIST_ITEM* gTaskItem_final = pxTaskItem;
//@ DLS_open_2(gTaskItem_final); //@ DLS_open_2(gTaskItem_final);
@ -1115,8 +1099,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
//@ DLS_close_2(gTaskItem_final, gCells, gVals, gOwners); //@ DLS_close_2(gTaskItem_final, gCells, gVals, gOwners);
// Getting access to fields of `pxTCB` // Getting access to fields of `pxTCB`
//@ open_valid_sharedSeg_TCBs(gTaskLists, gOwners); //@ assert( subset(gOwners, gTasks) == true );
//@ foreach_remove(pxTCB, gOwners); //@ mem_subset(pxTCB, gOwners, gTasks);
//@ foreach_remove(pxTCB, gTasks);
//@ open sharedSeg_TCB_p(pxTCB); //@ open sharedSeg_TCB_p(pxTCB);
/*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() ); */
@ -1144,30 +1129,15 @@ static void prvYieldForTask( TCB_t * pxTCB,
#endif #endif
#endif #endif
{ {
//@ assert( foreach(remove(pxTCB, gOwners), sharedSeg_TCB_p) ); //@ assert( foreach(remove(pxTCB, gTasks), sharedSeg_TCB_p) );
//@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] ); //@ assert( gCurrentTCB == pxCurrentTCBs[ xCoreID ] );
/*@ /*@
if( gCurrentTCB == pxTCB ) { if( gCurrentTCB == pxTCB ) {
// We can use the opened `sharedSeg_TCB_p` chunk // We can use the opened `sharedSeg_TCB_p` chunk
// for `pxTCB`. // for `pxTCB`.
} else { } else {
if( gCurrentTCB_category == gOwners ) { neq_mem_remove(gCurrentTCB, pxTCB, gTasks);
// `gCurrentTCB` is different from `pxTCB` but foreach_remove(gCurrentTCB, remove(pxTCB, gTasks));
// they belong to the same ready list.
assert( mem(gCurrentTCB, gOwners) == true );
mem_after_remove(gCurrentTCB, gOwners, pxTCB);
assert( mem(gCurrentTCB, remove(pxTCB, gOwners)) == true );
foreach_remove(gCurrentTCB, remove(pxTCB, gOwners));
} else {
assert( mem(gCurrentTCB_category, gTaskLists) == true );
mem_after_remove(gCurrentTCB_category, gTaskLists, gOwners);
assert( mem(gCurrentTCB_category, remove(gOwners, gTaskLists)) == true );
open_valid_sharedSeg_TCBs(remove(gOwners, gTaskLists),
gCurrentTCB_category);
foreach_remove(gCurrentTCB, gCurrentTCB_category);
}
open sharedSeg_TCB_p(gCurrentTCB); open sharedSeg_TCB_p(gCurrentTCB);
} }
@*/ @*/
@ -1182,37 +1152,23 @@ static void prvYieldForTask( TCB_t * pxTCB,
/*@ /*@
if( gCurrentTCB == pxTCB ) { if( gCurrentTCB == pxTCB ) {
// We can used the opened `sharedSeg_TCB_p` chunk // We used the opened `sharedSeg_TCB_p` chunk
// for `pxTCB`. // for `pxTCB`.
// => We don't have to close anything. // => We don't have to close anything.
} else { } else {
// Above, we extracted `sharedSeg_TCB_p(gCurrentTCB)`
// from the collection of all remaining shared TCB
// segments and opened it.
// => Close predicate and restore collection.
close sharedSeg_TCB_p(gCurrentTCB); close sharedSeg_TCB_p(gCurrentTCB);
foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks));
if( gCurrentTCB_category == gOwners ) {
// `gCurrentTCB` is different from `pxTCB` but
// they belong to the same ready list.
foreach_unremove(gCurrentTCB, remove(pxTCB, gOwners));
} else {
foreach_unremove(gCurrentTCB, gCurrentTCB_category);
close_valid_sharedSeg_TCBs(remove(gOwners, gTaskLists),
gCurrentTCB_category);
}
} }
@*/ @*/
// Ensure we restored the collection as it was // Ensure we restored the collection as it was
// at the beginning of the block. // at the beginning of the block.
//@ assert( foreach(remove(pxTCB, gOwners), sharedSeg_TCB_p) ); //@ assert( foreach(remove(pxTCB, gTasks), sharedSeg_TCB_p) );
} }
} }
else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) else if( pxTCB == pxCurrentTCBs[ xCoreID ] )
{ {
//@ assume(false);
configASSERT( ( pxTCB->xTaskRunState == xCoreID ) || ( pxTCB->xTaskRunState == taskTASK_YIELDING ) ); configASSERT( ( pxTCB->xTaskRunState == xCoreID ) || ( pxTCB->xTaskRunState == taskTASK_YIELDING ) );
#if ( configNUM_CORES > 1 ) #if ( configNUM_CORES > 1 )
#if ( configUSE_CORE_AFFINITY == 1 ) #if ( configUSE_CORE_AFFINITY == 1 )
@ -1240,8 +1196,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
} }
//@ close sharedSeg_TCB_p(pxTCB); //@ close sharedSeg_TCB_p(pxTCB);
//@ foreach_unremove(pxTCB, gOwners); //@ foreach_unremove(pxTCB, gTasks);
//@ close_valid_sharedSeg_TCBs(gTaskLists, gOwners);
} while( pxTaskItem != pxLastTaskItem ); } while( pxTaskItem != pxLastTaskItem );
@ -1273,7 +1228,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
configASSERT( ( uxCurrentPriority > tskIDLE_PRIORITY ) || ( xTaskScheduled == pdTRUE ) ); configASSERT( ( uxCurrentPriority > tskIDLE_PRIORITY ) || ( xTaskScheduled == pdTRUE ) );
uxCurrentPriority--; uxCurrentPriority--;
} }
// TODO: Remove tmp assumption, prevents checking of rest of function // ensure that we covered all cases above
//@ assume(false); //@ assume(false);
configASSERT( taskTASK_IS_RUNNING( pxCurrentTCBs[ xCoreID ]->xTaskRunState ) ); configASSERT( taskTASK_IS_RUNNING( pxCurrentTCBs[ xCoreID ]->xTaskRunState ) );

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

@ -25,9 +25,10 @@ predicate List_array_p(List_t* array, int size,
cellLists == cons(?gCells, ?gTailCellLists) &*& cellLists == cons(?gCells, ?gTailCellLists) &*&
ownerLists == cons(?gOwners, ?gTailOwnerLists) &*& ownerLists == cons(?gOwners, ?gTailOwnerLists) &*&
pointer_within_limits(array) == true &*& pointer_within_limits(array) == true &*&
xLIST(array, ?gNumberOfItems, ?gIndex, ?gListEnd, gCells, ?gVals, xLIST(array, ?gLen, ?gIndex, ?gListEnd, gCells, ?gVals,
gOwners) gOwners)
&*& &*&
gLen < INT_MAX &*&
List_array_p(array + 1, size - 1, gTailCellLists, gTailOwnerLists) List_array_p(array + 1, size - 1, gTailCellLists, gTailOwnerLists)
) )
: ( : (
@ -56,7 +57,8 @@ ensures
gPrefCellLists == take(index, gCellLists) &*& gPrefCellLists == take(index, gCellLists) &*&
gPrefOwnerLists == take(index, gOwnerLists) &*& gPrefOwnerLists == take(index, gOwnerLists) &*&
pointer_within_limits(array) == true &*& pointer_within_limits(array) == true &*&
xLIST(array + index, _, _, _, ?gCells, ?gVals, ?gOwners) &*& xLIST(array + index, ?gLen, _, _, ?gCells, ?gVals, ?gOwners) &*&
gLen < INT_MAX &*&
gCells == nth(index, gCellLists) &*& gCells == nth(index, gCellLists) &*&
gOwners == nth(index, gOwnerLists) &*& gOwners == nth(index, gOwnerLists) &*&
mem(gOwners, gOwnerLists) == true &*& mem(gOwners, gOwnerLists) == true &*&
@ -76,7 +78,8 @@ ensures
lemma void List_array_join(List_t* array) lemma void List_array_join(List_t* array)
requires requires
List_array_p(array, ?gPrefSize, ?gPrefCellLists, ?gPrefOwnerLists) &*& List_array_p(array, ?gPrefSize, ?gPrefCellLists, ?gPrefOwnerLists) &*&
xLIST(array + gPrefSize, _, _, _, ?gCells, _, ?gOwners) &*& xLIST(array + gPrefSize, ?gLen, _, _, ?gCells, _, ?gOwners) &*&
gLen < INT_MAX &*&
pointer_within_limits(array + gPrefSize) == true &*& pointer_within_limits(array + gPrefSize) == true &*&
List_array_p(array + gPrefSize + 1, ?gSufSize, ?gSufCellLists, ?gSufOwnerLists); List_array_p(array + gPrefSize + 1, ?gSufSize, ?gSufCellLists, ?gSufOwnerLists);
ensures ensures

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

@ -104,16 +104,23 @@ requires true;
ensures drop(n, drop(m, xs)) == drop(n + m, xs); ensures drop(n, drop(m, xs)) == drop(n + m, xs);
// Can use `forall_mem` from `listex.gh` instead
// TODO: Can we prove this in VeriFast or do we have to axiomatise? // TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void forall_instantiate<t>(t x, list<t> xs, fixpoint(t, bool) f); lemma void forall_instantiate<t>(t x, list<t> xs, fixpoint(t, bool) f);
requires forall(xs, f) == true &*& mem(x, xs) == true; requires forall(xs, f) == true &*& mem(x, xs) == true;
ensures forall(xs, f) == true &*& f(x) == true; ensures forall(xs, f) == true &*& f(x) == true;
// Can use `neq_mem_remove` from `listex.gh` instead
// TODO: Can we prove this in VeriFast or do we have to axiomatise? // TODO: Can we prove this in VeriFast or do we have to axiomatise?
lemma void mem_after_remove<t>(t x, list<t> xs, t r); lemma void mem_after_remove<t>(t x, list<t> xs, t r);
requires true; requires true;
ensures mem(x, remove(r, xs)) == (mem(x, xs) && x != r); ensures mem(x, remove(r, xs)) == (mem(x, xs) && x != r);
fixpoint bool superset<t>(list<t> super, list<t> sub) {
return subset(sub, super);
}
@*/ @*/

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

@ -95,19 +95,20 @@ predicate taskISRLockInv_p() =
0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES
&*& &*&
// tasks / TCBs // tasks / TCBs
exists<list<list<void*> > >(?gTaskLists) exists_in_taskISRLockInv_p(?gTasks)
&*& &*&
// ∀l ∈ gTaskLists. ∀t ∈ l. sharedSeg_TCB_p(l) // Access permissions for every task
valid_sharedSeg_TCBs_p(gTaskLists) // TODO: Convert to read permissions
// ∀t ∈ gTasks. sharedSeg_TCB_p(t)
foreach(gTasks, sharedSeg_TCB_p)
&*& &*&
readyLists_p(?gCellLists, ?gOwnerLists) readyLists_p(?gCellLists, ?gOwnerLists)
&*& &*&
// gOwnerLists ⊆ gTaskLists // gTasks contains all relevant tasks
forall(gOwnerLists, (mem_list_elem)(gTaskLists)) == true mem(gCurrentTCB, gTasks) == true
&*& &*&
exists<list<void*> >(?gCurrentTCB_category) &*& // ∀l ∈ gOwnerLists. l ⊆ gTasks
mem(gCurrentTCB_category, gTaskLists) == true &*& forall(gOwnerLists, (superset)(gTasks)) == true;
mem(gCurrentTCB, gCurrentTCB_category) == true;
lemma void produce_taskISRLockInv(); lemma void produce_taskISRLockInv();
@ -125,6 +126,13 @@ requires locked_p( cons( pair(_, taskISRLockID_f()), ?otherLocks) ) &*&
ensures locked_p(otherLocks); ensures locked_p(otherLocks);
// Auxiliary predicate to assing names to existentially quantified variables.
// Having multiple `exists` chunks on the heap makes matching against their
// arguments ambiguous in most cases.
predicate exists_in_taskISRLockInv_p(list<void*> gTasks) =
exists(gTasks);
// Auxiliary function that allows us to partially apply the list argument. // Auxiliary function that allows us to partially apply the list argument.
// //
// Notes: // Notes: