Trustworthy Systems

COMPLX: A verification framework for concurrent imperative programs

Authors

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

DATA61

UNSW Sydney

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,
    address          = {Paris, France},
    author           = {Amani, Sidney and Andronick, June and Bortin, Maksym and Lewis, Corey and Rizkallah, Christine and
                        Tuong, Joey},
    booktitle        = {International Conference on Certified Programs and Proofs},
    date             = {2017-1-17},
    doi              = {https://doi.org/10.1145/3018610.3018627},
    keywords         = {formal verification, programming languages, imperative code, concurrency, owicki-gries, isabelle/hol},
    month            = jan,
    pages            = {138--150},
    paperurl         = {https://trustworthy.systems/publications/full_text/Amani_ABLRT_17.pdf},
    publisher        = {SIGPLAN Notices},
    title            = {{COMPLX}: a verification framework for concurrent imperative programs},
    year             = {2017}
  }

Download