PaperlayerView exact revision on arXiv

Source-linked AI summary

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

Daniel Bund, Julian Erhard, Michael Petter, Michael Schwarz

arXiv:2609.00246v1cs.PLcs.SE

TL;DR

Static race detection often overlooks valid synchronization mechanisms beyond mutexes and thread creation or joining, despite the need to keep false positives manageable. The paper extends digest-driven abstract interpretation with digests for barriers, pthread once, and ancestor-thread locksets, then evaluates these features against static analyzers. The comparison finds that existing state-of-the-art tools lack support for the tested features.

  • Problem

    Static race analyses often overlook synchronization primitives such as barriers and pthread once, while false positives threaten their practical usability.

  • Method

    The paper extends digest-driven abstract interpretation with history abstractions for barriers, pthread once, and mutex locksets held by ancestor threads.

  • Results

    The implementation was evaluated on focused tests covering barriers, pthread once, creationLockset, and descendantLockset, and existing analyzers lacked support for these features.

  • Takeaways & Limitations

    The digest framework provides sound concurrency information for discarding access pairs that cannot occur in parallel across the supported synchronization patterns.

  • Takeaways & Limitations

    The approach is parametric in the may-alias analysis, and recursive pthread once behavior is fixed to glibc’s deadlocking behavior.

Abstract

from arXiv · show

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.

1 Introduction

Static race detection must handle synchronization beyond mutexes and thread creation or joining. This work extends digest-driven analysis to barriers, pthread once, and lock patterns involving ancestor threads.

  • Sound static race analyses can flag potential races but must control false positives to remain practical.The paper notes that nondeterministic scheduling makes races difficult to debug and that manageable false-positive rates are essential for usability.
  • The approach is parametric in may-alias analysis, allowing different speed–precision tradeoffs.The proposed digests were implemented in an abstract interpreter and evaluated on hand-crafted examples involving the supported constructs.
  • Digest-driven abstract interpretation records execution-history abstractions at shared-memory accesses to improve sound race detection precision.Digests distinguish program points and shared-variable states according to observed thread histories and can be configured independently of the analysis domain.
  • The framework extends static race detection to Pthreads barriers, which can order accesses even when multiple worker threads synchronize concurrently.In the motivating example, the main thread’s write to g precedes the workers’ later accesses after all threads pass the barrier.
  • It introduces a pthread once digest to exploit that code guarded by the same control variable executes exactly once and within one thread.This supports ruling out races even when the relative order of protected accesses cannot be established.
  • The paper also develops digest-based reasoning for mutexes held across child-thread creation and throughout child execution.These descendantLockset and creationLockset patterns require handling beyond existing per-thread lockset analyses.

2 Digest-Driven Data Race Detection

Digest-driven race detection summarizes each thread’s observed execution history and uses these summaries to rule out infeasible races. The framework combines local-trace semantics, admissible digests, and sound abstract interpretation.

  • Digest-driven analysis: The analysis propagates abstract states indexed by digests, then checks potentially conflicting accesses with a may-happen-in-parallel predicate.A pair is discarded when any active digest proves the accesses cannot occur concurrently; otherwise it is reported as a potential race.
  • Local trace semantics: Local traces encode one ego thread’s history together with observable information about other threads, including locks and global accesses.Each trace contains locally consistent thread swim-lanes and auxiliary dependencies induced by creation, mutex, and global-variable orders.
  • Synchronization extensions: The framework extends local-trace reasoning to multi-thread synchronization actions, including barriers, whose recorded arrivals are incorporated at a later check.Barrier records are observable, while barrier checks observe the traces accumulated from the required arrivals.
  • Race criterion: Bidirectional trace compatibility characterizes when two accesses are unordered, yielding an exact correspondence with intuitive data races.Two accesses are racy exactly when at least one is a write and compatible traces exist in both directions.
  • Soundness: Admissible digests preserve soundness when refining a sound abstract interpretation of a concurrent program.The framework supports sound abstract operations for trace extension and thread creation.
  • Modularity: Products of admissible digests remain admissible, enabling modular combinations of history abstractions such as locksets and thread identifiers.This supports precision and speed tradeoffs through combinations with different may-alias analyses.

3 Synchronization via pthread once

