論文の概要: Trace Validation of Unmodified Concurrent Systems with OmniLink
- arxiv url: http://arxiv.org/abs/2601.11836v1
- Date: Fri, 16 Jan 2026 23:51:31 GMT
- ステータス: 情報取得中
- システム内更新日: 2026-01-21 12:51:02.617909
- Title: Trace Validation of Unmodified Concurrent Systems with OmniLink
- Title（参考訳）: OmniLinkを用いた無修正並行系のトレース検証
- Authors: Finn Hackett, Evan Wrench, Peter Macko, A. Jesse Jiryu Davis, Yuanhao Wei, Ivan Beschastnikh,
- Abstract要約: 我々は,TLA+の高レベル仕様に対して並列実装を検証するための新しい方法論であるOmniLinkを提案する。
トレースバリデーションと呼ばれるテクニックを使った従来のTLA+ベースのアプローチとは異なり、OmniLinkはシステムイベントを、発生したタイムボックスとTLA+の意味を持ったブラックボックスとして扱う。
我々は、WiredTigerの既存のTLA+モデルを改善するためにOmniLinkを使用し、非線形な振る舞いを含むモデル化されたシステムの振舞いに密接に適合する新しいTLA+モデルを開発した。
- 参考スコア（独自算出の注目度）: 2.930914222575954
- License:
- Abstract: Concurrent systems are notoriously difficult to validate: subtle bugs may only manifest under rare thread interleavings, and existing tools often require intrusive instrumentation or unrealistic execution models. We present OmniLink, a new methodology for validating concurrent implementations against high-level specifications in TLA+. Unlike prior TLA+ based approaches which use a technique called trace validation, OmniLink treats system events as black boxes with a timebox in which they occurred and a meaning in TLA+, solving for a logical total order of actions. Unlike prior approaches based on linearizability checking, which already solves for total orders of actions with timeboxes, OmniLink uses a flexible specification language, and offers a different linearizability checking method based on off-the-shelf model checking. OmniLink offers different features compared existing linearizability checking tools, and we show that it outperforms the state of the art on large scale validation tasks. Our evaluation validates WiredTiger, a state-of-the-art industrial database storage layer, as well as Balanced Augmented Tree (BAT), a state-of-the art lock-free data structure from the research community, and ConcurrentQueue, a popular lock-free queue featuring aggressive performance optimizations. We use OmniLink to improve WiredTiger's existing TLA+ model, as well as develop new TLA+ models that closely match the behavior of the modeled systems, including non-linearizable behaviors. OmniLink is able to find known bugs injected into the systems under test, as well as help discover two previously unknown bugs (1 in BAT, 1 in ConcurrentQueue), which we have confirmed with the authors of those systems.
- Abstract（参考訳）: 微妙なバグは希少なスレッドインターリーブの下でのみ発生し、既存のツールは侵入的なインスツルメンテーションや非現実的な実行モデルを必要とすることが多い。
我々は,TLA+の高レベル仕様に対して並列実装を検証するための新しい方法論であるOmniLinkを提案する。
トレースバリデーションと呼ばれるテクニックを使った従来のTLA+ベースのアプローチとは異なり、OmniLinkはシステムイベントをブラックボックスとして扱う。
従来のリニアライザビリティチェックに基づくアプローチとは異なり、OmniLinkはフレキシブルな仕様言語を使用しており、既製のモデルチェックに基づいて異なるリニアライザビリティチェック方法を提供している。
OmniLinkは、既存の線形化可能性チェックツールと比較して異なる機能を提供しており、大規模検証タスクにおける最先端のタスクよりも優れていることを示す。
我々は、最先端産業データベースストレージ層であるWiredTigerと、研究コミュニティの最先端のロックフリーデータ構造であるBa balanced Augmented Tree(BAT)と、積極的なパフォーマンス最適化を特徴とする一般的なロックフリーキューであるConcurrentQueueを評価した。
我々は、WiredTigerの既存のTLA+モデルを改善するためにOmniLinkを使用し、非線形な振る舞いを含むモデル化されたシステムの振舞いに密接に適合する新しいTLA+モデルを開発した。
OmniLinkは、テスト中のシステムに注入された既知のバグを見つけるだけでなく、2つの既知のバグ(BATでは1つ、ConcurrentQueueでは1つ)を発見するのにも役立ちます。
関連論文リスト
- DRIFT: Dynamic Rule-Based Defense with Injection Isolation for Securing LLM Agents [52.92354372596197]
大規模言語モデル(LLM)は、強力な推論と計画能力のため、エージェントシステムの中心となってきています。
この相互作用は、外部ソースからの悪意のある入力がエージェントの振る舞いを誤解させる可能性がある、インジェクション攻撃のリスクも引き起こす。
本稿では,信頼に値するエージェントシステムのための動的ルールベースの分離フレームワークを提案する。
論文 参考訳（メタデータ） (2025-06-13T05:01:09Z) - Auditing Black-Box LLM APIs with a Rank-Based Uniformity Test [24.393978712663618]
APIプロバイダは、コスト削減やモデル動作の不正な変更のために、量子化または微調整の亜種を慎重に提供することができる。
そこで我々は,ブラックボックスLLMの挙動等式を局所的に展開した認証モデルに検証できるランクベース均一性試験を提案する。
我々は、量子化、有害な微調整、脱獄プロンプト、完全なモデル置換など、さまざまな脅威シナリオに対するアプローチを評価する。
論文 参考訳（メタデータ） (2025-06-08T03:00:31Z) - Beyond 'Aha!': Toward Systematic Meta-Abilities Alignment in Large Reasoning Models [86.88657425848547]
大型推論モデル(LRMs)はすでに長い連鎖推論のための潜在能力を持っている。
我々は、自動生成の自己検証タスクを使用して、モデルに推論、帰納、誘拐の3つのメタ能力を持たせることを明確にした。
我々の3つのステージ・パイプラインの個別アライメント、パラメータ空間のマージ、ドメイン固有の強化学習は、命令調整ベースラインと比較して10%以上のパフォーマンス向上を実現します。
論文 参考訳（メタデータ） (2025-05-15T17:58:33Z) - CAMELTrack: Context-Aware Multi-cue ExpLoitation for Online Multi-Object Tracking [68.24998698508344]
CAMELはコンテキスト対応型マルチキューExpLoitationのための新しいアソシエイトモジュールである。
エンド・ツー・エンドの検知・バイ・トラック方式とは異なり,本手法は軽量かつ高速にトレーニングが可能であり,外部のオフ・ザ・シェルフモデルを活用することができる。
提案するオンライントラッキングパイプラインであるCAMELTrackは,複数のトラッキングベンチマークで最先端のパフォーマンスを実現する。
論文 参考訳（メタデータ） (2025-05-02T13:26:23Z) - LTL Verification of Memoryful Neural Agents [16.353043979615496]
本稿では,LTL(Linear Temporal Logic)仕様に対して,MN-MAS(Memoryful Neural Multi-Agent Systems)を検証するためのフレームワークを提案する。
MN-MASの例としては、フィードフォワードとリカレントニューラルネットワークに基づくマルチエージェントシステムや状態空間モデルがある。
論文 参考訳（メタデータ） (2025-03-04T11:20:19Z) - Joint Feature Learning and Relation Modeling for Tracking: A One-Stream
Framework [76.70603443624012]
特徴学習と関係モデリングを統合した新しい一ストリーム追跡(OSTrack)フレームワークを提案する。
このようにして、相互誘導により識別的目標指向特徴を動的に抽出することができる。
OSTrackは、複数のベンチマークで最先端のパフォーマンスを実現しており、特に、ワンショットトラッキングベンチマークのGOT-10kでは印象的な結果を示している。
論文 参考訳（メタデータ） (2022-03-22T18:37:11Z) - Policy Analysis using Synthetic Controls in Continuous-Time [101.35070661471124]
因果推論における手法開発において, 合成制御を用いた因果推定は最も成功した手法の1つである。
本稿では,制御された微分方程式の定式化を明示的に用い,潜在反事実経路をモデル化する連続時間代替法を提案する。
論文 参考訳（メタデータ） (2021-02-02T16:07:39Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。