Fugu-MT 論文翻訳(概要): A Simple Way to Verify Linearizability of Concurrent Stacks

論文の概要: A Simple Way to Verify Linearizability of Concurrent Stacks

arxiv url: http://arxiv.org/abs/2110.05801v2
Date: Tue, 9 Jul 2024 11:48:00 GMT
ステータス: 処理完了
システム内更新日: 2024-07-11 00:57:55.825646
Title: A Simple Way to Verify Linearizability of Concurrent Stacks
Title（参考訳）: 並列スタックの線形化可能性の簡易検証法
Authors: Tangliu Wen,
Abstract要約: 並列スタックの線形化可能性を検証するための,単純かつ完全な証明手法を提案する。本手法は,並列スタックの線形化性を,条件セットの確立に還元する。並列データ構造のデザイナは,証明技術の使用を容易かつ迅速に学ぶことができる。
参考スコア（独自算出の注目度）: 0.0
License: http://creativecommons.org/licenses/by/4.0/
Abstract: Linearizability is a commonly accepted correctness criterion for concurrent data structures. However, verifying linearizability of highly concurrent data structures is still a challenging task. In this paper, we present a simple and complete proof technique for verifying linearizability of concurrent stacks. Our proof technique reduces linearizability of concurrent stacks to establishing a set of conditions. These conditions are based on the happened-before order of operations, intuitively express the LIFO semantics and can be proved by simple arguments. Designers of concurrent data structures can easily and quickly learn to use the proof technique. We have successfully applied the method to several challenging concurrent stacks: the TS stack, the HSY stack, and the FA stack, etc.
Abstract（参考訳）: リニアライザビリティ(Linearizability)は、並列データ構造に対する一般的な正当性基準である。しかし、高度に並列したデータ構造の線形化性を検証することは依然として難しい課題である。本稿では,並列スタックの線形化可能性を検証するための,単純かつ完全な証明手法を提案する。本手法は,並列スタックの線形化性を,条件セットの確立に還元する。これらの条件は、LIFOセマンティクスを直感的に表現し、単純な議論によって証明できる操作の偶然の順序に基づいている。並列データ構造のデザイナは,証明技術の使用を容易かつ迅速に学ぶことができる。我々は、TSスタック、HSYスタック、FAスタックなど、いくつかの挑戦的な並行スタックに対して、このメソッドをうまく適用しました。

関連論文リスト

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)

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