The paper models pthread_once by compiling it into observable and observing actions and tracking active or completed control variables. This digest can exclude races within initialization and between initialization and later code.

  • Motivation: pthread_once executes initialization code at most once, supporting resource setup before threads access shared resources.Library developers use it because they cannot place initialization directly in the application’s main function.
  • Semantic decomposition: The semantics compile pthread_once into start, branch, optional initialization, and end actions governed by a control variable.The control variable is initialized at program start, and the system treats running the function and setting the variable as atomic.
  • Digest: The pthread_once digest tracks active control variables during initialization and completed variables after initialization has definitely finished.The active set changes at startO(o), while endO(o) moves the variable into the completed set; guards inspect completion status.
  • Race exclusion: The digest’s compatibility predicate excludes races when a control variable is active in both accesses or active in one and completed in the other.These conditions capture both accesses within the called function and accesses spanning initialization and later code.
  • Result: An analysis using the pthread_once digest establishes race freedom for the program decomposed into individual once steps.The paper states that the corresponding digest is admissible and its compatibility predicate is sound.

4 Synchronization via Barriers

The barrier extension models multi-thread synchronization through history digests, using barrier actions to detect unreachable executions and establish ordering that can rule out races.

  • Barrier semantics: Barriers block callers until the configured capacity of threads has waited, then unblock all waiting threads.The semantics represent each wait as a non-blocking record followed by an observing, N-ary check action.
  • Barrier semantics: The barrier check succeeds only when the recorded calls can occur together in a compatible local trace; otherwise, the execution is unreachable.This also detects stuck executions when too few other waits can happen in parallel.
  • Race-freedom reasoning: Passing a barrier supplies cross-thread history that can order accesses and exclude some data races.If one thread has passed a barrier that another has not, their accesses are not bidirectionally compatible.
  • Barrier digest: The barrier digest extends a base digest with the current thread’s passed barriers and observed barriers associated with thread ids.The product tracks sets R and map O, with compatibility exploiting observed actions when a thread identity is unique.
  • Race-freedom reasoning: In the example, main’s write to g precedes worker reads because main accesses g before waiting and workers access it after passing the barrier.The resulting analysis proves race-freedom for those accesses.
  • Implementation scope: The implementation supports dynamic capacities and pointer-based accesses, but treats inter-process barriers as no-ops because Goblint lacks process-level concurrency.The latter treatment is sound but coarse.

5 Synchronization via Mutexes and Creation Orders

The creation-order mutex pattern can establish ordering between an ancestor’s access and descendant-thread accesses without requiring descendants to synchronize with one another.

  • Creation-order synchronization: Creating threads while holding a mutex can simulate a barrier when workers later acquire that mutex.This pattern lets worker threads proceed without waiting for one another.
  • Creation-order synchronization: In the example, workers acquire m only after main unlocks it, so their accesses to g follow main’s access and cannot race.A worker need not wait for another worker to reach the lock.
  • Creation-order synchronization: The analysis requires descendant creation under a locked mutex and no subsequent unlock after the relevant creations.It also checks that the accessed thread is an ancestor-created descendant, preventing alternative creation paths from invalidating the reasoning.
  • Creation-order synchronization: At the later access, the analysis records which threads locked each mutex and excludes a race when an appropriate descendant lock follows creation.The condition can apply transitively through descendants.

6 Digests for Creation Locksets

Creation-lockset digests capture mutexes held by an ancestor throughout a descendant’s execution, allowing protected descendant accesses to be separated from ancestor accesses.

  • Creation locksets: A mutex held by an ancestor throughout a descendant’s execution can protect that descendant from concurrent accesses using the same mutex.The pattern supports parallel computation while retaining exclusive access to a global.
  • Creation locksets: The example proves that work’s access to g cannot race with t1 because m remains locked throughout work and is also in t1’s lockset.The protection relies on the shared mutex being present in both relevant locksets.
  • Creation locksets: The digest must record the creator’s lock and require that no unlock occurs while the descendant may run in parallel.It also requires transitive creation under the locked mutex.
  • Creation locksets: Parallel descendants are identified from transitive creations, subtracting threads already joined back, using thread-id and join digests.Appendix F supplies a digest for checking these conditions.

7 Experiments and Benchmark Set

