VeriFix: Verifying Your Fix Towards An Atomicity Violation

• URL: http://arxiv.org/abs/2504.16354v1
• Date: Wed, 23 Apr 2025 02:11:07 GMT
• Title: VeriFix: Verifying Your Fix Towards An Atomicity Violation
• Abstract summary: This paper presents textsfVeriFix, a new approach for verifying atomicity violation fixes.<n>Given a buggy trace that exposes an atomicity violation and a corresponding fix, textsfVeriFix effectively verifies if the fix introduces sufficient synchronizations to repair the atomicity violation without introducing new deadlocks.
• Score: 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.

Related papers

• Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version) [3.5832940717897217]
  We extend the digest framework to handle constructs and synchronization mechanisms that have been ignored in static race detection.<n>We introduce mechanisms for the commonly used thread barriers, as well as pthread_once, which allows to ensure that an action is executed only once.
  arXiv  Detail & Related papers  (2026-08-31T18:47:23Z)
• Towards Automated Formal Verification of zkEVMs Using LLM-Guided Constraint Synthesis [14.825615940318038]
  ZkEVMs generate zero-knowledge that guarantee off-chain execution correctness.<n> subtle implementation bugs can lead to valid proofs certifying semantically faulty states.<n>Formal verification via SMT solvers can prevent this, but is bottlenecked by specification.<n>We propose Veri Synth, a framework that synthesizes executable Python/Z3 verification models from Rust.
  arXiv  Detail & Related papers  (2026-07-22T06:20:36Z)
• The Illusion of High Utility in Safety Alignment of Text-to-Image Diffusion Models [49.67749928542536]
  Safety alignment of text-to-image (T2I) diffusion models aims to suppress harmful generations while preserving utility on benign prompts.<n>Recent methods often appear to deliver high safety with high utility, but this conclusion rests largely on coarse global utility metrics.<n>We show that when utility is measured with structured evaluation, this illusion breaks: onA (Text-to-Image Faithfulness evaluation with Question Answering)<n>We propose StructureAware Geometric Regularization (SAGE), a safety alignment objective that explicitly preserves embedding spread and inter-prompt relational structure.
  arXiv  Detail & Related papers  (2026-07-01T04:00:27Z)
• An End-to-End Approach for Fixing Concurrency Bugs via SHB-Based Context Extractor [8.427017198449912]
  This paper introduces ConFixAgent, an agent capable of fixing various types of bugs in an end-to-end manner.<n>We propose a novel context extraction approach designed for bug repair, utilizing Static-Before Happens Graphs to identify bug-relevant sections.<n>Our experiments demonstrate that ConFixAgent significantly outperforms state-of-the-art tools in addressing diverse types of bugs.
  arXiv  Detail & Related papers  (2026-04-07T11:56:35Z)
• Rejection Mixing: Fast Semantic Propagation of Mask Tokens for Efficient DLLM Inference [58.189320101488725]
  DLLMs promise fast non-autoregressive inference but suffer a severe quality-speed trade-off in parallel decoding.<n>We address this by integrating continuous representations into the discrete decoding process, as they preserve rich inter-position dependency.<n>We propose ReMix, a framework that introduces a novel Continuous Mixing State as an intermediate between the initial masked state and the final decoded token state.
  arXiv  Detail & Related papers  (2026-02-26T11:08:11Z)
• AlgoVeri: An Aligned Benchmark for Verified Code Generation on Classical Algorithms [54.99368693313797]
  Existing benchmarks test only individual languages/tools, so the performance numbers are not directly comparable.<n>We address this gap with AlgoVeri, a benchmark that evaluates vericoding of $77$ classical algorithms in Dafny, Verus, and Lean.
  arXiv  Detail & Related papers  (2026-02-10T06:58:26Z)
• RealSec-bench: A Benchmark for Evaluating Secure Code Generation in Real-World Repositories [58.32028251925354]
  Large Language Models (LLMs) have demonstrated remarkable capabilities in code generation, but their proficiency in producing secure code remains a critical, under-explored area.<n>We introduce RealSec-bench, a new benchmark for secure code generation meticulously constructed from real-world, high-risk Java repositories.
  arXiv  Detail & Related papers  (2026-01-30T08:29:01Z)
• Overcoming Joint Intractability with Lossless Hierarchical Speculative Decoding [58.92526489742584]
  We propose provably lossless.<n> verification method that significantly boosts the expected number of accepted tokens.<n>We show that HSD yields consistent improvements in acceptance rates across diverse model families and benchmarks.
  arXiv  Detail & Related papers  (2026-01-09T11:10:29Z)
