論文の概要: Efficient Decrease-and-Conquer Linearizability Monitoring

• arxiv url: http://arxiv.org/abs/2410.04581v5
• Date: Mon, 25 Aug 2025 10:38:06 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-28 15:30:14.320135
• Title: Efficient Decrease-and-Conquer Linearizability Monitoring
• Title（参考訳）: 効率のよいデフレ・アンド・コンカウンタリライナライザビリティモニタリング
• Authors: Lee Zheng Han, Umang Mathur,
• Abstract要約: リニアライザビリティは、並列データ構造の実装における事実上の正当性仕様となっている。 本研究では,リニアライザビリティモニタリングについて検討し,実装の実行履歴がリニアライザビリティであるかどうかを確認する。 本稿では,線形化可能性監視のための一貫した減少・縮小型アルゴリズムフレームワークを提案する。
• 参考スコア（独自算出の注目度）: 0.9654084121255876
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Linearizability has become the de facto correctness specification for implementations of concurrent data structures. While formally verifying such implementations remains challenging, linearizability monitoring has emerged as a promising first step to rule out early problems in the development of custom implementations, and serves as a key component in approaches that stress test such implementations. In this work, we investigate linearizability monitoring -- check if an execution history of an implementation is linearizable. While this problem is intractable in general, a systematic understanding of when it becomes tractable has remained elusive. We revisit this problem and first present a unified `decrease-and-conquer' algorithmic framework for linearizability monitoring. At its heart, this framework asks to identify special linearizability-preserving values in a given history -- values whose presence yields an equilinearizable sub-history when removed, and whose absence indicates non-linearizability. We prove that a polynomial time algorithm for the problem of identifying linearizability-preserving values, yields a polynomial time algorithm for linearizability monitoring, while conversely, intractability of this problem implies intractability of the monitoring problem. We demonstrate our framework's effectiveness by instantiating it for several popular data types -- sets, stacks, queues and priority queues -- deriving polynomial time algorithms for each, with the unambiguity restriction, where each insertion to the underlying data structure adds a distinct value. We optimize these algorithms to achieve the optimal log-linear time complexity by amortizing the cost of solving sub-problems through efficient data structures. Our implementation and evaluation on publicly available implementations show that our approach scales to large histories and outperforms existing tools.
• Abstract（参考訳）: リニアライザビリティは、並列データ構造の実装における事実上の正当性仕様となっている。 このような実装を公式に検証することは依然として難しいが、リニアライザビリティ監視は、カスタム実装の開発における早期の問題を排除し、そのような実装をテストするアプローチにおいて重要なコンポーネントとして機能する、有望な第一歩として登場した。 本研究では,リニアライザビリティモニタリングについて検討し,実装の実行履歴がリニアライザビリティであるかどうかを確認する。 この問題は一般には難解であるが、いつ難解になるかという体系的な理解はいまだ解明されていない。 この問題を再考し、まず線形化可能性監視のための統合された'decrease-and-conquer'アルゴリズムフレームワークを提案する。 この枠組みの核心は、与えられた歴史の中で特別な線形化可能性保存値(英語版)を同定することであり、その存在が除去されたときに同値なサブヒストリーをもたらし、非線型化可能性を示す。 線形化可能性保存問題の多項式時間アルゴリズムは、線形化可能性監視のための多項式時間アルゴリズムを導出するが、逆に、この問題の難易度はモニタリング問題の難易度を意味する。 いくつかの一般的なデータ型 -- セット,スタック,キュー,優先度待ち行列 -- に対してインスタンス化を行うことで,フレームワークの有効性を実証する。 我々はこれらのアルゴリズムを最適化し、効率的なデータ構造を通してサブプロブレムを解くコストを減らし、最適な対数線形時間複雑性を実現する。 公開実装の実装と評価は、我々のアプローチが大規模な履歴にスケールし、既存のツールより優れていることを示している。

関連論文リスト

• Learning to optimize with guarantees: a complete characterization of linearly convergent algorithms [1.4747234049753448]
  高度な工学的応用では、最適化アルゴリズムは数学的に定義された問題のクラスよりも証明可能な証明可能なケースを保証する必要がある。 非滑らかな合成最適化問題のクラスに対して線形収束を実現するアルゴリズムのクラスを記述する。
  論文  参考訳（メタデータ） (2025-08-01T16:56:42Z)
• Efficient Causal Discovery for Autoregressive Time Series [0.0]
  提案アルゴリズムは,既存の手法に比べて計算複雑性を著しく低減し,より大きな問題に対してより効率的かつスケーラブルにする。 我々は合成データセットの性能を厳格に評価し、我々のアルゴリズムが現在の技術を上回るだけでなく、限られたデータ可用性のシナリオでも優れていることを示した。
  論文  参考訳（メタデータ） (2025-07-10T16:27:33Z)
• Short-Long Convolutions Help Hardware-Efficient Linear Attention to Focus on Long Sequences [60.489682735061415]
  本稿では,状態空間モデルを短時間の畳み込みに置き換えたCHELAを提案する。 提案手法の有効性を示すために,Long Range Arenaベンチマークと言語モデリングタスクについて実験を行った。
  論文  参考訳（メタデータ） (2024-06-12T12:12:38Z)
• Iteratively Refined Behavior Regularization for Offline Reinforcement Learning [57.10922880400715]
  本稿では,保守的政策反復に基づく行動規則化を大幅に強化する新しいアルゴリズムを提案する。 行動規則化に使用される基準ポリシーを反復的に洗練することにより、保守的な政策更新は徐々に改善される。 D4RLベンチマークの実験結果から,本手法は従来のタスクのベースラインよりも優れていたことが示唆された。
  論文  参考訳（メタデータ） (2023-06-09T07:46:24Z)
• Unsupervised Automata Learning via Discrete Optimization [4.5726613073750135]
  与えられたラベルなし単語の多元集合から決定論的有限オートマトン(DFA)を学習するためのフレームワークを提案する。 この問題は計算的に困難であることが示され,制約最適化に基づく3つの学習アルゴリズムが開発された。 DFAの全体的な解釈性を改善するため,最適化問題に対する新たな正規化手法を導入する。
  論文  参考訳（メタデータ） (2023-03-24T16:19:15Z)
• Offline Policy Optimization with Eligible Actions [34.4530766779594]
  オフラインポリシーの最適化は多くの現実世界の意思決定問題に大きな影響を与える可能性がある。 重要度サンプリングとその変種は、オフラインポリシー評価において一般的に使用されるタイプの推定器である。 そこで本稿では, 州ごとの正規化制約によって過度に適合することを避けるアルゴリズムを提案する。
  論文  参考訳（メタデータ） (2022-07-01T19:18:15Z)
• Stabilizing Q-learning with Linear Architectures for Provably Efficient Learning [53.17258888552998]
  本研究では,線形関数近似を用いた基本的な$Q$-learningプロトコルの探索変種を提案する。 このアルゴリズムの性能は,新しい近似誤差というより寛容な概念の下で,非常に優雅に低下することを示す。
  論文  参考訳（メタデータ） (2022-06-01T23:26:51Z)
• Instance-Dependent Confidence and Early Stopping for Reinforcement Learning [99.57168572237421]
  強化学習(RL)のための様々なアルゴリズムは、その収束率の劇的な変動を問題構造の関数として示している。 この研究は、観察されたパフォーマンスの違いについて、textitexを説明する保証を提供する。 次の自然なステップは、これらの理論的保証を実際に有用なガイドラインに変換することです。
  論文  参考訳（メタデータ） (2022-01-21T04:25:35Z)
• Dealing With Misspecification In Fixed-Confidence Linear Top-m Identification [0.0]
  固定誤差率$delta$(固定信頼度Top-m識別)の下で最大の手段を持つmアームの識別問題について検討する。 この問題は、特に医療やレコメンデーションシステムにおける実践的な応用によって動機付けられている。
  論文  参考訳（メタデータ） (2021-11-02T10:27:17Z)
• Sparse PCA via $l_{2,p}$-Norm Regularization for Unsupervised Feature Selection [138.97647716793333]
  再構成誤差を$l_2,p$ノルム正規化と組み合わせることで,単純かつ効率的な特徴選択手法を提案する。 提案する非教師付きモデルを解くための効率的な最適化アルゴリズムを提案し,アルゴリズムの収束と計算の複雑さを理論的に解析する。
  論文  参考訳（メタデータ） (2020-12-29T04:08:38Z)

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

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