### Abstract

The concurrent refinement algebra developed here is designed to provide a foundation for rely/guarantee reasoning about concurrent programs. The algebra builds on a complete lattice of commands by providing sequential composition, parallel composition and a novel weak conjunction operator. The weak conjunction operator coincides with the lattice supremum providing its arguments are non-aborting, but aborts if either of its arguments do. Weak conjunction provides an abstract version of a guarantee condition as a guarantee process. We distinguish between models that distribute sequential composition over non-deterministic choice from the left (referred to as being conjunctive in the refinement calculus literature) and those that don't. Least and greatest fixed points of monotone functions are provided to allow recursion and iteration operators to be added to the language. Additional iteration laws are available for conjunctive models. The rely quotient of processes c and i is the process that, if executed in parallel with i implements c. It represents an abstract version of a rely condition generalised to a process.

### License

BSD License

### Topics

- Computer science/Concurrency

### Session Concurrent_Ref_Alg

- Refinement_Lattice
- Sequential
- Parallel
- Conjunction
- CRA
- Galois_Connections
- Iteration
- Conjunctive_Sequential
- Infimum_Nat
- Conjunctive_Iteration
- Rely_Quotient

## Cite

×

Concurrent_Ref_Alg-AFP

    @article{Concurrent_Ref_Alg-AFP,
      author  = {Julian Fell and Ian J. Hayes and Andrius Velykis},
      title   = {Concurrent Refinement Algebra and Rely Quotients},
      journal = {Archive of Formal Proofs},
      month   = {December},
      year    = {2016},
      note    = {\url{https://isa-afp.org/entries/Concurrent_Ref_Alg.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
- Jan 4, 2017 : Isabelle2016-1