• AtomGraph: Tackling Atomicity Violation in Smart Contracts using Multimodal GCNs [12.255018487780703]
  We introduce AtomGraph, an automated framework designed for detecting atomicity violations in smart contracts.<n>This framework uses Graph Convolutional Networks to identify atomicity violations through multimodal feature learning and fusion.<n>AtomGraph achieves 96.88% accuracy and 96.97% F1 score, outperforming existing tools.
  arXiv  Detail & Related papers  (2025-12-02T04:20:02Z)
• SIM-CoT: Supervised Implicit Chain-of-Thought [108.30049193668083]
  Implicit Chain-of-Thought (CoT) methods offer a token-efficient alternative to explicit CoT reasoning in Large Language Models.<n>We identify a core latent instability issue when scaling the computational budget of implicit CoT.<n>We propose SIM-CoT, a plug-and-play training module that introduces step-level supervision to stabilize and enrich the latent reasoning space.
  arXiv  Detail & Related papers  (2025-09-24T17:01:32Z)
• Deep Learning Based Concurrency Bug Detection and Localization [9.2389985253336]
  Concurrency bugs are notoriously hard to detect and compromise software reliability and security.<n>Existing deep learning methods face three main limitations.<n>We propose a novel method for effective bug detection as well as localization.
  arXiv  Detail & Related papers  (2025-08-28T15:40:20Z)
• Static Analysis for Detecting Transaction Conflicts in Ethereum Smart Contracts [2.6703221234079946]
  We propose a novel static analysis method to detect potential transaction conflicts in smart contracts.<n>Our method identifies read-write, write-write, and function call conflicts by analyzing state variable access patterns in Solidity contracts.
  arXiv  Detail & Related papers  (2025-07-06T11:42:40Z)
• AutoLayout: Closed-Loop Layout Synthesis via Slow-Fast Collaborative Reasoning [102.71841660031065]
  Auto is a fully automated method that integrates a closed-loop self-validation process within a dual-system framework.<n>The effectiveness of Auto was validated across 8 distinct scenarios, where it demonstrated a significant 10.1% improvement over SOTA methods.
  arXiv  Detail & Related papers  (2025-07-06T08:35:22Z)
• Rethinking Cross-Modal Interaction in Multimodal Diffusion Transformers [79.94246924019984]
  Multimodal Diffusion Transformers (MM-DiTs) have achieved remarkable progress in text-driven visual generation.<n>We propose textbfTemperature-Adjusted Cross-modal Attention (TACA), a parameter-efficient method that dynamically rebalances multimodal interactions.<n>Our findings highlight the importance of balancing cross-modal attention in improving semantic fidelity in text-to-image diffusion models.
  arXiv  Detail & Related papers  (2025-06-09T17:54:04Z)
• CRUST-Bench: A Comprehensive Benchmark for C-to-safe-Rust Transpilation [63.23120252801889]
  CRUST-Bench is a dataset of 100 C repositories, each paired with manually-written interfaces in safe Rust as well as test cases.<n>We evaluate state-of-the-art large language models (LLMs) on this task and find that safe and idiomatic Rust generation is still a challenging problem.<n>The best performing model, OpenAI o1, is able to solve only 15 tasks in a single-shot setting.
  arXiv  Detail & Related papers  (2025-04-21T17:33:33Z)
• Tuning-Free Image Editing with Fidelity and Editability via Unified Latent Diffusion Model [60.82962950960996]
  We introduce UnifyEdit, a tuning-free method that performs diffusion latent optimization. We develop two attention-based constraints: a self-attention (SA) preservation constraint for structural fidelity, and a cross-attention (CA) alignment constraint to enhance text alignment. Our approach achieves a robust balance between structure preservation and text alignment across various editing tasks, outperforming other state-of-the-art methods.
  arXiv  Detail & Related papers  (2025-04-08T01:02:50Z)
• Automated detection of atomicity violations in large-scale systems [5.652514080341844]
  We propose Clover, a framework that integrates static analysis with large language model (LLM) agents to detect atomicity violations in real-world programs.<n>Clover achieves a precision/recall of 92.3%/86.6%, outperforming existing approaches by 27.4-118.2% on F1-score.
  arXiv  Detail & Related papers  (2025-04-01T08:13:29Z)
• Atom of Thoughts for Markov LLM Test-Time Scaling [18.288669306091155]
  Large Language Models (LLMs) achieve superior performance through training-time scaling.<n>As the scale of reasoning increases, existing test-time scaling methods suffer from accumulated historical information.<n>We observe that complex reasoning can be achieved by solving a series of independent and self-contained subquestions.
  arXiv  Detail & Related papers  (2025-02-17T16:52:42Z)
