An official website of the United States government
Distributed consensus algorithms such as Paxos have been studied extensively. Many different liveness properties and assumptions have been stated for them, but there are no systematic comparisons for better understanding of these properties. This paper systematically studies and compares different liveness properties stated for over 30 prominent consensus algorithms and variants. We introduced a precise high-level language and formally specified these properties in the language. We then create a hierarchy of liveness properties combining two hierarchies of the assumptions used and a hierarchy of the assertions made, and compare the strengths and weaknesses of algorithms that ensure these properties. Our formal specifications and systematic comparisons led to the discovery of a range of problems in various stated liveness properties. We also developed TLA+ specifications of these liveness properties, and we used model checking of execution steps to illustrate liveness patterns for Paxos.
more »
« less
Examples and conjectures on the regularity of solutions to balance laws
The paper discusses various regularity properties for solutions to a scalar, 1-dimensional conservation law with strictly convex flux and integrable source. In turn, these yield compactness estimates on the solution set. Similar properties are expected to hold for 2x2 genuinely nonlinear systems.
more »
« less
- Award ID(s):
- 2154201
- PAR ID:
- 10398446
- Date Published:
- Journal Name:
- Quarterly of Applied Mathematics
- ISSN:
- 0033-569X
- Format(s):
- Medium: X
- Sponsoring Org:
- National Science Foundation
More Like this
-
-
Distributed protocols have long been formulated in terms of their safety and liveness properties. Much recent work has focused on automatically verifying the safety properties of distributed protocols, but doing so for liveness properties has remained a challenging, unsolved problem. We present LVR, the first framework that can mostly automatically verify liveness properties for distributed protocols. Our key insight is that most liveness properties for distributed protocols can be reduced to a set of safety properties with the help of ranking functions. Such ranking functions for practical distributed protocols have certain properties that make them straightforward to synthesize, contrary to conventional wisdom. We prove that verifying a liveness property can then be reduced to a simpler problem of verifying a set of safety properties, namely that the ranking function is strictly decreasing and nonnegative for any protocol state transition, and there is no deadlock. LVR automatically synthesizes ranking functions by formulating a parameterized function of integer protocol variables, statically analyzing the lower and upper bounds of the variables as well as how much they can change on each state transition, then feeding the constraints to an SMT solver to determine the coefficients of the ranking function. It then uses an off-the-shelf verification tool to find inductive invariants to verify safety properties for both ranking functions and deadlock freedom. We show that LVR can mostly automatically verify the liveness properties of several distributed protocols, including various versions of Paxos, with limited user guidance.more » « less
-
Abstract Machine learning interatomic potential (MLIP) has been widely adopted for atomistic simulations. While errors and discrepancies for MLIPs have been reported, a comprehensive examination of the MLIPs’ performance over a broad spectrum of material properties has been lacking. This study introduces an analysis process comprising model sampling, benchmarking, error evaluations, and multi-dimensional statistical analyses on an ensemble of MLIPs for prediction errors over a diverse range of properties. By carrying out this analysis on 2300 MLIP models based on six different MLIP types, several properties that pose challenges for the MLIPs to achieve small errors are identified. The Pareto front analyses on two or more properties reveal the trade-offs in different properties of MLIPs, underscoring the difficulties of achieving low errors for a large number of properties simultaneously. Furthermore, we propose correlation graph analyses to characterize the error performances of MLIPs and to select the representative properties for predicting other property errors. This analysis process on a large dataset of MLIP models sheds light on the underlying complexities of MLIP performance, offering crucial guidance for the future development of MLIPs with improved predictive accuracy across an array of material properties.more » « less
-
ifferent mechanisms are used for the discovery of materials. These include creating a material by trial-and-error process without knowing its properties. Other methods are based on computational simulations or mathematical and statistical approaches, such as Density Functional Theory (DFT). A well-known strategy combines elements to predict their properties and selects a set of those with the properties of interest. Carrying out exhaustive calculations to predict the properties of these found compounds may require a high computational cost. Therefore, there is a need to create methods for identifying materials with a desired set of properties while reducing the search space and, consequently, the computational cost. In this work, we present a genetic algorithm that can find a higher percentage of compounds with specific properties than state-of-the-art methods, such as those based on combinatorial screening. Both methods are compared in the search for ternary compounds in an unconstrained space, using a Deep Neural Network (DNN) to predict properties such as formation enthalpy, band gap, and stability; we will focus on formation enthalpy. As a result, we provide a genetic algorithm capable of finding up to 60% more compounds with atypical values of properties, using DNNs for their prediction.more » « less
-
In this work, we investigate magnetic monolayers of the form A i A ii B 4 X 8 based on the well-known intrinsic topological magnetic van der Waals (vdW) material MnBi 2 Te 4 (MBT) using first-principles calculations and machine learning techniques. We select an initial subset of structures to calculate the thermodynamic properties, electronic properties, such as the band gap, and magnetic properties, such as the magnetic moment and magnetic order using density functional theory (DFT). Data analytics approaches are used to gain insight into the microscopic origin of materials’ properties. The dependence of materials’ properties on chemical composition is also explored. For example, we find that the formation energy and magnetic moment depend largely on A and B sites whereas the band gap depends on all three sites. Finally, we employ machine learning tools to accelerate the search for novel vdW magnets in the MBT family with optimized properties. This study creates avenues for rapidly predicting novel materials with desirable properties that could enable applications in spintronics, optoelectronics, and quantum computing.more » « less
- Free Publicly Accessible Full Text
-
Accepted Manuscript1.0
- Journal Article:
- https://doi.org/10.1090/qam/1647
