Thu 16 Jun 2022 11:40 - 12:00 at Kon-Tiki - Distribution Chair(s): Constantin Enea
Thu 16 Jun 2022 23:40 - 00:00 at Kon-Tiki - Distribution

Finding the right abstraction is critical for reasoning about complex systems such as distributed protocols like Paxos and Raft. Despite a recent abundance of impressive verification work in this area, we claim the ways that past efforts model distributed state are not ideal for protocol-level reasoning: they either hide important details, or leak too much complexity from the network. As evidence we observe that nearly all of them avoid the complex, but important issue of reconfiguration. Reconfiguration’s primary challenge lies in how it interacts with a protocol’s core safety invariants. To handle this increased complexity, we introduce the Adore model, whose novel abstract state hides network-level communications while capturing dependencies between committed and uncommitted states, as well as metadata like election quorums. It includes first-class support for a generic reconfiguration command that can be instantiated with a variety of implementations. Under this model, the subtle interactions between reconfiguration and the core protocol become clear, and with this insight we completed the first mechanized proof of safety of a reconfigurable consensus protocol.

Thu 16 Jun

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

10:40 - 12:00
DistributionPLDI at Kon-Tiki +12h
Chair(s): Constantin Enea Ecole Polytechnique / LIX / CNRS
10:40
20m
Talk
Certified Mergeable Replicated Data Types
PLDI
Vimala Soundarapandian IIT Madras, Adharsh Kamath NITK Surathkal, Kartik Nagar IIT Madras, KC Sivaramakrishnan IIT Madras and Tarides
DOI Pre-print
11:00
20m
Talk
Hamband: RDMA Replicated Data Types
PLDI
Farzin Houshmand University of California, Riverside, Javad Saberlatibari University of California Riverside, Mohsen Lesani University of California at Riverside
DOI
11:20
20m
Talk
RunTime-Assisted Convergence in Replicated Data Types
PLDI
Gowtham Kaki University of Colorado Boulder, Prasanth Prahladan University of Colorado Boulder, Nicholas V. Lewchenko University of Colorado Boulder
DOI
11:40
20m
Talk
Adore: Atomic Distributed Objects with Certified Reconfiguration
PLDI
Wolf Honore Yale University, Ji-Yong Shin Northeastern University, Jieung Kim Yale University, USA, Zhong Shao Yale University
DOI Pre-print
22:40 - 00:00
DistributionPLDI at Kon-Tiki
22:40
20m
Talk
Certified Mergeable Replicated Data Types
PLDI
Vimala Soundarapandian IIT Madras, Adharsh Kamath NITK Surathkal, Kartik Nagar IIT Madras, KC Sivaramakrishnan IIT Madras and Tarides
DOI Pre-print
23:00
20m
Talk
Hamband: RDMA Replicated Data Types
PLDI
Farzin Houshmand University of California, Riverside, Javad Saberlatibari University of California Riverside, Mohsen Lesani University of California at Riverside
DOI
23:20
20m
Talk
RunTime-Assisted Convergence in Replicated Data Types
PLDI
Gowtham Kaki University of Colorado Boulder, Prasanth Prahladan University of Colorado Boulder, Nicholas V. Lewchenko University of Colorado Boulder
DOI
23:40
20m
Talk
Adore: Atomic Distributed Objects with Certified Reconfiguration
PLDI
Wolf Honore Yale University, Ji-Yong Shin Northeastern University, Jieung Kim Yale University, USA, Zhong Shao Yale University
DOI Pre-print