-
Specifying and Verifying Persistent Libraries
Authors:
Léo Stefanesco,
Azalea Raad,
Viktor Vafeiadis
Abstract:
We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correctness of individual libraries (horizontal and vertical compositionality) and is general enough to encompass all existing persisten…
▽ More
We present a general framework for specifying and verifying persistent libraries, that is, libraries of data structures that provide some persistency guarantees upon a failure of the machine they are executing on. Our framework enables modular reasoning about the correctness of individual libraries (horizontal and vertical compositionality) and is general enough to encompass all existing persistent library specifications ranging from hardware architectural specifications to correctness conditions such as durable linearizability. As case studies, we specify the FliT and Mirror libraries, verify their implementations over Px86, and use them to build higher-level durably linearizable libraries, all within our framework. We also specify and verify a persistent transaction library that highlights some of the technical challenges which are specific to persistent memory compared to weak memory and how they are handled by our framework.
△ Less
Submitted 2 June, 2023;
originally announced June 2023.
-
Trillium: Higher-Order Concurrent and Distributed Separation Logic for Intensional Refinement
Authors:
Amin Timany,
Simon Oddershede Gregersen,
Léo Stefanesco,
Jonas Kastberg Hinrichsen,
Léon Gondelman,
Abel Nieto,
Lars Birkedal
Abstract:
Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step-indexing comes, however, with an inherent cost: it restricts the adequacy theorem of program logics to a fairly simple class of safety properties. In this paper, we explore if and how inte…
▽ More
Expressive state-of-the-art separation logics rely on step-indexing to model semantically complex features and to support modular reasoning about imperative higher-order concurrent and distributed programs. Step-indexing comes, however, with an inherent cost: it restricts the adequacy theorem of program logics to a fairly simple class of safety properties. In this paper, we explore if and how intensional refinement is a viable methodology for strengthening higher-order concurrent (and distributed) separation logic to prove non-trivial safety and liveness properties. Specifically, we introduce Trillium, a language-agnostic separation logic framework for showing intensional refinement relations between traces of a program and a model. We instantiate Trillium with a concurrent language and develop Fairis, a concurrent separation logic, that we use to show liveness properties of concurrent programs under fair scheduling assumptions through a fair liveness-preserving refinement of a model. We also instantiate Trillium with a distributed language and obtain an extension of Aneris, a distributed separation logic, which we use to show refinement relations between distributed systems and TLA+ models.
△ Less
Submitted 6 December, 2023; v1 submitted 16 September, 2021;
originally announced September 2021.
-
Game Semantics: Easy as Pi
Authors:
Nobuko Yoshida,
Simon Castellan,
Léo Stefanesco
Abstract:
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order programming languages. However, due to the complexity of most game models, game semantics has remained unapproachable for non-experts.
In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation into a session typed pi-calculus, referred to as…
▽ More
Game semantics has proven to be a robust method to give compositional semantics for a variety of higher-order programming languages. However, due to the complexity of most game models, game semantics has remained unapproachable for non-experts.
In this paper, we aim at making game semantics more accessible by viewing it as a syntactic translation into a session typed pi-calculus, referred to as metalanguage, followed by a semantics interpretation of the metalanguage into a particular game model. The syntactic translation can be defined for a wide range of programming languages without knowledge of the particular game model used. Simple reasoning on the model (soundness, and adequacy) can be done at the level of the metalanguage, esca** tedious technical proofs usually found in game semantics. We call this methodology programming game semantics.
We design a metalanguage (PiDiLL) inspired from Differential Linear Logic (DiLL), which is concise but expressive enough to support features required by concurrent game semantics. We then demonstrate our methodology by yielding the first causal, non-angelic and interactive game model of CML, a higher-order call-by-value language with shared memory concurrency. We translate CML into PiDiLL and show that the translation is adequate. We give a causal and non-angelic game semantics model using event structures, which supports a simple semantics interpretation of PiDiLL. Combining both of these results, we obtain the first interactive model of a concurrent language of this expressivity which is adequate with respect to the standard weak bisimulation, and fully abstract for the contextual equivalence on second-order terms.
We have implemented a prototype which can explore the generated causal object from a subset of OCaml.
△ Less
Submitted 10 November, 2020;
originally announced November 2020.
-
Concurrent Separation Logic Meets Template Games
Authors:
Paul-André Melliès,
Léo Stefanesco
Abstract:
An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for higher-order programs, and Hoare logic for concurrent programs with shared memory and locks. In this paper, we establish a deep and unexpected connection between two recent lines of work on concurrent separ…
▽ More
An old dream of concurrency theory and programming language semantics has been to uncover the fundamental synchronization mechanisms which regulate situations as different as game semantics for higher-order programs, and Hoare logic for concurrent programs with shared memory and locks. In this paper, we establish a deep and unexpected connection between two recent lines of work on concurrent separation logic (CSL) and on template game semantics for differential linear logic (DiLL). Thanks to this connection, we reformulate in the purely conceptual style of template games for DiLL the asynchronous and interactive interpretation of CSL designed by Melliès and Stefanesco. We believe that the analysis reveals something important about the secret anatomy of CSL, and more specifically about the subtle interplay, of a categorical nature, between sequential composition, parallel product, errors and locks.
△ Less
Submitted 9 May, 2020;
originally announced May 2020.
-
An Asynchronous soundness theorem for concurrent separation logic
Authors:
Paul-André Melliès,
Léo Stefanesco
Abstract:
Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program $C$, we associate a pair of asynchronous transition systems $[C]_S$ and $[C]_L$ which describe the operational behavior of the Code when confr…
▽ More
Concurrent separation logic (CSL) is a specification logic for concurrent imperative programs with shared memory and locks. In this paper, we develop a concurrent and interactive account of the logic inspired by asynchronous game semantics. To every program $C$, we associate a pair of asynchronous transition systems $[C]_S$ and $[C]_L$ which describe the operational behavior of the Code when confronted to its Environment or Frame --- both at the level of machine states ($S$) and of machine instructions and locks ($L$). We then establish that every derivation tree $π$ of a judgment $Γ\vdash\{P\}C\{Q\}$ defines a winning and asynchronous strategy $[π]_{Sep}$ with respect to both asynchronous semantics $[C]_S$ and $[C]_L$. From this, we deduce an asynchronous soundness theorem for CSL, which states that the canonical map $\mathcal{L}:[C]_S\to[C]_L$ from the stateful semantics $[C]_S$ to the stateless semantics $[C]_L$ satisfies a basic fibrational property. We advocate that this provides a clean and conceptual explanation for the usual soundness theorem of CSL, including the absence of data races.
△ Less
Submitted 21 July, 2018;
originally announced July 2018.
-
A Game Semantics of Concurrent Separation Logic
Authors:
Paul-André Melliès,
Léo Stefanesco
Abstract:
In this paper, we develop a game-theoretic account of concurrent separation logic. To every execution trace of the Code confronted to the Environment, we associate a specification game where Eve plays for the Code, and Adam for the Environment. The purpose of Eve and Adam is to decompose every intermediate machine state of the execution trace into three pieces: one piece for the Code, one piece fo…
▽ More
In this paper, we develop a game-theoretic account of concurrent separation logic. To every execution trace of the Code confronted to the Environment, we associate a specification game where Eve plays for the Code, and Adam for the Environment. The purpose of Eve and Adam is to decompose every intermediate machine state of the execution trace into three pieces: one piece for the Code, one piece for the Environment, and one piece for the available shared resources. We establish the soundness of concurrent separation logic by interpreting every derivation tree of the logic as a winning strategy of this specification game.
△ Less
Submitted 6 October, 2017;
originally announced October 2017.
-
Relational reasoning via probabilistic coupling
Authors:
Gilles Barthe,
Thomas Espitau,
Benjamin Grégoire,
Justin Hsu,
Léo Stefanesco,
Pierre-Yves Strub
Abstract:
Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance---a…
▽ More
Probabilistic coupling is a powerful tool for analyzing pairs of probabilistic processes. Roughly, coupling two processes requires finding an appropriate witness process that models both processes in the same probability space. Couplings are powerful tools proving properties about the relation between two processes, include reasoning about convergence of distributions and stochastic dominance---a probabilistic version of a monotonicity property.
While the mathematical definition of coupling looks rather complex and cumbersome to manipulate, we show that the relational program logic pRHL---the logic underlying the EasyCrypt cryptographic proof assistant---already internalizes a generalization of probabilistic coupling. With this insight, constructing couplings is no harder than constructing logical proofs. We demonstrate how to express and verify classic examples of couplings in pRHL, and we mechanically verify several couplings in EasyCrypt.
△ Less
Submitted 14 October, 2015; v1 submitted 11 September, 2015;
originally announced September 2015.
