Proof of OS Scheduling Behavior in the Presence of Interrupt-Induced Concurrency

ITP, pp. 52-68, 2016.

Cited by: 10|Bibtex|Views55
EI
Other Links: dblp.uni-trier.de|academic.microsoft.com

Abstract:

We present a simple yet scalable framework for formal reasoning and machine-assisted proof of interrupt-driven concurrency in operating-system code, and use it to prove the principal scheduling property of the embedded, real-time eChronos OS: that the running task is always the highest-priority runnable task. The key differentiator of thi...More

Code:

Data:

Your rating :
0

 

Tags
Comments