The implementation integrates the enhanced synchronization features into Goblint and evaluates both their runtime cost and analyzers’ ability to certify race-freedom on focused tests.

  • Implementation: Goblint supports pthread once, barriers, and thread-creation/mutex interactions using direct Pthreads support, abstract digests, and mixed flow-sensitivity.The implementation differs slightly from the idealized presentation.
  • Scalability and runtime: Across ≈30,000 SV-Comp benchmarks, enabling enhanced synchronization features increased total runtime by ≈2%.The largest stated individual overhead is 30.5% for locked-creation handling on df.
  • Benchmark set: The comparison suite contains 90 focused benchmarks: 28 pthread once, 26 barrier, 18 creationLockset, and 18 descendantLockset tests.The tests target correct certification of data-race freedom and encode expected behavior as SV-Comp verdicts.
  • Results: The authors’ implementation produced no false positives or false negatives on the benchmark set.Because it uses abstract interpretation, false positives may still occur on other programs with these features.
  • Results: Compared analyzers missed races in both lockset categories, while several returned ERROR or UNKNOWN for barriers or pthread once.Barriers were treated soundly but their information was not fully exploited to reduce false positives.

8 Related Work

The paper extends digest-based static race detection to synchronization mechanisms and thread–mutex patterns that prior analyses largely overlooked, contrasting its sound abstract-interpretation approach with related techniques.

  • The authors generalize local traces and digests to cover additional synchronization mechanisms beyond prior thread-history abstractions.The extension targets mechanisms that have received little attention in sound static race detection.
  • Terauchi frames race freedom as a typing problem covering signaling, semaphores, and read-write locks, whereas this paper uses abstract interpretation and different synchronization mechanisms.The comparison emphasizes methodological and feature-set differences rather than a shared implementation.
  • Barriers: For Pthreads barriers, syntactically different wait calls may belong together, and barrier capacity need not equal the number of running threads.These properties distinguish Pthreads barriers from OpenMP-style barriers, where all threads arrive at the same syntactic barrier.
  • Feature pthread once: The paper presents, to the authors’ knowledge, the first static analysis beyond syntactic checks for pthread once.Earlier work identified missing pthread once support as a limitation.
  • Mutexes and Creation Orders: The paper’s mutex and creation-order analysis is sound and overapproximates all executions, unlike predictive analyses that start from a single observed execution.The authors contrast their approach with prior work that is unsound on several litmus tests or lacks an analysis for descendant-held mutexes.

9 Conclusion and Future Work

The paper builds digest-driven abstract interpretation into a sound static race-detection framework that addresses under-supported concurrency primitives and synchronization patterns. It concludes that these techniques improve the framework’s scope and may extend to other concurrency bugs.

  • Sound static race detection offers strong guarantees, but reducing false positives is crucial for practical usability.The conclusion identifies false-positive reduction as a central usability requirement.
  • The framework refines thread-modular abstract interpretation by distinguishing program points according to thread histories.This history-sensitive representation is the basis for the paper’s digest approach.
  • Novel digests support concurrency primitives that have received little to no attention in sound static race detection.The conclusion summarizes the paper’s central extension beyond previously represented history information.
  • Future Work: The authors identify deadlocks and termination as possible future applications of the techniques.This is presented as future work rather than an evaluated result of the current paper.

B Proofs for Propositions 1 and 2

The appendixed proofs establish the relationship between intuitive races, digest compatibility, and soundness of digest refinement. They also note that extending lockset-digest admissibility to barriers and pthread once is straightforward.

  • Proposition 5: Two accesses to a global variable are intuitively racy exactly when they meet the shared-memory, write-involvement, and bidirectional trace-compatibility conditions.The proposition characterizes races using traces ending at the respective control-flow predecessors.
  • Proposition 5: The proof simplifies an earlier soundness proof by using the same trace-based race characterization with higher-arity observing actions.The existence of actions involving more than two threads does not complicate this proof.
  • Proposition 6: Refining a sound abstract interpretation with an admissible digest yields another sound abstract interpretation.The proof constructs an equivalent refined concrete semantics and then derives soundness from the base analysis.
  • The admissibility of the lockset digest extends straightforwardly because barriers and pthread once leave held-lock sets unchanged.The additional actions return the digest unmodified and do not affect locksets.

C Details on & Extended Support for pthread once

