Showing 1–13 of 13 results for author: Schultz, W

Efficient Synthesis of Symbolic Distributed Protocols by Sketching

Authors: Derek Egolf, William Schultz, Stavros Tripakis

Abstract: 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… ▽ More 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. △ Less

Submitted 13 May, 2024; originally announced May 2024.

Scalable, Interpretable Distributed Protocol Verification by Inductive Proof Slicing

Authors: William Schultz, Edward Ashton, Heidi Howard, Stavros Tripakis

Abstract: Many techniques for automated inference of inductive invariants for distributed protocols have been developed over the past several years, but their performance can still be unpredictable and their failure modes opaque for large-scale verification tasks. In this paper, we present inductive proof slicing, a new automated, compositional technique for inductive invariant inference that scales effecti… ▽ More Many techniques for automated inference of inductive invariants for distributed protocols have been developed over the past several years, but their performance can still be unpredictable and their failure modes opaque for large-scale verification tasks. In this paper, we present inductive proof slicing, a new automated, compositional technique for inductive invariant inference that scales effectively to large distributed protocol verification tasks. Our technique is built on a core, novel data structure, the inductive proof graph, which explicitly represents the lemma and action dependencies of an inductive invariant and is built incrementally during the inference procedure, backwards from a target safety property. We present an invariant inference algorithm that integrates localized syntax-guided lemma synthesis routines at nodes of this graph, which are accelerated by computation of localized grammar and state variable slices. Additionally, in the case of failure to produce a complete inductive invariant, maintenance of this proof graph structure allows failures to be localized to small sub-components of this graph, enabling fine-grained failure diagnosis and repair by a user. We evaluate our technique on several complex distributed and concurrent protocols, including a large scale specification of the Raft consensus protocol, which is beyond the capabilities of modern distributed protocol verification tools, and also demonstrate how its interpretability features allow effective diagnosis and repair in cases of initial failure. △ Less

Submitted 27 April, 2024; originally announced April 2024.

Turbulence Supported Massive Star Envelopes

Authors: William Schultz, Lars Bildsten, Yan-Fei Jiang

Abstract: 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. Onl… ▽ More 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. △ Less

Submitted 13 June, 2023; originally announced June 2023.

Comments: 8 pages, 4 figures, 1 table

Synthesizing Spectra from 3D Radiation Hydrodynamic Models of Massive Stars Using Monte Carlo Radiation Transport

Authors: William C. Schultz, Benny T. H. Tsang, Lars Bildsten, Yan-Fei Jiang

Abstract: Observations indicate that turbulent motions are present on most massive star surfaces. Starting from the observed phenomena of spectral lines with widths much larger than thermal broadening (e.g. micro- and macroturbulence) to the detection of stochastic low-frequency variability (SLFV) in the Transiting Exoplanet Survey Satellite photometry, these stars clearly have large scale turbulent motions… ▽ More Observations indicate that turbulent motions are present on most massive star surfaces. Starting from the observed phenomena of spectral lines with widths much larger than thermal broadening (e.g. micro- and macroturbulence) to the detection of stochastic low-frequency variability (SLFV) in the Transiting Exoplanet Survey Satellite photometry, these stars clearly have large scale turbulent motions on their surfaces. The cause of this turbulence is debated, with near-surface convection zones, core internal gravity waves, and wind variability being proposed. Our 3D grey radiation hydrodynamic (RHD) models characterized the surfaces' convective dynamics driven by near-surface convection zones and provided a reasonable match to the observed SLFV in the most luminous massive stars. We now explore the complex emitting surfaces of these 3D RHD models, which strongly violate the 1D assumption of a plane parallel atmosphere. By post-processing the grey RHD models with the Monte Carlo radiation transport code SEDONA, we synthesize stellar spectra and extract information from the broadening of individual photospheric lines. The use of SEDONA enables the calculation of the viewing angle and temporal dependence of spectral absorption line profiles. Combining uncorrelated temporal snapshots together, we compare the broadening from the 3D RHD models' velocity fields to the thermal broadening of the extended emitting region, showing that our synthesized spectral lines closely resemble the observed macroturbulent broadening from similarly luminous stars. More generally, the new techniques we have developed will allow for systematic studies of the origin of turbulent velocity broadening from any future 3D simulations. △ Less

Submitted 29 September, 2022; originally announced September 2022.

Comments: 16 pages, 9 figures, 1 table

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

Authors: William Schultz, Ian Dardik, Stavros Tripakis

Abstract: 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, potential… ▽ More 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. △ Less

Submitted 1 October, 2022; v1 submitted 12 May, 2022; originally announced May 2022.

Stochastic Low Frequency Variability in 3-Dimensional Radiation Hydrodynamical Models of Massive Star Envelopes

