Gernot.Heiser@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 get optimal service.
I see. Though wouldn't it make more sense for the server to check, instead of the client? Because the server needs to check anyway, so that a misbehaving client can't DoS other clients by repeatedly calling the server with insufficient budget and forcing the server to repeatedly time out and recover. And because the server is in a better position to handle its data-dependent execution times (i.e. as you said, not just pessimistically bail if remaining budget < WCET). So, the client can call unconditionally, the server can return an error code whenever it discovers it won't be able to finish in time, and the client's error checking doesn't depend on timing info about the server.
Anyway, that made me think of where else limited server time is a problem. At 19:13 in your presentation “Mixed-criticality support in seL4” at https://www.youtube.com/watch?v=ijTTZgQ8cB4 you gave the example of network drivers needing timely response to avoid packet loss. The solution at 30:47 was a scheduling context with high priority, short period, and budget