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

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