priority checks in seL4_TCB_SetSchedParams()

[hexcoder-]

While doing a small review on the user manual, I saw in section 10.3.7.13 (seL4_TCB_SetSchedParams) that parameters mcp and priority are checked against authority, which is fine. But the relation mcp >= priority is not enforced, so for example the call would be accepted with authority->priority=10, priority=10, and mcp=9, thus yielding an inconsistent internal state (i think), where priority > mcp.

I consulted the source code for decodeSetSchedParams (

seL4/src/object/tcb.c

Line 1326 in 503ad77

tcb_t *authTCB = TCB_PTR(cap_thread_cap_get_capTCBPtr(authCap));

and the next lines). There are two calls for checkPriority(), each against authority.

invokeTCB_ThreadControl, which is called at the end of seL4_TCB_SetSchedParams seems to have the precondition that these values (mcp and priority) are already checked.

[Indanz]

There is nothing wrong with a state where priority > mcp, it just means a task is allowed to drop the priority, but not to increase it back to the original level.

[hexcoder-]

Thanks, this issue can than be closed.