Authors: William C. Schultz, Lars Bildsten, Yan-Fei Jiang

Abstract: Increasing main sequence stellar luminosity with stellar mass leads to the eventual dominance of radiation pressure in stellar envelope hydrostatic balance. As the luminosity approaches the Eddington limit, additional instabilities (beyond conventional convection) can occur. These instabilities readily manifest in the outer envelopes of OB stars, where the opacity increase associated with iron yie… ▽ More Increasing main sequence stellar luminosity with stellar mass leads to the eventual dominance of radiation pressure in stellar envelope hydrostatic balance. As the luminosity approaches the Eddington limit, additional instabilities (beyond conventional convection) can occur. These instabilities readily manifest in the outer envelopes of OB stars, where the opacity increase associated with iron yields density and gas pressure inversions in 1D models. Additionally, recent photometric surveys (e.g. TESS) have detected excess broadband low frequency variability in power spectra of OB star lightcurves, called stochastic low frequency variability (SLFV). This motivates our novel 3D Athena++ radiation hydrodynamical (RHD) simulations of two 35$\,$M$_\odot$ star envelopes (the outer $\approx$15$\%$ of the stellar radial extent), one on the zero-age main sequence and the other in the middle of the main sequence. Both models exhibit turbulent motion far above and below the conventional iron opacity peak convection zone (FeCZ), obliterating any ``quiet" part of the near-surface region and leading to velocities at the photosphere of 10-100$\,$km$\,$s$^{-1}$, directly agreeing with spectroscopic data. Surface turbulence also produces SLFV in model lightcurves with amplitudes and power-law slopes that are strikingly similar to those of observed stars. The characteristic frequencies associated with SLFV in our models are comparable to the thermal time in the FeCZ ($\approx$3-7$\,$days$^{-1}$). These simulations, which have no free parameters, are directly validated by observations and, though more models are needed, we remain optimistic that 3D RHD models of main sequence O star envelopes exhibit SLFV originating from the FeCZ. △ Less

Submitted 26 October, 2021; originally announced October 2021.

Comments: 7 pages, 5 figures

Formal Verification of a Distributed Dynamic Reconfiguration Protocol

Authors: William Schultz, Ian Dardik, Stavros Tripakis

Abstract: 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… ▽ More 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. △ Less

Submitted 17 December, 2021; v1 submitted 24 September, 2021; originally announced September 2021.

Comments: First two authors contributed equally

Predicting the imagined contents using brain activation

Authors: Krishna Prasad Miyapuram, Wolfram Schultz, Philippe N. Tobler

Abstract: Mental imagery refers to percept-like experiences in the absence of sensory input. Brain imaging studies suggest common, modality-specific, neural correlates imagery and perception. We associated abstract visual stimuli with either visually presented or imagined monetary rewards and scrambled pictures. Brain images for a group of 12 participants were collected using functional magnetic resonance i… ▽ More Mental imagery refers to percept-like experiences in the absence of sensory input. Brain imaging studies suggest common, modality-specific, neural correlates imagery and perception. We associated abstract visual stimuli with either visually presented or imagined monetary rewards and scrambled pictures. Brain images for a group of 12 participants were collected using functional magnetic resonance imaging. Statistical analysis showed that human midbrain regions were activated irrespective of the monetary rewards being imagined or visually present. A support vector machine trained on the midbrain activation patterns to the visually presented rewards predicted with 75% accuracy whether the participants imagined the monetary reward or the scrambled picture during imagination trials. Training samples were drawn from visually presented trials and classification accuracy was assessed for imagination trials. These results suggest the use of machine learning technique for classification of underlying cognitive states from brain imaging data. △ Less

Submitted 14 June, 2021; originally announced June 2021.

Comments: Published In 2013 Fourth National Conference on Computer Vision, Pattern Recognition, Image Processing and Graphics (NCVPRIPG) (pp. 1-3)

Design and Analysis of a Logless Dynamic Reconfiguration Protocol

Authors: William Schultz, Siyuan Zhou, Ian Dardik, Stavros Tripakis

Abstract: 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 t… ▽ More 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. △ Less

Submitted 19 November, 2021; v1 submitted 23 February, 2021; originally announced February 2021.

Comments: 35 pages, 2 figures

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

Authors: William Schultz, Lars Bildsten, Yan-Fei Jiang

Abstract: 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… ▽ More 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. △ Less

Submitted 2 September, 2020; originally announced September 2020.

Comments: 15 pages, 10 figures, 1 table. Accepted for publication in ApJ

Heat transport bounds for a truncated model of Rayleigh-Bénard convection via polynomial optimization

Authors: Matthew L. Olson, David Goluskin, William W. Schultz, Charles R. Doering

