-
Bluebell: An Alliance of Relational Lifting and Independence For Probabilistic Reasoning
Authors:
Jialu Bao,
Emanuele D'Osualdo,
Azadeh Farzan
Abstract:
We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shine…
▽ More
We present Bluebell, a program logic for reasoning about probabilistic programs where unary and relational styles of reasoning come together to create new reasoning tools. Unary-style reasoning is very expressive and is powered by foundational mechanisms to reason about probabilistic behaviour like independence and conditioning. The relational style of reasoning, on the other hand, naturally shines when the properties of interest compare the behaviour of similar programs (e.g. when proving differential privacy) managing to avoid having to characterize the output distributions of the individual programs. So far, the two styles of reasoning have largely remained separate in the many program logics designed for the deductive verification of probabilistic programs. In Bluebell, we unify these styles of reasoning through the introduction of a new modality called "joint conditioning" that can encode and illuminate the rich interaction between conditional independence and relational liftings; the two powerhouses from the two styles of reasoning.
△ Less
Submitted 28 February, 2024;
originally announced February 2024.
-
The Path to Durable Linearizability
Authors:
Emanuele D'Osualdo,
Azalea Raad,
Viktor Vafeiadis
Abstract:
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of \emph{durable linearizability} (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent w…
▽ More
There is an increasing body of literature proposing new and efficient persistent versions of concurrent data structures ensuring that a consistent state can be recovered after a power failure or a crash. Their correctness is typically stated in terms of \emph{durable linearizability} (DL), which requires that individual library operations appear to be executed atomically in a sequence consistent with the real-time order and, moreover, that recovering from a crash return a state corresponding to a prefix of that sequence. Sadly, however, there are hardly any formal DL proofs, and those that do exist cover the correctness of rather simple persistent algorithms on specific (simplified) persistency models.
In response, we propose a general, powerful, modular, and incremental proof technique that can be used to guide the development and establish DL. Our technique is (1) general, in that it is not tied to a specific persistency and/or consistency model, (2) powerful, in that it can handle the most advanced persistent algorithms in the literature, (3) modular, in that it allows the reuse of an existing linearizability argument, and (4) incremental, in that the additional requirements for establishing DL depend on the complexity of the algorithm to be verified. We illustrate this technique on various versions of a persistent set, leading to the link-free set of Zuriel et al.
△ Less
Submitted 14 November, 2022;
originally announced November 2022.
-
Proving Hypersafety Compositionally
Authors:
Emanuele D'Osualdo,
Azadeh Farzan,
Derek Dreyer
Abstract:
Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between th…
▽ More
Hypersafety properties of arity $n$ are program properties that relate $n$ traces of a program (or, more generally, traces of $n$ programs). Classic examples include determinism, idempotence, and associativity. A number of relational program logics have been introduced to target this class of properties. Their aim is to construct simpler proofs by capitalizing on structural similarities between the $n$ related programs. We propose an unexplored, complementary proof principle that establishes hyper-triples (i.e. hypersafety judgments) as a unifying compositional building block for proofs, and we use it to develop a Logic for Hyper-triple Composition (LHC), which supports forms of proof compositionality that were not achievable in previous logics. We prove LHC sound and apply it to a number of challenging examples.
△ Less
Submitted 27 October, 2022; v1 submitted 15 September, 2022;
originally announced September 2022.
-
A Bunch of Sessions: A Propositions-as-Sessions Interpretation of Bunched Implications in Channel-Based Concurrency
Authors:
Dan Frumin,
Emanuele D'Osualdo,
Bas van den Heuvel,
Jorge A. Pérez
Abstract:
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic.
In this paper, we investigate a new point in the design space of session type systems fo…
▽ More
The emergence of propositions-as-sessions, a Curry-Howard correspondence between propositions of Linear Logic and session types for concurrent processes, has settled the logical foundations of message-passing concurrency. Central to this approach is the resource consumption paradigm heralded by Linear Logic.
In this paper, we investigate a new point in the design space of session type systems for message-passing concurrent programs. We identify O'Hearn and Pym's Logic of Bunched Implications (BI) as a fruitful basis for an interpretation of the logic as a concurrent programming language. This leads to a treatment of non-linear resources that is radically different from existing approaches based on Linear Logic. We introduce a new $π$-calculus with sessions, called $π$BI; its most salient feature is a construct called spawn, which expresses new forms of sharing that are induced by structural principles in BI. We illustrate the expressiveness of $π$BI and lay out its fundamental theory: type preservation, deadlock-freedom, and weak normalization results for well-typed processes; an operationally sound and complete typed encoding of an affine $λ$-calculus; and a non-interference result for access of resources.
△ Less
Submitted 12 September, 2022;
originally announced September 2022.
-
Decidable Inductive Invariants for Verification of Cryptographic Protocols with Unbounded Sessions
Authors:
Emanuele D'Osualdo,
Felix Stutz
Abstract:
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is s…
▽ More
We develop a theory of decidable inductive invariants for an infinite-state variant of the Applied pi-calculus, with applications to automatic verification of stateful cryptographic protocols with unbounded sessions/nonces. Since the problem is undecidable in general, we introduce depth-bounded protocols, a strict generalisation of a class from the literature, for which our decidable analysis is sound and complete. Our core contribution is a procedure to check that an invariant is inductive, which implies that every reachable configuration satisfies it. Our invariants can capture security properties like secrecy, can be inferred automatically, and represent an independently checkable certificate of correctness.
We provide a prototype implementation and we report on its performance on some textbook examples.
△ Less
Submitted 19 July, 2020; v1 submitted 13 November, 2019;
originally announced November 2019.
-
TaDA Live: Compositional Reasoning for Termination of Fine-grained Concurrent Programs
Authors:
Emanuele D'Osualdo,
Azadeh Farzan,
Philippa Gardner,
Julian Sutherland
Abstract:
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 w…
▽ More
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 which 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.
△ Less
Submitted 29 November, 2021; v1 submitted 17 January, 2019;
originally announced January 2019.
-
On Hierarchical Communication Topologies in the pi-calculus
Authors:
Emanuele D'Osualdo,
C. -H. Luke Ong
Abstract:
This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T-shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system tha…
▽ More
This paper is concerned with the shape invariants satisfied by the communication topology of π-terms, and the automatic inference of these invariants. A π-term P is hierarchical if there is a finite forest T such that the communication topology of every term reachable from P satisfies a T-shaped invariant. We design a static analysis to prove a term hierarchical by means of a novel type system that enjoys decidable inference. The soundness proof of the type system employs a non-standard view of π-calculus reactions. The coverability problem for hierarchical terms is decidable. This is proved by showing that every hierarchical term is depth-bounded, an undecidable property known in the literature. We thus obtain an expressive static fragment of the π-calculus with decidable safety verification problems.
△ Less
Submitted 19 April, 2016; v1 submitted 7 January, 2016;
originally announced January 2016.
-
A Type System for proving Depth Boundedness in the pi-calculus
Authors:
Emanuele D'Osualdo,
Luke Ong
Abstract:
The depth-bounded fragment of the pi-calculus is an expressive class of systems enjoying decidability of some important verification problems. Unfortunately membership of the fragment is undecidable. We propose a novel type system, parameterised over a finite forest, that formalises name usage by pi-terms in a manner that respects the forest. Type checking is decidable and type inference is comput…
▽ More
The depth-bounded fragment of the pi-calculus is an expressive class of systems enjoying decidability of some important verification problems. Unfortunately membership of the fragment is undecidable. We propose a novel type system, parameterised over a finite forest, that formalises name usage by pi-terms in a manner that respects the forest. Type checking is decidable and type inference is computable; furthermore typable pi-terms are guaranteed to be depth bounded.
The second contribution of the paper is a proof of equivalence between the semantics of typable terms and nested data class memory automata, a class of automata over data words. We believe this connection can help to establish new links between the rich theory of infinite-alphabet automata and nominal calculi.
△ Less
Submitted 23 February, 2015; v1 submitted 3 February, 2015;
originally announced February 2015.
-
Automatic Verification of Erlang-Style Concurrency
Authors:
Emanuele D'Osualdo,
Jonathan Kochems,
C. -H. Luke Ong
Abstract:
This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce Lambda-Actor, a prototypical functional language with pattern-matching algebraic data types, augmented with process creation and asynchronous message-passing primitives. We formalise an abstract model of Lambda-Actor programs called Acto…
▽ More
This paper presents an approach to verify safety properties of Erlang-style, higher-order concurrent programs automatically. Inspired by Core Erlang, we introduce Lambda-Actor, a prototypical functional language with pattern-matching algebraic data types, augmented with process creation and asynchronous message-passing primitives. We formalise an abstract model of Lambda-Actor programs called Actor Communicating System (ACS) which has a natural interpretation as a vector addition system, for which some verification problems are decidable. We give a parametric abstract interpretation framework for Lambda-Actor and use it to build a polytime computable, flow-based, abstract semantics of Lambda-Actor programs, which we then use to bootstrap the ACS construction, thus deriving a more accurate abstract model of the input program. We have constructed Soter, a tool implementation of the verification method, thereby obtaining the first fully-automatic, infinite-state model checker for a core fragment of Erlang. We find that in practice our abstraction technique is accurate enough to verify an interesting range of safety properties. Though the ACS coverability problem is Expspace-complete, Soter can analyse these verification problems surprisingly efficiently.
△ Less
Submitted 9 March, 2013;
originally announced March 2013.
