Data types, tools, and techniques for building available and correct distributed applications - Carla Ferreira Abstract: When developing global applications there is a constant tension between consistency and availability. Strong consistent databases have the advantage of clear semantics and guarantees, but at the expense of efficiency and availability. Eventual consistent databases ensure high availability and efficiency, but provide weaker guarantees and are difficult to reason about. Because nowadays user experience is paramount, most global scale applications choose eventual consistent databases at the cost of data consistency. In this (eventual consistent) context the developer has to guarantee that distributed data eventually converges to a common state. To address this issue, developers can rely on ready available libraries of conflict-free replicated data types (CRDTs). A CRDT is a data type that encapsulates a deterministic reconciliation policy that ensures that data converges. The first part of the tutorial discusses the concepts and designing principles of CRDTs. Recently, industry has started moving away from the all-or-nothing, strong-or-eventual, correct-or-available consistency models. Instead, the developer has the possibility of selecting the consistency model for each operation that is sufficient to ensure the application's data integrity invariants. We discuss a static analysis tool that helps developers in this process of adjusting the consistency level of each operation towards application's safety. It allows developers to start by defining a sequential (non distributed) specification of the application and eschew initially the complexities of concurrency and distribution. The tool will check commutativity between operations (needed for convergence) and whether the invariant is ensured in a distributed context. Then the analysis will indicate the problematic operations, if any. The developer can iterate over the analysis by adding synchronisation to the problematic operations and by using CRDTs to address non commutative operations. The tutorial will show, through a few simple case studies, how the tool can be used to customise a consistency protocol that ensures the application's safety. |
Isabelle Tutorial - Gerwin Klein Abstract: This tutorial will give a brief introduction to the interactive theorem prover Isabelle/HOL, covering basic reasoning, specification techniques, proof automation, and program verification. |
Generic Fixpoint Engines for Interprocedural Analyses with Widening and Narrowing - Helmut Seidl Abstract: This tutorial summarizes joint work with Kalmer Apinis, Stefan Schulze Frielinghaus, Ralf Vogler and Vesal Vojdani. Analyzer infra-structures such as Goblint which are based on abstract interpretation, rely on equation systems to represent the abstract semantics of the program to be analyzed. The algorithmic core of the analysis then is given by some fixpoint engine which effectively computes decently small post-solutions. From a software engineering as well as correctness point of view, fixpoint engines should be as generic as possible, i.e., be unaware of the specific structure of the given equation system. We report on newest developments in the construction of such generic fixpoint engines, in particular, local generic fixpoint engines. Locality here means that a given equation system is explored starting from a query, i.e., an unknown whose value is of interest. Other unknowns and equations of the system are considered only as much as neccesary in order to answer the given query. As the exploration of the equation system happens on demand, no pre-processing is possible for such solvers. Accordingly, important structural properties such as strongly connected components must be detected on the fly. The same holds true for widening and narrowing points or even defining right-hand sides of unknowns in case that only a minimum of intermediate data should be stored. Interestingly, these solvers no longer proceed in phases, namely, a widening phase to reach a first post-solution follwed by a narrowing phase where the given post-solution is improved. Instead, widening and narrowing is combined into an intertwined iteration. |