ETAPS 2019
Sat 6 - Thu 11 April 2019 Prague, Czech Republic
Wed 10 Apr 2019 11:00 - 11:30 at SUN I - Concurrent and Distributed Systems Chair(s): Marieke Huisman

Many transaction systems distribute, partition, and replicate their data for scalability, availability, and fault tolerance. However, observing and maintaining strong consistency of distributed and partially replicated data leads to high transaction latencies. Since different applications require different consistency guarantees, there is a plethora of consistency properties—from weak ones such as read atomicity through various forms of snapshot isolation to stronger serializability properties—and distributed transaction systems (DTSs) guaranteeing such properties. This paper presents a general framework for formally specifying a DTS in Maude, and formalizes in Maude nine common consistency properties for DTSs so defined. Furthermore, we provide a fully automated method for analyzing whether the DTS satisfies the desired property for all initial states up to given bounds on system parameters. This is based on automatically recording relevant history during a Maude run and defining the consistency properties on such histories. To the best of our knowledge, this is the first time that model checking of all these properties in a unified, systematic manner is investigated. We have implemented a tool that automates our method, and use it to model check state-of-the-art DTSs such as P-Store, RAMP, Walter, Jessy, and ROLA.

Wed 10 Apr (GMT+02:00) Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

tacas-2019-papers
10:30 - 12:30: TACAS 2019 - Concurrent and Distributed Systems at SUN I
Chair(s): Marieke HuismanUniversity of Twente
tacas-2019-papers10:30 - 11:00
Talk
Tom van DijkUniversity of Twente, Jeroen Meijer, Jaco van de PolAarhus University
Link to publication
tacas-2019-papers11:00 - 11:30
Talk
Si Liu, Peter Ölveczky, Min ZhangEast China Normal University, Qi Wang, José Meseguer
Link to publication
tacas-2019-papers11:30 - 12:00
Talk
Link to publication
tacas-2019-papers12:00 - 12:30
Talk
Marius BozgaVerimag/CNRS, Radu IosifVERIMAG, CNRS, Université Grenoble-Alpes, Joseph SifakisVerimag/CNRS
Link to publication