Imagelibrary/seL4
1
0
Fork 1
mirror of https://github.com/seL4/seL4.git synced 2026-04-09 16:59:55 +00:00
Code Issues Packages Projects Releases Wiki Activity

mcs: Explicitly check that sporadic scs are active

Browse Source 
Easier to check this explicitly than prove the invariant.

Signed-off-by: Curtis Millar <curtis@curtism.me>
This commit is contained in:
Curtis Millar
2021-08-02 16:30:38 +10:00
committed by Gerwin Klein
parent 43b2029d02
commit 17109eb8c9
1 changed files with 4 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files

5
include/kernel/sporadic.h
View File

@@ -159,7 +159,10 @@ static inline bool_t sc_released(sched_context_t *sc)
*/
static inline bool_t sc_sporadic(sched_context_t *sc)
{
return sc != NULL && sc->scSporadic;
/* We do expect sc_active to be always true if sc is not NULL when
sc_sporadic is called, but we have not proved it yet. */
assert(sc == NULL || sc_active(sc));
return sc != NULL && sc_active(sc) && sc->scSporadic;
}
/*