Parsimonious Optimal Dynamic Partial Order Reduction
- URL: http://arxiv.org/abs/2405.11128v1
- Date: Sat, 18 May 2024 00:07:26 GMT
- Title: Parsimonious Optimal Dynamic Partial Order Reduction
- Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, Konstantinos Sagonas,
- Abstract summary: We present Parsimonious-OPtimal (POP) DPOR algorithm for analyzing multi-threaded programs under sequential consistency.
POP combines several novel techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, and (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions.
Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption.
- Score: 1.5029560229270196
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Stateless model checking is a fully automatic verification technique for concurrent programs that checks for safety violations by exploring all possible thread schedulings. It becomes effective when coupled with Dynamic Partial Order Reduction (DPOR), which introduces an equivalence on schedulings and reduces the amount of needed exploration. DPOR algorithms that are \emph{optimal} are particularly effective in that they guarantee to explore \emph{exactly} one execution from each equivalence class. Unfortunately, existing sequence-based optimal algorithms may in the worst case consume memory that is exponential in the size of the analyzed program. In this paper, we present Parsimonious-OPtimal (POP) DPOR, an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency, whose space consumption is polynomial in the worst case. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race, (ii) an eager race reversal strategy to avoid storing initial fragments of to-be-explored executions, and (iii) a space-efficient scheme for preventing redundant exploration, which replaces the use of sleep sets. Our implementation in Nidhugg shows that these techniques can significantly speed up the analysis of concurrent programs, and do so with low memory consumption. Comparison to a related optimal DPOR algorithm for a different representation of concurrent executions as graphs shows that POP has comparable worst-case performance for smaller benchmarks and outperforms the other one for larger programs.
Related papers
- A Mirror Descent-Based Algorithm for Corruption-Tolerant Distributed Gradient Descent [57.64826450787237]
We show how to analyze the behavior of distributed gradient descent algorithms in the presence of adversarial corruptions.
We show how to use ideas from (lazy) mirror descent to design a corruption-tolerant distributed optimization algorithm.
Experiments based on linear regression, support vector classification, and softmax classification on the MNIST dataset corroborate our theoretical findings.
arXiv Detail & Related papers (2024-07-19T08:29:12Z) - Tailoring Stateless Model Checking for Event-Driven Multi-Threaded
Programs [1.2948955292336792]
We present Event-DPOR, a DPOR algorithm tailored to event-driven programs.
It is based on Optimal-DPOR, an optimal DPOR algorithm for multi-threaded programs.
We prove correctness of Event-DPOR for all programs, and optimality for a large subclass.
arXiv Detail & Related papers (2023-07-29T08:43:49Z) - Accelerating Cutting-Plane Algorithms via Reinforcement Learning
Surrogates [49.84541884653309]
A current standard approach to solving convex discrete optimization problems is the use of cutting-plane algorithms.
Despite the existence of a number of general-purpose cut-generating algorithms, large-scale discrete optimization problems continue to suffer from intractability.
We propose a method for accelerating cutting-plane algorithms via reinforcement learning.
arXiv Detail & Related papers (2023-07-17T20:11:56Z) - Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
We exploit between first-order algorithms for constrained optimization and non-smooth systems to design a new class of accelerated first-order algorithms.
An important property of these algorithms is that constraints are expressed in terms of velocities instead of sparse variables.
arXiv Detail & Related papers (2023-02-01T08:50:48Z) - Decision Diagram-Based Branch-and-Bound with Caching for Dominance and
Suboptimality Detection [9.175779296469194]
This paper presents new ingredients to speed up the search by exploiting the structure of dynamic programming models.
The key idea is to prevent the repeated expansion of nodes corresponding to the same dynamic programming states by querying expansion thresholds cached throughout the search.
Experiments show that the pruning brought by this caching mechanism allows significantly reducing the number of nodes expanded by the algorithm.
arXiv Detail & Related papers (2022-11-22T10:18:33Z) - Naive Automated Machine Learning [0.0]
We present Naive AutoML, an approach that does precisely this: It optimize the different algorithms of a pre-defined pipeline scheme in isolation.
The isolated generalization leads to substantially reduced search spaces.
arXiv Detail & Related papers (2021-11-29T13:12:54Z) - Optimal and Efficient Algorithms for General Mixable Losses against
Switching Oracles [0.0]
We study the online optimization of mixable loss functions in a dynamic environment.
Our results are guaranteed to hold in a strong deterministic sense in an individual sequence manner.
arXiv Detail & Related papers (2021-08-13T21:48:55Z) - Single-Timescale Stochastic Nonconvex-Concave Optimization for Smooth
Nonlinear TD Learning [145.54544979467872]
We propose two single-timescale single-loop algorithms that require only one data point each step.
Our results are expressed in a form of simultaneous primal and dual side convergence.
arXiv Detail & Related papers (2020-08-23T20:36:49Z) - Safeguarded Learned Convex Optimization [106.81731132086851]
Analytic optimization algorithms can be hand-designed to provably solve problems in an iterative fashion.
Data-driven algorithms can "learn to optimize" (L2O) with much fewer iterations and similar cost per iteration as general-purpose optimization algorithms.
We present a Safe-L2O framework to fuse the advantages of these approaches.
arXiv Detail & Related papers (2020-03-04T04:01:15Z) - Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
We propose the setting of extreme algorithm selection (XAS) where we consider fixed sets of thousands of candidate algorithms.
We assess the applicability of state-of-the-art AS techniques to the XAS setting and propose approaches leveraging a dyadic feature representation.
arXiv Detail & Related papers (2020-01-29T09:40:58Z)
This list is automatically generated from the titles and abstracts of the papers in this site.
This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.