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

Restored loop invariant at end of task-swapping branch

Browse source
This commit is contained in:
Tobias Reinhard 2022-12-04 10:33:36 -05:00
parent fbf4ba981f
commit b594404b59
1 changed files with 15 additions and 15 deletions
Download patch file Download diff file Expand all files Collapse all files

30
tasks.c
View file

@ -1135,6 +1135,7 @@ static void prvYieldForTask( TCB_t * pxTCB,
} }
#endif /* if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) */ #endif /* if ( ( configRUN_MULTIPLE_PRIORITIES == 0 ) && ( configNUM_CORES > 1 ) ) */
//@ bool gPxTCB_not_running = (pxTCB->xTaskRunState == taskTASK_NOT_RUNNING);
if( pxTCB->xTaskRunState == taskTASK_NOT_RUNNING ) if( pxTCB->xTaskRunState == taskTASK_NOT_RUNNING )
{ {
#if ( configNUM_CORES > 1 ) #if ( configNUM_CORES > 1 )
@ -1213,18 +1214,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
pxCurrentTCBs[ xCoreID ] = pxTCB; pxCurrentTCBs[ xCoreID ] = pxTCB;
xTaskScheduled = pdTRUE; xTaskScheduled = pdTRUE;
//@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStates2)) );
//@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates2)) );
//@ close exists_in_taskISRLockInv_p(gTasks, gStates2);
// Release second half of write permission for `pxTCB`
//@ foreach_unremove(pxTCB, gTasks);
// Ensure we restored the collection as it was
// at the beginning of the block.
//@ assert( foreach(remove(pxTCB, gTasks), readOnly_sharedSeg_TCB_p(gTasks, gStates)) );
//@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStates)) );
} }
} }
else if( pxTCB == pxCurrentTCBs[ xCoreID ] ) else if( pxTCB == pxCurrentTCBs[ xCoreID ] )
@ -1242,6 +1234,14 @@ static void prvYieldForTask( TCB_t * pxTCB,
xTaskScheduled = pdTRUE; xTaskScheduled = pdTRUE;
} }
} }
/*@
if( !gPxTCB_not_running ) { // else branch of swapping if-statement above
// Put read permission for `pxTCB` back
close [1/2]sharedSeg_TCB_p(pxTCB, _);
close readOnly_sharedSeg_TCB_p(gTasks, gStates)(pxTCB);
foreach_unremove(pxTCB, gTasks);
}
@*/
//@ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners); //@ close xLIST(gReadyList, gSize, gIndex, gEnd, gCells, gVals, gOwners);
@ -1256,9 +1256,9 @@ static void prvYieldForTask( TCB_t * pxTCB,
break; break;
} }
//@ close sharedSeg_TCB_p(pxTCB); //@ assert( exists_in_taskISRLockInv_p(gTasks, ?gStatesEnd) );
//@ close readOnly_sharedSeg_TCB(pxTCB); //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_p(gTasks, gStatesEnd)) );
//@ foreach_unremove(pxTCB, gTasks); //@ assert( foreach(gTasks, readOnly_sharedSeg_TCB_IF_not_running_p(gTasks, gStatesEnd)) );
} while( pxTaskItem != pxLastTaskItem ); } while( pxTaskItem != pxLastTaskItem );