98 citations
- Universidad Politécnica de MadridES38 papers
- Madrid Institute for Advanced StudiesES15 papers
- Roskilde UniversityDK11 papers
- University of PennsylvaniaUS11 papers
- Max Planck Institute for Software SystemsDE10 papers
- University at Buffalo, State University of New YorkUS9 papers
- Institut national de recherche en sciences et technologies du numériqueFR8 papers
- Universidad Complutense de MadridES7 papers
- Consejo Superior de Investigaciones CientíficasES5 papers
- Saarland UniversityDE5 papers
- University College LondonGB5 papers
- Centre National de la Recherche ScientifiqueFR4 papers
6 papers · 1 filter
Proving Highly-Concurrent Traversals Correct
Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea +4
Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any sy…
Reconfigurable Atomic Transaction Commit (Extended Version)
Manuel Bravo, Alexey Gotsman
Modern data stores achieve scalability by partitioning data into shards and fault-tolerance by replicating each shard across several servers. A key component of such systems is a T…
Federated Byzantine Quorum Systems (Extended Version)
Álvaro García-Pérez, Alexey Gotsman
Some of the recent blockchain proposals, such as Stellar and Ripple, use quorum-like structures typical for Byzantine consensus while allowing for open membership. This is achieved…
Distributed transactional reads: the strong, the quick, the fresh \& the impossible
Alejandro Z. Tomsic, Manuel Bravo, Marc Shapiro
This paper studies the costs and trade-offs of providing transactional consistent reads in a distributed storage system. We identify the following dimensions: read consistency, rea…
Paxos Consensus, Deconstructed and Abstracted (Extended Version)
Álvaro García-Pérez, Alexey Gotsman, Yuri Meshman +1
Lamport's Paxos algorithm is a classic consensus protocol for state machine replication in environments that admit crash failures. Many versions of Paxos exploit the protocol's int…
Model Checking Parameterized Asynchronous Shared-Memory Systems
Antoine Durand-Gasselin, Javier Esparza, Pierre Ganty +1
We characterize the complexity of liveness verification for parameterized systems consisting of a leader process and arbitrarily many anonymous and identical contributor processes.…