The Logical Timestamp Skew Anomaly in Event-Replicated Transaction Schedulers

To sidestep reasoning about the complex effects of concurrent execution, many system designers have conveniently embraced strict serializability on the strength of its claims, support from commercial and open-source database communities and ubiquitous levels of industry adoption. Crucially, distributed components are built on this model; multiple schedulers are composed in an event-driven architecture to form larger, ostensibly correct systems. This paper examines the oft-misconstrued position of strict serializability as a composable correctness criterion in the design of such systems. An anomaly is presented wherein a strict serializable scheduler in one system produces a history that cannot be serially applied to even a weak prefix-consistent replica in logical timestamp order. Several solutions are presented under varying isolation properties, including novel isolation properties contributed by this paper. We also distinguish between concurrent schedulers based on their propensity to produce deterministic histories. It is further shown that every nondeterministic scheduler is anomaly-prone, every nonconcurrent scheduler is anomaly-free, and that at least one deterministic concurrent scheduler is anomaly-free.

The Logical Timestamp Skew Anomaly in Event-Replicated Transaction Schedulers

To sidestep reasoning about the complex effects of concurrent execution, many system designers have conveniently embraced strict serializability on the strength of its claims, support from commercial and open-source database communities and ubiquitous levels of industry adoption. Crucially, distributed components are built on this model; multiple schedulers are composed in an event-driven architecture to form larger, ostensibly correct systems. This paper examines the oft-misconstrued position of strict serializability as a composable correctness criterion in the design of such systems. An anomaly is presented wherein a strict serializable scheduler in one system produces a history that cannot be serially applied to even a weak prefix-consistent replica in logical timestamp order. Several solutions are presented under varying isolation properties, including novel isolation properties contributed by this paper. We also distinguish between concurrent schedulers based on their propensity to produce deterministic histories. It is further shown that every nondeterministic scheduler is anomaly-prone, every nonconcurrent scheduler is anomaly-free, and that at least one deterministic concurrent scheduler is anomaly-free.

Verifying correctness of persistent concurrent data structures: a sound and complete method

Non-volatile memory (NVM), aka persistent memory, is a new memory paradigm that preserves its contents even after power loss. The expected ubiquity of NVM has stimulated interest in the design of persistent concurrent data structures, together with associated notions of correctness. In this paper, we present a formal proof technique for durable linearizability, which is a correctness criterion that extends linearizability to handle crashes and recovery in the context ofNVM.Our proofs are based on refinement of Input/Output automata (IOA) representations of concurrent data structures. To this end, we develop a generic procedure for transforming any standard sequential data structure into a durable specification and prove that this transformation is both sound and complete. Since the durable specification only exhibits durably linearizable behaviours, it serves as the abstract specification in our refinement proof. We exemplify our technique on a recently proposed persistentmemory queue that builds on Michael and Scott’s lock-free queue. To support the proofs, we describe an automated translation procedure from code to IOA and a thread-local proof technique for verifying correctness of invariants.

Beyond Tests

Automated program repair is an emerging technology that seeks to automatically rectify program errors and vulnerabilities. Repair techniques are driven by a correctness criterion that is often in the form of a test suite. Such test-based repair may produce overfitting patches, where the patches produced fail on tests outside the test suite driving the repair. In this work, we present a repair method that fixes program vulnerabilities without the need for a voluminous test suite. Given a vulnerability as evidenced by an exploit, the technique extracts a constraint representing the vulnerability with the help of sanitizers. The extracted constraint serves as a proof obligation that our synthesized patch should satisfy. The proof obligation is met by propagating the extracted constraint to locations that are deemed to be “suitable” fix locations. An implementation of our approach (E xtract F ix ) on top of the KLEE symbolic execution engine shows its efficacy in fixing a wide range of vulnerabilities taken from the ManyBugs benchmark, real-world CVEs and Google’s OSS-Fuzz framework. We believe that our work presents a way forward for the overfitting problem in program repair by generalizing observable hazards/vulnerabilities (as constraint) from a single failing test or exploit.

Strict Linearizability and Abstract Atomicity

Linearizability is a commonly accepted consistency condition for concurrent objects. Filipović et al. show that linearizability is equivalent to observational refinement. However, linearizability does not permit concurrent objects to share memory spaces with their client programs. We show that linearizability (or observational refinement) can be broken even though a client program of an object accesses the shared memory spaces without interleaving with the methods of the object. In this paper, we present strict linearizability which lifts this limitation and can ensure client-side traces and final-states equivalence even in a relaxed program model allowing clients to directly access the internal states of concurrent objects. We also investigate several important properties of strict linearizability. At a high level of abstraction, a concurrent object can be viewed as a concurrent implementation of an abstract data type (ADT). We also present a correctness criterion for relating an ADT and its concurrent implementation, which is the combination of linearizability and data abstraction and can ensure observational equivalence. We also investigate its relationship with strict linearizability.

Blame and coercion: Together again for the first time

C#, Dart, Pyret, Racket, TypeScript, VB: many recent languages integrate dynamic and static types via gradual typing. We systematically develop four calculi for gradual typing and the relations between them, building on and strengthening previous work. The calculi are as follows: $\lambda{B}$ , based on the blame calculus of Wadler and Findler (2009); $\lambda{C}$ , inspired by the coercion calculus of Henglein (1994); $\lambda{S}$ inspired by the space-efficient calculus of Herman, Tomb, and Flanagan (2006); and $\lambda{T}$ based on the threesome calculus of Siek and Wadler (2010). While $\lambda{B}$ and $\lambda{T}$ are little changed from previous work, $\lambda{C}$ and $\lambda{S}$ are new. Together, $\lambda{B}$ , $\lambda{C}$ , $\lambda{S}$ , and $\lambda{T}$ provide a coherent foundation for design, implementation, and optimization of gradual types. We define translations from $\lambda{B}$ to $\lambda{C}$ , from $\lambda{C}$ to $\lambda{S}$ , and from $\lambda{S}$ to $\lambda{T}$ . Much previous work lacked proofs of correctness or had weak correctness criteria; here we demonstrate the strongest correctness criterion one could hope for, that each of the translations is fully abstract. Each of the calculi reinforces the design of the others: $\lambda{C}$ has a particularly simple definition, and the subtle definition of blame safety for $\lambda{B}$ is justified by the simple definition of blame safety for $\lambda{C}$ . Our calculus $\lambda{S}$ is implementation-ready: the first space-efficient calculus that is both straightforward to implement and easy to understand. We give two applications: first, using full abstraction from $\lambda{C}$ to $\lambda{S}$ to establish an equational theory of coercions; and second, using full abstraction from $\lambda{B}$ to $\lambda{S}$ to easily establish the Fundamental Property of Casts, which required a custom bisimulation and six lemmas in earlier work.

Proof nets for multiplicative cyclic linear logic and Lambek calculus

This paper presents a simple and intuitive syntax for proof nets of the multiplicative cyclic fragment (McyLL) of linear logic (LL). The main technical achievement of this work is to propose a correctness criterion that allows for sequentialization (recovering a proof from a proof net) for all McyLL proof nets, including those containing cut links. This is achieved by adapting the idea of contractibility (originally introduced by Danos to give a quadratic time procedure for proof nets correctness) to cyclic LL. This paper also gives a characterization of McyLL proof nets for Lambek Calculus and thus a geometrical (i.e., non-inductive) way to parse phrases or sentences by means of Lambek proof nets.