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

TCB of currently scheduled task on core C is interrupt protected on core C. Updated invariants to reflect that.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 11:25:37 -05:00
parent dbf03a0ab2
commit 327423ef67
3 changed files with 17 additions and 17 deletions
Download patch file Download diff file Expand all files Collapse all files

16
tasks.c
View file

@ -4134,7 +4134,10 @@ void vTaskSwitchContext( BaseType_t xCoreID )
interruptState_p(xCoreID, ?state) &*&
xCoreID == coreID_f() &*&
interruptsDisabled_f(state) == true &*&
coreLocalGlobalVars_p();
// opened predicate `coreLocalGlobalVars_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0);
@*/
//@ ensures true;
{
@ -4149,7 +4152,6 @@ void vTaskSwitchContext( BaseType_t xCoreID )
portGET_TASK_LOCK(); /* Must always acquire the task lock first */
portGET_ISR_LOCK();
//@ get_taskISRLockInv();
//@ open coreLocalGlobalVars_p();
{
/* vTaskSwitchContext() must never be called from within a critical section.
* This is not necessarily true for vanilla FreeRTOS, but it is for this SMP port. */
@ -4164,13 +4166,9 @@ void vTaskSwitchContext( BaseType_t xCoreID )
//
// TODO: Inspect reason.
TaskHandle_t currentHandle = pxCurrentTCB;
//@ open taskISRLockInv();
//@ assert( foreach(?tasks, _) );
//@ foreach_remove(currentHandle, tasks);
//@ open absTCB_p(currentHandle);
//@ open TCB_p(currentHandle, _);
//@ assert( currentHandle->uxCriticalNesting |-> _ );
//@ assert( tskTaskControlBlock_uxCriticalNesting(currentHandle, _) );
//@ assert( currentHandle == gCurrentTCB );
///@ open taskISRLockInv();
//@ open pubTCB_p(gCurrentTCB, 0);
UBaseType_t nesting = currentHandle->uxCriticalNesting;
configASSERT( nesting == 0 );
}

4
verification/verifast/proof/task_predicates.h
View file

@ -104,8 +104,8 @@ predicate absTCB_p(TCB_t* tcb) =
predicate prvTCB_p(TCB_t* tcb, uint32_t ulFreeBytesOnStack);
predicate pubTCB_p(TCB_t* tcb) =
tcb->uxCriticalNesting |-> ?uxCriticalNesting;
predicate pubTCB_p(TCB_t* tcb, UBaseType_t uxCriticalNesting) =
tcb->uxCriticalNesting |-> uxCriticalNesting;
@*/
#endif /* TASKS_GH */

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

@ -87,14 +87,16 @@ fixpoint int taskISRLockID_f();
predicate taskISRLockInv() =
integer_((int*) &uxSchedulerSuspended, sizeof(UBaseType_t), false, _) &*&
readyLists_p() &*&
// Update: The current task on this core is interrupt protected.
// TODO: Exclude from `allTasks`.
// `allTasks` stores pointers to all currently valid tasks (i.e. TCB_t instances)
foreach(?tasks, absTCB_p) &*&
//foreach(?tasks, absTCB_p) &*&
// If a task is scheduled, it must be valid
[0.5]pointer(&pxCurrentTCBs[coreID_f()], ?scheduledTask) &*&
scheduledTask != NULL
? mem(scheduledTask, tasks) == true
: true
&*&
//[0.5]pointer(&pxCurrentTCBs[coreID_f()], ?scheduledTask) &*&
//scheduledTask != NULL
// ? mem(scheduledTask, tasks) == true
// : true
//&*&
true;