論文の概要: Verify Linearizability of Concurrent Stacks

• arxiv url: http://arxiv.org/abs/2110.05801v3
• Date: Mon, 15 Sep 2025 08:26:10 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-09-16 17:26:22.548296
• Title: Verify Linearizability of Concurrent Stacks
• Title（参考訳）: 並行スタックの線形化可能性検証
• Authors: Tangliu Wen,
• Abstract要約: 並列スタックの線形化性を検証するための新しい証明手法を提案する。 まず,並列スタックにおける共通最適化である除去機構の健全性を証明する。 次に,一組の条件を確立するために線形化可能性を証明する問題を小さくするスタック定理を提案する。
• 参考スコア（独自算出の注目度）: 0.0
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Proving linearizability of concurrent data structures is crucial for ensuring their correctness, but is challenging especially for implementations that employ sophisticated synchronization techniques. In this paper, we propose a new proof technique for verifying linearizability of concurrent stacks. We first prove the soundness of the elimination mechanism, a common optimization used in concurrent stacks, which enables simplifying the linearizability proofs. We then present a stack theorem that reduces the problem of proving linearizability to establishing a set of conditions based on the happened-before order of operations. The key idea is to use an extended partial order to capture when a pop operation can observe the effect of a push operation. We apply our proof technique to verify two concurrent stack algorithms: the Treiber stack and the Time-Stamped stack, demonstrating its practicality. Our approach provides a systematic and compositional way to prove linearizability of concurrent stacks.
• Abstract（参考訳）: 並列データ構造の線形化性を証明することは、その正確性を保証するために重要であるが、特に高度な同期技術を用いた実装では困難である。 本稿では,並列スタックの線形化性を検証するための新しい証明手法を提案する。 まず,並列スタックにおける共通最適化である除去機構の健全性を証明し,線形化可能性証明の簡略化を実現する。 そこで我々は, 線形化可能性の証明問題を減らし, 発生前の操作順序に基づく条件セットを確立するスタック定理を提案する。 鍵となるアイデアは、あるポップ操作がプッシュ操作の効果を観測できるときに、拡張された部分順序を使ってキャプチャすることである。 本稿では,TreiberスタックとTime-Stampedスタックの2つの並列スタックアルゴリズムを検証し,その実用性を実証する。 我々の手法は並列スタックの線形化可能性を証明する体系的で構成的な方法を提供する。

関連論文リスト

• Reasoning by Superposition: A Theoretical Perspective on Chain of Continuous Thought [56.71873693264532]
  連続CoTのD$ステップを持つ2層トランスが有向グラフ到達可能性問題を解くことができることを証明した。 我々の構成では、各連続思考ベクトルは複数の探索フロンティアを同時に符号化する重ね合わせ状態である。
  論文  参考訳（メタデータ） (2025-05-18T18:36:53Z)
• Test-time Correlation Alignment [2.389598109913754]
  テスト時間適応(TTA)は、ラベルのないテストデータのみを使用して適応する。 テスト時間相関アライメント(TCA)は、理論的保証でテスト性能を向上させることができる。 LinearTCAは、追加のモデル更新なしでインスタンスと相関アライメントの両方を達成するために、単純な線形変換を適用します。 LinearTCA+は、既存のTTAメソッドを簡単に強化できるプラグイン・アンド・プレイモジュールとして機能する。
  論文  参考訳（メタデータ） (2025-05-01T13:59:13Z)
• MathGAP: Out-of-Distribution Evaluation on Problems with Arbitrarily Complex Proofs [80.96119560172224]
  MathGAPは、それらの算術的証明構造に関する仕様に従って、問題文と連鎖推論トレースを生成する。 MathGAP を用いて, LLM はより深く, より広くなるにつれて, 性能が著しく低下することがわかった。
  論文  参考訳（メタデータ） (2024-10-17T12:48:14Z)
• TSVD: Bridging Theory and Practice in Continual Learning with Pre-trained Models [103.45785408116146]
  連続学習(CL)は、連続的に提示される複数のタスクを解決できるモデルを訓練することを目的としている。 最近のCLアプローチは、ダウンストリームタスクをうまく一般化する大規模な事前学習モデルを活用することで、強力なパフォーマンスを実現している。 しかし、これらの手法には理論的保証がなく、予期せぬ失敗をしがちである。 理論的に健全で高性能な単純なCL法を設計することで,このギャップを埋めることを目指している。
  論文  参考訳（メタデータ） (2024-10-01T12:58:37Z)
