5 papers
Impossibility Results for Strong Linearizability: The Difficulty of Consistent Refereeing
Hagit Attiya, Armando Castañeda, Constantin Enea
This paper studies the relation between agreement and strongly linearizable implementations of various objects. This leads to new results about implementations of concurrent object…
On the Complexity of Checking Soundness of Natural Reductions (Extended Version)
Constantin Enea, Azadeh Farzan, Dominik Klumpp
The verification of reductions, representative subsets of interleavings, simplifies correctness proofs of parameterized concurrent programs. We introduce an expressive class of syn…
Reduction for Structured Concurrent Programs
Namratha Gangamreddypalli, Constantin Enea, Shaz Qadeer
Commutativity reasoning based on Lipton's movers is a powerful technique for verification of concurrent programs. The idea is to define a program transformation that preserves a su…
Arbitration-Free Consistency is Available (and Vice Versa)
Hagit Attiya, Constantin Enea, Enrique Román-Calvo
The fundamental tension between availability and consistency shapes the design of distributed storage systems. Classical results capture extreme points of this trade-off: the CAP t…
On the Complexity of Checking Mixed Isolation Levels for SQL Transactions
Ahmed Bouajjani, Constantin Enea, Enrique Román-Calvo
Concurrent accesses to databases are typically grouped in transactions which define units of work that should be isolated from other concurrent computations and resilient to failur…