SPLASH 2020
Sun 15 - Sat 21 November 2020 Online Conference
Fri 20 Nov 2020 15:40 - 16:00 at SPLASH-III - F-5B Chair(s): Aviral Goel, Mohsen Lesani
Sat 21 Nov 2020 03:40 - 04:00 at SPLASH-III - F-5B Chair(s): Sophia Drossopoulou, Julien Lange

Large scale production distributed systems are difficult to design and test.
Correctness must be ensured when processes run asynchronously, at arbitrary rates relative to each other,
and in the presence of failures, e.g., process crashes or message losses. These conditions
create a huge space of executions that is difficult to explore in a principled way.
Current testing techniques focus on systematic or randomized exploration of all executions
of an implementation while treating the implemented algorithms as black boxes.
On the other hand, proofs of correctness of many of the underlying algorithms often exploit
semantic properties that reduce reasoning about correctness to a subset of behaviors.
For example, the \emph{communication-closure} property, used in many proofs of distributed
consensus algorithms, shows that every asynchronous execution of the algorithm is equivalent to
a \emph{lossy synchronous} execution, thus reducing the burden of proof to only that subset.
In a lossy synchronous execution, processes execute in lock-step rounds, and messages are either
received in the same round or lost forever—such executions form a small subset of all asynchronous ones.

We formulate the \emph{communication-closure hypothesis},
which states that bugs in implementations of distributed consensus algorithms will already manifest in
lossy synchronous executions and present a testing algorithm based on this hypothesis.
We prioritize the search space based on a bound on the number of failures in the execution
and the rate at which these failures are recovered.
We show that a random testing algorithm based on sampling lossy synchronous executions
can empirically find a number of bugs—including previously unknown ones—in production
distributed systems such as Zookeeper, Cassandra, and Ratis,
and also produce more understandable bug traces.

Fri 20 Nov

Displayed time zone: Central Time (US & Canada) change

15:00 - 16:20
F-5BOOPSLA at SPLASH-III +12h
Chair(s): Aviral Goel Northeastern University, Mohsen Lesani University of California at Riverside, USA
15:00
20m
Talk
Programming at the Edge of Synchrony
OOPSLA
Cezara Drăgoi Inria / ENS / CNRS / PSL University / Informal Systems, Josef Widder Informal Systems, Damien Zufferey MPI-SWS
Link to publication DOI
15:20
20m
Talk
Rethinking Safe Consistency in Distributed Object-Oriented Programming
OOPSLA
Mirko Köhler TU Darmstadt, Nafise Eskandani TU Darmstadt, Pascal Weisenburger TU Darmstadt, Alessandro Margara Politecnico di Milano, Guido Salvaneschi University of St. Gallen
Link to publication DOI Media Attached
15:40
20m
Talk
Testing Consensus Implementations using Communication Closure
OOPSLA
Cezara Drăgoi Inria / ENS / CNRS / PSL University / Informal Systems, Constantin Enea University of Paris / IRIF / CNRS, Burcu Kulahcioglu Ozkan MPI-SWS, Rupak Majumdar MPI-SWS, Filip Niksic Google
Link to publication DOI Media Attached

Sat 21 Nov

Displayed time zone: Central Time (US & Canada) change

03:00 - 04:20
F-5BOOPSLA at SPLASH-III
Chair(s): Sophia Drossopoulou Imperial College London, Julien Lange Royal Holloway University of London
03:00
20m
Talk
Programming at the Edge of Synchrony
OOPSLA
Cezara Drăgoi Inria / ENS / CNRS / PSL University / Informal Systems, Josef Widder Informal Systems, Damien Zufferey MPI-SWS
Link to publication DOI
03:20
20m
Talk
Rethinking Safe Consistency in Distributed Object-Oriented Programming
OOPSLA
Mirko Köhler TU Darmstadt, Nafise Eskandani TU Darmstadt, Pascal Weisenburger TU Darmstadt, Alessandro Margara Politecnico di Milano, Guido Salvaneschi University of St. Gallen
Link to publication DOI Media Attached
03:40
20m
Talk
Testing Consensus Implementations using Communication Closure
OOPSLA
Cezara Drăgoi Inria / ENS / CNRS / PSL University / Informal Systems, Constantin Enea University of Paris / IRIF / CNRS, Burcu Kulahcioglu Ozkan MPI-SWS, Rupak Majumdar MPI-SWS, Filip Niksic Google
Link to publication DOI Media Attached