• Simple Ingredients for Offline Reinforcement Learning [86.1988266277766]
  オフライン強化学習アルゴリズムは、ターゲット下流タスクに高度に接続されたデータセットに有効であることが証明された。 既存の手法が多様なデータと競合することを示す。その性能は、関連するデータ収集によって著しく悪化するが、オフラインバッファに異なるタスクを追加するだけでよい。 アルゴリズム的な考慮以上のスケールが、パフォーマンスに影響を及ぼす重要な要因であることを示す。
  論文  参考訳（メタデータ） (2024-03-19T18:57:53Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• On the Robustness of Randomized Ensembles to Adversarial Perturbations [12.082239973914326]
  ランダム化アンサンブル分類器(REC)は従来のアンサンブル法に代わる魅力的な代替品として登場した。 近年の研究では、RECを構築するための既存の手法が、当初主張されていたよりも脆弱であることが示されている。 本稿では,ロバストなRECをトレーニングするための新しいブースティングアルゴリズム(BARRE)を提案する。
  論文  参考訳（メタデータ） (2023-02-02T19:17:34Z)
• CD Tools -- Condensed Detachment and Structure Generating Theorem Proving (System Description) [0.0]
  CD Toolsは、一階ATPの凝縮した剥離の実験のためのPrologライブラリである。 一階ATPの観点からすると、凝縮した分枝は比較的単純だが本質的な特徴と真剣な応用を持つ設定を提供する。 ATPでよく研究される歴史的な問題のために、既知のものよりもはるかに短い新しい証明を生み出した。
  論文  参考訳（メタデータ） (2022-07-18T09:15:08Z)
• Don't Explain Noise: Robust Counterfactuals for Randomized Ensembles [50.81061839052459]
  我々は確率論的問題として、堅牢な対実的説明の生成を定式化する。 アンサンブルモデルのロバスト性とベース学習者のロバスト性との関係を示す。 本手法は, 反実的説明から初期観測までの距離をわずかに増加させるだけで, 高いロバスト性を実現する。
  論文  参考訳（メタデータ） (2022-05-27T17:28:54Z)
• Recursive Causal Structure Learning in the Presence of Latent Variables and Selection Bias [27.06618125828978]
  本稿では,潜伏変数と選択バイアスの存在下での観測データからシステムの因果MAGを学習する問題を考察する。 本稿では,音と完全性を備えた計算効率のよい制約ベースの新しい手法を提案する。 提案手法と人工と実世界の両方の構造に関する技術の現状を比較した実験結果を提供する。
  論文  参考訳（メタデータ） (2021-10-22T19:49:59Z)
• An Efficient Diagnosis Algorithm for Inconsistent Constraint Sets [68.8204255655161]
  過制約問題における最小限の障害制約を識別する分割・分散型診断アルゴリズム(FastDiag)を提案する。 ヒットセットの競合指向計算とfastdiagを比較し,詳細な性能解析を行う。
  論文  参考訳（メタデータ） (2021-02-17T19:55:42Z)
• Efficient Generation of Structured Objects with Constrained Adversarial Networks [25.74932947671932]
  GAN(Generative Adversarial Networks)は、分子やゲームマップのような構造化オブジェクトを生成するのに苦労する。 本稿では,モデルに制約を埋め込んだGANの拡張であるConstrained Adversarial Networks (CANs)を提案する。 CANは(高い確率で)有効構造の効率的な推論をサポートし、推論時に学習した制約をオン/オフすることができる。
  論文  参考訳（メタデータ） (2020-07-26T19:04:37Z)
• Refined bounds for algorithm configuration: The knife-edge of dual class approximability [94.83809668933021]
  トレーニングセットが、トレーニングセット上でのパラメータの平均メトリックのパフォーマンスが、予想される将来的なパフォーマンスに最も近いことを保証するために、どの程度の規模が必要かを調査する。 この近似が L-無限ノルムの下で成り立つなら、強いサンプル複雑性境界を与えることができる。 我々は、コンピュータ科学において最も強力なツールの一つである整数プログラミングの文脈において、我々の限界を実証的に評価する。
  論文  参考訳（メタデータ） (2020-06-21T15:32:21Z)
• POINTER: Constrained Progressive Text Generation via Insertion-based Generative Pre-training [93.79766670391618]
  ハードコントラストテキスト生成のための新しい挿入ベースアプローチであるPOINTERを提案する。 提案手法は,既存のトークン間で段階的に新しいトークンを並列に挿入することによって動作する。 結果として生じる粗大な階層構造は、生成プロセスを直感的で解釈可能である。
  論文  参考訳（メタデータ） (2020-05-01T18:11:54Z)

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

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