The appendix details the pthread once digest, its admissibility and soundness arguments, and an extension that tracks completed controls and mutex interactions. It also explains why signaling cannot provide the same race-exclusion guarantee as barriers.

  • Soundness: The appendix states that the pthread once digest is admissible and that its may-happen-in-parallel predicate is sound.This claim is given as Proposition 7 after the detailed case analysis.
  • Admissibility: The digest’s start and end actions update active and completed control-variable sets, supporting admissibility proofs for the abstract semantics.The appendix shows startO adding a control variable and endO removing it from the active set while marking it completed.
  • Extended support: The extended digest can refine global-value reasoning by retaining only values possible after pthread once code has executed.In the example, the refinement lets both assertions establish that g is not null.
  • pthread once digest: The pthread once digest tracks active and completed control variables, while its extended form additionally records mutexes unlocked during active once regions.The extended tuple is described as (A, C, O), with O mapping mutexes to relevant control variables.
  • Barriers and signals: Pthreads signaling cannot exclude data races from a returned wait because spurious wakeups allow return without a signal.This distinguishes signaling from a barrier-style ordering guarantee.

E Digests for Descendant Lockset

The descendant lockset digest augments thread and current-lockset information with mutexes held during descendant creation. Its sound race predicate uses these histories to exclude incompatible executions.

  • Digest components: The digest tracks a thread-ID/lockset pair together with H, mapping mutexes to threads that held them, and D, mapping thread IDs to mutex sets.H records observed mutex ownership; D records mutexes held throughout relevant descendant creation.
  • Race predicate: The race predicate rejects a pair when one thread observed a mutex held by an ancestor while the other thread’s creation occurred under that mutex.The two disjuncts check the corresponding condition in either direction.
  • Example: At the analyzed accesses, H records m as held by main and D records both worker IDs as associated with m.These digest values support excluding the potential race in the example.
  • Soundness: Proposition 9 states that, assuming the base digest is admissible, the descendant-lockset digest is admissible and its race predicate is sound.The soundness proof derives incompatible trace histories from the digest conditions.
  • Transfer operations: A new thread inherits H and initializes D to map every thread ID to S, while locking and unlocking update the relevant digest components.Lock adds the current thread to H; unlock removes the mutex from every D entry.

F Digests for Creation Locksets

The creation-lockset digest records mutex protection and inter-thread observations to reason about ancestor-held locks. Its predicate and admissibility result support ruling out races between differently created threads.

  • Digest components: The creation-lockset digest is a triple ((A, S, J), C, O), combining the thread-ID/lockset digest with C and O maps.C records mutexes held throughout thread executions; O records the most recently observed sub-trace information.
  • Race predicate: The race predicate checks whether an observed thread held a mutex throughout another thread’s execution while the current access also holds that mutex.It evaluates the condition in either direction and includes creation and ancestor relationships.
  • Example: At the example access, the O component together with S = {m} suffices to rule out a race with a program point having thread id work.The result uses missing outer bindings as (∅, ∅) and missing inner bindings as S.
  • Soundness: Proposition 10 states that, assuming the base product digest is admissible, the creation-lockset digest is admissible and its race predicate is sound.The proof uses mutual exclusion to order critical sections observed through the digest.
  • Transfer operations: Creation intersects C with the current lockset, unlocking removes a mutex from relevant entries, and locking records observations in O.New threads start with initial values for both auxiliary maps.

G.4 Benchmark Execution Times

The benchmark evaluation compares analyzers on soundness and precision for barrier, pthread_once, and lockset-related programs. The reported results show inconclusive or incorrect tool behavior on several unsupported concurrency features.

  • Soundness: Soundness tests treat TRUE results on benchmarks expected to be FALSE as false negatives, while FALSE or UNKNOWN remains consistent with soundness.UNKNOWN does not establish that the property is false.
  • Soundness: Dartagnan and Ultimate Gemcutter recognize barriers and pthread once but return ERROR and UNKNOWN, providing no evidence of unsoundness or precision.RacerF is not evaluated for unreach-call, and Goblint returns UNKNOWN for false unreach-call properties.
  • Unsoundness examples: Compact examples expose unsound reports in which tools classify programs containing data races or reachable assertion failures as data-race-free.The examples include pthread_once and mutex/thread-creation patterns.
  • Precision: Precision tests treat FALSE results on benchmarks expected to be TRUE as false positives.Dartagnan and Ultimate Gemcutter again return ERROR and UNKNOWN on recognized barrier and pthread_once cases.
  • Results: The table reports varied tool verdicts across barrier, creation-lockset, descendant-lockset, and once benchmark rows.CPAchecker, Dartagnan, ESBMC, RacerF, Ultimate Gemcutter, and Goblint are compared by input file.
  • Imprecision examples: Other compact examples expose imprecision by reporting races in programs expected to satisfy no-data-race.A representative case uses a barrier initialized with capacity 2.
Loading 2609.00246v1…