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

• arxiv url: http://arxiv.org/abs/2405.11128v2
• Date: Mon, 23 Sep 2024 13:42:30 GMT
• ステータス: 処理完了
• システム内更新日: 2024-11-09 02:30:11.215512
• Title: Parsimonious Optimal Dynamic Partial Order Reduction
• Title（参考訳）: パルシモニアス最適動的部分順序の低減
• Authors: Parosh Aziz Abdulla, Mohamed Faouzi Atig, Sarbojit Das, Bengt Jonsson, Konstantinos Sagonas,
• Abstract要約: 本稿では,Parsimonious-Optimal DPOR(POP)を提案する。 POPは、(i)同じ人種の複数の逆転を避ける擬似的な人種反転戦略を含む、いくつかの新しいアルゴリズム技術を組み合わせている。 我々の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 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.
• Abstract（参考訳）: ステートレスモデルチェックは、全てのスレッドスケジューリングを探索して安全性違反をチェックする並列プログラムの完全な自動検証手法である。 動的部分順序減少(DPOR)と組み合わせることで、スケジューリングの等価性を導入し、必要な探索量を削減できる。 最適なDPORアルゴリズムは、各等価クラスから正確に1つの実行を探索することが保証されるという点で特に効果的である。 残念なことに、既存のシーケンスベースの最適アルゴリズムは、分析プログラムのサイズが指数関数的なメモリを消費する最悪のケースがある。 本稿では,POP (Parsimonious-Optimal DPOR) を提案する。POP (Parsimonious-Optimal DPOR) は,空間消費が最悪の場合において多項式である逐次一貫性の下で,マルチスレッドプログラムを解析するための最適DPORアルゴリズムである。 POPはいくつかの新しいアルゴリズム技術を組み合わせる (i)同じ人種の複数の逆転を避ける擬似的な人種逆転戦略。 (二 探索した実行の最初の断片の保存を避けるための熱狂的な競争逆転戦略、及び 三 余剰探査の防止のための空間効率のよいスキームで、睡眠セットの使用を代替する。 我々のNidhuggの実装は、これらの手法が並列プログラムの解析を著しく高速化し、メモリ消費を抑えられることを示している。 グラフとして実行を表現した関連するDPORアルゴリズムであるTruStと比較すると、POPの実装はより小さなベンチマークで同様のパフォーマンスを実現し、長時間実行したプログラム上でのTruStのスケールよりもはるかに優れている。

関連論文リスト

• 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)

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

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