論文の概要: VeriFix: Verifying Your Fix Towards An Atomicity Violation

• arxiv url: http://arxiv.org/abs/2504.16354v1
• Date: Wed, 23 Apr 2025 02:11:07 GMT
• ステータス: 翻訳完了
• システム内更新日: 2025-05-02 19:15:52.971929
• Title: VeriFix: Verifying Your Fix Towards An Atomicity Violation
• Title（参考訳）: VeriFix: 原子度違反に対する修正の検証
• Authors: Zhuang Li, Qiuping Yi, Jeff Huang,
• Abstract要約: 本稿では,原子性欠陥の修正を検証するための新しいアプローチであるtextsfVeriFixを提案する。 アトミック性違反とそれに対応する修正を公開するバギートレースが与えられたとき、textsfVeriFixは、新しいデッドロックを導入することなく、修正がアトミック性違反を修正するのに十分な同期を導入するかどうかを効果的に検証する。
• 参考スコア（独自算出の注目度）: 21.957127966452664
• License: http://creativecommons.org/licenses/by/4.0/
• Abstract: Atomicity violation is one of the most serious types of bugs in concurrent programs. Synchronizations are commonly used to enforce atomicity. However, it is very challenging to place synchronizations correctly and sufficiently due to complex thread interactions and large input space. This paper presents \textsf{VeriFix}, a new approach for verifying atomicity violation fixes. Given a buggy trace that exposes an atomicity violation and a corresponding fix, % in the form of locks, \textsf{VeriFix} effectively verifies if the fix introduces sufficient synchronizations to repair the atomicity violation without introducing new deadlocks. The key idea is that \textsf{VeriFix} transforms the fix verification problem into a property verification problem, in which both the observed atomicity violation and potential deadlocks are encoded as a safety property, and both the inputs and schedules are encoded as symbolic constraints. By reasoning the conjoined constraints with an SMT solver, \textsf{VeriFix} systematically explores all reachable paths %from the whole schedule and input space and verifies if there exists a concrete \textit{schedule+input} combination to manifest the intended atomicity or any new deadlocks. We have implemented and evaluated \verifix\ on a collection of real-world C/C++ programs. The result shows that \textsf{VeriFix} significantly outperforms the state-of-the-art.
• Abstract（参考訳）: アトミック性違反は、並列プログラムにおける最も深刻なバグの1つです。 シンクロナイゼーションは一般に原子性の強制に使用される。 しかし、複雑なスレッド相互作用と大きな入力空間のため、同期を正しく十分に配置することは極めて困難である。 本稿では、原子性欠陥の修正を検証するための新しいアプローチである「textsf{VeriFix}」を提案する。 アトミック性違反とそれに対応する修正を露呈するバギートレースがロックの形で%となると、 \textsf{VeriFix} は、新しいデッドロックを導入することなく、修正がアトミック性違反を修正するのに十分な同期を導入するかどうかを効果的に検証する。 鍵となる考え方は、 \textsf{VeriFix} が固定検証問題をプロパティ検証問題に変換し、観察された原子性違反と潜在的なデッドロックの両方を安全特性として符号化し、入力とスケジュールの両方を象徴的制約として符号化する。 SMTソルバと結合した制約を推論することにより、 \textsf{VeriFix} はスケジュールと入力空間全体から % の到達可能なすべてのパスを体系的に探索し、意図した原子性や新しいデッドロックを示す具体的な \textit{schedule+input} 組み合わせが存在するかどうかを検証する。 我々は,現実世界のC/C++プログラムのコレクション上に \verifix\ を実装し,評価した。 その結果、 \textsf{VeriFix} は最先端よりも大幅に優れていた。

関連論文リスト

• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [63.23120252801889]
  CRUST-Benchは100のCリポジトリのデータセットで、それぞれが安全なRustとテストケースで手書きのインターフェースとペアリングされている。 我々は、このタスクで最先端の大規模言語モデル(LLM)を評価し、安全で慣用的なRust生成が依然として難しい問題であることを確認した。 最高のパフォーマンスモデルであるOpenAI o1は、ワンショット設定で15タスクしか解決できない。
  論文  参考訳（メタデータ） (2025-04-21T17:33:33Z)
