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

DOI10.1007/978-3-319-43144-4_4zbMATH Open1478.68050OpenAlexW2416645316MaRDI QIDQ2829245FDOQ2829245

Christine Rizkallah, Corey Lewis, June Andronick, Daniel Matichuk, 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

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

Mathematics Subject Classification ID

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

Cites Work

• Isabelle/HOL. A proof assistant for higher-order logic
• An axiomatic proof technique for parallel programs
• Certifying low-level programs with hardware interrupts and preemptive threads
• Title not available (Why is that?)
• Using formal reasoning on a model of tasks for FreeRTOS
• Modular verification of preemptive OS kernels

Cited In (2)

• An intuitive formal proof for deadline driven scheduler
• Toward compositional verification of interruptible OS kernels and device drivers

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)