From e403e8bc74d94da36b330c9c6df66ddb1c82ab0b Mon Sep 17 00:00:00 2001 From: Tobias Reinhard <16916681+tobireinhard@users.noreply.github.com> Date: Sat, 3 Dec 2022 18:05:15 -0500 Subject: [PATCH] Added lemma to update the read permissions for unscheduled tasks after a task has been stopped. --- tasks.c | 64 +++++++++---------- .../verifast/proof/verifast_lock_predicates.h | 53 ++++++++++++++- 2 files changed, 83 insertions(+), 34 deletions(-) diff --git a/tasks.c b/tasks.c index 577afa43a..14522b505 100644 --- a/tasks.c +++ b/tasks.c @@ -1057,7 +1057,9 @@ static void prvYieldForTask( TCB_t * pxTCB, foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) &*& // Write permission for task scheduled on this core - [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) + [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*& + gCurrentTCB_state != taskTASK_NOT_RUNNING &*& + nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state &*& // TODO: // Write permissions for unscheduled tasks @@ -1155,56 +1157,54 @@ static void prvYieldForTask( TCB_t * pxTCB, //@ close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB); //@ foreach_unremove(pxTCB, gTasks); //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); // Get 2nd half of write permission for `gCurrentTCB` //@ foreach_remove(gCurrentTCB, gTasks); //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); - //@ int gCurrentTCB_index = index_of(gCurrentTCB, gTasks); - /*@ list gStates1 = - update(gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates); - @*/ - /* If the task is not being executed by any core swap it in */ pxCurrentTCBs[ xCoreID ]->xTaskRunState = taskTASK_NOT_RUNNING; - //@ assert( foreach(remove(gCurrentTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) ); + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + /*@ list gStates1 = + update(index_of(gCurrentTCB, gTasks), taskTASK_NOT_RUNNING, gStates); + @*/ //@ open exists_in_taskISRLockInv_p(gTasks, gStates); - /*@ close_updated_foreach_readOnly_sharedSeg_TCB - (gCurrentTCB, gTasks, gStates, - gStates1, taskTASK_NOT_RUNNING); + /*@ close_updated_foreach_readOnly_sharedSeg_TCB(gCurrentTCB, gTasks, gStates, + gStates1, taskTASK_NOT_RUNNING); @*/ - -//@ assume(false); - /*@ list gStates2 = - update(gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates); + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates1)) ); + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + /*@ stopUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running + (gCurrentTCB, gTasks, gTasks, gStates, gStates1); @*/ + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates1)) ); - // If we acquired an additional second half of a - // write permission for `gCurrentTCB`, release it. - /*@ - if( gCurrentTCB == pxTCB ) { - // We used the opened `sharedSeg_TCB_p` chunk - // for `pxTCB`. - // => We don't have to close anything. - } else { - close sharedSeg_TCB_p(gCurrentTCB, taskTASK_NOT_RUNNING); - assert( gCurrentTCB_index < length(gTasks) ); - assert( gCurrentTCB_index < length(gStates) ); - // nonauto_nth_update(gCurrentTCB_index, gCurrentTCB_index, taskTASK_NOT_RUNNING, gStates); - // assert( taskTASK_NOT_RUNNING == nth(gCurrentTCB_index, gStates2) ); - assume( taskTASK_NOT_RUNNING == nth(gCurrentTCB_index, gStates2) ); - close readOnly_sharedSeg_TCB_p(gTasks, gStates2)(gCurrentTCB); - foreach_unremove(gCurrentTCB, remove(pxTCB, gTasks)); - } - @*/ + + // Get write permission for `pxTCB` + //@ foreach_remove(pxTCB, gTasks); + //@ foreach_remove(pxTCB, gTasks); #if ( ( configNUM_CORES > 1 ) && ( configUSE_CORE_AFFINITY == 1 ) ) pxPreviousTCB = pxCurrentTCBs[ xCoreID ]; #endif pxTCB->xTaskRunState = ( TaskRunning_t ) xCoreID; + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates1)) ); + //@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) ); + /*@ list gStates2 = + update(index_of(pxTCB, gTasks), xCoreID, gStates1); + @*/ + + /*@ close_updated_foreach_readOnly_sharedSeg_TCB(pxTCB, gTasks, gStates1, + gStates2, xCoreID); + @*/ + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates2)) ); + //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates2)) ); + + pxCurrentTCBs[ xCoreID ] = pxTCB; xTaskScheduled = pdTRUE; diff --git a/verification/verifast/proof/verifast_lock_predicates.h b/verification/verifast/proof/verifast_lock_predicates.h index 27f4b2388..1a23bd9f9 100644 --- a/verification/verifast/proof/verifast_lock_predicates.h +++ b/verification/verifast/proof/verifast_lock_predicates.h @@ -107,9 +107,10 @@ predicate taskISRLockInv_p() = &*& // (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) + [1/2]sharedSeg_TCB_p(gCurrentTCB, ?gCurrentTCB_state) &*& + gCurrentTCB_state != taskTASK_NOT_RUNNING &*& + nth(index_of(gCurrentTCB, gTasks), gStates) == gCurrentTCB_state &*& - // TODO: // (RP-Unsched) Read permissions for unscheduled tasks // (RP-All) + (RP-Unsched) => Write permissions for unscheduled tasks // ∀t ∈ tasks. t->xTaskState == taskTASK_NOT_RUNNING @@ -283,6 +284,54 @@ ensures states, states2, s); foreach_unremove(updatedTask, tasks); } + + +lemma void stopUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running + (TCB_t* stoppedTask, list tasks, list subTasks, + list states, list states2) +requires + distinct(tasks) == true &*& + distinct(subTasks) == true &*& + length(tasks) == length(states) &*& + foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)) &*& + states2 == update(index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states) &*& + nth(index_of(stoppedTask, tasks), states) != taskTASK_NOT_RUNNING &*& + subset(subTasks, tasks) == true &*& + mem(stoppedTask, tasks) == true &*& + mem(stoppedTask, subTasks) + ? [1/2]sharedSeg_TCB_p(stoppedTask, taskTASK_NOT_RUNNING) + : true; +ensures + foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)); +{ + switch(subTasks) { + case nil: + open foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)); + close foreach(nil, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)); + case cons(h, t): + if( h == stoppedTask ) { + assert( remove(stoppedTask, subTasks) == t ); + distinct_mem_remove(stoppedTask, subTasks); + assert( mem(stoppedTask, t) == false ); + mem_index_of(stoppedTask, tasks); + } else { + mem_index_of(stoppedTask, tasks); + nth_update(index_of(h, tasks), index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states); + index_of_different(h, stoppedTask, tasks); + assert( index_of(h, tasks) != index_of(stoppedTask, tasks) ); + assert( nth(index_of(h, tasks), states) == nth(index_of(h, tasks), states2) ); + } + + nth_update(index_of(stoppedTask, tasks), index_of(stoppedTask, tasks), taskTASK_NOT_RUNNING, states); + open foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)); + open readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states)(h); + assert( nth(index_of(stoppedTask, tasks), states2) == taskTASK_NOT_RUNNING ); + close readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)(h); + stopUpdate_foreach_readOnly_sharedSeg_TCB_IF_not_running + (stoppedTask, tasks, t, states, states2); + close foreach(subTasks, readOnly_sharedSeg_TCB_IF_not_running_p(tasks, states2)); + } +} @*/