arXiv Science⌕ Search
Home/Archive/arXiv

arXiv · 2609.00246

Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version)

Daniel Bund·Julian Erhard·Michael Petter·Michael Schwarz
View original source ↗Read source document ↗Export metadata ↓

Abstract

Maintaining an abstraction of the execution history of threads can improve the precision of data race detection in static analysis. Here, we extend the digest framework to handle concurrency constructs and synchronization mechanisms that have been ignored in static race detection. 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. We also instantiate the framework with an abstraction of locksets held by ancestor threads. We propose a suite of litmus tests to evaluate analyses for these features and compare our implementation to state-of-the-art tools, finding that they lack support.

Explore related subjects

cs.PLcs.SE

Keep this discovery

BibTeXRIS

Daniel Bund, Julian Erhard, Michael Petter, Michael Schwarz. 2026-08-31. Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version). https://arxiv.org/abs/2609.00246

Cite the original work for its findings. Save a collection to share your selection of sources.

Discover connections

cs.PL subjectcs.SE subject

Connections use source metadata and explicit phrase matches, not verified experimental comparisons.

KEEP EXPLORING

Related papers

arXiv2026

FlowCheck: Helping End-Users Specify and Verify Intent in Vibe-Coded Web Apps

Vibe-coded applications often contain silent behavioral failures in which the interface appears functional even though user-visible information does not flow to the expected state or output. We introduce FlowCheck, a constraint language to specify these user-visible information flows directly through the application interface, where constraints can also be displayed and inspected without reading code, and are structured enough for reliable LLM generation. FlowCheck translates the constraints into deterministic CodeQL analyses, and we evaluate it across four applications generated via Claude Code, and compare with three coding models as bug-finding baselines. We find that FlowCheck correctly translates and flags all 30 of our injected constraint violations with no false positives. In contrast, frontier models (Claude Opus 4.7, DeepSeek V3, and Gemini Pro) showed significantly lower accuracy when prompted to find bugs in the same code, with none achieving full accuracy. This approach lets vibe coders state intent in terms of the interface they understand, and checks it deterministically against the code they do not.

cs.SE↗
arXiv2026

From C to Idiomatic Rust: A Ship-of-Theseus Agentic Translation

C underpins operating systems, embedded platforms, and network infrastructure as its abstractions map directly to machine behaviour. Its explicit memory model, predictable data representations, and minimal runtime allow compilers to generate fast, deterministic code. These properties also leave correctness and memory safety entirely to the programmer, making undefined behaviour, pointer misuse, and lifetime errors persistent sources of defects and security vulnerabilities in long-lived C codebases. Rust eliminates most failure modes through a static ownership and borrowing model that enforces memory safety and aliasing constraints at compile time. However, mature C systems cannot be translated directly: implicit layout assumptions, aliasing patterns, and undefined behaviour must be reconstructed before safe Rust can be produced. This paper presents a migration methodology that first generates a semantics-preserving, non-idiomatic Rust baseline and then incrementally rewrites it into idiomatic Rust using agentic AI, validating each step through compilation and behavioural testing. Applied to iodine, a real-world DNS tunnel, the approach demonstrates that reliable C-to-Rust migration is a structured transformation workflow rather than a single translation step.

cs.SE↗
arXiv2026

MIRAGE-CAD: Construction-Mediated Multimodal Generation of Executable CAD Programs

Recovering an executable parametric CAD program from an observed object is fundamentally ambiguous, because the same final geometry can result from different construction procedures. We study this problem from four types of input: natural-language descriptions, rendered images, point clouds, and STEP/B-Rep geometry. MIRAGE-CAD maps each input to a shared construction representation and mediates program generation through an explicit construction-plan interface. The resulting Python CAD code is executed by an OpenCASCADE kernel to build the solid and export it as STEP. On 2,500 held-out queries per modality, the system achieves 55.4-70.0% build success and 52.3-66.2% STEP export success without retrieval at inference. Controlled comparisons show that strong reconstruction does not depend on expressing the construction representation as text: a decoder conditioned directly on the continuous representation also reconstructs strongly, while an exposure-matched plan-based decoder shows no detected material loss in per-part geometric fidelity. The explicit plan instead provides a readable and separately measurable intermediate representation whose agreement with the reference construction is informative about downstream execution success. Finally, we show that executable validity, geometric fidelity, and parametric responsiveness can diverge substantially and should therefore be evaluated separately.

cs.CV↗