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
• Authors: Zhuang Li, Qiuping Yi, Jeff Huang,
• 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

• 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.