• LIAR: Leveraging Inference Time Alignment (Best-of-N) to Jailbreak LLMs in Seconds [98.20826635707341]
  Jailbreak attacks expose vulnerabilities in safety-aligned LLMs by eliciting harmful outputs through carefully crafted prompts.<n>We frame jailbreaks as inference-time misalignment and introduce LIAR, a fast, black-box, best-of-$N$ sampling attack requiring no training.<n>We also introduce a theoretical "safety net against jailbreaks" metric to quantify safety alignment strength and derive suboptimality bounds.
  arXiv  Detail & Related papers  (2024-12-06T18:02:59Z)
• Localizing Factual Inconsistencies in Attributable Text Generation [91.981439746404]
  We introduce QASemConsistency, a new formalism for localizing factual inconsistencies in attributable text generation. We first demonstrate the effectiveness of the QASemConsistency methodology for human annotation. We then implement several methods for automatically detecting localized factual inconsistencies.
  arXiv  Detail & Related papers  (2024-10-09T22:53:48Z)
• SNIP: Speculative Execution and Non-Interference Preservation for Compiler Transformations [0.15800607910450126]
  We address the problem of preserving non-interference across compiler transformations under speculative semantics. We develop a proof method that ensures the preservation uniformly across all source programs.
  arXiv  Detail & Related papers  (2024-07-21T07:30:30Z)
• A robust and composable device-independent protocol for oblivious transfer using (fully) untrusted quantum devices in the bounded storage model [4.644619667965337]
  We present a device-independent (DI) quantum protocol between two parties for oblivious transfer (OT) using Magic Square devices.<n>After a fixed constant (real-world) time interval, referred to as DELAY, the quantum states decohere completely.<n>Our protocol has negligible (in lambda) correctness and security errors and can be implemented in the NISQ era.
  arXiv  Detail & Related papers  (2024-04-17T11:46:36Z)
• JailbreakBench: An Open Robustness Benchmark for Jailbreaking Large Language Models [123.66104233291065]
  Jailbreak attacks cause large language models (LLMs) to generate harmful, unethical, or otherwise objectionable content. evaluating these attacks presents a number of challenges, which the current collection of benchmarks and evaluation techniques do not adequately address. JailbreakBench is an open-sourced benchmark with the following components.
  arXiv  Detail & Related papers  (2024-03-28T02:44:02Z)
• RaceFixer -- An Automated Data Race Fixer [0.0]
  RaceFixer automates the process of fixing one common type of bug: single-variable atomicity violations. It tries to combine the patches of multiple bugs for better performance and code readability.
  arXiv  Detail & Related papers  (2024-01-08T20:25:14Z)
• Guess & Sketch: Language Model Guided Transpilation [59.02147255276078]
  Learned transpilation offers an alternative to manual re-writing and engineering efforts. Probabilistic neural language models (LMs) produce plausible outputs for every input, but do so at the cost of guaranteed correctness. Guess & Sketch extracts alignment and confidence information from features of the LM then passes it to a symbolic solver to resolve semantic equivalence.
  arXiv  Detail & Related papers  (2023-09-25T15:42:18Z)
• Quantum Proofs of Deletion for Learning with Errors [91.3755431537592]
  We construct the first fully homomorphic encryption scheme with certified deletion. Our main technical ingredient is an interactive protocol by which a quantum prover can convince a classical verifier that a sample from the Learning with Errors distribution in the form of a quantum state was deleted.
  arXiv  Detail & Related papers  (2022-03-03T10:07:32Z)
• Fault-tolerant parity readout on a shuttling-based trapped-ion quantum computer [64.47265213752996]
  We experimentally demonstrate a fault-tolerant weight-4 parity check measurement scheme. We achieve a flag-conditioned parity measurement single-shot fidelity of 93.2(2)%. The scheme is an essential building block in a broad class of stabilizer quantum error correction protocols.
  arXiv  Detail & Related papers  (2021-07-13T20:08:04Z)
• An efficient constraint based framework forhandling floating point SMT problems [0.5161531917413706]
  This paper introduces the 2019 version of us, a novel Constraint Programming framework for floating point verification problems. In us, constraints over the floats are first class objects, and the purpose is to expose and exploit structures of floating point domains.
  arXiv  Detail & Related papers  (2020-02-27T21:11:22Z)

This list is automatically generated from the titles and abstracts of the papers in this site.

This site does not guarantee the quality of this site (including all information) and is not responsible for any consequences.