Steel: proof-oriented programming in a dependently typed concurrent separation logic

Steel is a language for developing and proving concurrent programs embedded in F ⋆ , a dependently typed programming language and proof assistant. Based on SteelCore, a concurrent separation logic (CSL) formalized in F ⋆ , our work focuses on exposing the proof rules of the logic in a form that enables programs and proofs to be effectively co-developed. Our main contributions include a new formulation of a Hoare logic of quintuples involving both separation logic and first-order logic, enabling efficient verification condition (VC) generation and proof discharge using a combination of tactics and SMT solving. We relate the VCs produced by our quintuple system to solving a system of associativity-commutativity (AC) unification constraints and develop tactics to (partially) solve these constraints using AC-matching modulo SMT-dischargeable equations. Our system is fully mechanized and implemented in F ⋆ . We evaluate it by developing several verified programs and libraries, including various sequential and concurrent linked data structures, proof libraries, and a library for 2-party session types. Our experience leads us to conclude that our system enables a mixture of automated and interactive proof, making it productive to build programs foundationally verified against a highly expressive, state-of-the-art CSL.

Download Full-text

TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs

ACM Transactions on Programming Languages and Systems ◽

10.1145/3477082 ◽

2021 ◽

Vol 43 (4) ◽

pp. 1-134

Author(s):

Emanuele D’Osualdo ◽

Julian Sutherland ◽

Azadeh Farzan ◽

Philippa Gardner

Keyword(s):

Case Studies ◽

Separation Logic ◽

Proof System ◽

Concurrent Programs ◽

Semantic Model ◽

Compositional Reasoning ◽

Fine Grained ◽

Fundamental Innovation ◽

Concurrent Separation Logic

We present TaDA Live, a concurrent separation logic for reasoning compositionally about the termination of blocking fine-grained concurrent programs. The crucial challenge is how to deal with abstract atomic blocking : that is, abstract atomic operations that have blocking behaviour arising from busy-waiting patterns as found in, for example, fine-grained spin locks. Our fundamental innovation is with the design of abstract specifications that capture this blocking behaviour as liveness assumptions on the environment. We design a logic that can reason about the termination of clients that use such operations without breaking their abstraction boundaries, and the correctness of the implementations of the operations with respect to their abstract specifications. We introduce a novel semantic model using layered subjective obligations to express liveness invariants and a proof system that is sound with respect to the model. The subtlety of our specifications and reasoning is illustrated using several case studies.

Download Full-text

Skipping the binder bureaucracy with mixed embeddings in a semantics course (functional pearl)

Proceedings of the ACM on Programming Languages ◽

10.1145/3473599 ◽

2021 ◽

Vol 5 (ICFP) ◽

pp. 1-28

Author(s):

Adam Chlipala

Keyword(s):

Order Reduction ◽

Separation Logic ◽

Variable Binding ◽

Type Checking ◽

Session Types ◽

The Coq Proof Assistant ◽

Reduction Program ◽

Coq Proof Assistant ◽

Big Ideas ◽

Concurrent Separation Logic

Rigorous reasoning about programs calls for some amount of bureaucracy in managing details like variable binding, but, in guiding students through big ideas in semantics, we might hope to minimize the overhead. We describe our experiment introducing a range of such ideas, using the Coq proof assistant, without any explicit representation of variables, instead using a higher-order syntax encoding that we dub "mixed embedding": it is neither the fully explicit syntax of deep embeddings nor the syntax-free programming of shallow embeddings. Marquee examples include different takes on concurrency reasoning, including in the traditions of model checking (partial-order reduction), program logics (concurrent separation logic), and type checking (session types) -- all presented without any side conditions on variables.

Download Full-text

Cosmo: a concurrent separation logic for multicore OCaml

Proceedings of the ACM on Programming Languages ◽

10.1145/3408978 ◽

2020 ◽

Vol 4 (ICFP) ◽

pp. 1-29

Author(s):

Glen Mével ◽

Jacques-Henri Jourdan ◽

François Pottier

Keyword(s):

Separation Logic ◽

Concurrent Separation Logic

Download Full-text

A Stable Mixed Element Method for the Biharmonic Equation with First-Order Function Spaces

Computational Methods in Applied Mathematics ◽

10.1515/cmam-2017-0002 ◽

2017 ◽

Vol 17 (4) ◽

pp. 601-616 ◽

Cited By ~ 4

Author(s):

Zheng Li ◽

Shuo Zhang

Keyword(s):

Biharmonic Equation ◽

Two Dimensions ◽

Zero Order ◽

Helmholtz Decomposition ◽

Numerical Verification ◽

Order Function ◽

First Order ◽

Mixed Element ◽

New Formulation ◽

Element Method

AbstractThis paper studies the mixed element method for the boundary value problem of the biharmonic equation {\Delta^{2}u=f} in two dimensions. We start from a {u\sim\nabla u\sim\nabla^{2}u\sim\operatorname{div}\nabla^{2}u} formulation that is discussed in [4] and construct its stability on {H^{1}_{0}(\Omega)\times\tilde{H}^{1}_{0}(\Omega)\times\bar{L}_{\mathrm{sym}}^% {2}(\Omega)\times H^{-1}(\operatorname{div},\Omega)}. Then we utilise the Helmholtz decomposition of {H^{-1}(\operatorname{div},\Omega)} and construct a new formulation stable on first-order and zero-order Sobolev spaces. Finite element discretisations are then given with respect to the new formulation, and both theoretical analysis and numerical verification are given.

Download Full-text