論文の概要: 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はより小さなベンチマークに対して同等の最悪の性能を示し、より大きなプログラムでは他方よりも優れている。

関連論文リスト

• Faster WIND: Accelerating Iterative Best-of-$N$ Distillation for LLM Alignment [81.84950252537618]
  本稿では,反復的BONDと自己プレイアライメントの統一的なゲーム理論接続を明らかにする。 WINレート支配(WIN rate Dominance, WIND)という新しいフレームワークを構築し, 正規化利率支配最適化のためのアルゴリズムを多数提案する。
  論文  参考訳（メタデータ） (2024-10-28T04:47:39Z)
• OptEx: Expediting First-Order Optimization with Approximately Parallelized Iterations [12.696136981847438]
  ほぼ並列化されたイテレーション (OptEx) で高速化された一階最適化を導入する。 OptExは、並列コンピューティングを活用して、その反復的ボトルネックを軽減することで、FOOの効率を高める最初のフレームワークである。 我々は、カーネル化された勾配推定の信頼性とSGDベースのOpsExの複雑さを理論的に保証する。
  論文  参考訳（メタデータ） (2024-02-18T02:19:02Z)
• 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)
• Efficiency Ordering of Stochastic Gradient Descent [9.634481296779057]
  我々は、任意のグラフ上のノイズやランダムウォークを含む一般的なサンプリングシーケンスによって駆動される勾配降下(SGD)アルゴリズムについて検討する。 我々は、マルコフ・チェイン・モンテカルロサンプリング器の性能を比較するためのよく分析されたツールである「効率順序付け」の概念を採用している。
  論文  参考訳（メタデータ） (2022-09-15T16:50:55Z)
• Efficient Neural Network Analysis with Sum-of-Infeasibilities [64.31536828511021]
  凸最適化における総和係数法に着想を得て,広範な分岐関数を持つネットワーク上での検証クエリを解析するための新しい手法を提案する。 標準ケース分析に基づく完全探索手順の拡張は、各検索状態で実行される凸手順をDeepSoIに置き換えることによって達成できる。
  論文  参考訳（メタデータ） (2022-03-19T15:05:09Z)
• Naive Automated Machine Learning [0.0]
  事前に定義されたパイプラインスキームの異なるアルゴリズムを分離して最適化します。 孤立した一般化は、探索空間を著しく減少させる。
  論文  参考訳（メタデータ） (2021-11-29T13:12:54Z)
• Combining Deep Learning and Optimization for Security-Constrained Optimal Power Flow [94.24763814458686]
  セキュリティに制約のある最適電力フロー(SCOPF)は、電力システムの基本である。 SCOPF問題におけるAPRのモデル化は、複雑な大規模混合整数プログラムをもたらす。 本稿では,ディープラーニングとロバスト最適化を組み合わせた新しい手法を提案する。
  論文  参考訳（メタデータ） (2020-07-14T12:38:21Z)
• Extreme Algorithm Selection With Dyadic Feature Representation [78.13985819417974]
  我々は,数千の候補アルゴリズムの固定セットを考慮に入れた,極端なアルゴリズム選択(XAS)の設定を提案する。 我々は、XAS設定に対する最先端のAS技術の適用性を評価し、Dyadic特徴表現を利用したアプローチを提案する。
  論文  参考訳（メタデータ） (2020-01-29T09:40:58Z)

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

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