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

Formulated first version of contract for prvSelectHighestPriorityTask and adapted proof of vTaskSwitchContext accordingly.

Browse source
This commit is contained in:
Tobias Reinhard 2022-11-17 12:55:01 -05:00
parent fb01980b63
commit 9b2871bc92
1 changed files with 37 additions and 4 deletions
Download patch file Download diff file Expand all files Collapse all files

41
tasks.c
View file

@ -894,8 +894,40 @@ static void prvYieldForTask( TCB_t * pxTCB,
#if ( configUSE_PORT_OPTIMISED_TASK_SELECTION == 0 ) #if ( configUSE_PORT_OPTIMISED_TASK_SELECTION == 0 )
static BaseType_t prvSelectHighestPriorityTask( const BaseType_t xCoreID ) static BaseType_t prvSelectHighestPriorityTask( const BaseType_t xCoreID )
//@ requires true; /*@ requires 0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
//@ ensures true; xCoreID == coreID_f() &*&
// interrupts are disabled and locks acquired
interruptState_p(xCoreID, ?state) &*&
interruptsDisabled_f(state) == true &*&
taskLockInv() &*&
isrLockInv() &*&
taskISRLockInv()
&*&
// opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], ?gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
&*&
// read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ?ulFreeBytesOnStack);
@*/
/*@ ensures 0 <= xCoreID &*& xCoreID < configNUM_CORES &*&
xCoreID == coreID_f() &*&
// interrupts are disabled and locks acquired
interruptState_p(xCoreID, state) &*&
interruptsDisabled_f(state) == true &*&
taskLockInv() &*&
isrLockInv() &*&
taskISRLockInv()
&*&
// opened predicate `coreLocalInterruptInv_p()`
pointer(&pxCurrentTCBs[coreID_f], gCurrentTCB) &*&
pubTCB_p(gCurrentTCB, 0) &*&
integer_(&xYieldPendings[coreID_f], sizeof(BaseType_t), true, _)
&*&
// read access to current task's stack pointer, etc
prvTCB_p(gCurrentTCB, ulFreeBytesOnStack);
@*/
{ {
UBaseType_t uxCurrentPriority = uxTopReadyPriority; UBaseType_t uxCurrentPriority = uxTopReadyPriority;
BaseType_t xTaskScheduled = pdFALSE; BaseType_t xTaskScheduled = pdFALSE;
@ -4169,7 +4201,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
prvTCB_p(gCurrentTCB, ?ulFreeBytesOnStack); prvTCB_p(gCurrentTCB, ?ulFreeBytesOnStack);
@*/ @*/
/*@ ensures // all locks release and interrupts remain disabled /*@ ensures // all locks are released and interrupts remain disabled
locked(nil) &*& locked(nil) &*&
[f_ISR]isrLock() &*& [f_ISR]isrLock() &*&
[f_task]taskLock() &*& [f_task]taskLock() &*&
@ -4227,6 +4259,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
/* The scheduler is currently suspended - do not allow a context /* The scheduler is currently suspended - do not allow a context
* switch. */ * switch. */
xYieldPendings[ xCoreID ] = pdTRUE; xYieldPendings[ xCoreID ] = pdTRUE;
//@ close taskISRLockInv();
} }
else else
{ {
@ -4273,6 +4306,7 @@ void vTaskSwitchContext( BaseType_t xCoreID )
/* Select a new task to run using either the generic C or port /* Select a new task to run using either the generic C or port
* optimised asm code. */ * optimised asm code. */
//@ close taskISRLockInv();
( void ) prvSelectHighestPriorityTask( xCoreID ); ( void ) prvSelectHighestPriorityTask( xCoreID );
traceTASK_SWITCHED_IN(); traceTASK_SWITCHED_IN();
@ -4297,7 +4331,6 @@ void vTaskSwitchContext( BaseType_t xCoreID )
#endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */ #endif /* ( configUSE_NEWLIB_REENTRANT == 1 ) && ( configNEWLIB_REENTRANT_IS_DYNAMIC == 0 ) */
} }
} }
//@ close taskISRLockInv();
//@ consume_taskISRLockInv(); //@ consume_taskISRLockInv();
portRELEASE_ISR_LOCK(); portRELEASE_ISR_LOCK();
portRELEASE_TASK_LOCK(); portRELEASE_TASK_LOCK();