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

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.

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

2021 ◽  
Vol 5 (ICFP) ◽  
pp. 1-30
Author(s):  
Aymeric Fromherz ◽  
Aseem Rastogi ◽  
Nikhil Swamy ◽  
Sydney Gibson ◽  
Guido Martínez ◽  
...  
Keyword(s):  
Linked Data ◽  
Separation Logic ◽  
Concurrent Programs ◽  
Interactive Proof ◽  
First Order ◽  
Session Types ◽  
Verification Condition ◽  
New Formulation ◽  
Concurrent Separation Logic ◽  
Efficient Verification

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.

scholarly journals Linear capabilities for fully abstract compilation of separation-logic-verified code

2021 ◽  
Vol 31 ◽  
Author(s):  
THOMAS VAN STRYDONCK ◽  
FRANK PIESSENS ◽  
DOMINIQUE DEVRIESE
Keyword(s):  
Spatial Separation ◽  
Separation Logic ◽  
Target Language ◽  
Fine Grained ◽  
Dynamic Contract ◽  
Modular Verification ◽  
Source Program ◽  
Memory Accesses ◽  
Memory Resources ◽  
Efficient Memory

Abstract Separation logic is a powerful program logic for the static modular verification of imperative programs. However, dynamic checking of separation logic contracts on the boundaries between verified and untrusted modules is hard because it requires one to enforce (among other things) that outcalls from a verified to an untrusted module do not access memory resources currently owned by the verified module. This paper proposes an approach to dynamic contract checking by relying on support for capabilities, a well-studied form of unforgeable memory pointers that enables fine-grained, efficient memory access control. More specifically, we rely on a form of capabilities called linear capabilities for which the hardware enforces that they cannot be copied. We formalize our approach as a fully abstract compiler from a statically verified source language to an unverified target language with support for linear capabilities. The key insight behind our compiler is that memory resources described by spatial separation logic predicates can be represented at run time by linear capabilities. The compiler is separation-logic-proof-directed: it uses the separation logic proof of the source program to determine how memory accesses in the source program should be compiled to linear capability accesses in the target program. The full abstraction property of the compiler essentially guarantees that compiled verified modules can interact with untrusted target language modules as if they were compiled from verified code as well. This article is an extended version of one that was presented at ICFP 2019 (Van Strydonck et al., 2019).

scholarly journals Cosmo: a concurrent separation logic for multicore OCaml

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

scholarly journals Mechanized verification of fine-grained concurrent programs

2015 ◽  
Vol 50 (6) ◽  
pp. 77-87 ◽  
Author(s):  
Ilya Sergey ◽  
Aleksandar Nanevski ◽  
Anindya Banerjee
Keyword(s):  
Concurrent Programs ◽  
Fine Grained ◽  
Mechanized Verification

scholarly journals Program extraction applied to monadic parsing

2019 ◽  
Vol 29 (4) ◽  
pp. 487-518 ◽  
Author(s):  
Ulrich Berger ◽  
Alison Jones ◽  
Monika Seisenberger
Keyword(s):  
Natural Language ◽  
Case Studies ◽  
Proof System ◽  
Theoretic Approach ◽  
Formal Proofs ◽  
Interactive Proof ◽  
Program Extraction ◽  
Interactive Proof System

Abstract This article outlines a proof-theoretic approach to developing correct and terminating monadic parsers. Using modified realizability, we extract formally verified and terminating programs from formal proofs. By extracting both primitive parsers and parser combinators, it is ensured that all complex parsers built from these are also correct, complete and terminating for any input. We demonstrate the viability of our approach by means of two case studies: we extract (i) a small arithmetic calculator and (ii) a non-deterministic natural language parser. The work is being carried out in the interactive proof system Minlog.

Martha Komter, Dilemmas in the courtroom: A study of trials of violent crime in the Netherlands. (Everyday communication: Case studies of behavior in context.) Mahwah, NJ: Erlbaum, 1998. Pp. xxix, 186. Hb $49.95, pb $27.50.

2000 ◽  
Vol 29 (1) ◽  
pp. 133-136
Author(s):  
Greg Matoesian
Keyword(s):  
The Netherlands ◽  
Case Studies ◽  
Violent Crime ◽  
Multiplex Analysis ◽  
Fine Grained ◽  
Compliment Responses ◽  
Everyday Communication

Among the most relevant, practical issues in the courtroom – and explicitly recognized by attorneys well in advance of their occurrence – are the potential dilemmas involved in the questioning of witnesses. Practicing attorneys (and often their trial consultants) spend much time considering strategies for managing these. If we do X, this will happen; if we do Y, that will happen. Komter's book is a fine-grained and multiplex analysis of the interactional dilemmas that confront courtroom participants in cases of violent crime in the Netherlands. Using a conversation-analytic/ethnomethodological framework, she examines the communicative dilemmas that arise in a system with both adversarial and inquisitorial elements, and she shows how these dilemmas are shaped by the institutional interests of the participants. In a much broader sense, her study continues a strong empirical program initiated by Atkinson & Drew 1979 on the attribution and negotiation of blame in accusation sequences; but other readers may find Komter's work strikingly reminiscent of Pomerantz's classic analysis (1978) of the interactional dilemmas that shape compliment responses.

Sign in / Sign up

Export Citation Format

Share Document