Skip to main content

COMPLX: A verification framework for concurrent imperative programs

Authors

Sidney Amani, June Andronick, Maksym Bortin, Corey Lewis, Christine Rizkallah and Joey Tuong

DATA61

Abstract

We propose a concurrency reasoning framework for C programs, based on the Owicki-Gries (OG) foundational reasoning technique for shared-variable concurrency. Our framework, mechanised in the Isabelle/HOL theorem prover, combines the approaches of Hoare-Parallel, a formalisa- tion of OG in Isabelle/HOL for a simple while-language, and Simpl, a generic imperative language embedded in Is- abelle/HOL allowing formal reasoning of C programs. We define the COMPLX language extending the syntax and semantics of Simpl to include Parallel and Await constructs. We extend the OG proof rules to account for involved low- level C constructs such as function calls and abrupt termina- tion. We prove soundness of our rules w.r.t. our COMPLX semantics. We adapt and extend Hoare-Parallel’s verification condition generator tactic to account for the additional con- structs of the COMPLX language. We present several case studies demonstrating the practicality of our framework. In summary, we bridge the gap between model-level ver- ification and C implementation guarantees for concurrent code, with the aim to verify concurrent operating systems, such as the interruptible eChronos embedded operating sys- tem for which we already have a model-level proof using Hoare-Parallel.

BibTeX Entry

  @inproceedings{Amani_ABLRT_17,
    publisher        = {ACM-SIGPLAN},
    booktitle        = {International Conference on Certified Programs and Proofs},
    author           = {Amani, Sidney and Andronick, June and Bortin, Maksym and Lewis, Corey and Rizkallah, Christine and
                        Tuong, Joey},
    month            = jan,
    keywords         = {formal verification, programming languages, imperative code, concurrency, owicki-gries, isabelle/hol},
    year             = {2017},
    date             = {2017-1-17},
    title            = {{COMPLX}: a verification framework for concurrent imperative programs},
    pages            = {138--150},
    address          = {Paris, France}
  }

Download

Served by Apache on Linux on seL4.