### 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.

### License

BSD License

### History

January 13, 2017
  Improve VCG for nested parallels and sequential sections (revision 30739dbc3dcb)

### Topics

- Computer science/Programming languages/Logics
- Computer science/Programming languages/Language definitions

### Session Complx

- Language
- SmallStep
- OG_Annotations
- OG_Hoare
- SeqCatch_decomp
- OG_Soundness
- Cache_Tactics
- OG_Tactics
- OG_Syntax
- Examples
- SumArr

### Depends on

- Finite Machine Word Library

### Auto-related entries

- Combinatorial Enumeration Algorithms
- IMP2 – Simple Program Verification in Isabelle/HOL
- Verifying Imperative Programs using Auto2
- Hoare Logics for Time Bounds
- A Sequential Imperative Programming Language Syntax, Semantics, Hoare Logics and Verification Environment

## Cite

×

Complx-AFP

    @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   = {November},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Complx.html},
                 Formal proof development},
      ISSN    = {2150-914x},
    }

Download

## Download

× Download latest

Older releases:

- Sep 13, 2023 : Isabelle2023
- Oct 27, 2022 : Isabelle2022
- Dec 14, 2021 : Isabelle2021-1
- Feb 23, 2021 : Isabelle2021
- Apr 18, 2020 : Isabelle2020
- Jun 11, 2019 : Isabelle2019
- Aug 16, 2018 : Isabelle2018
- Oct 10, 2017 : Isabelle2017
- Dec 17, 2016 : Isabelle2016-1
- Nov 29, 2016 : Isabelle2016