Gabriele Monaco [off-list ref] writes:

Alright, that /should/ be possible, provided the value used to set invariants is
constant or at least doesn't change until we leave the state.
This seems a fair assumption to make but doesn't stand for the throttle monitor,
in that case I read the remaining runtime from the dl entity, that one is
updated frequently, for instance when a task is throttled, it's negative, but
this doesn't mean the invariant should expect time to be negative.

Runtime is consumed only when a task is running, so here I use an invariant set
up on the /remaining/ runtime when reaching the running state, that's why also
switch_in resets the clock (runtime is not replenished, but the runtime_left
value doesn't need to be subtracted anything).

An alternative would be to have some sort of pause/resume operations on clocks,
and a task would just pause the clock when preempted, but those operations are
not backed up by theory and wouldn't really simplify the implementation (use 2
variables per clock or a single one and some hack to mark it as paused).

Again, there may be better ways, but I found this one the "simplest".

Does it makes sense or am I just crystallising to this implementation?

Ok, now it makes sense.

I have been thinking about this in the past days, and didn't come up
with anything better. Let's leave it be.

Nam