We'll need to check what the formal spec says and how much work it would be to change it if it is the same as the code and not the same as the manual.

We'll need to check what the formal spec says and how much work it would be to change it if it is the same as the code and not the same as the manual.

The spec does the same as the code at the moment, so this would need re-verification. @michaelmcinerney is currently on leave, but when he is back he might be able to say if this one is quick and easy or the opposite.

We'll need to check what the formal spec says and how much work it would be to change it if it is the same as the code and not the same as the manual.

The spec does the same as the code at the moment, so this would need re-verification. @michaelmcinerney is currently on leave, but when he is back he might be able to say if this one is quick and easy or the opposite.

This should be a very straightforward update to the proofs, maybe just a day or so.

Turns out this is a bit more complex in the proofs. We specifically introduced this case 6 years ago in ba78e3b (and forgot to update the manual), because we were hitting lots of special casing when SC/TCB were already bound, even if it is just overwritten to be the same. Michael is looking into what would need to be done.

Current thinking is that we should make use of the updateFlags parameter to explicitly skip the update in this case. This should give us the behaviour the API reference has without needing more cases deeper down in the proof, only in the decode function, which is less critical.

I agree that not passing thread_control_sched_update_sc makes more sense when tcb->tcbSchedContext == sc (which implies sc->scTcb == tcb).

Will squash the new commit with the first if it's okay

I have been able to get the abstract invariants working with something analogous to the C in this PR as it is currently, but removing the check on line 1874 performed just before schedContext_bindTCB, given that we now know that we will be performing the bind in this case. So I think this behaviour will be fine for verification.

But my initial thoughts on this were that the old error behaviour was much more clear, and that if the TCB is bound to a sched context and we do not want to unbind them, then it is strange that the user would need to provide a cap to this sc just to end up performing a no-op. I would prefer to have the user pass in a bool as to whether they would like the sc changed. However, I'm not sure whether it's reasonable to expect the user to always know whether the TCB is bound, and if so, what sc it is bound to. I think the user does need to know this, but others in the verification team aren't sure. Introducing this user-provided bool would be a change to the API, so maybe we do not want to do that, but maybe it is a way of simplifying the code, in a way.

Adding a bool to the API would require an RFC, and it's not worth it. So if we can go ahead with Indan's suggestion of an outer if, then I should be able to get the proofs sorted within a couple of days, and then this can be merged.

But my initial thoughts on this were that the old error behaviour was much more clear,

The old behaviour was to always fail the call if the thread already had an SC bound, is that what you are referring to?

Sure it is clear, but it would make the syscall useless to call more than once during init. All the parameters can be configured with other system calls, so perhaps that's not a problem, but why have such a system call at all then?

and that if the TCB is bound to a sched context and we do not want to unbind them, then it is strange that the user would need to provide a cap to this sc just to end up performing a no-op.

Yes, very strange. I think the only purpose of seL4_TCB_SetSchedParams is to create tasks with slightly less system calls.

I would prefer to have the user pass in a bool as to whether they would like the sc changed. However, I'm not sure whether it's reasonable to expect the user to always know whether the TCB is bound, and if so, what sc it is bound to. I think the user does need to know this, but others in the verification team aren't sure. Introducing this user-provided bool would be a change to the API, so maybe we do not want to do that, but maybe it is a way of simplifying the code, in a way.

For passive tasks it is not reasonable to expect the user to know the current SC.

My personal preference would be to get rid of seL4_TCB_SetSchedParams altogether, both on MCS and non-MCS. The function can be emulated with multiple calls for backwards API compatibility.

But if we're doing such big breaking changes, the whole init functions could be cleared up. Currently there is way too much overlap between seL4_TCB_Configure, seL4_TCB_SetSpace and seL4_TCB_SetSchedParams. The only thing missing is an easy way to change or set fault_ep.

But if we're doing such big breaking changes, the whole init functions could be cleared up. Currently there is way too much overlap between seL4_TCB_Configure, seL4_TCB_SetSpace and seL4_TCB_SetSchedParams. The only thing missing is an easy way to change or set fault_ep.

Agreed, the only reason I stumbled on this at all is because I wanted to change the priority and fault_ep of a thread and set_sched_params seemed like the easiest of the three to use in my case.

The old behaviour was to always fail the call if the thread already had an SC bound, is that what you are referring to?

Yes, that's what I was referring to. I suppose that before, it was a much less useful call since it can't be called for TCBs that did have a bound SC, but my objection was really just to providing the cap to the SC and then getting a no-op.

But if we're doing such big breaking changes, the whole init functions could be cleared up. Currently there is way too much overlap between seL4_TCB_Configure, seL4_TCB_SetSpace and seL4_TCB_SetSchedParams. The only thing missing is an easy way to change or set fault_ep.

I hadn't thought about that. That could be interesting. Given that CRefine is still in progress and that the ccorres rules for these functions will need to be updated, if there is a significant simplification that could be made, then it might be worth it. We would need to make an RFC, so it could end up just taking too much time, but @lsf37 might have some thoughts on it.

But if we're doing such big breaking changes, the whole init functions could be cleared up. Currently there is way too much overlap between seL4_TCB_Configure, seL4_TCB_SetSpace and seL4_TCB_SetSchedParams. The only thing missing is an easy way to change or set fault_ep.

I hadn't thought about that. That could be interesting. Given that CRefine is still in progress and that the ccorres rules for these functions will need to be updated, if there is a significant simplification that could be made, then it might be worth it. We would need to make an RFC, so it could end up just taking too much time, but @lsf37 might have some thoughts on it.

In my opinion we should definitely not do bigger breaking changes without properly strong reasons -- we have no way to even estimate how much impact that would have on current users who'd all need to update their code.

This doesn't seem quite right to me yet. The current code doesn't update the flags in the null_cap case, which means that the syscall can't be used to unbind an sc.

I guess there's multiple ways to do this, but how about moving the flags update to after the scCap switch statement, with something like this?

if (tcb->tcbSchedContext != sc) {
    update_flags |= thread_control_sched_update_sc;
}

That should also make it a no-op when trying to unbind a thread that is already unbound, which to me feels like the appropriate generalisation of the change we're already making.

All of this would also let us remove the second half of the if statements at

Thanks for picking up on that, I think you're right. I've updated the flags update as you suggested and changed the checks in tcb.c in a separate commit.