Expressive Modular Fine-Grained Concurrency Specification
Machine-Checked Theory

Bart Jacobs and Frank Piessens

Coq 8.2pl1 sources

Browse online:
(Best viewed with Firefox; IE has trouble with Coqdoc-generated HTML)

• The metatheory
  • Programs - The syntax of programs
  • Runs - Program executions
    In the form of an algorithm for computing the configuration that results from a given sequence of execution steps; this facilitates testing the semantics.
  • Assertions - Chunks (= basic permissions), bundles, and assertions
    Chunks may mention assertions (specifically, lock invariants and thread postconditions). Recursion is enabled by lazy unrolling.
  • AssertionTrue - Semantics of assertions
    The meaning of recursive assertions is given as usual as a fixpoint.
  • Correct - The proof rules of the program logic
  • Valid - Defines a weakest precondition-like predicate transformer called Valid, used as an intermediate step between the proof rules and the preservation proof
  • Soundness - The soundness proof
    Defines validity of a configuration, and proves that execution steps preserve it.
• Example modular proofs of programs
  • Incr - The Owicki-Gries example
    • IncrSpec - Specification of the Incr module
      In the form of a Coq module type.
    • Incr - Implementation of the Incr module
    • IncrCorrect - Proof of the Incr module
      Implements the IncrSpec module type
    • IncrClient - Implementation of the client program
      In the form of a function from proc to cmd
    • IncrClientCorrect - Proof of the client program
      In the form of a parameterized Coq module (similar to an O'Caml functor) that takes an IncrSpec instance as an argument.
    • IncrProgramSafe - Proof that the client program composed with the Incr module never aborts
    • IncrRuns - Some example executions
  • Ghost Sets - An implementation and proof of ghost sets
    Same modularity approach as for the Incr example
    • GhostSetsSpec - Specification of the ghost sets module
      The gset and gseth predicates are Coq module type parameters of type "function from arguments to syntactic assertion"
    • GhostSets - Implementation of ghost sets
    • GhostSetsCorrect - Proof of the ghost sets module
      Uses recursive assertions.
    • GhostSetsTests - Some example executions
  • CAS - A compare-and-swap (CAS) procedure and a tiny client program
    • AtomicsSpec - CAS specification
    • Atomics - CAS implementation
    • AtomicsCorrect - CAS proof
    • AtomicsClient - A tiny client program
    • AtomicsClientCorrect - Proof of the client program
    • AtomicsProgramSafe - Combines both proofs and applies the soundness theorem to obtain safety
    • AtomicsClientRuns - Some example executions
  • LCSet implementation - No specs or proofs at this time
    A verified LCSet implementation is included in the VeriFast distribution.
    Also, a full proof outline for the LCSet implementation is included in appendix in CW-590.
    • Semaphores
    • LCSet
    • Client

Index