論文の概要: Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)
- arxiv url: http://arxiv.org/abs/2511.11055v1
- Date: Fri, 14 Nov 2025 08:11:31 GMT
- ステータス: 翻訳完了
- システム内更新日: 2025-11-17 22:42:18.492033
- Title: Data Race Detection by Digest-Driven Abstract Interpretation (Extended Version)
- Title（参考訳）: ダイジェスト駆動抽象解釈によるデータ競合検出(拡張版)
- Authors: Michael Schwarz, Julian Erhard,
- Abstract要約: 音の静的解析は、2つの競合するメモリアクセスが同時に発生しないことを確立することで、データ競合がないことを証明することができる。
我々はダイジェストを使用して、競合するアクセスが並列に起こらない状況を把握する。
本稿では,静的解析器Goblintにおけるダイジェスト駆動型データ競合検出の実装について報告し,SV-COMPベンチマークスイートで評価する。
- 参考スコア（独自算出の注目度）: 4.3994959886619185
- License: http://creativecommons.org/licenses/by/4.0/
- Abstract: Sound static analysis can prove the absence of data races by establishing that no two conflicting memory accesses can occur at the same time. We repurpose the concept of digests -- summaries of computational histories originally introduced to bring tunable concurrency-sensitivity to thread-modular value analysis by abstract interpretation, extending this idea to race detection: We use digests to capture the conditions under which conflicting accesses may not happen in parallel. To formalize this, we give a definition of data races in the thread-modular local trace semantics and show how exclusion criteria for potential conflicts can be expressed as digests. We report on our implementation of digest-driven data race detection in the static analyzer Goblint, and evaluate it on the SV-COMP benchmark suite. Combining the lockset digest with digests reasoning on thread ids and thread joins increases the number of correctly solved tasks by more than a factor of five compared to lockset reasoning alone.
- Abstract（参考訳）: サウンド静的解析は、競合する2つのメモリアクセスが同時に発生しないことを確立することで、データの競合がないことを証明することができる。
私たちはダイジェストの概念を再利用します -- もともとは計算履歴の要約は、抽象的な解釈によってスレッドモジュール値分析に調整可能な並列性をもたらすために導入され、このアイデアをレース検出にまで拡張します。
これを形式化するために、スレッドモジュールのローカルトレースセマンティクスにおけるデータ競合の定義と、潜在的な競合の排除基準がダイジェストとしてどのように表現できるかを示す。
本稿では,静的解析器Goblintにおけるダイジェスト駆動型データ競合検出の実装について報告し,SV-COMPベンチマークスイートで評価する。
ロックセットダイジェストとスレッドIDとスレッド結合のダイジェストのダイジェストを組み合わせることで、ロックセット推論単独と比較して、正しく解決されたタスクの数を5倍に増やす。
関連論文リスト
- Context-Aware Search and Retrieval Over Erasure Channels [12.794591022795355]
本稿では,シンボル消去チャネル上で動作している遠隔文書検索システムの情報理論解析について述べる。
提案モデルは、言語コーパスの項周波数重みから導かれるクエリの特徴ベクトルを符号化する。
我々は、検索誤差確率、すなわち、より類似の少ない文書が選択される確率の明示的な式を導出する。
論文 参考訳（メタデータ） (2025-07-16T04:21:46Z) - Empirical Evaluation of Embedding Models in the Context of Text Classification in Document Review in Construction Delay Disputes [6.076874513889027]
テキスト埋め込みはテキストデータの数値表現であり、単語、フレーズ、文書全体を実数のベクトルに変換する。
本稿では,4つの異なるモデルの包括的比較分析を通じて,異なる埋め込みを評価する作業について述べる。
K-Nearest Neighbors (KNN) と Logistic Regression (LR) の両方を用いてバイナリ分類タスクを行い、特にラベル付きデータセット内でテキストスニペットが 'delay' あるいは 'not delay' に関連付けられているかどうかを判断する。
論文 参考訳（メタデータ） (2025-01-16T22:12:11Z) - Intelligent Multi-Document Summarisation for Extracting Insights on Racial Inequalities from Maternity Incident Investigation Reports [0.8609957371651683]
医療では、毎年何千もの安全事故が発生するが、これらの事故から学ぶことは効果的に集約されない。
本稿では,安全事故報告の集約と分析を容易にするためのフレームワークであるI-SIRch:CSを提案する。
このフレームワークは、セーフティ・インテリジェンス・リサーチ(SIRch)の分類学を用いた概念アノテーションと、クラスタリング、要約、分析機能を統合する。
論文 参考訳（メタデータ） (2024-07-11T09:11:20Z) - AMRFact: Enhancing Summarization Factuality Evaluation with AMR-Driven Negative Samples Generation [57.8363998797433]
抽象的意味表現(AMR)を用いた摂動要約を生成するフレームワークであるAMRFactを提案する。
提案手法は,AMRグラフに一貫した要約を解析し,制御された事実不整合を注入して負の例を生成し,一貫性のない事実不整合要約を高い誤差型カバレッジで生成する。
論文 参考訳（メタデータ） (2023-11-16T02:56:29Z) - Interpretable Automatic Fine-grained Inconsistency Detection in Text
Summarization [56.94741578760294]
本研究の目的は, 要約中の事実誤りの微粒化を予測し, 微粒化不整合検出の課題を提案することである。
要約における現実的不整合の検査方法に触発され,解析可能な微粒不整合検出モデルであるFinGrainFactを提案する。
論文 参考訳（メタデータ） (2023-05-23T22:11:47Z) - Understanding and Mitigating Spurious Correlations in Text
Classification with Neighborhood Analysis [69.07674653828565]
機械学習モデルは、トレーニングセットに存在するが一般的な状況では当てはまらない急激な相関を利用する傾向にある。
本稿では, 周辺分析と呼ばれる新しい視点から, 突発的相関がもたらす意味について考察する。
本稿では,テキスト分類における素早い相関を緩和する正規化手法であるNFL(doN't Forget your Language)を提案する。
論文 参考訳（メタデータ） (2023-05-23T03:55:50Z) - BERM: Training the Balanced and Extractable Representation for Matching
to Improve Generalization Ability of Dense Retrieval [54.66399120084227]
本稿では,BERMと呼ばれるマッチング信号の取得により,高密度検索の一般化を改善する手法を提案する。
センス検索は、ドメイン内のラベル付きデータセットでトレーニングされた場合、第1段階の検索プロセスにおいて有望であることが示されている。
論文 参考訳（メタデータ） (2023-05-18T15:43:09Z)
関連論文リストは本サイト内にある論文のタイトル・アブストラクトから自動的に作成しています。
指定された論文の情報です。
本サイトの運営者は本サイト（すべての情報・翻訳含む）の品質を保証せず、本サイト（すべての情報・翻訳含む）を使用して発生したあらゆる結果について一切の責任を負いません。