Skip to main content

OS Concurrency Verification

Concurrency in Operating Systems

Interleaving of the eChronos RTOS
  • Aim: This project aims to develop and apply frameworks for reasoning about concurrency in OS-code.
  • Context: Formal verification is important in safety critical software. To make sure that a verified system runs correctly one also needs to provide formal guarantees about the correctness of the underlying operating system (OS) that the program runs on. Data61's Trustworthy Systems group is famous for its formal verification of the seL4 microkernel in the Isabelle-HOL theorem prover.
    Most recent successfully verified operating systems, including seL4, run on uniprocessor platforms and with interrupts largely disabled. However, there is an increasing demand for verified real-time operating systems (RTOS) which require support for concurrency.
  • Approach: The project extends existing concurrency methods for verifying shared-variable programs, such as the foundational Owicki-Gries and Rely-Guarantee approaches. To reach our goal of improving the ease at which concurrent programs can be verified we have had a particular focus on increasing the automation and scalability of these methods, especially within the Isabelle-HOL theorem prover. We are also aiming to create a sound, modular and useful framework for proving refinement of concurrent programs.
  • Case Study: As part of this project we are modelling and verifying two example operating systems. These are the small, embedded eChronos RTOS, and a multicore version of seL4. Both have been embedded in high-assurance autonomous flying vehicles that have been developed in collaboration with industry and university partners as part of the DARPA-funded SMACCM project.

Activities

  • Functional Correctness of the eChronos RTOS: We have developed an abstract model of the eChronos RTOS that accurately represents the interleaving of the real implementation. Using this model we have then verified the main correctness property of the eChronos RTOS with a formal machine-checked proof within Isabelle/HOL.
  • Refinement to the Implementation: To complete the verification of the eChronos RTOS we wish to provide a refinement between the above abstract model and the actual implementation. This requires developing a scalable framework that supports both atomicity and data refinement.
  • Verification of Multicore seL4: The verification of multicore seL4 is a new project, targeting the "big lock" version of seL4 [1] and aiming at providing a formal model of interleaved execution. This will also include investigation of the best logic and concurrency model to use.
    [1] APSys For a microkernel, a big lock is fine, 2015

Availability

The proofs for the eChronos RTOS are open source and are available under the BSD 2-clause license on github.

Contact

June Andronick, june.andronick <at> data61.csiro.au

People


Publications

2017

Abstract PDF Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joseph Tuong
COMPLX: A verification framework for concurrent imperative programs
International Conference on Certified Programs and Proofs, pp. 138-150, Paris, France, January, 2017

2016

Abstract PDF June Andronick, Corey Lewis, Daniel Matichuk, Carroll Morgan and Christine Rizkallah
Proof of OS scheduling behavior in the presence of interrupt-induced concurrency
International Conference on Interactive Theorem Proving, pp. 52-68, Nancy, France, August, 2016

2015

Abstract
Slides
PDF June Andronick, Corey Lewis and Carroll Morgan
Controlled owicki-gries concurrency: reasoning about the preemptible eChronos embedded operating system
Workshop on Models for Formal Analysis of Real Systems (MARS 2015), pp. 10-24, Suva, Fiji, November, 2015