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

Added preliminary post condition for vTaskSwitchContext

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-16 14:26:37 -05:00
parent 4eb2fa573e
commit b330847935
1 changed files with 20 additions and 8 deletions
Download patch file Download diff file Expand all files Collapse all files

16
tasks.c
View file

@ -4128,11 +4128,12 @@ BaseType_t xTaskIncrementTick( void )
void vTaskSwitchContext( BaseType_t xCoreID )
/*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
xCoreID == coreID_f() &*&
// access to locks and disabled interrupts
locked(nil) &*&
[?f_ISR]isrLock() &*&
[?f_task]taskLock() &*&
interruptState_p(xCoreID, ?state) &*&
xCoreID == coreID_f() &*&
interruptsDisabled_f(state) == true &*&
// opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
@ -4140,7 +4141,17 @@ void vTaskSwitchContext( BaseType_t xCoreID )
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
@*/
//@ ensures true;
/*@ ensures // all locks release and interrupts remain disabled
locked(nil) &*&
[f_ISR]isrLock() &*&
[f_task]taskLock() &*&
interruptState_p(xCoreID, state) &*&
// opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gNewCurrentTCB) &*&
pubTCB_p(gNewCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _);
// Remark: the part of the post condition relating to TCBs will have to change.
@*/
{
/* Acquire both locks:
* - The ISR lock protects the ready list from simultaneous access by
@ -4253,6 +4264,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
#endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */
}
}
//@ close pubTCB_p(gCurrentTCB, 0);
//@ close taskISRLockInv();
//@ consume_taskISRLockInv();
portRELEASE_ISR_LOCK();