Proof of OS scheduling behavior in the presence of interrupt-induced concurrency

DOI10.1007/978-3-319-43144-4_4MaRDI QIDQ2829245zbMATH OpenOpenAlexFDO

Authors June Andronick, Corey Lewis, Daniel Matichuk, Christine Rizkallah, Carroll Morgan

Publication date 27 October 2016

Published in Interactive Theorem Proving (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-43144-4_4

Mathematics Subject Classification ID

Theory of operating systems (68N25) Theorem proving (automated and interactive theorem provers, deduction, resolution, etc.) (68V15)

Recommendations

• Toward compositional verification of interruptible OS kernels and device drivers
• Modular verification of preemptive OS kernels
• Certifying low-level programs with hardware interrupts and preemptive threads
• Modular verification of preemptive OS kernels
• Proving fairness and implementation correctness of a microkernel scheduler

Cites work

• scientific article; zbMATH DE number 1330044 (Why is no real title available?)
• An axiomatic proof technique for parallel programs
• Certifying low-level programs with hardware interrupts and preemptive threads
• Isabelle/HOL. A proof assistant for higher-order logic
• Modular verification of preemptive OS kernels
• Using formal reasoning on a model of tasks for FreeRTOS

Cited in

(6)

• Certifying low-level programs with hardware interrupts and preemptive threads
• Toward compositional verification of interruptible OS kernels and device drivers
• Proving fairness and implementation correctness of a microkernel scheduler
• Using formal reasoning on a model of tasks for FreeRTOS
• Modular verification of preemptive OS kernels
• An intuitive formal proof for deadline driven scheduler

Describes a project that uses

Uses Software

• Isabelle
• Isabelle/HOL
• HOL
• Poly/ML
• FreeRTOS
• GitHub

This page was built for publication: Proof of OS scheduling behavior in the presence of interrupt-induced concurrency

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q2829245)