Verifying strong eventual consistency in distributed systems V. B. F. Gomes, M. Kleppmann, D. P. Mulligan and A. R. Beresford.PACMPL 1 (OOPSLA 2017). (Distinguish Paper and Artifact Awards)
[doi]
[abstract]
[bibtex]
[Isabelle/HOL files]
Abstract.
Data replication is used in distributed systems to maintain up-to-date copies of shared data across multiple computers in a network. However, despite decades of research, algorithms for achieving consistency in replicated systems are still poorly understood. Indeed, many published algorithms have later been shown to be incorrect, even some that were accompanied by supposed mechanised proofs of correctness. In this work, we focus on the correctness of Conflict-free Replicated Data Types (CRDTs), a class of algorithm that provides strong eventual consistency guarantees for replicated data. We develop a modular and reusable framework in the Isabelle/HOL interactive proof assistant for verifying the correctness of CRDT algorithms. We avoid correctness issues that have dogged previous mechanised proofs in this area by including a network model in our formalisation, and proving that our theorems hold in all possible network behaviours. Our axiomatic network model is a standard abstraction that accurately reflects the behaviour of real-world computer networks. Moreover, we identify an abstract convergence theorem, a property of order relations, which provides a formal definition of strong eventual consistency. We then obtain the first machine-checked correctness theorems for three concrete CRDTs: the Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement Counter. We find that our framework is highly reusable, developing proofs of correctness for the latter two CRDTs in a few hours and with relatively little CRDT-specific code.
@article{GomesKMB17,
author = {Victor B. F. Gomes and
Martin Kleppmann and
Dominic P. Mulligan and
Alastair R. Beresford},
title = {Verifying strong eventual consistency in distributed systems},
journal = {{PACMPL}},
volume = {1},
number = {{OOPSLA}},
pages = {109:1--109:28},
year = {2017},
doi = {10.1145/3133933}
}
Building Program Construction and Verification Tools
from Algebraic Principles A. Armstrong, V. B. F. Gomes and G. Struth.Formal Aspects of Computing (2016).
[doi]
[abstract]
[bibtex]
[Isabelle/HOL files]
Abstract.
We present a principled modular approach to the development of construction and
verification tools for imperative programs, in which the control flow and the
data flow are cleanly separated. Our simplest verification tool uses Kleene
algebra with tests for the control flow of while-programs and their standard
relational semantics for the data flow. It is expanded to a basic program
construction tool by adding an operation for the specification statement and one
single axiom. To include recursive procedures, Kleene algebras with tests are
expanded further to quantales with tests. In this more expressive setting,
iteration and the specification statement can be defined explicitly and stronger
program transformation rules can be derived. Programming our approach in the
Isabelle/HOL interactive theorem prover yields simple lightweight mathematical
components as well as program construction and verification tools that are
correct by construction themselves. Verification condition generation and
program construction rules are based on equational reasoning and supported by
powerful Isabelle tactics and automated theorem proving. A number of examples
shows our tools at work.
@article{ArmstrongGS15,
author = {Alasdair Armstrong and
Victor B. F. Gomes and
Georg Struth},
title = {Building Program Construction and Verification Tools from
Algebraic Principles},
journal = {Formal Aspects of Computing},
pages = {1-29},
publisher = {Springer London},
year = {2015}
}
Conference papers
Programming and Proving with Classical Types C. Matache, V. B. F. Gomes and D. P. Mulligan.APLAS'17.
[pdf]
[abstract]
[bibtex]
[Isabelle/HOL files]
Abstract.
The propositions-as-types correspondence is ordinarily presented as linking the
metatheory of typed λ-calculi and the proof theory of intuitionistic logic.
Griffin observed that this correspondence could be extended to classical logic
through the use of control operators. This observation set off a flurry of
further research, leading to the development of Parigot’s λμ -calculus. In
this work, we use the λμ -calculus as the foundation for a system of proof
terms for classical first-order logic. In particular, we define an extended
call-by-value λμ -calculus with a type system in correspondence with full
classical logic. We extend the language with polymorphic types, add a host of
data types in ‘direct style’, and prove several metatheoretical properties. All
of our proofs and definitions are mechanised in Isabelle/HOL, and we
automatically obtain an interpreter for a system of proof terms cum programming
language—called μML, using Isabelle’s code generation mechanism. Atop our
proof terms, we build a prototype LCF-style interactive theorem prover—called
μTP, for classical first-order logic, capable of synthesising μML programs
from completed tactic-driven proofs. We present example closed μML programs
with classical tautologies for types, including some inexpressible as closed
programs in the original λμ-calculus, and some example tactic-driven μTP
proofs of classical tautologies.
@inproceedings{MatacheGM17,
author = {Cristina Matache and
Victor B. F. Gomes and
Dominic P. Mulligan},
title = {Programming and Proving with Classical Types},
booktitle = {{APLAS}},
series = {Lecture Notes in Computer Science},
volume = {10695},
pages = {215--234},
publisher = {Springer},
year = {2017}
}
Abstract.
Modal Kleene algebras are relatives of dynamic logics that support program construction and verification by equational reasoning. We describe their application in implementing versatile program correctness components in interactive theorem provers such as Isabelle/HOL. Starting from a weakest precondition based component with a simple relational store model, we show how variants for Hoare logic, strongest postconditions and program refinement can be built in a principled way. Modularity of the approach is demonstrated by variants that capture program termination and recursion, memory models for programs with pointers, and program trace semantics.
@inproceedings{GomesS16,
author = {Victor B. F. Gomes and
Georg Struth},
title = {Modal Kleene Algebra Applied to Program Correctness},
booktitle = {{FM}},
series = {Lecture Notes in Computer Science},
volume = {9995},
pages = {310--325},
year = {2016}
}
A Program Construction and Verification Tool for
Separation Logic B. Dongol, V. B. F. Gomes and G. Struth.MPC'15.
[pdf]
[abstract]
[bibtex]
[Isabelle/HOL files]
Abstract.
An algebraic approach to the design of program construction and
verification tools is applied to separation logic. The control-flow level
is modelled by power series with convolution as separating
conjunction. A generic construction lifts resource monoids to
assertion and predicate transformer quantales. The data domain is
captured by concrete store-heap models. These are linked to the
separation algebra by soundness proofs. Verification conditions and
transformation or refinement laws are derived by equational
reasoning within the predicate transformer quantale. This
separation of concerns makes an implementation in the Isabelle/HOL
proof assistant simple and highly automatic. The resulting tool is
itself correct by construction; it is explained on three simple examples.
@inproceedings{DongolGS15,
author = {Brijesh Dongol and
Victor B. F. Gomes and
Georg Struth},
editor = {Ralf Hinze and
Janis Voigtl{\"{a}}nder},
title = {A Program Construction and Verification Tool for Separation Logic},
booktitle = {{MPC} 2015},
series = {Lecture Notes in Computer Science},
volume = {9129},
pages = {137--158},
publisher = {Springer},
year = {2015}
}
Lightweight Program Construction and Verification Tools
in Isabelle/HOL A. Armstrong, V. B. F. Gomes and G. Struth.SEFM'14. (Best Paper Award)
[pdf]
[abstract]
[bibtex]
[Isabelle/HOL files]
[slides]
Abstract.
We present a principled approach to the development of construction
and verification tools for while-programs. Our verification tool
uses Kleene algebra with tests to capture the control flow of
programs and its relational semantics for their data flow. It is
extended to a Morgan-style program construction tool by adding one
single axiom to the algebra. Our formalisation in Isabelle/HOL makes
these tools themselves correct by construction. Verification
condition generation and program construction steps are based on
simple equational reasoning and supported by powerful Isabelle
tactics. Two case studies on program construction and verification show
our tools at work.
@inproceedings{ArmstrongGS14c,
author = {Alasdair Armstrong and
Victor B. F. Gomes and
Georg Struth},
title = {Lightweight Program Construction and Verification Tools in
{I}sabelle/{HOL}},
booktitle = {{SEFM} 2014},
pages = {5--19},
year = {2014},
editor = {Dimitra Giannakopoulou and
Gwen Sala{\"{u}}n},
series = {Lecture Notes in Computer Science},
volume = {8702},
publisher = {Springer}
}
Algebraic Principles for Rely-Guarantee Style
Concurrency Verification Tools A. Armstrong, V. B. F. Gomes and G. Struth.FM'14.
[pdf]
[abstract]
[bibtex]
[Isabelle/HOL files]
Abstract.
We provide simple equational principles for deriving rely-guarantee-style
inference rules and refinement laws based on idempotent semirings.
We link the algebraic layer with concrete models of programs based
on languages and execution traces. We have implemented the approach
in Isabelle/HOL as a lightweight concurrency verification tool that
supports reasoning about the control and data flow of concurrent programs
with shared variables at different levels of abstraction.
This is illustrated on a simple verification example.
@inproceedings{ArmstrongGS14b,
author = {Alasdair Armstrong and
Victor B. F. Gomes and
Georg Struth},
title = {Algebraic Principles for Rely-Guarantee Style Concurrency Verification Tools},
booktitle = {{FM} 2014},
pages = {78--93},
year = {2014},
editor = {Cliff B. Jones and
Pekka Pihlajasaari and
Jun Sun},
series = {Lecture Notes in Computer Science},
volume = {8442},
publisher = {Springer}
}
Abstract.
We present a reference formalisation of Kleene algebra and demonic
refinement algebra with tests in Isabelle/HOL. It provides three
different formalisations of tests. Our structured comprehensive
libraries for these algebras extend an existing Kleene algebra
library. It includes an algebraic account of Hoare logic for partial
correctness and several refinement and concurrency control laws in a
total correctness setting. Formalisation examples include a complex
refinement theorem, a generic proof of a loop transformation theorem
for partial and total correctness and a simple prototypical
verification tool for while programs, which is itself formally verified.
@inproceedings{ArmstrongGS14a,
author = {Alasdair Armstrong and
Victor B. F. Gomes and
Georg Struth},
title = {Algebras for Program Correctness in {I}sabelle/{HOL}},
booktitle = {{RAMICS} 2014},
pages = {49--64},
year = {2014},
editor = {Peter H{\"{o}}fner and
Peter Jipsen and
Wolfram Kahl and
Martin Eric M{\"{u}}ller},
series = {Lecture Notes in Computer Science},
volume = {8428},
publisher = {Springer}
}
Archive of Formal Proofs
The LambdaMu-calculus C. Matache, V. B. F. Gomes and D. P. Mulligan.Archive of Formal Proofs (2017).
[url]
[abstract]
[bibtex]
Abstract.
The propositions-as-types correspondence is ordinarily presented as linking the metatheory of typed λ-calculi and the proof theory of intuitionistic logic. Griffin observed that this correspondence could be extended to classical logic through the use of control operators. This observation set off a flurry of further research, leading to the development of Parigots λμ-calculus. In this work, we formalise λμ- calculus in Isabelle/HOL and prove several metatheoretical properties such as type preservation and progress.
@article{DBLP:journals/afp/MatacheGM17,
author = {Cristina Matache and
Victor B. F. Gomes and
Dominic P. Mulligan},
title = {The LambdaMu-calculus},
journal = {Archive of Formal Proofs},
volume = {2017},
year = {2017}
}
A framework for establishing strong eventual consistency for Conflict-free Replicated Datatypes. V. B. F. Gomes, M. Kleppmann, D. P. Mulligan, and A. R. Beresford.Archive of Formal Proofs (2017).
[url]
[abstract]
[bibtex]
Abstract.
In this work, we focus on the correctness of Conflict-free Replicated Data
Types (CRDTs), a class of algorithm that provides strong eventual consistency
guarantees for replicated data. We develop a modular and reusable framework for
verifying the correctness of CRDT algorithms. We avoid correctness issues that
have dogged previous mechanised proofs in this area by including a network
model in our formalisation, and proving that our theorems hold in all possible
network behaviours. Our axiomatic network model is a standard abstraction that
accurately reflects the behaviour of real-world computer networks. Moreover, we
identify an abstract convergence theorem, a property of order relations, which
provides a formal definition of strong eventual consistency. We then obtain the
first machine-checked correctness theorems for three concrete CRDTs: the
Replicated Growable Array, the Observed-Remove Set, and an Increment-Decrement
Counter.
@article{GomesKMB17,
author = {Victor B. F. Gomes and
Martin Kleppmann and
Dominic P. Mulligan and
Alastair R. Beresford},
title = {A framework for establishing Strong Eventual Consistency for Conflict-free
Replicated Datatypes},
journal = {Archive of Formal Proofs},
volume = {2017},
year = {2017}
}
Partial Semigroups and Convolution Algebras B. Dongol, V. B. F. Gomes, I. J. Hayes and G. Struth.Archive of Formal Proofs (2017).
[url]
[abstract]
[bibtex]
Abstract.
Partial Semigroups are relevant to the foundations of quantum mechanics and combinatorics as well as to interval and separation logics. Convolution algebras can be understood either as algebras of generalised binary modalities over ternary Kripke frames, in particular over partial semigroups, or as algebras of quantale-valued functions which are equipped with a convolution-style operation of multiplication that is parametrised by a ternary relation. Convolution algebras provide algebraic semantics for various substructural logics, including categorial, relevance and linear logics, for separation logic and for interval logics; they cover quantitative and qualitative applications. These mathematical components for partial semigroups and convolution algebras provide uniform foundations from which models of computation based on relations, program traces or pomsets, and verification components for separation or interval temporal logics can be built with little effort.
@article{DongolGHS17,
author = {Brijesh Dongol and
Victor B. F. Gomes and
Ian J. Hayes and
Georg Struth},
title = {Partial Semigroups and Convolution Algebras},
journal = {Archive of Formal Proofs},
volume = {2017},
year = {2017}
}
Kleene Algebra with Domain V. B. F. Gomes, W. Guttmann, P. Höfner, G. Struth and T. Weber.Archive of Formal Proofs (2016).
[url]
[abstract]
[bibtex]
Abstract.
Kleene algebras with domain are Kleene algebras endowed with an operation that maps each element of the algebra to its domain of definition (or its complement) in abstract fashion. They form a simple algebraic basis for Hoare logics, dynamic logics or predicate transformer semantics. We formalise a modular hierarchy of algebras with domain and antidomain (domain complement) operations in Isabelle/HOL that ranges from domain and antidomain semigroups to modal Kleene algebras and divergence Kleene algebras. We link these algebras with models of binary relations and program traces. We include some examples from modal logics, termination and program analysis.
@article{GomesGHSW16,
author = {Victor B. F. Gomes and
Walter Guttmann and
Peter H{\"{o}}fner and
Georg Struth and
Tjark Weber},
title = {Kleene Algebras with Domain},
journal = {Archive of Formal Proofs},
volume = {2016},
year = {2016}
}
Program Construction and Verification Components Based on Kleene Algebra V. B. F. Gomes and G. Struth.Archive of Formal Proofs (2016).
[url]
[abstract]
[bibtex]
Abstract.
Variants of Kleene algebra support program construction and verification by algebraic reasoning. This entry provides a verification component for Hoare logic based on Kleene algebra with tests, verification components for weakest preconditions and strongest postconditions based on Kleene algebra with domain and a component for step-wise refinement based on refinement Kleene algebra with tests. In addition to these components for the partial correctness of while programs, a verification component for total correctness based on divergence Kleene algebras and one for (partial correctness) of recursive programs based on domain quantales are provided. Finally we have integrated memory models for programs with pointers and a program trace semantics into the weakest precondition component.
@article{GomesS16,
author = {Victor B. F. Gomes and
Georg Struth},
title = {Program Construction and Verification Components Based on {K}leene Algebra},
journal = {Archive of Formal Proofs},
volume = {2016},
year = {2016}
}
Residuated Lattices V. B. F. Gomes and G. Struth.Archive of Formal Proofs (2015).
[url]
[abstract]
[bibtex]
Abstract.
The theory of residuated lattices, first proposed by Ward and Dilworth,
is formalised in Isabelle/HOL. This includes concepts of residuated
functions; their adjoints and conjugates. It also contains necessary and
sufficient conditions for the existence of these operations in an arbitrary
lattice. The mathematical components for residuated lattices are linked to
the AFP entry for relation algebra. In particular, we prove Jonsson and
Tsinakis conditions for a residuated boolean algebra to form a relation
algebra.
@article{GomesGS15,
author = {Victor B. F. Gomes and
Georg Struth},
title = {Residuated Lattices},
journal = {Archive of Formal Proofs},
volume = {2015},
year = {2015}
}
Kleene Algebra with Tests and Demonic Refinement Algebras A. Armstrong, V. B. F. Gomes and G. Struth.Archive of Formal Proofs (2014).
[url]
[abstract]
[bibtex]
Abstract.
We formalise Kleene algebra with tests (KAT) and demonic refinement
algebra (DRA) in Isabelle/HOL. KAT is relevant for program verification
and correctness proofs in the partial correctness setting. While DRA
targets similar applications in the context of total correctness.
Our formalisation contains the two most important models of these
algebras: binary relations in the case of KAT and predicate transformers
in the case of DRA. In addition, we derive the inference rules for
Hoare logic in KAT and its relational model and present a simple
formally verified program verification tool prototype based on the
algebraic approach.
@article{ArmstrongGS14,
author = {Alasdair Armstrong and
Victor B. F. Gomes and
Georg Struth},
title = {Kleene Algebra with Tests and Demonic Refinement Algebras},
journal = {Archive of Formal Proofs},
volume = {2014},
year = {2014}
}
PhD Thesis
Algebraic Principles for Program Correctness Tools in Isabelle/HOL V. B. F. Gomes.PhD Thesis, University of Sheffield. 2016.
[pdf]
[abstract]
[bibtex]
[Isabelle/HOL files]
Abstract.
This thesis puts forward a flexible and principled approach to the development of construction and verification tools for imperative pro- grams, in which the control flow and the data level are cleanly sep- arated. The approach is inspired by algebraic principles and bene- fits from an algebraic semantics layer. It is programmed in the Is- abelle/HOL interactive theorem prover and yields simple lightweight mathematical components as well as program construction and veri- fication tools that are themselves correct by construction.
First, a simple tool is implemented using Kleeene algebra with tests (KAT) for the control flow of while-programs, which is the most com- pact verification formalism for imperative programs, and their stan- dard relational semantics for the data level. A reference formalisation of KAT in Isabelle/HOL is then presented, providing three different formalisations of tests. The structured comprehensive libraries for these algebras include an algebraic account of Hoare logic for par- tial correctness. Verification condition generation and program con- struction rules are based on equational reasoning and supported by powerful Isabelle tactics and automated theorem proving.
Second, the tool is expanded to support different programming fea- tures and verification methods. A basic program construction tool is developed by adding an operation for the specification statement and one single axiom. To include recursive procedures, KATs are expanded further to quantales with tests, where iteration and the specification statement can be defined explicitly. Additionally, a nondeterministic extension supports the verification of simple concurrent programs.
Finally, the approach is also applied to separation logic, where the control-flow is modelled by power series with convolution as sepa- rating conjunction. A generic construction lifts resource monoids to assertion and predicate transformer quantales. The data level is cap- tured by concrete store-heap models. These are linked to the algebra by soundness proofs.
A number of examples shows the tools at work.
@phdthesis{GomesThesis,
author = {Victor B. F. Gomes},
title = {Algebraic Principles for Program Correctness Tools in {I}sabelle/{HOL}},
school = {University of Sheffield},
year = 2016,
month = 2
}
Master Dissertation
Controllers for Navigation using Reinforcement Learning V. B. F. Gomes.Master dissertation, University of Sheffield and INSA Lyon (2012).
[pdf]
[abstract]
[bibtex]
[source files]
Abstract.
Understanding the human brain and its behaviour is the main aim of Neuroscience, therefore forming a model with the objective of imitating a special biological behaviour, like the ability to learn, is a research problem with many potential applications. This thesis aims to present a simulation of the Morris water maze using a robot in order to compare two different Reinforcement Learning techniques; model-based, where the transition function between each state is calculated during the interaction with the environment, and model-free, without a fully specified model of the environment. It will provide an overview of both principles and algorithms that can be used for Machine Learning in order to simulate animal behaviour, their advantages and disadvantages. A platform will be created to easily determine the best algorithm in both techniques. During the experiment, the robot will produce learning behaviour in order to be able to self-localise in his environment.
@mastersthesis{mastersthesis,
author = {Victor B. F. Gomes},
title = {Controllers for Navigation using Reinforcement Learning},
school = {University of Sheffield and {INSA} Lyon},
year = 2012
}
Teaching
Part II project (Cambridge)
Michael Rawson, Part II Cambridge Computer Science Tripos project supervision with Dominic Mulligan. Project title: Verified metatheory and type checking for the simply-typed lambda calculus.
Cristina Matache, Part II Cambridge Computer Science Tripos project supervision. Project title: Formalisation of the lambda-mu-T calculus in Isabelle/HOL.