diff --git a/tasks.c b/tasks.c index 19fc931cf..e2380e65b 100644 --- a/tasks.c +++ b/tasks.c @@ -946,7 +946,7 @@ static void prvYieldForTask( TCB_t * pxTCB, #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) BaseType_t xPriorityDropped = pdFALSE; #endif - //@ close taskISRLockInv_p(); + //@ close _taskISRLockInv_p(gTopReadyPriority); while( xTaskScheduled == pdFALSE ) /*@ invariant @@ -958,7 +958,7 @@ static void prvYieldForTask( TCB_t * pxTCB, interruptsDisabled_f(state) == true &*& taskLockInv_p() &*& isrLockInv_p() &*& - taskISRLockInv_p() + _taskISRLockInv_p(gTopReadyPriority) &*& // opened predicate `coreLocalInterruptInv_p()` [0.5]pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*& @@ -971,8 +971,8 @@ static void prvYieldForTask( TCB_t * pxTCB, &*& // additional knowledge 0 <= uxCurrentPriority &*& uxCurrentPriority <= gTopReadyPriority &*& - gTopReadyPriority < configMAX_PRIORITIES - ; + gTopReadyPriority < configMAX_PRIORITIES; +// 0 <= uxCurrentPriority &*& uxCurrentPriority < configMAX_PRIORITIES; @*/ { #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) @@ -987,8 +987,10 @@ static void prvYieldForTask( TCB_t * pxTCB, } #endif - //@ open taskISRLockInv_p(); + //@ open _taskISRLockInv_p(gTopReadyPriority); //@ assert( exists_in_taskISRLockInv_p(?gTasks, ?gStates0) ); + //@ assert( integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, gTopReadyPriority) ); + //@ assert( gTopReadyPriority == uxTopReadyPriority); //@ open readyLists_p(?gCellLists, ?gOwnerLists); //@ List_array_p_index_within_limits(&pxReadyTasksLists, uxCurrentPriority); @@ -999,6 +1001,7 @@ static void prvYieldForTask( TCB_t * pxTCB, //@ assert( mem(gOwners, gOwnerLists) == true ); //@ open xLIST(gReadyList, _, _, _, _, _, _); + //@ assert( length(gCells) == gReadyList->uxNumberOfItems + 1 ); if( listLIST_IS_EMPTY( &( pxReadyTasksLists[ uxCurrentPriority ] ) ) == pdFALSE ) { List_t * const pxReadyList = &( pxReadyTasksLists[ uxCurrentPriority ] ); @@ -1058,11 +1061,9 @@ static void prvYieldForTask( TCB_t * pxTCB, &*& // Write permission for task scheduled on this core [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*& -// gCurrentTCB_state != taskTASK_NOT_RUNNING &*& (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*& nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state &*& - // TODO: // Write permissions for unscheduled tasks foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) &*& @@ -1281,8 +1282,6 @@ static void prvYieldForTask( TCB_t * pxTCB, { if( xDecrementTopPriority != pdFALSE ) { -// TODO: Remove tmp assumptions -//@ assume( uxTopReadyPriority > 0); uxTopReadyPriority--; #if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) { diff --git a/verification/verifast/proof/ready_list_predicates.h b/verification/verifast/proof/ready_list_predicates.h index 1a416a3a8..aec568dea 100644 --- a/verification/verifast/proof/ready_list_predicates.h +++ b/verification/verifast/proof/ready_list_predicates.h @@ -11,7 +11,10 @@ predicate readyLists_p(list > gCellLists, list > gOwnerLists) = configMAX_PRIORITIES == length(gCellLists) &*& List_array_p(&pxReadyTasksLists, configMAX_PRIORITIES, - gCellLists, gOwnerLists); + gCellLists, gOwnerLists) &*& + // List of priority 0 always contains the idle task and the end marker + // nothing else + length( nth(0, gCellLists) ) == 2; predicate List_array_p(List_t* array, int size, diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index c6eea6a7f..c4592b2d0 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -127,6 +127,51 @@ predicate taskISRLockInv_p() = forall(gOwnerLists, (superset)(gTasks)) == true; +// Auxiliary predicate. Equal to the lock invariant above but exposes +// some details. +predicate _taskISRLockInv_p(UBaseType_t gTopReadyPriority) = + // Access to global variables + [0.5]pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*& + integer_((void*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*& + integer_(&xSchedulerRunning, sizeof(BaseType_t), true, _) + &*& + // top ready priority must be in range + integer_((void*) &uxTopReadyPriority, sizeof(UBaseType_t), false, gTopReadyPriority) &*& + 0 <= gTopReadyPriority &*& gTopReadyPriority < configMAX_PRIORITIES + &*& + // tasks / TCBs + exists_in_taskISRLockInv_p(?gTasks, ?gStates) + &*& + // (RP-All) Read permissions for every task + // and recording of task states in state list + // (∀t ∈ gTasks. + // [1/2]sharedSeg_TCB_p(t, _)) + // ∧ + // ∀i. ∀t. gTasks[i] == t -> gStates[i] == t->xTaskRunState + foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) + &*& + // (RP-Current) Read permission for task currently scheduled on this core + // (RP-All) + (RP-Current) => Write permission for scheduled task + [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*& +// gCurrentTCB_state != taskTASK_NOT_RUNNING &*& + (gCurrentTCB_state == coreID_f() || gCurrentTCB_state == taskTASK_YIELDING) &*& + nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state + &*& + // (RP-Unsched) Read permissions for unscheduled tasks + // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks + // ∀t ∈ tasks. t->xTaskState == taskTASK_NOT_RUNNING + // -> [1/2]shared_TCB_p(t, taskTASK_NOT_RUNNING) + foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) + &*& + readyLists_p(?gCellLists, ?gOwnerLists) + &*& + // gTasks contains all relevant tasks + mem(gCurrentTCB, gTasks) == true + &*& + // ∀l ∈ gOwnerLists. l ⊆ gTasks + forall(gOwnerLists, (superset)(gTasks)) == true; + + lemma void produce_taskISRLockInv(); requires locked_p(?heldLocks) &*& heldLocks == cons(?i, cons(?t, nil)) &*&