arXiv subjects

William Schultz

Publications and source records attributed to William Schultz.

7 recordsLinked to original sources

arXiv2024

Efficient Synthesis of Symbolic Distributed Protocols by Sketching

We present a novel and efficient method for synthesis of parameterized distributed protocols by sketching. Our method is both syntax-guided and counterexample-guided, and utilizes a fast equivalence reduction technique that enables efficient completion of protocol sketches, often significantly reducing the search space of candidate completions by several orders of magnitude. To our knowledge, our tool, Scythe, is the first synthesis tool for the widely used specification language TLA+. We evaluate Scythe on a diverse benchmark of distributed protocols, demonstrating the ability to synthesize a large scale distributed Raft-based dynamic reconfiguration protocol beyond the scale of what existing synthesis techniques can handle.

cs.LO↗

arXiv2024

Interactive Safety Verification of Distributed Protocols by Inductive Proof Decomposition

Many techniques for the automated verification of distributed protocols have been developed over the past several years, but their performance is still unpredictable and their failure modes can be opaque for industrial scale verification tasks. Thus, in practice, large-scale verification efforts typically require some amount of human guidance. In this paper, we present inductive proof decomposition, a new methodology for interactive safety verification that provides a compositional, interactive approach to inductive invariant development. Our approach guides the human-aided development of inductive invariants via a novel structure, an inductive proof graph, which is built incrementally by a human verifier, working backwards from a target safety property. A user is guided by induction counterexamples that are localized to specific nodes of this graph, and nodes of this proof graph are further decomposed based on logical actions that appear in a protocol's transition relation. Our decomposition also enables a localized variable slicing technique that hides irrelevant protocol state at each sub-component of an inductive proof, allowing a user to focus on fine-grained sub-problems rather than a large, monolithic inductive invariant. We present our technique and experience applying it to develop inductive safety proofs of several complex distributed protocols, including the Raft consensus protocol, which is beyond the capabilities of modern automated verification tools. We also demonstrate how the developed proof graphs provide additional insight into the structure of a protocol proof and its correctness.

cs.DC↗

arXiv2023

Turbulence Supported Massive Star Envelopes

The outer envelopes of massive ($M\gtrsim10\,M_{\odot}$) stars exhibit large increases in opacities from forests of lines and ionization transitions (particularly from iron and helium) that trigger near-surface convection zones. One-dimensional models predict density inversions and supersonic motions that must be resolved with computationally intensive 3D radiation hydrodynamic (RHD) modeling. Only in the last decade have computational tools advanced to the point where ab initio 3D models of these turbulent envelopes can be calculated, enabling us to present five 3D RHD Athena++ models (four previously published and one new 13$M_{\odot}$ model). When convective motions are sub-sonic, we find excellent agreement between 3D and 1D velocity magnitudes, stellar structure, and photospheric quantities. However when convective velocities approach the sound speed, hydrostatic balance fails as the turbulent pressure can account for 80% of the force balance. As predicted by Henyey, we show that this additional pressure support leads to a modified temperature gradient which reduces the superadiabaticity where convection is occurring. In addition, all five models display significant overshooting from the convection in the Fe convection zone. As a result, the turbulent velocities at the surface are indicative of those in the Fe zone. There are no confined convection zones as seen in 1D models. In particular, helium convection zones seen in 1D models are significantly modified. Stochastic low frequency brightness variability is also present in the 13$M_{\odot}$ model with comparable amplitude and characteristic frequency to observed stars.

astro-ph.SR↗

arXiv2022

Plain and Simple Inductive Invariant Inference for Distributed Protocols in TLA+

We present a new technique for automatically inferring inductive invariants of parameterized distributed protocols specified in TLA+. Ours is the first such invariant inference technique to work directly on TLA+, an expressive, high level specification language. To achieve this, we present a new algorithm for invariant inference that is based around a core procedure for generating plain, potentially non-inductive lemma invariants that are used as candidate conjuncts of an overall inductive invariant. We couple this with a greedy lemma invariant selection procedure that selects lemmas that eliminate the largest number of counterexamples to induction at each round of our inference procedure. We have implemented our algorithm in a tool, endive, and evaluate it on a diverse set of distributed protocol benchmarks, demonstrating competitive performance and ability to uniquely solve an industrial scale reconfiguration protocol.

cs.LO↗

arXiv2021

Formal Verification of a Distributed Dynamic Reconfiguration Protocol

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.

cs.DC↗

arXiv2021

Design and Analysis of a Logless Dynamic Reconfiguration Protocol

Distributed replication systems based on the replicated state machine model have become ubiquitous as the foundation of modern database systems. To ensure availability in the presence of faults, these systems must be able to dynamically replace failed nodes with healthy ones via dynamic reconfiguration. MongoDB is a document oriented database with a distributed replication mechanism derived from the Raft protocol. In this paper, we present MongoRaftReconfig, a novel dynamic reconfiguration protocol for the MongoDB replication system. MongoRaftReconfig utilizes a logless approach to managing configuration state and decouples the processing of configuration changes from the main database operation log. The protocol's design was influenced by engineering constraints faced when attempting to redesign an unsafe, legacy reconfiguration mechanism that existed previously in MongoDB. We provide a safety proof of MongoRaftReconfig, along with a formal specification in TLA+. To our knowledge, this is the first published safety proof and formal specification of a reconfiguration protocol for a Raft-based system. We also present results from model checking its safety properties on finite protocol instances. Finally, we discuss the conceptual novelties of MongoRaftReconfig, how it can be understood as an optimized and generalized version of the single server reconfiguration algorithm of Raft, and present an experimental evaluation of how its optimizations can provide performance benefits for reconfigurations.

cs.DC↗

arXiv2020

Convectively Driven Three Dimensional Turbulence in Massive Star Envelopes: I. A 1D Implementation of Diffusive Radiative Transport

Massive ($M >30\,$M$_{\odot}$) stars exhibit luminosities that are near the Eddington-limit for electron scattering causing the increase in opacity associated with iron at $T\approx180,000\,$K to trigger supersonic convection in their outer envelopes. Three dimensional radiative hydrodynamics simulations by Jiang and collaborators with the Athena++ computational tool have found order of magnitude density and radiative flux fluctuations in these convective regions, even at optical depths $\gg100$. We show here that radiation can diffuse out of a parcel during the timescale of convection in these optically thick parts of the star, motivating our use of a "pseudo" Mach number to characterize both the fluctuation amplitudes and their correlations. In this first paper, we derive the impact of these fluctuations on the radiative pressure gradient needed to carry a given radiative luminosity. This implementation leads to a remarkable improvement between 1D and 3D radiative pressure gradients, and builds confidence in our path to an eventual 1D implementation of these intrinsically 3D envelopes. However, simply reducing the radiation pressure gradient is not enough to implement a new 1D model. Rather, we must also account for the impact of two other aspects of turbulent convection: the substantial pressure, and the ability to transport an appreciable fraction of the luminosity, which will be addressed in upcoming works. This turbulent convection also arises in other instances where the stellar luminosity approaches the Eddington luminosity. Hence, our effort should apply to other astrophysical situations where an opacity peak arises in a near Eddington limited, radiation pressure dominated plasma.

astro-ph.SR↗