-
Actris 2.0: Asynchronous Session-Type Based Reasoning in Separation Logic
Authors:
Jonas Kastberg Hinrichsen,
Jesper Bengtson,
Robbert Krebbers
Abstract:
Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actr…
▽ More
Message passing is a useful abstraction for implementing concurrent programs. For real-world systems, however, it is often combined with other programming and concurrency paradigms, such as higher-order functions, mutable state, shared-memory concurrency, and locks. We present Actris: a logic for proving functional correctness of programs that use a combination of the aforementioned features. Actris combines the power of modern concurrent separation logics with a first-class protocol mechanism -- based on session types -- for reasoning about message passing in the presence of other concurrency paradigms. We show that Actris provides a suitable level of abstraction by proving functional correctness of a variety of examples, including a channel-based merge sort, a channel-based load-balancing mapper, and a variant of the map-reduce model, using concise specifications. While Actris was already presented in a conference paper (POPL'20), this paper expands the prior presentation significantly. Moreover, it extends Actris to Actris 2.0 with a notion of subprotocols -- based on session-type subtyping -- that permits additional flexibility when composing channel endpoints, and that takes full advantage of the asynchronous semantics of message passing in Actris. Soundness of Actris 2.0 is proven using a model of its protocol mechanism in the Iris framework. We have mechanised the theory of Actris, together with custom tactics, as well as all examples in the paper, in the Coq proof assistant.
△ Less
Submitted 8 June, 2022; v1 submitted 28 October, 2020;
originally announced October 2020.
-
ReLoC Reloaded: A Mechanized Relational Logic for Fine-Grained Concurrency and Logical Atomicity
Authors:
Dan Frumin,
Robbert Krebbers,
Lars Birkedal
Abstract:
We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : τ$, which states that a program $e$ refines a program $e'$ at type $τ$. ReLoC provides type-directed structural rules and symbolic execution rules in se…
▽ More
We present a new version of ReLoC: a relational separation logic for proving refinements of programs with higher-order state, fine-grained concurrency, polymorphism and recursive types. The core of ReLoC is its refinement judgment $e \precsim e' : τ$, which states that a program $e$ refines a program $e'$ at type $τ$. ReLoC provides type-directed structural rules and symbolic execution rules in separation-logic style for manipulating the judgment, whereas in prior work on refinements for languages with higher-order state and concurrency, such proofs were carried out by unfolding the judgment into its definition in the model. ReLoC's abstract proof rules make it simpler to carry out refinement proofs, and enable us to generalize the notion of logically atomic specifications to the relational case, which we call logically atomic relational specifications.
We build ReLoC on top of the Iris framework for separation logic in Coq, allowing us to leverage features of Iris to prove soundness of ReLoC, and to carry out refinement proofs in ReLoC. We implement tactics for interactive proofs in ReLoC, allowing us to mechanize several case studies in Coq, and thereby demonstrate the practicality of ReLoC.
ReLoC Reloaded extends ReLoC (LICS'18) with various technical improvements, a new Coq mechanization, and support for Iris's prophecy variables. The latter allows us to carry out refinement proofs that involve reasoning about the program's future. We also expand ReLoC's notion of logically atomic relational specifications with a new flavor based on the HOCAP pattern by Svendsen et al.
△ Less
Submitted 20 July, 2021; v1 submitted 24 June, 2020;
originally announced June 2020.
-
Compositional Non-Interference for Fine-Grained Concurrent Programs
Authors:
Dan Frumin,
Robbert Krebbers,
Lars Birkedal
Abstract:
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means of type checking), but they are inherently restrictive in the kind of programs they support. Program logics support challe…
▽ More
Non-interference is a program property that ensures the absence of information leaks. In the context of programming languages, there exist two common approaches for establishing non-interference: type systems and program logics. Type systems provide strong automation (by means of type checking), but they are inherently restrictive in the kind of programs they support. Program logics support challenging programs, but they typically require significant human assistance, and cannot handle modules or higher-order programs.
To connect these two approaches, we present SeLoC---a separation logic for non-interference, on top of which we build a type system using the technique of logical relations. By building a type system on top of separation logic, we can compositionally verify programs that consist of typed and untyped parts. The former parts are verified through type checking, while the latter parts are verified through manual proof.
The core technical contribution of SeLoC is a relational form of weakest preconditions that can track information flow using separation logic resources. SeLoC is fully machine-checked, and built on top of the Iris framework for concurrent separation logic in Coq. The integration with Iris provides seamless support for fine-grained concurrency, which was beyond the reach of prior type systems and program logics for non-interference.
△ Less
Submitted 6 March, 2020; v1 submitted 2 October, 2019;
originally announced October 2019.
-
A benchmark for C program verification
Authors:
Marko van Eekelen,
Daniil Frumin,
Herman Geuvers,
Léon Gondelman,
Robbert Krebbers,
Marc Schoolderman,
Sjaak Smetsers,
Freek Verbeek,
Benoît Viguier,
Freek Wiedijk
Abstract:
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last purpose, we give a scoring formula that allows a verification system to score up to a hundred points.
We present twenty-five C programs, as a benchmark for C program verification using formal methods. This benchmark can be used for system demonstration, for comparison of verification effort between systems, and as a friendly competition. For this last purpose, we give a scoring formula that allows a verification system to score up to a hundred points.
△ Less
Submitted 1 April, 2019;
originally announced April 2019.
-
A Formal C Memory Model for Separation Logic
Authors:
Robbert Krebbers
Abstract:
The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions) and low-level (by means of bit manipulation) memory accesses. The C11 standard has restricted the…
▽ More
The core of a formal semantics of an imperative programming language is a memory model that describes the behavior of operations on the memory. Defining a memory model that matches the description of C in the C11 standard is challenging because C allows both high-level (by means of typed expressions) and low-level (by means of bit manipulation) memory accesses. The C11 standard has restricted the interaction between these two levels to make more effective compiler optimizations possible, on the expense of making the memory model complicated.
We describe a formal memory model of the (non-concurrent part of the) C11 standard that incorporates these restrictions, and at the same time describes low-level memory operations. This formal memory model includes a rich permission model to make it usable in separation logic and supports reasoning about program transformations. The memory model and essential properties of it have been fully formalized using the Coq proof assistant.
△ Less
Submitted 10 September, 2015;
originally announced September 2015.
-
A call-by-value lambda-calculus with lists and control
Authors:
Robbert Krebbers
Abstract:
Calculi with control operators have been studied to reason about control in programming languages and to interpret the computational content of classical proofs. To make these calculi into a real programming language, one should also include data types.
As a step into that direction, this paper defines a simply typed call-by-value lambda calculus with the control operators catch and throw, a dat…
▽ More
Calculi with control operators have been studied to reason about control in programming languages and to interpret the computational content of classical proofs. To make these calculi into a real programming language, one should also include data types.
As a step into that direction, this paper defines a simply typed call-by-value lambda calculus with the control operators catch and throw, a data type of lists, and an operator for primitive recursion (a la Goedel's T). We prove that our system satisfies subject reduction, progress, confluence for untyped terms, and strong normalization for well-typed terms.
△ Less
Submitted 10 October, 2012;
originally announced October 2012.
-
The lambda-mu-T-calculus
Authors:
Herman Geuvers,
Robbert Krebbers,
James McKinna
Abstract:
Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand control operators, one should also include these in the calculus. As a first step in that direction, we introduce lambda-mu-T, a combination of Parigot's lambda-mu-calculus and Gödel's T, to extend a calculus with control operators with a datat…
▽ More
Calculi with control operators have been studied as extensions of simple type theory. Real programming languages contain datatypes, so to really understand control operators, one should also include these in the calculus. As a first step in that direction, we introduce lambda-mu-T, a combination of Parigot's lambda-mu-calculus and Gödel's T, to extend a calculus with control operators with a datatype of natural numbers with a primitive recursor.
We consider the problem of confluence on raw terms, and that of strong normalization for the well-typed terms. Observing some problems with extending the proofs of Baba at al. and Parigot's original confluence proof, we provide new, and improved, proofs of confluence (by complete developments) and strong normalization (by reducibility and a postponement argument) for our system.
We conclude with some remarks about extensions, choices, and prospects for an improved presentation.
△ Less
Submitted 2 April, 2012;
originally announced April 2012.
-
Type classes for efficient exact real arithmetic in Coq
Authors:
Robbert Krebbers,
Bas Spitters
Abstract:
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. Previously, we [Krebbers/Spitters 2011] provided a fast implementation of the exact real numbers in the Coq proof assistant…
▽ More
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. Previously, we [Krebbers/Spitters 2011] provided a fast implementation of the exact real numbers in the Coq proof assistant. Our implementation improved on an earlier implementation by O'Connor by using type classes to describe an abstract specification of the underlying dense set from which the real numbers are built. In particular, we used dyadic rationals built from Coq's machine integers to obtain a 100 times speed up of the basic operations already. This article is a substantially expanded version of [Krebbers/Spitters 2011] in which the implementation is extended in the various ways. First, we implement and verify the sine and cosine function. Secondly, we create an additional implementation of the dense set based on Coq's fast rational numbers. Thirdly, we extend the hierarchy to capture order on undecidable structures, while it was limited to decidable structures before. This hierarchy, based on type classes, allows us to share theory on the naturals, integers, rationals, dyadics, and reals in a convenient way. Finally, we obtain another dramatic speed-up by avoiding evaluation of termination proofs at runtime.
△ Less
Submitted 13 February, 2013; v1 submitted 17 June, 2011;
originally announced June 2011.
-
Computer certified efficient exact reals in Coq
Authors:
Robbert Krebbers,
Bas Spitters
Abstract:
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. We provide an implementation of the exact real numbers in the Coq proof assistant. This improves on the earlier Coq-impleme…
▽ More
Floating point operations are fast, but require continuous effort on the part of the user in order to ensure that the results are correct. This burden can be shifted away from the user by providing a library of exact analysis in which the computer handles the error estimates. We provide an implementation of the exact real numbers in the Coq proof assistant. This improves on the earlier Coq-implementation by O'Connor in two ways: we use dyadic rationals built from the machine integers and we optimize computation of power series by using approximate division. Moreover, we use type classes for clean mathematical interfaces. This appears to be the first time that type classes are used in heavy computation. We obtain over a 100 times speed up of the basic operations and indications for improving the Coq system.
△ Less
Submitted 13 May, 2011;
originally announced May 2011.
-
Pure Type Systems without Explicit Contexts
Authors:
Herman Geuvers,
Robbert Krebbers,
James McKinna,
Freek Wiedijk
Abstract:
We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments of shape "A : B". A key feature is that we distinguish free and bound variables even in pseudo-terms.
Specifically we give the rules of the "Pure Type System" class of type theories in this style. We prove that the typi…
▽ More
We present an approach to type theory in which the typing judgments do not have explicit contexts. Instead of judgments of shape "Gamma |- A : B", our systems just have judgments of shape "A : B". A key feature is that we distinguish free and bound variables even in pseudo-terms.
Specifically we give the rules of the "Pure Type System" class of type theories in this style. We prove that the typing judgments of these systems correspond in a natural way with those of Pure Type Systems as traditionally formulated. I.e., our systems have exactly the same well-typed terms as traditional presentations of type theory.
Our system can be seen as a type theory in which all type judgments share an identical, infinite, typing context that has infinitely many variables for each possible type. For this reason we call our system "Gamma_infinity". This name means to suggest that our type judgment "A : B" should be read as "Gamma_infinity |- A : B", with a fixed infinite type context called "Gamma_infinity".
△ Less
Submitted 14 September, 2010;
originally announced September 2010.