Abstract: Upper bounds on time-averaged heat transport are obtained for an eight-mode Galerkin truncation of Rayleigh's 1916 model of natural thermal convection. Bounds for the ODE model---an extension of Lorenz's three-ODE system---are derived by constructing auxiliary functions that satisfy sufficient conditions wherein certain polynomial expressions must be nonnegative. Such conditions are enforced by re… ▽ More Upper bounds on time-averaged heat transport are obtained for an eight-mode Galerkin truncation of Rayleigh's 1916 model of natural thermal convection. Bounds for the ODE model---an extension of Lorenz's three-ODE system---are derived by constructing auxiliary functions that satisfy sufficient conditions wherein certain polynomial expressions must be nonnegative. Such conditions are enforced by requiring the polynomial expressions to admit sum-of-squares representations, allowing the resulting bounds to be minimized using semidefinite programming. Sharp or nearly sharp bounds on mean heat transport are computed numerically for numerous values of the model parameters: the Rayleigh and Prandtl numbers and the domain aspect ratio. In all cases where the Rayleigh number is small enough for the ODE model to be quantitatively close to the PDE model, mean heat transport is maximized by steady states. In some cases at larger Rayleigh number, time-periodic states maximize heat transport in the truncated model. Analytical parameter-dependent bounds are derived using quadratic auxiliary functions, and they are sharp for sufficiently small Rayleigh numbers. △ Less

Submitted 1 September, 2020; v1 submitted 15 April, 2020; originally announced April 2020.

Comments: 37 pages; v2: minor revisions

Journal ref: Physics D 415, 132748 (2020)

Deep Neural Network Classifier for Variable Stars with Novelty Detection Capability

Authors: Benny T. -H. Tsang, William C. Schultz

Abstract: Common variable star classifiers are built only with the goal of producing the correct class labels, leaving much of the multi-task capability of deep neural networks unexplored. We present a periodic light curve classifier that combines a recurrent neural network autoencoder for unsupervised feature extraction and a dual-purpose estimation network for supervised classification and novelty detecti… ▽ More Common variable star classifiers are built only with the goal of producing the correct class labels, leaving much of the multi-task capability of deep neural networks unexplored. We present a periodic light curve classifier that combines a recurrent neural network autoencoder for unsupervised feature extraction and a dual-purpose estimation network for supervised classification and novelty detection. The estimation network optimizes a Gaussian mixture model in the reduced-dimension feature space, where each Gaussian component corresponds to a variable class. An estimation network with a basic structure of a single hidden layer attains a cross-validation classification accuracy of ~99%, on par with the conventional workhorses, random forest classifiers. With the addition of photometric features, the network is capable of detecting previously unseen types of variability with precision 0.90, recall 0.96, and an F1 score of 0.93. The simultaneous training of the autoencoder and estimation network is found to be mutually beneficial, resulting in faster autoencoder convergence, and superior classification and novelty detection performance. The estimation network also delivers adequate results even when optimized with pre-trained autoencoder features, suggesting that it can readily extend existing classifiers to provide added novelty detection capabilities. △ Less

Submitted 14 May, 2019; originally announced May 2019.

Comments: 9 pages, 3 figures, 2 tables. Accepted to ApJ Letters

Stacking catalog sources in WMAP data

Authors: Kasey W. Schultz, Kevin M. Huffenberger

Abstract: We stack WMAP 7-year temperature data around extragalactic point sources, showing that the profiles are consistent with WMAP's beam models, in disagreement with the findings of Sawangwit & Shanks (2010). These results require that the source sample's selection is not biased by CMB fluctuations. We compare profiles from sources in the standard WMAP catalog, the WMAP catalog selected from a CMB-free… ▽ More We stack WMAP 7-year temperature data around extragalactic point sources, showing that the profiles are consistent with WMAP's beam models, in disagreement with the findings of Sawangwit & Shanks (2010). These results require that the source sample's selection is not biased by CMB fluctuations. We compare profiles from sources in the standard WMAP catalog, the WMAP catalog selected from a CMB-free combination of data, and the NVSS catalog, and quantify the agreement with fits to simple parametric beam models. We estimate the biases in source profiles due to alignments with positive CMB fluctuations, finding them roughly consistent with those biases found with the WMAP standard catalog. Addressing those biases, we find source spectral indices significantly steeper than those used by WMAP, with strong evidence for spectral steepening above 61 GHz. Such changes modify the power spectrum correction required for unresolved point sources, and tend to weaken somewhat the evidence for deviation from a Harrison-Zel'dovich primordial spectrum, but more analysis is required. Finally, we discuss implications for current CMB experiments. △ Less

Submitted 30 November, 2011; originally announced November 2011.

Comments: 10 pages, 7 figures, 2 tables, submitted to MNRAS