論文の概要: Parsimonious Optimal Dynamic Partial Order Reduction

• arxiv url: http://arxiv.org/abs/2405.11128v1
• Date: Sat, 18 May 2024 00:07:26 GMT
• ステータス: 処理完了
• システム内更新日: 2024-05-21 19:17:16.150175
• Title: Parsimonious Optimal Dynamic Partial Order Reduction
• Title（参考訳）: パルシモニアス最適動的部分順序の低減
• Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, Konstantinos Sagonas,
• Abstract要約: 本稿ではPOP(Parsimonious-Optimal)DPORアルゴリズムを提案する。 POPは、(i)同じ人種の複数の逆転を避ける擬似的な人種逆転戦略、(ii)探索された実行の最初の断片を保存することを避けるための熱狂的な人種逆転戦略など、いくつかの新しい技術を組み合わせている。 我々のNidhuggの実装は、これらの手法が並列プログラムの解析を著しく高速化し、メモリ消費を抑えられることを示している。
• 参考スコア（独自算出の注目度）: 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.
• Abstract（参考訳）: ステートレスモデルチェックは、全てのスレッドスケジューリングを探索して安全性違反をチェックする並列プログラムの完全な自動検証手法である。 動的部分順序減少(DPOR)と組み合わせることで、スケジューリングの等価性を導入し、必要な探索量を削減できる。 emph{optimal} である DPOR アルゴリズムは、各同値類から \emph{exactly} 1 つの実行を探索することを保証するという点で特に有効である。 残念なことに、既存のシーケンスベースの最適アルゴリズムは、分析プログラムのサイズが指数関数的なメモリを消費する最悪のケースがある。 本稿では,POP(Parsimonious-Optimal) DPORを提案する。POP(Parsimonious-Optimal) DPORは,POP(Parsimonious-Optimal) とPOP(Parsimonious-Optimal) DPOR(Parsimonious-Optimal) とPOP(Parsimonious-Optimal) DPOR(Parsimonious-Optimal) とPOP(Parsimonious-Optimal) DPOR(Parsimonious-Optimal) DPOR) の2つのアルゴリズムである。 POPはいくつかの新しいアルゴリズム技術を組み合わせる (i)同じ人種の複数の逆転を避ける擬似的な人種逆転戦略。 (二 探索した実行の最初の断片の保存を避けるための熱狂的な競争逆転戦略、及び 三 余剰探査の防止のための空間効率のよいスキームで、睡眠セットの使用を代替する。 我々のNidhuggの実装は、これらの手法が並列プログラムの解析を著しく高速化し、メモリ消費を抑えられることを示している。 グラフが示すように、並列実行の異なる表現に対する関連する最適DPORアルゴリズムと比較すると、POPはより小さなベンチマークに対して同等の最悪の性能を示し、より大きなプログラムでは他方よりも優れている。

関連論文リスト

• A Mirror Descent-Based Algorithm for Corruption-Tolerant Distributed Gradient Descent [57.64826450787237]
  本研究では, 分散勾配降下アルゴリズムの挙動を, 敵対的腐敗の有無で解析する方法を示す。 汚職耐性の分散最適化アルゴリズムを設計するために、(怠慢な)ミラー降下からアイデアをどう使うかを示す。 MNISTデータセットの線形回帰、サポートベクトル分類、ソフトマックス分類に基づく実験は、我々の理論的知見を裏付けるものである。
  論文  参考訳（メタデータ） (2024-07-19T08:29:12Z)
• Tailoring Stateless Model Checking for Event-Driven Multi-Threaded Programs [1.2948955292336792]
  イベント駆動型プログラムに適したDPORアルゴリズムであるEvent-DPORを提案する。 これはマルチスレッドプログラムのための最適DPORアルゴリズムであるOptimal-DPORに基づいている。 全てのプログラムに対して Event-DPOR の正当性を証明し,大規模サブクラスに対して最適性を示す。
  論文  参考訳（メタデータ） (2023-07-29T08:43:49Z)
• Accelerating Cutting-Plane Algorithms via Reinforcement Learning Surrogates [49.84541884653309]
  凸離散最適化問題に対する現在の標準的なアプローチは、カットプレーンアルゴリズムを使うことである。 多くの汎用カット生成アルゴリズムが存在するにもかかわらず、大規模な離散最適化問題は、難易度に悩まされ続けている。 そこで本研究では,強化学習による切削平面アルゴリズムの高速化手法を提案する。
  論文  参考訳（メタデータ） (2023-07-17T20:11:56Z)
• Accelerated First-Order Optimization under Nonlinear Constraints [73.2273449996098]
  我々は、制約付き最適化のための一階アルゴリズムと非滑らかなシステムの間で、新しい一階アルゴリズムのクラスを設計する。 これらのアルゴリズムの重要な性質は、制約がスパース変数の代わりに速度で表されることである。
  論文  参考訳（メタデータ） (2023-02-01T08:50:48Z)
• Decision Diagram-Based Branch-and-Bound with Caching for Dominance and Suboptimality Detection [9.175779296469194]
  本稿では動的プログラミングモデルの構造を利用して探索を高速化する新しい要素を提案する。 鍵となる考え方は、検索中にキャッシュされた拡張しきい値に問い合わせることによって、同じ動的プログラミング状態に対応するノードの繰り返し拡張を防止することである。 このキャッシング機構によって引き起こされるプルーニングは、アルゴリズムによって拡張されたノード数を著しく削減できることを示す実験である。
  論文  参考訳（メタデータ） (2022-11-22T10:18:33Z)
• Naive Automated Machine Learning [0.0]
  事前に定義されたパイプラインスキームの異なるアルゴリズムを分離して最適化します。 孤立した一般化は、探索空間を著しく減少させる。
  論文  参考訳（メタデータ） (2021-11-29T13:12:54Z)
• Optimal and Efficient Algorithms for General Mixable Losses against Switching Oracles [0.0]
  動的環境における混合損失関数のオンライン最適化について検討する。 我々の結果は、個々のシーケンス方式で強い決定論的意味を持つことが保証されている。
  論文  参考訳（メタデータ） (2021-08-13T21:48:55Z)
• Single-Timescale Stochastic Nonconvex-Concave Optimization for Smooth Nonlinear TD Learning [145.54544979467872]
  本稿では,各ステップごとに1つのデータポイントしか必要としない2つの単一スケールシングルループアルゴリズムを提案する。 本研究の結果は, 同時一次および二重側収束の形で表される。
  論文  参考訳（メタデータ） (2020-08-23T20:36:49Z)
• Safeguarded Learned Convex Optimization [106.81731132086851]
  解析最適化アルゴリズムは、反復的な方法で問題を確実に解くために手作業で設計することができる。 データ駆動アルゴリズムは、汎用最適化アルゴリズムと同様のイテレーション当たりのコストと、はるかに少ないイテレーションで"L2O"を最適化する。 我々はこれらのアプローチの利点を融合させるSafe-L2Oフレームワークを提案する。
  論文  参考訳（メタデータ） (2020-03-04T04:01:15Z)
• Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
  我々は,数千の候補アルゴリズムの固定セットを考慮に入れた,極端なアルゴリズム選択(XAS)の設定を提案する。 我々は、XAS設定に対する最先端のAS技術の適用性を評価し、Dyadic特徴表現を利用したアプローチを提案する。
  論文  参考訳（メタデータ） (2020-01-29T09:40:58Z)

関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。

指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。