The article “Mixed-criticality support in seL4” at
https://lwn.net/Articles/745946/ says seL4's solution to the problem of CPU
budget exhaustion while in a non-reentrant shared data-structure server is
timeout exceptions. The server might time out by chance, through no fault of
its own.
A
Kelly Dean writes:
> But network traffic might be mixed criticality. For example, real-time sensor
> data mixed with bulk file transfers. Suppose the most critical thread must be
> allocated 90% to cover its worst case utilization
Er, I worded that poorly. Should have been explicit
gernot.hei...@data61.csiro.au writes:
> The server’s apparent WCET is only 2W if the client fails to ensure that it’s
> got enough budget left. That’s a client bug, the client can ensure that it
> invokes the server with a fresh budget. It’s not the kernel’s job to ensure
> that buggy clients
gernot.hei...@data61.csiro.au writes:
> The server attempting to gate-keep and ensure that there’s enough time left
> for the request would be quite complex and probably expensive, as it would
> need a full model of its own execution. It would also be very pessimistic,
> given the pessimism
