Parsimonious Optimal Dynamic Partial Order Reduction

• URL: http://arxiv.org/abs/2405.11128v2
• Date: Mon, 23 Sep 2024 13:42:30 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 DPOR (POP), an optimal DPOR algorithm for analyzing multi-threaded programs under sequential consistency. POP combines several novel algorithmic techniques, including (i) a parsimonious race reversal strategy, which avoids multiple reversals of the same race. 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 optimal are particularly effective in that they guarantee to explore 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 DPOR (POP), 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 TruSt, a related optimal DPOR algorithm that represents executions as graphs, shows that POP's implementation achieves similar performance for smaller benchmarks, and scales much better than TruSt's on programs with long executions.

Related papers

• Faster WIND: Accelerating Iterative Best-of-$N$ Distillation for LLM Alignment [81.84950252537618]
  This paper reveals a unified game-theoretic connection between iterative BOND and self-play alignment. We establish a novel framework, WIN rate Dominance (WIND), with a series of efficient algorithms for regularized win rate dominance optimization.
  arXiv  Detail & Related papers  (2024-10-28T04:47:39Z)
• OptEx: Expediting First-Order Optimization with Approximately Parallelized Iterations [12.696136981847438]
  We introduce first-order optimization expedited with approximately parallelized iterations (OptEx) OptEx is the first framework that enhances the efficiency of FOO by leveraging parallel computing to mitigate its iterative bottleneck. We provide theoretical guarantees for the reliability of our kernelized gradient estimation and the complexity of SGD-based OptEx.
  arXiv  Detail & Related papers  (2024-02-18T02:19:02Z)
• 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)
• Efficiency Ordering of Stochastic Gradient Descent [9.634481296779057]
  We consider the gradient descent (SGD) algorithm driven by a general sampling sequence, including i.i.i.d noise and random walk on an arbitrary graph. We employ the notion of efficiency ordering', a well-analyzed tool for comparing the performance of Markov Chain Monte Carlo samplers.
  arXiv  Detail & Related papers  (2022-09-15T16:50:55Z)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  Inspired by sum-of-infeasibilities methods in convex optimization, we propose a novel procedure for analyzing verification queries on networks with extensive branching functions. An extension to a canonical case-analysis-based complete search procedure can be achieved by replacing the convex procedure executed at each search state with DeepSoI.
  arXiv  Detail & Related papers  (2022-03-19T15:05:09Z)
• 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)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  Security-constrained optimal power flow (SCOPF) is fundamental in power systems. Modeling of APR within the SCOPF problem results in complex large-scale mixed-integer programs. This paper proposes a novel approach that combines deep learning and robust optimization techniques.
  arXiv  Detail & Related papers  (2020-07-14T12:38:21Z)
• 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.