have just been informed of the super fucking sick 2018 lyons et al paper which moves time around like a fluid
https://sel4.systems/Research/pdfs/scheduling-context-capabilities.pdf
The implication is that capabilities for time have a different flavour from those for spatial resources. They cannot support hierarchical delegation without loss, and cannot be recursively virtualised.
first example of realtime schedule i actually like
3.2.1 Budgets and scheduling contexts. At the core of the model is the scheduling context (SC) as the fundamental abstraction for time allocation. An SC is a representation of a reservation in the object-capability system, which means that SCs are first-class objects, like threads, address spaces, or communication endpoints (ports). An SC is represented by a capability to a scheduling context object (scCap).
so strongly analogous to the synchronization context (also called SC). i could even consider a mode that raises an exception if write beyond the amount previously allocated into the sync context by the task
