論文の概要: 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つの並列スタックアルゴリズムを検証し,その実用性を実証する。 我々の手法は並列スタックの線形化可能性を証明する体系的で構成的な方法を提供する。

関連論文リスト

• FlashEvaluator: Expanding Search Space with Parallel Evaluation [27.839033452409428]
  我々は,全シーケンスを1つのフォワードパスで処理し,クロスシーケンストークンの情報共有を可能にするFlashEvaluatorを提案する。 これにより、システムの効率を向上し、シーケンス間直接比較をサポートするサブ線形計算複雑性が得られる。 FlashEvaluatorは、Kuaishouのオンラインレコメンデーションシステムにデプロイされ、実質的で持続的な収益を実際に提供してきた。
  論文  参考訳（メタデータ） (2026-03-03T03:35:34Z)
• PRISM: Parallel Residual Iterative Sequence Model [52.26239951489612]
  我々はこの緊張を解決するためにPRISM(Parallel Residual Iterative Sequence Model)を提案する。 PRISMは、パラレル化可能な形で多段階精製の重要な構造特性を捉える、ソルバに着想を得た帰納バイアスを導入している。 この定式化が Rank-$L$ の蓄積を達成することを証明し、更新多様体を単一ステップの Rank-$1$ ボトルネックを超えて構造的に拡張する。
  論文  参考訳（メタデータ） (2026-02-11T12:39:41Z)
• Fractional Reasoning via Latent Steering Vectors Improves Inference Time Compute [60.151643048803145]
  本稿では,推論時の推論強度を連続的に制御するフレームワークであるフラクショナル推論を提案する。 提案手法は, より深い推論を伴う潜在ステアリングベクトルを抽出し, 調整可能なスケーリング係数で再適用することによって機能する。 GSM8K、MATH500、GPQAの実験により、フラクショナル推論は様々な推論タスクやモデルのパフォーマンスを一貫して改善することを示した。
  論文  参考訳（メタデータ） (2025-06-18T21:15:59Z)
• Scaling Probabilistic Circuits via Monarch Matrices [109.65822339230853]
  確率回路(PC)は確率分布の抽出可能な表現である。 そこで本研究では,PCの和ブロックに対する新しいスパースパラメータと構造化パラメータ化を提案する。
  論文  参考訳（メタデータ） (2025-06-14T07:39:15Z)
• 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)
• Towards Transformer-Based Aligned Generation with Self-Coherence Guidance [51.42269790543461]
  トランスフォーマーを用いたテキストガイド拡散モデル(TGDM)におけるアライメント向上のためのトレーニング不要アプローチを提案する。 既存のTGDMは、特に複雑なテキストプロンプトやマルチコンセプト属性バインディングの問題を扱う場合、意味的に整合した画像を生成するのに苦労することが多い。 本手法は,生成過程において,相互注意マップを直接最適化することにより,これらの課題に対処する。
  論文  参考訳（メタデータ） (2025-03-22T07:03:57Z)
• 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)
• Stable Nonconvex-Nonconcave Training via Linear Interpolation [51.668052890249726]
  本稿では,ニューラルネットワークトレーニングを安定化(大規模)するための原理的手法として,線形アヘッドの理論解析を提案する。 最適化過程の不安定性は、しばしば損失ランドスケープの非単調性によって引き起こされるものであり、非拡張作用素の理論を活用することによって線型性がいかに役立つかを示す。
  論文  参考訳（メタデータ） (2023-10-20T12:45:12Z)
• Tractable Bounding of Counterfactual Queries by Knowledge Compilation [51.47174989680976]
  本稿では, パール構造因果モデルにおいて, 因果関係などの部分的特定可能なクエリのバウンダリングの問題について議論する。 最近提案された反復EMスキームは初期化パラメータをサンプリングしてそれらの境界を内部近似する。 シンボルパラメータを実際の値に置き換えた回路構造を,単一のシンボル知識コンパイルによって得られることを示す。
  論文  参考訳（メタデータ） (2023-10-05T07:10:40Z)
• Range-Restricted Interpolation through Clausal Tableaux [0.0]
  一階述語論理の入力からクレイグの出力へ、範囲制限とホーン特性の変動がどのように受け継がれるかを示す。 証明システムは、一階ATPに由来するクラウスアル・タドーである。
  論文  参考訳（メタデータ） (2023-06-06T10:42:40Z)
• Forward LTLf Synthesis: DPLL At Work [1.370633147306388]
  有限トレース(LTLf)上での線形時間論理の合成のための新しいAND-ORグラフ探索フレームワークを提案する。 このようなフレームワーク内では、Davis-Putnam-Logemann-Loveland (DPLL)アルゴリズムにインスパイアされたプロシージャを考案し、次に利用可能なエージェント環境の動きを生成する。 また,状態公式の構文的等価性に基づく探索ノードの等価性チェックも提案する。
  論文  参考訳（メタデータ） (2023-02-27T14:33:50Z)
• 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)
• Online Matching in Sparse Random Graphs: Non-Asymptotic Performances of Greedy Algorithm [20.582965700659788]
  我々は、最も単純なアルゴリズムであるGREEDYの競合比を、関連する離散過程を連続的に近似することによって推定する。 驚くべきことに、GREEDYは、オンラインマッチングのためのもう1つの有名なアルゴリズムであるRANKINGよりも優れたパフォーマンスを保証することができる。
  論文  参考訳（メタデータ） (2021-07-02T12:18:19Z)
• 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)
• Lagrangian Decomposition for Neural Network Verification [148.0448557991349]
  ニューラルネットワーク検証の基本的なコンポーネントは、出力が取ることのできる値のバウンダリの計算である。 ラグランジアン分解に基づく新しい手法を提案する。 ランニングタイムのごく一部で、既成の解法に匹敵するバウンダリが得られることを示す。
  論文  参考訳（メタデータ） (2020-02-24T17:55:10Z)

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

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