* ICSE 2018 *
Sun 27 May - Sun 3 June 2018 Gothenburg, Sweden
Fri 1 Jun 2018 14:00 - 14:20 at H1 room - Inference and Invariants Chair(s): Robert Feldt

Distributed systems are difficult to debug and understand. A key reason for this is distributed state, which is not easily accessible and must be pieced together from the states of the individual nodes in the system.

We propose Dinv, an automatic approach to help developers of distributed systems uncover the runtime distributed state properties of their systems. Dinv uses static and dynamic program analyses to infer relations between variables at different nodes. For example, in a leader election algorithm, Dinv can relate the variable leader at different nodes to derive the invariant ∀ nodes i, j, leader_i = leader_j.

This can increase the developer’s confidence in the correctness of their system. The developer can also use Dinv to convert an inferred invariant into a distributed runtime assertion on distributed state. We applied Dinv to several popular distributed systems, such as etcd Raft, Hashicorp Serf, and Taipei-Torrent, which have between 1.7K and 144K LOC and are widely used. Dinv derived useful invariants for these systems, including invariants that capture the correctness of distributed routing strategies, leadership, and key hash distribution. We also used Dinv to assert correctness of the inferred etcd Raft invariants at runtime, using these asserts to detect injected silent bugs.

Conference Day
Fri 1 Jun

Displayed time zone: Amsterdam, Berlin, Bern, Rome, Stockholm, Vienna change

14:00 - 15:30
Inference and InvariantsTechnical Papers at H1 room
Chair(s): Robert FeldtChalmers University of Technology
14:00
20m
Talk
Inferring and Asserting Distributed System Invariants
Technical Papers
Stewart Grant, Hendrik Cech, Ivan BeschastnikhUniversity of British Columbia
Link to publication Media Attached
14:20
20m
Talk
DroidStar: Callback Typestates for Android Classes
Technical Papers
Arjun RadhakrishnaMicrosoft, Nicholas Lewchenko, Shawn Meier, Sergio MoverUniversity of Colorado Boulder, Krishna Chaitanya Sripada, Damien ZuffereyMPI-SWS, Bor-Yuh Evan ChangUniversity of Colorado Boulder, Pavol CernyUniversity of Colorado Boulder
14:40
20m
Talk
Debugging with Intelligence via Probabilistic Inference
Technical Papers
Zhaogui XuNanjing University, China, Shiqing MaPurdue University, USA, Xiangyu ZhangPurdue University, Shuofei ZhuNanjing University, China, Baowen Xu
15:00
20m
Talk
Reducer-Based Construction of Conditional Verifiers
Technical Papers
Pre-print File Attached
15:20
10m
Talk
Q&A in groups
Technical Papers