|
COMPLX:
A
Verification
Framework
for
Concurrent
Imperative
Programs
Title: |
COMPLX: A Verification Framework for Concurrent Imperative Programs |
Authors:
|
Sidney Amani,
June Andronick,
Maksym Bortin,
Corey Lewis,
Christine Rizkallah and
Joseph Tuong
|
Submission date: |
2016-11-29 |
Abstract: |
We propose a concurrency reasoning framework for imperative programs,
based on the Owicki-Gries (OG) foundational shared-variable
concurrency method. Our framework combines the approaches of
Hoare-Parallel, a formalisation of OG in Isabelle/HOL for a simple
while-language, and Simpl, a generic imperative language embedded in
Isabelle/HOL, allowing formal reasoning on C programs. We define the
Complx language, extending the syntax and semantics of Simpl with
support for parallel composition and synchronisation. We additionally
define an OG logic, which we prove sound w.r.t. the semantics, and a
verification condition generator, both supporting involved low-level
imperative constructs such as function calls and abrupt termination.
We illustrate our framework on an example that features exceptions,
guards and function calls. We aim to then target concurrent operating
systems, such as the interruptible eChronos embedded operating system
for which we already have a model-level OG proof using Hoare-Parallel. |
Change history: |
[2017-01-13]:
Improve VCG for nested parallels and sequential sections
(revision 30739dbc3dcb) |
BibTeX: |
@article{Complx-AFP,
author = {Sidney Amani and June Andronick and Maksym Bortin and Corey Lewis and Christine Rizkallah and Joseph Tuong},
title = {COMPLX: A Verification Framework for Concurrent Imperative Programs},
journal = {Archive of Formal Proofs},
month = nov,
year = 2016,
note = {\url{http://isa-afp.org/entries/Complx.html},
Formal proof development},
ISSN = {2150-914x},
}
|
License: |
BSD License |
Depends on: |
Word_Lib |
Status: [ok] |
This is a development version of this entry. It might change over time
and is not stable. Please refer to release versions for citations.
|
|