Compositional Virtual Timelines: Verifying Dynamic-Priority Partitions with Algorithmic Tem

on YouTube ↗27m

" summary

Claims a formally verified real-time OS kernel that enforces budget-enforcing EDF partitions and proves temporal isolation between partitions under the constraint that every task period is a multiple of its partition period. Proofs use a new braided virtual timeline abstraction and show schedulability by LCM/GCD transformations (example lifts three partitions to an LCM of 600). All code and proofs are mechanized in Coq and run on a small self‑driving car prototype.

AI-written summary · about

" chapters (16)

1. 0:00Real-time system partitioning
2. 1:03Temporal isolation in dynamic schedulers
3. 2:06Terminology and scheduling basics
4. 3:33Partition schedule flipping vulnerability
5. 4:57Static virtual timelines limitations
6. 6:47EDF scheduling for compositionality
7. 8:57Braided virtual timelines for priorities
8. 10:01Formal proof overview
9. 12:32Partition scheduler abstraction
10. 13:57Dynamic virtual timeline updates
11. 15:45Schedulability proof with timelines
12. 16:47Adjusting partition parameters
13. 19:39Temporal isolation in local schedulers
14. 22:29Avoiding information flow leaks
15. 23:13Demo: scheduling under interference
16. 25:06Summary and verified OS results