• Tuning-Free Image Editing with Fidelity and Editability via Unified Latent Diffusion Model [60.82962950960996]
  拡散遅延最適化を行うチューニング不要なUnifyEditを導入する。 本研究では, 自己注意保持制約(SA)と相互注意アライメント制約(CA)の2つを開発し, テキストアライメントの強化を図る。 提案手法は,様々な編集作業における構造保存とテキストアライメントのバランスを保ち,他の最先端手法よりも優れている。
  論文  参考訳（メタデータ） (2025-04-08T01:02:50Z)
• Automated detection of atomicity violations in large-scale systems [5.652514080341844]
  我々は,大規模言語モデル (LLM) エージェントと静的解析を統合し,実世界のプログラムにおける原子性違反を検出するフレームワークであるCloverを提案する。 Cloverは92.3%/86.6%の精度/リコールを達成した。
  論文  参考訳（メタデータ） (2025-04-01T08:13:29Z)
• Atom of Thoughts for Markov LLM Test-Time Scaling [18.288669306091155]
  大規模言語モデル(LLM)は、トレーニング時間スケーリングによって優れたパフォーマンスを達成する。 推論の規模が大きくなるにつれて、既存のテストタイムスケーリング手法は、蓄積した履歴情報に悩まされる。 複雑な推論は、独立して自己完結した一連のサブクエストを解くことで達成できる。
  論文  参考訳（メタデータ） (2025-02-17T16:52:42Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
  本稿では,帰属可能なテキスト生成における事実の不整合をローカライズするための新しい形式であるQASemConsistencyを紹介する。 まず,人間のアノテーションに対するQASemConsistency法の有効性を示す。 そこで我々は,局所的な事実の不整合を自動的に検出するいくつかの手法を実装した。
  論文  参考訳（メタデータ） (2024-10-09T22:53:48Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  投機的意味論に基づくコンパイラ変換における非干渉保存の問題に対処する。 我々は,すべてのソースプログラムに対して一様に保存を保証できる検証方法を開発した。
  論文  参考訳（メタデータ） (2024-07-21T07:30:30Z)
• JailbreakBench: An Open Robustness Benchmark for Jailbreaking Large Language Models [123.66104233291065]
  ジェイルブレイク攻撃は、大きな言語モデル(LLM)が有害、非倫理的、またはその他の不快なコンテンツを生成する原因となる。 これらの攻撃を評価することは、現在のベンチマークと評価テクニックの収集が適切に対処していない、多くの課題を提示します。 JailbreakBenchは、以下のコンポーネントを備えたオープンソースのベンチマークである。
  論文  参考訳（メタデータ） (2024-03-28T02:44:02Z)
• RaceFixer -- An Automated Data Race Fixer [0.0]
  RaceFixerは、ひとつの一般的なタイプのバグを修正するプロセスを自動化する。 複数のバグのパッチを組み合わせることで、パフォーマンスとコードの可読性を向上する。
  論文  参考訳（メタデータ） (2024-01-08T20:25:14Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  学習されたトランスパイレーションは、手作業による書き直しやエンジニアリングの取り組みに代わるものだ。 確率的ニューラルネットワークモデル(LM)は、入力毎に可塑性出力を生成するが、正確性を保証するコストがかかる。 Guess & Sketch は LM の特徴からアライメントと信頼性情報を抽出し、意味的等価性を解決するためにシンボリック・ソルバに渡す。
  論文  参考訳（メタデータ） (2023-09-25T15:42:18Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  完全同型暗号方式として, 完全同型暗号方式を初めて構築する。 我々の主要な技術要素は、量子証明器が古典的検証器に量子状態の形でのLearning with Errors分布からのサンプルが削除されたことを納得させる対話的プロトコルである。
  論文  参考訳（メタデータ） (2022-03-03T10:07:32Z)
• An efficient constraint based framework forhandling floating point SMT problems [0.5161531917413706]
  本稿では,浮動小数点検証問題に対する新しい制約プログラミングフレームワークである,私たちによる2019年版を紹介する。 私たちにとって、フロートに対する制約は第一級のオブジェクトであり、浮動小数点領域の構造を公開して活用することを目的としています。
  論文  参考訳（メタデータ） (2020-02-27T21:11:22Z)

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

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