skip to main content

Attention:

The NSF Public Access Repository (NSF-PAR) system and access will be unavailable from 11:00 PM ET on Thursday, May 23 until 2:00 AM ET on Friday, May 24 due to maintenance. We apologize for the inconvenience.


Title: Adore: atomic distributed objects with certified reconfiguration
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.  more » « less
Award ID(s):
2019285 2118851 1945541
NSF-PAR ID:
10359232
Author(s) / Creator(s):
; ; ;
Date Published:
Journal Name:
PLDI 2022: Proceedings of the 43rd ACM SIGPLAN International Conference on Programming Language Design and Implementation
Page Range / eLocation ID:
379 to 394
Format(s):
Medium: X
Sponsoring Org:
National Science Foundation
More Like this
  1. Public random beacons publish random numbers at regular intervals, which anyone can obtain and verify. The design of public distributed random beacons has been an exciting research direction with significant implications for blockchains, voting, and beyond. Distributed random beacons, in addition to being bias-resistant and unpredictable, also need to have low communication overhead and latency, high resilience to faults, and ease of reconfigurability. Existing synchronous random beacon protocols sacrifice one or more of these properties. In this work, we design an efficient unpredictable synchronous random beacon protocol, OptRand, with quadratic (in the number $n$ of system nodes) communication complexity per beacon output. First, we innovate by employing a novel combination of bilinear pairing based publicly verifiable secret-sharing and non-interactive zero-knowledge proofs to build a linear (in $n$) sized publicly verifiable random sharing. Second, we develop a state machine replication protocol with linear-sized inputs that is also optimistically responsive, i.e., it can progress responsively at actual network speed during optimistic conditions, despite the synchrony assumption, and thus incur low latency. In addition, we present an efficient reconfiguration mechanism for OptRand that allows nodes to leave and join the system. Our experiments show our protocols perform significantly better compared to state-of-the-art protocols under optimistic conditions and on par with state-of-the-art protocols in the normal case. We are also the first to implement a reconfiguration mechanism for distributed beacons and demonstrate that our protocol continues to be live during reconfigurations. 
    more » « less
  2. Abstract

    While the brain’s functional network architecture is largely conserved between resting and task states, small but significant changes in functional connectivity support complex cognition. In this study, we used a modified Raven’s Progressive Matrices Task to examine symbolic and perceptual reasoning in human participants undergoing fMRI scanning. Previously, studies have focused predominantly on discrete symbolic versions of matrix reasoning, even though the first few trials of the Raven’s Advanced Progressive Matrices task consist of continuous perceptual stimuli. Our analysis examined the activation patterns and functional reconfiguration of brain networks associated with resting state and both symbolic and perceptual reasoning. We found that frontoparietal networks, including the cognitive control and dorsal attention networks, were significantly activated during abstract reasoning. We determined that these same task-active regions exhibited flexibly-reconfigured functional connectivity when transitioning from resting state to the abstract reasoning task. Conversely, we showed that a stable network core of regions in default and somatomotor networks was maintained across both resting and task states. We propose that these regionally-specific changes in the functional connectivity of frontoparietal networks puts the brain in a “task-ready” state, facilitating efficient task-based activation.

     
    more » « less
  3. Despite recent advances, guaranteeing the correctness of large-scale distributed applications without compromising performance remains a challenging problem. Network and node failures are inevitable and, for some applications, careful control over how they are handled is essential. Unfortunately, existing approaches either completely hide these failures behind an atomic state machine replication (SMR) interface, or expose all of the network-level details, sacrificing atomicity. We propose a novel, compositional, atomic distributed object (ADO) model for strongly consistent distributed systems that combines the best of both options. The object-oriented API abstracts over protocol-specific details and decouples high-level correctness reasoning from implementation choices. At the same time, it intentionally exposes an abstract view of certain key distributed failure cases, thus allowing for more fine-grained control over them than SMR-like models. We demonstrate that proving properties even of composite distributed systems can be straightforward with our Coq verification framework, Advert, thanks to the ADO model. We also show that a variety of common protocols including multi-Paxos and Chain Replication refine the ADO semantics, which allows one to freely choose among them for an application's implementation without modifying ADO-level correctness proofs. 
    more » « less
  4. We present a formal, machine checked TLA+ safety proof of MongoRaftReconfig, a distributed dynamic reconfiguration protocol. MongoRaftReconfig was designed for and implemented in MongoDB, a distributed database whose replication protocol is derived from the Raft consensus algorithm. We present an inductive invariant for MongoRaftReconfig that is formalized in TLA+ and formally proved using the TLA+ proof system (TLAPS). We also present a formal TLAPS proof of two key safety properties of MongoRaftReconfig, LeaderCompleteness and StateMachineSafety. To our knowledge, these are the first machine checked inductive invariant and safety proof of a dynamic reconfiguration protocol for a Raft based replication system. 
    more » « less
  5. Introduction

    Dissolved organic matter (DOM) composition varies over space and time, with a multitude of factors driving the presence or absence of each compound found in the complex DOM mixture. Compounds ubiquitously present across a wide range of river systems (hereafter termed core compounds) may differ in chemical composition and reactivity from compounds present in only a few settings (hereafter termed satellite compounds). Here, we investigated the spatial patterns in DOM molecular formulae presence (occupancy) in surface water and sediments across 97 river corridors at a continental scale using the “Worldwide Hydrobiogeochemical Observation Network for Dynamic River Systems—WHONDRS” research consortium.

    Methods

    We used a novel data-driven approach to identify core and satellite compounds and compared their molecular properties identified with Fourier-transform ion cyclotron resonance mass spectrometry (FT-ICR MS).

    Results

    We found that core compounds clustered around intermediate hydrogen/carbon and oxygen/carbon ratios across both sediment and surface water samples, whereas the satellite compounds varied widely in their elemental composition. Within surface water samples, core compounds were dominated by lignin-like formulae, whereas protein-like formulae dominated the core pool in sediment samples. In contrast, satellite molecular formulae were more evenly distributed between compound classes in both sediment and water molecules. Core compounds found in both sediment and water exhibited lower molecular mass, lower oxidation state, and a higher degree of aromaticity, and were inferred to be more persistent than global satellite compounds. Higher putative biochemical transformations were found in core than satellite compounds, suggesting that the core pool was more processed.

    Discussion

    The observed differences in chemical properties of core and satellite compounds point to potential differences in their sources and contribution to DOM processing in river corridors. Overall, our work points to the potential of data-driven approaches separating rare and common compounds to reduce some of the complexity inherent in studying riverine DOM.

     
    more » « less