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

Beyond Locks and Thread IDs: Static Data Race Detection Off The Beaten Path (Extended Version) Daniel Bund1 , Julian Erhard2 , Michael Petter1 , and Michael Schwarz3

arXiv:2609.00246v1 [cs.PL] 31 Aug 2026

1

Technical University of Munich, Garching, Germany {daniel.bund,michael.petter}@tum.de 2 CISPA Helmholtz-Zentrum, Garching, Germany julian.erhard@cispa.de 3 National University of Singapore, Singapore m.schwarz@nus.edu.sg

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. Keywords: data races, concurrency, static program analysis, software verification, abstract interpretation

1

Introduction

Data races are a class of errors that is particularly hard to debug, partially due to the nondeterministic nature of the scheduling, i.e., bugs not materializing in every execution. To ensure correctness of code, particularly in domains where bugs are unacceptable, sound static analyses have been proposed that are guaranteed to flag any potential data race. However, these analyses typically suffer from false positives. For such tools to be practical, the number of false positives must remain manageable [3, 11]. Nevertheless, much of the literature on static data-race detection considers only mutexes and thread creation and joining as synchronization, overlooking less common but equally valid ways to prevent conflicting accesses from occurring concurrently. One such feature are barriers as provided by Pthreads: Example 1. Figure 1 is a program fragment using barriers. The main thread creates two workers, which compute with the value of a global variable g and their string argument. The barrier b is used to ensure that both workers can only

2 1

D. Bund, J. Erhard, M. Petter, and M. Schwarz int g;

15

2 3

16

pthread_barrier_t b;

4 5 6

17

pthread_barrier_init(&b, NULL, 3);

18

void* worker(void* arg) { // Worker initialization

7

19

pthread_create(&w1, NULL, worker, "1"); pthread_create(&w2, NULL, worker, "2");

20 21

pthread_barrier_wait(&b);

8 9

22

// Main initialization code g = 2;

23

int f = compute(g,arg); // Do something with f

10 11 12

24 25

pthread_barrier_wait(&b); // ...

26

return NULL;

13 14

int main() { pthread_t w1, w2; // Worker threads

}

27 28

}

Fig. 1. Program using Pthreads barriers.

perform their computation (line 10) after the main thread has set the global in line 24. Once all three threads have called wait for b, all of them can proceed. Assuming that the variable g is only accessed in the three locations given in the program fragment, there is no data race: The write to g in line 24 happens before all threads have reached the barrier, and the other two accesses to g happen later. On top of synchronization by barriers, we also consider the pthread once feature library developers often rely on (see the example Figure 4 in Section 3) and two patterns combining reasoning about threads and synchronization by mutexes (see the descendantLocksets example in Figure 8 in Section 5, as well as the creationLocksets examples in Figure 9). We focus on the temporal aspect of race detection, providing sound methods to prove that two access instructions cannot happen in parallel. This takes different forms: For barriers, our approach determines that certain accesses must happen before others. For pthread once, this is combined with establishing that all accesses protected by the same pthread once control variable happen in the same thread and can thus not race, even when their specific order cannot be established. When it comes to reasoning about threads and mutexes, in the descendantLocksets case (Section 5), it is once more must-happen-before relationships that are established, while for creationLocksets (Appendix F), it is only the fact that accesses are in fact ordered by critical sections even though they may not appear to be at first glance. Broadly, these mechanisms fall into two categories: barriers, pthread once, and descendant locksets use additional history information to establish must-happen-before relationships between accesses, whereas creation locksets (Appendix F) extend conventional lockset reasoning by recognizing protection through critical sections spanning multiple threads. Our approach is parametric in the other important ingredient of static race detection, namely a may-alias analysis, and can be combined with different such analyses to obtain different speed–precision tradeoffs. We base our work on digest-driven abstract interpretation. Abstract interpretation [4] is a principled way to overapproximate the concrete semantics of programs using abstract domains. Digests [28] were originally designed as a mechanism to improve the precision of thread-modular value analyses using abstract interpretation. Digests allow an analysis to distinguish program points as

Static Data Race Detection Off The Beaten Path

3

well as the states of shared variables according to the execution history observed by the thread executing the statement. They thus generalize trace partitioning [20] to concurrent programs, providing concurrency-sensitivity that can be configured independently of the analysis domain. In the result computed by an analysis with digests, potentially reachable accesses to shared variables are annotated with digests, i.e., an abstraction of the execution history observed by the thread in question. This can be exploited to enhance the precision of sound static data race detection [26]: When considering two accesses to a shared variable, both annotated with a digest, data races can be excluded when the two accesses cannot happen concurrently—as judged by their digests. While previous work [25, 26, 28] proposes digests for history information such as whether the execution is single-threaded or multi-threaded, or which mutexes are locked by the current thread, libraries such as Pthreads offer further concurrency and synchronization primitives, which have often been ignored. In particular, we provide digests for barriers, a mechanism to synchronize multiple threads. To do so, we extend the semantic framework underlying the digest framework to actions that involve more than two threads (Section 2). We show how digests are used to argue about whether two arbitrary operations may possibly happen in parallel4 , which is not only a key ingredient of our barrier digest but also paves the way towards further applications of the digest framework. We show in Section 4 how a history abstraction, i.e., a digest, relating to the operations performed on the barrier, is used to deduce race freedom for the programs using barriers, such as Example 1. There, the predicate ||? , introduced for checking whether two accesses to the same variable may race, is used for a different purpose in the definition of the barrier digest itself, to determine whether a sufficient number of threads may wait at the barrier at the same time. Section 3 proposes a digest for pthread once for more precise data-race detection. pthread once is a feature used in particular by library developers to ensure that some code is executed exactly once. Sometimes a thread locks a mutex before creating child threads and does not release it until certain protected operations have completed. This pattern requires intricate handling beyond existing per-thread lockset analyses. Partially inspired by Lu et al. [19], we propose a way of handling such patterns with digests in Section 5. Another pattern, where locks are held by a thread during the entire execution of its child is covered in Section 6. We implemented the proposed digests in an abstract interpreter. The experiments we conducted on a set of hand-crafted examples using these constructs are discussed in Section 7.

2

Digest-Driven Data Race Detection

At a high level, digest-driven data race detection [26] proceeds in two phases. First, an abstract interpreter propagates abstract program states indexed by digests, compact summaries of the execution history observed by the current 4

While may happen concurrently is perhaps the more accurate term, we use may happen in parallel for consistency with the literature on MHP analysis.

4

D. Bund, J. Erhard, M. Petter, and M. Schwarz

thread, such as its thread id, currently held locks, or completed synchronization events. Several digests, each tailored to a different aspect of concurrency, can be active simultaneously and jointly index the abstract states. Whenever the analysis reaches a shared-memory access, it records the access together with its digest. Second, the race detector considers pairs of accesses that may refer to the same memory location and of which at least one is a write. It applies a may-happen-in-parallel predicate to each active digest: if any one of them establishes from the aspect of the histories it records that the accesses cannot occur concurrently, the pair is discarded; otherwise, it is reported as a potential data race. Thus, digests provide the concurrency information used both to partition abstract states during the analysis and to rule out infeasible races afterward. We next introduce the local trace semantics underlying the digest framework, and formally define digests and the may-happen-in-parallel predicate. The local trace semantics precisely describes concurrent programs while abstracting away irrelevant details such as the order of local actions of independent threads, which are differentiated in an interleaving semantics. It has served as the justification for thread-modular analyses and the digest framework. Observable and observing actions play a key role: they may be ordered relative to actions of other threads. Previous work fixed observing actions to arity two, so features such as pthread once or barriers could not be expressed. We directly present our generalization to observing actions of arbitrary arity. Previous work encoded atomic global accesses using cumbersome atomicity mutexes. We instead allow operations to be both observable and observing, avoiding atomicity mutexes. 2.1

Local Trace Semantics

A program is a set of labelled control-flow graphs (CFGs), one for each thread entry point. Let N be the CFG nodes (program points), Act the actions, and E ⊆ N × Act × N the labelled CFG edges. Program text can be translated into this representation using standard compiler techniques. A local trace encodes the history of one ego thread — the thread whose perspective is taken — and the parts of other threads’ histories it can know. The knowledge comes from observing actions, which observe observable actions of other threads. Examples include locking (observing), unlocking (observable), and global-variable accesses (both). Table 1 summarizes observing and observable actions. Further, there are local actions (neither observing nor observable). A local trace contains one action-interleaved configuration sequence per appearing thread. Each sequence follows a path through the CFG and is locally consistent: its local-variable reads, writes, and taken guards agree [24]. This sequence is the thread’s swim-lane, ordered by the program order →po . For each non-main thread, a →c edge connects its create action to the first node of its swim-lane. Observing and observable actions induce further dependencies between configurations, possibly across threads, ensuring global consistency. For example—given mutex m from the set of mutexes S—there is a dependency →m from an unlock(m) to the next lock(m) operation, where each unlock of m (and the initialization action) has at most one outgoing edge →m and each

Static Data Race Detection Off The Beaten Path

5

Table 1. Observable and observing actions for primitives addressed in this paper. Feature

Observable Action

Observing Action

Access to a global Mutexes Joining Barriers pthread once

g=x/x=g unlock(a) return x barrier N record(b) endO(o) / initO(o)

g=x/x=g lock(a) x′ =join(x′′ ) barrier N check(b) startO(o)

initMT

create(w1)

→g create(w2)

g=2

barrier 3 record(b) →g

→c

barrier 3 record(b) →c

→b barrier 3 check(b)

x=g

→b →b barrier 3 record(b)

Fig. 2. Stylized local trace for Figure 1 with ego thread w1, assuming the first step of compute(g, arg) is storing g into x. Black arrows indicate the order of configurations within threads, red arrows indicate the order induced by accesses to g. Green arrows indicate the barrier order from the recorded arrivals at b to the check, blue arrows the order between a configuration creating a new thread and its first configuration.

lock has exactly one incoming edge →m (for the first lock, this edge originates at the endpoint of a special observable action initMT5 ). Thus, mutex operations are totally ordered, so at most one thread holds a mutex at a time. Likewise, a →g edge connects each access to global g to the next, encoding atomic global accesses. We revisit its relation to race reporting at the section’s end. In a local trace, then, – Each swim-lane is locally consistent; – Each auxiliary order (e.g., creation order →c and mutex orders →m ) meets its requirements; – The transitive closure of the combined program and auxiliary orders is acyclic, with a least element representing the main thread’s initial configuration and a maximal element. The maximal element is the ego thread’s last configuration, ensuring that the local trace represents one thread’s perspective. Figure 2 shows an example representation for a local trace of the program in Figure 1 with ego thread w1. Let T denote the program’s local traces, defined inductively later. For now, let init ⊂ T contain the initial local traces, each consisting only of the main thread’s initial configuration. Given a local trace t and a CFG edge e = (u, act, v) 5

This program-start action executes first and is observed when a mutex is first locked or a global first accessed. We elide this purely technical action henceforth.

6

D. Bund, J. Erhard, M. Petter, and M. Schwarz

where act is not observing, we define the semantics by a function JeK(t) : T → (T opt) which either returns Some t′ if t can be extended to a new local trace t′ by executing act along e, or None otherwise, e.g., if t ends in a program point u′ ̸= u. For k-ary observing actions act, we define the semantics using a function JeK(t0 , . . . , tk−1 ) : T k → (T opt) which returns the resulting local trace if the provided local traces can be combined into a new local trace.6 If JeK(t0 , . . . , tk−1 ) = Some t′ , then t0 , . . . , tk−1 are compatible w.r.t. the edge e and each other. Otherwise, they are incompatible. For example, J(u, lock(a), v)K t0 t1 returns Some t′ if t0 ends in u and t1 ends in an unlock(a) action and taking the union of these two local traces and adding an edge →a from unlock(a) to the newly introduced successor node of lock(a) yields a new local trace t′ . Otherwise, it returns None. There is also a function new : N → N → T → (T opt), where new u u1 t = Some t′ computes the initial local trace of the new thread, if there is an edge (u, create u1 , u′ ) in the CFG and t ends in u1 , and None otherwise. The set T is the least fixpoint obtained by applying J·K and new to init and to traces generated along the way. For abstract interpretations, an equivalent constraint-system view is more useful. We use variables (unknowns) [u] for each program point u ∈ N and [act] for observable actions act. The resulting constraint system then takes the following form: [u0 ] ⊇ init [act] ⊇ J(u1 , act, u2 )K([u1 ])

[u2 ] ⊇ J(u1 , act, u2 )K([u1 ])

(for (u1 , act, u2 ) ∈ E, act observable) (for (u1 , act, u2 ) ∈ E, act not observing)

[u2 ] ⊇ J(u1 , act, u2 )K([u1 ], [act0 ], . . . , [actk−2 ]) (for (u1 , act, u2 ) ∈ E, act of arity k, act0 . . . actk−2 observed by act)

[u′ ] ⊇ new([u1 ], u1 , u′ )

(for (u1 , x = create u′ , u2 ) ∈ E) (1) where u0 is the main thread’s initial program point and the functions J·K and new are lifted point-wise to sets of local traces. For an edge e with an action of arity k and sets (Ti , 0 ≤ i < k of local traces we define JeK(T0 , . . . , Tk−1 ) := S {t′ } if JeK(t0 , . . . , tk−1 ) = Some t′ . t0 ∈T0 ,...,tk−1 ∈Tk−1 ∅ otherwise In Eq. (1), observable-action edges have two constraints. One propagates traces to the CFG successor unknown; the other records them in the observable action unknown. In the concrete semantics, the right-hand sides for both are identical. We leave local actions unspecified as our approach is parametric in them. Data Races. Since local trace semantics totally orders all accesses to a global g via →g edges, its use for data-race detection may seem surprising. Schwarz and Erhard [26] show that it is possible: bidirectional trace compatibility coincides with the intuitive notion of two accesses to a global being unordered. 6

Thus, successor computation is deterministic; nondeterminism can instead be encoded by multiple CFG edges. We use the curried version of J·K interchangeably.

Static Data Race Detection Off The Beaten Path

7

Definition 1. Traces t0 and t1 ending in nodes u0 and u1 with outgoing edges (u0 , act0 , u′0 ) and (u1 , act1 , u′1 ) where act0 and act1 are accesses to the same global variable, are bidirectionally trace compatible, if, with appropriately lifted JeK, ∃t′ ∈ T : None ̸= J(u0 , act0 , u′0 )K(t0 , J(u1 , act1 , u′1 )K(t1 , t′ ))∧ None ̸= J(u1 , act1 , u′1 )K(t1 , J(u0 , act0 , u′0 )K(t0 , t′ )).

This means that the accesses can immediately follow each other in either order, matching the intuitive notion of being unordered. Proposition 1. Two accesses to a global variable g are racy in the intuitive sense if and only if at least one is a write and traces t0 and t1 ending in the respective CFG predecessors exist, s.t. they are bidirectionally trace compatible. Proof. Similar to [26, Theorem 1]; see Appendix B. 2.2

⊔ ⊓

Digests and Digest-Driven Data Race Detection

Digests [24, 25, 28] abstract thread histories and can refine abstract interpretations of concurrent programs. They exploit that some thread histories are incompatible, a notion transferable from local traces to digests. Let A be the set of digests. αA maps a local trace t to its digest αA t ∈ A. 7 We require digests to be computable inductively. For the initial set of digests at the program start, we define init♯A = {αA t | t ∈ init}.

(2)

♯

Further, we introduce a digest counterpart Ju, actKA : Ak → (A opt) of the semantics Ju, act, vK inheriting its arity from the concrete semantics but operating on digests instead of traces. We call these functions right-hand side functions. More concretely, for an edge e = (u, act, v) we demand ∀t0 , · · · , tk−1 ∈ T ˆ Ju, actK♯ (αA t0 , · · · , αA tk−1 ) map αA (JeK(t0 , · · · , tk−1 ))⊑ A

(3)

♯ ˆ ∀t ∈ T : map αA (new t u u1 )⊑new A (αA t) u u1

(4)

where αA is mapped over the trace option returned by JeK(t0 , · · · , tk−1 ), and ˆ is the partial order on A opt with None as bottom and all other elements ⊑ ♯ incomparable. Equation (3) says that J·KA soundly overapproximates J·K. For newly created threads, a function new♯A : A → N → N → A opt returns the digest of a thread starting at u1 , created at u by a thread with digest A. We demand that new♯A soundly abstracts new:

If the thread calling create has a successor digest, then new♯A must return a digest for the created thread: ♯

∀A ∈ A : Ju, x = create(u1 )KA (A) ̸= None =⇒ new♯A A u u1 ̸= None Digests satisfying (2) to (5) are admissible. 7

We denote by γA A = {t | αA t = A} the concretization function for a digest.

(5)

8

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Digest-Driven Abstract Interpretation. An analysis can be refined using any admissible digest. We quickly present the requirements for an analysis. An analysis constraint system is obtained from the concrete constraint system by replacing sets of traces with an analysis domain and concrete transfer functions with abstract ones. Let D be the abstract domain used by the analysis, which forms a complete lattice with operations join ⊔ and meet ⊓. A monotonic function γD : D → 2T provides the concretization of a given domain element. The analy♯ sis must define abstract transfer functions J·K , as well as abstract versions new♯ ♯ ♯ and init of new and init. Given soundness of J·K , new♯ , and init♯ w.r.t. their con♯ crete counterparts, related by γD , and the monotonicity of J·K and J·K, it follows that the concretization of a solution of the analysis constraint system is greater than the least solution of the concrete constraint system (see [25, Theorem 1]). When refining an analysis with a digest, the constraint system is adapted by splitting unknowns according to digests, yielding a constraint system of form: (for A0 ∈ init♯A )

[u0 , A0 ] ⊒ init♯ ♯

[act, A′ ] ⊒ J(u1 , act)K ([u1 , A]) ♯

[u2 , A′ ] ⊒ J(u1 , act, u2 )K ([u1 , A])

(for (u1 , act, u2 ) ∈ E, act observable, ♯ Some A′ = Ju1 , actKA A)

(for (u1 , act, u2 ) ∈ E, act not observing, ♯ Some A′ = Ju1 , actKA A) ♯ [u2 , A′ ] ⊒ J(u1 , act, u2 )K ([u1 , A1 ], [act0 , A2 ], . . . , [actk−2 , Ak ]) (for (u1 , act, u2 ) ∈ E, act of arity k, act0 . . . actk−2 observed by act, ♯ Some A′ = Ju1 , actKA (A1 , A2 , . . . Ak ))

[u′ , A′ ] ⊒ new♯ ([u1 , A], u1 , u′ )

(for (u1 , x = create u′ , u2 ) ∈ E, Some A′ = new♯A A u1 u′ )

Proposition 2. Refining a sound abstract interpretation of a concurrent program with an admissible digest yields a sound abstract interpretation. Proof. By giving a digest-refined concrete semantics and showing that soundness of the original abstract interpretation w.r.t. the original semantics carries over to the refined setting. See Appendix B for details. ⊔ ⊓ As examples, we consider the lockset digest, which tracks each thread’s currently held locks (see Figure 3), and the thread id digest for dynamically created threads: Schwarz et al. [28] propose a digest computing thread id s for pthreads. It identifies threads by the sequence of create edges involved in their creation: the main thread receives main, a thread it creates along edge e receives main · e, and so on. To account for cycles in the creation history caused by recursively creating threads or threads being created in a loop, non-definite thread id s are used. For details, see [28]. In the rest of the paper, we use generic thread id s with the following assumptions. A thread id is information that remains constant for all operations of a given concrete thread and can be projected from a digest A1 by πtid : A1 → TID. We further assume the existence of functions:

Static Data Race Detection Off The Beaten Path

9

( A = 2S None if a ∈ S0 ♯ J , lock(a)KA (S0 , S1 ) = init♯A = {∅} Some (S ∪ {a}) otherwise 0 ( new♯A S u1 = Some ∅ None if a ̸∈ S J , unlock(a)K♯A S = Ju, actK♯A (S0 , · · · , Si ) = Some S0 Some (S \ {a}) otherwise (other edge (u, act, v)) Fig. 3. Right-hand sides for lockset digest [25], generalized to our setting. Underscores serve as wildcards that do not bind the matched value.

– unique : TID → Bool checking whether, in any execution, at most one concrete thread can have this abstract thread id. – must anc : TID → 2TID returning the set of must ancestors, i.e., threads that must have been involved in the creation of the current thread. – may create : A1 → 2TID returning the may-created thread id s, i.e., childthread id s the ego thread may have created given a digest. The product of admissible digests is also an admissible digest [25]. This allows for a modular design where digests tracking different aspects of the history can seamlessly be combined during an analysis. May-Happen-In-Parallel Predicate. Digests support reasoning about the temporal separation aspect of data races [26]. For two accesses to race, they must potentially happen concurrently: by Proposition 1, there must be bidirectionally trace-compatible traces ending just before them. Thus, compatibility of digests, an abstraction of local-trace compatibility, can exclude data races. Two digests A0 and A1 are compatible with an edge e and each other if there are traces t0 and t1 with these digests that are compatible with e and each other. Thus, if two digests are not bidirectionally compatible, the corresponding traces are not either. This yields a first definition of a may-happen-in-parallel predicate ||?e1 ,e2 : A → A → {false, ⊤} for checking whether two accesses to a variable may race, where e1 and e2 are the CFG edges in question. We outline the detailed requirements for ||?e1 ,e2 in Appendix A. When edges are clear or irrelevant, we write ||? . The answers form the lattice false ⊑ ⊤. For product digests, answers can be combined using meet (⊓). For thread id s, the ||? definition arising from bidirectional digest compatibility is maximally precise. However, this is not the case for all digests. For instance, with the lockset digest, two actions with overlapping locksets cannot run concurrently, so the corresponding concrete accesses cannot race. However, bidirectional digest compatibility cannot infer this, because overlapping locksets need not prevent the respective accesses to a global g from directly following each other in the →g order. Thus, one may instead provide a more precise ||? and justify it directly w.r.t. bidirectional trace compatibility. We generalize ||?e1 ,e2 to show that two arbitrary-action edges e1 , e2 cannot happen in parallel: introduce a fresh global variable and replace the actions by writes to it, yielding edges e′1 , e′2 . Then A1 ||?e1 ,e2 A2 is defined as A1 ||?e′ ,e′ A2 . 1

2

10

D. Bund, J. Erhard, M. Petter, and M. Schwarz

// Library file pthread_once_t once; schmilblick* dev; // Some device void init_lib() { dev = malloc(size_of(schmilblick)); init_schmilblick(dev); } void maluba(){ // Ensure the library is initialized pthread_once(once,init_lib); assert(dev != NULL); // ... }

// Main file void *t1(void *arg) { maluba(); // ... return NULL; } int main() { pthread_t t; pthread_create(&t, t1, NULL); maluba(); // ... }

Fig. 4. Pthread program using pthread once

Race Detection. Schwarz and Erhard [26] give a data race detection algorithm using digests. First, one performs digest-driven abstract interpretation, collecting digests associated with accesses. Then, for each shared memory location, one iterates over all access pairs. For accesses at edges e1 and e2 with digests A1 and A2 , a potential race is flagged if at least one access is a write and A1 ||?e1 ,e2 A2 = ⊤.

3

Synchronization via pthread once

Pthreads offers a mechanism for executing code at most once. This enables resource initialization before thread access, such as opening a shared log file or database connection. Application developers can place such code in main, but library developers do not control main and instead rely on pthread once [2]. It provides a type for control variables (which we assume are from set O) and a function pthread once(o,f) which executes f and sets o if it is unset, and otherwise does nothing. The system makes running f and setting o appear atomic. Consider the program in Figure 4. init lib must allocate and initialize the device before any other library function runs. pthread once ensures that init lib is called exactly once and that the device is initialized before use. pthread once is often overlooked by static analyzers or abstracted very crudely. With digests, it can be handled precisely without complicating the underlying analysis; all handling happens inside the digest. This excludes two race classes: within the called function and between initialization and later code. Extension of the concrete semantics. We introduce a new observable action initO(o) to initialize a control variable o at program start8 and compile pthread once(o,f) to a sequence calling startO(o), branching on ran(o), executing the inlined code from f if ran(o) is false, and finally performing endO(o). Here, initO(o) and endO(o) are observable, while startO(o) is observing, analogous to initMT/unlock(a) and lock(a) for mutex a. The once order →o follows 8

Unlike library developers, a whole-program analyzer can conceptually insert helper code at program start, so this action does not negate the need for pthread once.

Static Data Race Detection Off The Beaten Path

11

the mutex-order requirements main : t1 : initO(o); // ... from Section 2.1. The actions create(t1); startO(o); // ... if (!ran(o)) Pos(ran(o)) and Neg(ran(o)) startO(o); dev = malloc(42); guard whether the code assoif (!ran(o)) endO(o); dev = malloc(42); ciated with pthread once is endO(o); // ... to be executed: the former reassert(dev != NULL); assert(dev != NULL); turns a local trace only when endO(o) appears in the trace, Fig. 5. Program highlighting how pthread once is and the latter only when it decomposed into individual steps. does not.9 The program in Figure 5 corresponds to the one in Figure 4 after abstracting away details and expressing pthread once as above. A digest for this feature (Figure 6) may then track two sets in a tuple (A, C): – A set A of active control variables, i.e., those for which the ego thread is currently inside the section between startO(o) and endO(o). – A set C of completed control variables, i.e., those for which the associated fragment has surely been run, as a call to endO(o) was observed. The guards Pos(ran(o)) and Neg(ran(o)) check whether o has already completed, i.e., whether it is in C. startO(o) adds o to the active set, and endO(o) moves it from the active to the completed set. ||? can then be defined as: ( false if (A ∩ (A′ ∪ C ′ ) ̸= ∅) ∨ (A′ ∩ (A ∪ C) ̸= ∅) ? ′ ′ (A, C) || (A , C ) = ⊤ otherwise, i.e., accesses may not race when a control variable is active during both accesses, or active in one and completed in the other. Example 2. Consider again the program in Figure 5. An analysis using the digest from Figure 6 succeeds in establishing race freedom. ⊓ ⊔ 9

Recursively calling pthread once(o,f) is not conclusively specified in the standard; here, we decided to go for the behavior of glibc, which deadlocks upon such calls.

A = 2O × 2 O init♯A = {(∅, ∅)} new♯A (A, C) u u1 = Some (∅, C) ♯ J , Pos(ran(o))K A (A, C) = (

♯ J , startO(o)K A (A0 , C0 ) (A1 , C1 ) = ( Some (A0 ∪ {o}, C0 ∪ C1 ) o ̸∈ A0 None otherwise J , endO(o)K♯A (A, C) = Some (A \ {o}, C ∪ {o})

♯ J , Neg(ran(o))K None if o ̸∈ C A (A, C) = ( None if o ∈ C Some (A, C) otherwise ♯ Some (A, C) otherwise Ju, actKA (A, C) · · · (Ai , Ci ) = Some (A, C) (other edge (u, act, v))

Fig. 6. Right-hand sides for excluding races based on pthread once.

12

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Proposition 3. The digest given above is admissible, and its predicate ||? sound. See Appendix C for the proof (by contradiction) and an extended digest making the analysis of global variables more precise.

4

Synchronization via Barriers

Pthreads provides barriers: after initialization by calling pthread barrier init(b, c) for a barrier b and capacity c ∈ N+ , callers to pthread barrier wait(b) block until c threads have called it, at which point all waiters are unblocked. Figure 1 shows a barrier example whose pthread barrier wait(b) calls may all happen in parallel. In fact, this always needs to be the case, as any call to pthread barrier wait(b) happening after another call has returned, cannot contribute to reaching the required capacity. The predicate ||? also detects stuck executions when fewer than c − 1 other pthread barrier wait(b) calls may happen in parallel. Passing a barrier reveals cross-thread information that excludes some races. Extension of the concrete semantics. Let B be a set of barriers. For presentation, we initially assume static capacities (eliminating pthread barrier init) and replace each pthread barrier wait(b) with barrier N record(b); barrier N check(b), where N ∈ N+ is b’s capacity. The action barrier N record(b) is non-blocking and observable, i.e., the local trace ending in it is recorded at the corresponding unknown. The action barrier N check(b) is observing and N -ary, incorporating local traces stored at the unknown corresponding to barrier N record(b), i.e., those ending in that action.10 Figure 2 shows an example local trace. By construction of the constraint system, for JeK(t0 , . . . , tN −1 ) for an edge e = (u, barrier N check(b), v), t0 is a local trace ending in u with last action barrier N record(b), and the other N −1 local traces provided as an argument also end in barrier N record(b), as that is the action observed by the check action. The call yields Some t′ only if its arguments are distinct and their union, augmented with dependency edges from the record endpoints to the check endpoint, is a local trace. For each barrier b, the barrier order →b goes from nodes with an incoming edge barrier N record(b) to those with an incoming edge barrier N check(b); call these sets B + and B − , respectively. Each B + node has at most 1 outgoing →b edge, while B − node has exactly N incoming →b edges, including one from the control-flow predecessor, i.e., the thread passing the barrier was involved in the barrier being passed. This order then forms part of the causality order of a local trace. Consider the N subtraces ending at B + nodes that directly →b -precede a B − node. None of these subtraces may contain any of the relevant calls to barrier N record(b). This ensures that all N calls happened in parallel. Before deriving a digest tracking information about barriers, we first observe that for any digest that provides the predicate ||? for checking for data races and does not track information about barriers, i.e., is unaffected by executing actions ♯ barrier N record(b) and barrier N check(b), a definition of J , barrier N check(b)KA

10

This uses our generalization to higher-arity observing actions.

Static Data Race Detection Off The Beaten Path

13

can be given that detects some instances where the execution must become stuck: ♯ J , barrier N check(b)KA (A0 , . . . , AN −1 ) = ( Some A0 if ∀i, j ∈ [0, N − 1] : i ̸= j =⇒ Ai ||? Aj = ⊤ None otherwise This uses the predicate ||? to check whether the N calls to barrier N record(b) can all happen in parallel. When this is not the case, the execution must become stuck, and None is returned, denoting unreachability. The predicate thus turns out to be not only useful when considering whether accesses can happen in parallel, but also when considering richer synchronization primitives. Example 3. Consider Figure 1 and assume that the developer has, by mistake, surrounded calls to pthread barrier wait(b) with locking and unlocking of mutex m. Then, one thread reaches the call to pthread barrier wait(b) while holding m. However, it will not release m until the barrier is passed, and the other threads do not call pthread barrier wait(b) until they have acquired m. The execution deadlocks. With the lockset digest from [26] with the definition of ||? returning false when locksets overlap, the analysis will detect this as {m}||? {m} = false. ⊔ ⊓ Showing certain accesses unreachable may improve the precision of race detection. If a digest tracks thread id s, we can define a more precise digest that excludes more races by tracking barriers passed by the current thread and observed barrier actions of other threads. If, for two accesses, one thread knows that the other has passed a barrier that it has not yet passed, the accesses are ordered w.r.t. each other and thus not bidirectionally compatible and not racy. The new digest is the product of the original digest A1 and two components11 : – a set R ⊆ B of barriers for which the current thread has called barrier N record(b) – a map O : TID → 2B from thread id s to sets of barriers for which the respective thread has been observed to have called barrier N record(b). The corresponding right-hand sides for the digest are given in Figure 7 in terms of those for A1 . The predicate then is given by: (A0 , R0 , O0 ) ||? (A1 , R1 , O1 ) =   false if (unique (πtid A0 ) ∧ O1 (πtid A0 ) ̸⊆ R0 ) = (A0 ||?A1 A1 ) ⊓ ∨(unique (πtid A1 ) ∧ O0 (πtid A1 ) ̸⊆ R1 )   ⊤ otherwise On top of the predicate for the base digests, this exploits the fact that if A0 is unique, any of its actions that have been observed by the other thread must already have happened for the accesses to potentially happen concurrently. Example 4. Consider again Figure 1 and assume a digest identifies all threads as unique12 and assigns them id s main, w1, and w2. The access in main happens before calling pthread barrier wait(b), and has digest (A0 , ∅, {}); the worker accesses 11

The tracking of separate components for R and O is to simplify presentation here: Whenever the thread id in A is unique, R can be reconstructed from O. 12 This is, e.g., the case for the digest-based thread id s abstracting creation history [28].

14

D. Bund, J. Erhard, M. Petter, and M. Schwarz

A = A1 × 2B × (TID → 2B ) init♯A = {(A1 , ∅, ∅) | A1 ∈ init♯A1 } ( Some (A′ , ∅, O) if new♯A1 A u u1 = Some A′ new♯A (A, R, O) u u1 = None otherwise ♯ barrier N check(b)KA ((A0 , R0 , O0 ), . . . , (AN −1 , RN −1 , ON −1 )) = J , S ?   Some (A0 , R0 , i Oi ) if ∀i, j ∈ [0, N − 1] : (i ̸= j =⇒ Ai || Aj )∧ (unique (πtid Ai ) =⇒ Oj (πtid Ai ) ⊆ Ri )   None otherwise J , barrier N record(b)K♯A (A, R, O) = Some (A, R ∪ {b}, O ⊕ {(πtid A) 7→ (O (πtid A)) ∪ {b}}) ♯ J , actK ( A ((A0 , R0 , O0 ),S. . . , (AN −1 , RN −1 , ON −1 )) = Some (A′ , R0 , i Oi ) if J , actK♯A1 (A0 , . . . , A1 ) = Some A′ None otherwise (other n-ary action)

Fig. 7. Barrier digest where ⊕ denotes updating a map, missing bindings are assumed to be ∅, and the union of maps is defined pointwise per binding.

have digests (Aj , {b}, {main 7→ {b}, w1 7→ {b}, w2 7→ {b}}) for some Aj , where we omit empty bindings. As πtid A0 = main, unique main holds but {b} ̸⊆ ∅, the write in main happens before any of the reads, and race-freedom is shown. ⊓ ⊔ Proposition 4. The digest given above is admissible, and its predicate ||? sound. The proof is by contradiction; see Appendix D. This digest generalizes straightforwardly to tracking how often barriers have been waited for, possibly stopping exact bookkeeping at a fixed constant k to avoid a blowup. Conversely, for a more tractable analysis, one can switch to an abstract digest to avoid keeping track of exact sets, along the lines of [25]. Remark 1. Our implementation supports dynamic barrier capacities and pointerbased accesses. Barriers may also be used for inter-process communication, but since the Goblint framework does not support process-level concurrency, our implementation soundly and coarsely treats such barriers as no-ops.

5

Synchronization via Mutexes and Creation Orders

While previous sections covered features that are often completely unhandled, here we deal with complex patterns combining thread creation and mutexes: Creating threads while holding a mutex can simulate barriers on platforms lacking them. Also, then, worker threads do not have to wait for one another: Example 5. In Figure 8, main creates workers i1 and i2 while holding m. Each worker initializes, then immediately acquires and releases m. These locks occur only after main unlocks m, so worker accesses to g follow main’s access and cannot race. Notably, i1 need not wait for i2 to reach the lock.

Static Data Race Detection Off The Beaten Path int g = 0; pthread_mutex_t m;

int main() { // Worker threads pthread_t i1, i2;

void *worker(void *arg) { // Worker Initialization...

pthread_mutex_lock(&m); pthread_create(&i1, NULL, worker, NULL); pthread_create(&i2, NULL, worker, NULL); g++; // Initialization code

pthread_mutex_lock(&m); pthread_mutex_unlock(&m); int f = compute(g, arg); // ... return NULL; }

15

pthread_mutex_unlock(&m); return 0; }

Fig. 8. Access to g in main must happen before accesses in worker threads.

For accesses in thread i0 and a thread i1 it created, the following conditions rule out conflicts via mutex m. At the first access, we require that 1. i1 was created in i0 , ensuring i0 is its ancestor. This check matters because an ancestor of i0 might otherwise have created i1 , enabling races. 2. At all of those creations, m is locked—c.f. lockset digest (Figure 3). 3. m was not unlocked after any such creation. Note that i1 does not need to be a child of i0 , but can be more generally a descendant. So, we account for transitive creations of i1 , enhancing the precision. At the second access, we record which threads have locked each mutex. We can exclude a race if a lock of m has happened at some point after the creation in i0 in the created thread or—for the same reason as above—one of its descendants. If m was locked in iH , this is the case if i0 must be an ancestor of iH . We describe a suitable digest in Appendix E.

6

Digests for Creation Locksets

The pattern described in Section 5 is not the only one where thread creations with mutexes held can ensure mutual exclusion. This time, we are interested in programs where a mutex m is held in i0 throughout the entire execution of a descendant thread i1 . In consequence, i1 is protected in some way by m. This may sometimes be useful: Imagine, e.g., that a thread needs to do two expensive computations in parallel while having exclusive access to a global. Then, it may spawn a new thread while holding the protecting mutex to do one part of the work, while performing some other work in another task. Before releasing the mutex again, the worker thread is joined again. While this is probably more common for programming languages such as Go, where thread creation is cheap, it applies just as well to C programs, as we show in the next example: Example 6. Consider the program given in Figure 9. Throughout the entire execution of work, the mutex m is locked. As m is also in the lockset at the access to g in t1, this access cannot race with the one in work. Note that it is important to record that a mutex m is locked in the creator thread i0 and held throughout the execution of a descendant thread i1 , as it

16

D. Bund, J. Erhard, M. Petter, and M. Schwarz

int g = 0; pthread_mutex_t m ; pthread_t i1, i2;

int main() { pthread_create(&i1, NULL, t1, NULL); ... pthread_mutex_lock(&m);

void* t1(void* arg) { pthread_mutex_lock(&m); g++; // not racing! pthread_mutex_unlock(&m); return NULL; } // main holds m throughout work void* work(void* arg) { // Expensive computations g = ...; // not racing! return NULL; }

// Two expensive computations // some of it happens in work // work created while m is locked pthread_create(&i2, NULL, work, NULL); // no unlock of m while work running pthread_join(i2, NULL); pthread_mutex_unlock(&m); return 0; }

Fig. 9. Creation Locksets: Mutex m protects accesses to global—even though work never acquires it.

does not protect i1 from accesses happening in i0 . To detect that i1 is protected from i0 with m, we propose the following conditions: 1. i1 was transitively created in i0 , ensuring i0 must be an ancestor of it. We require the latter condition for the same reason as given in Section 5—there should be no alternative way of creating i0 other than via i1 . 2. At all of those creations, m must be locked, as recorded by the lockset digest. 3. There exists no unlock of m while i1 may run in parallel. For the last point, one can compute the id s of the descendant threads running in parallel by determining all threads that were transitively created from the current thread and subtracting threads that were joined back. Using the thread id digest, we obtain the former. For the latter information, we use the join digest suggested by Schwarz and Erhard [25]. Appendix F gives a digest for checking the conditions above.

7

Experiments and Benchmark Set

We enhanced the Goblint [23] static analyzer to support pthread once, barriers, and complex interactions between thread creation and mutex locking. The implementations deviate slightly from the presentation here: they support Pthreads directly rather than idealized primitives and use abstract digests in the sense of [25]. For thread-creation and mutex-locking interactions, they use mixed flow-sensitivity [29] to compute abstract digests at global unknowns. We evaluate scalability and runtime on 60k–80k-LOC GNU Coreutils. Their size precludes ground-truth annotations, but they allow measuring the runtime impact of the new digests against a minimal baseline and the SV-Comp configuration. We ran each benchmark on Ubuntu 26.04 with a 2.5 GHz Intel Core i7-11700, a 5-minute timeout, and a 20 GB memory limit. Table 2 shows the cost of the enhanced synchronization features. It is most pronounced for the lockedcreation feature. For df, locked creation handling adds 30.5% to the baseline

Static Data Race Detection Off The Beaten Path

17

Table 2. Runtime comparison. Runtime in seconds. Benchmark LOC Baseline cksum cp cut dd df du nohup ptx tail Average

68k 75k 69k 72k 70k 70k 68k 71k 72k

Once (∆%) Barriers (∆%)

Locked (∆%)

1.00 1.02 (+2.0%) 1.04 (+4.0%) 1.13 (+13.0%) 11.86 12.45 (+5.0%) 12.36 (+4.2%) 14.44 (+21.8%) 1.79 1.85 (+3.4%) 1.84 (+2.8%) 2.10 (+17.3%) 2.68 2.77 (+3.4%) 2.74 (+2.2%) 3.30 (+23.1%) 13.86 14.55 (+5.0%) 14.65 (+5.7%) 18.09 (+30.5%) 9.13 9.72 (+6.5%) 9.81 (+7.4%) 11.27 (+23.4%) 1.97 1.95 (-1.0%) 1.91 (-3.0%) 2.25 (+14.2%) 4.20 4.49 (+6.9%) 4.45 (+6.0%) 5.11 (+21.7%) 3.44 3.62 (+5.2%) 3.68 (+7.0%) 4.18 (+21.5%) +4.0%

+4.0%

+20.7%

time. However, across ≈ 30,000 SV-Comp benchmarks enabling the enhanced synchronization features increased total runtime by ≈ 2%, which is negligible. We also compare our implementation with other static analyzers. We gathered 90 small benchmarks, 20–70 lines of code each, testing the correct handling of each of our four features: 28 pthread once, 26 barriers, 18 creationLockset, and 18 descendantLockset tests. Each file contains one focused test annotated with the expected ground truth and sometimes motivated by a real-world use case. Our main goal is to determine whether analyzers can correctly certify the absence of data races in the presence of these features. A false positive is an unexpected warning; avoiding them is crucial for the acceptance of static analyzers in practice. Conversely, a false negative is a missed race; even one compromises soundness. We encode the desired behavior as SV-Comp verdicts. We compared our implementation with CPAChecker [1], Dartagnan [17], UGemcutter [13], ESBMC-kind [7], and RacerF [5]. We also wanted to check whether soundness concerns about [19] carry over to the implementation, but the code is unavailable and the authors did not respond to inquiries. Table 3 summarizes the experiment, detailed in Appendix G. The benchmark set reveals no false positives or false negatives in our implementation. Since our implementation builds on abstract interpretation, it may produce false positives on other programs with the considered features. All tools treat barriers in a sound way (which can be trivially achieved by not providing specific handling), they however do not exploit the information completely to reduce false positives. Dartagnan and UGemcutter avoid false negatives but return ERROR and UNKNOWN, respectively, when barriers or pthread once are present. For pthread once, CPAChecker, RacerF, and ESBMC-kind miss races, but do not produce false positives except for RacerF. All tools miss races in the creationLockset and descendantLockset categories, demonstrating unsound behavior. Dartagnan, ESBMC-kind, and UGemcutter produce no false positives. We hope contributing these tests to Sv-Comp will encourage tools to support these features and spur competition.

18

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Table 3. Capability of static analyzers to establish data-race freedom in the presence of enhanced synchronization features. The table reports the number of false negatives ( - , unsound) and false-positive race warnings ( + ) for each tool. Tool

pthread once - / +

barrier wait - / +

creationLockset - / +

descendantLockset - / +

0/0 9/0 0/0 0/0 6/0 3/7

0/0 0 / 12 0/0 0/0 0/4 0/7

0/0 2/1 3/0 2/0 5/0 1/3

0/0 2/0 3/0 2/0 3/0 2/3

Goblint (this work) CPAChecker Dartagnan Ultimate Gemcutter ESBMC-kind RacerF

8

Related Work

Local traces and digests were proposed in a series of papers on thread-modular value analyses [24, 25, 27, 28]. Recent work [26] re-uses them for race detection. We generalize both to cover more synchronization mechanisms, and show that ||? can check whether two actions may run concurrently, which we use for barriers. Terauchi [37] presents an approach for framing race-freedom of programs as a typing problem, which in turn is solved using rational linear programming. It covers classical lock-based synchronization and mechanisms rarely supported by static analyses, including signaling, semaphores, and read-write locks. However, the approach differs from ours both in the used techniques, type-checking rather than abstract interpretation, and in the considered synchronization mechanisms. Barriers. Barriers have been widely studied [14, 15, 21, 22], including analyses of OpenMP-style barriers [18, 35, 36]. In OpenMP, all threads in a team share the same code and must arrive at the syntactically same barrier, so code before a barrier cannot run in parallel with code after it. This does not carry over to Pthreads: different syntactic calls to wait may belong together, and the capacity of a barrier need not equal the number of running threads. Here, we focus on work on Pthreads-style barriers. Mittermayr and Blieberger [21] extend the use of Kronecker algebra from the static analysis of semaphores to barriers. Kokologiannakis and Vafeiadis [14] speed up stateless model checking by merging interleavings that differ only in barrier-arrival order. There, it is required that the initial capacity of a barrier is an upper bound to the number of wait calls that happen in parallel. The analysis is justified w.r.t. a execution graph semantics. Murthy et al. [22] verify (using SPIN) a distributed phaser, a synchronization construct similar to barriers, but do not analyze code using it. Le et al. [15] propose a separation-logic using bounded partial permissions to show that participating threads execute in lockstep phases separated by barriers, thereby excluding races across phases. Their approach and others [9] rely on user annotations; ours is fully automatic. Jeremiassen and Eggers [10] split executions into barrier-delimited phases to determine which sections cannot run concurrently, aiming to reduce compiler-introduced false sharing and cache misses, while Das et al. [6] do so to reduce the instrumentation overhead of dynamic approaches.

Static Data Race Detection Off The Beaten Path

19

Feature pthread once. For pthread once, missing support has been noted as a limitation [16, 30]; to our knowledge, ours is the first analysis beyond syntactic checks [32], both for race detection or static analysis more broadly. Mutexes and Creation Orders. In static analysis, research on the patterns from Section 5 is sparse. To our knowledge, only Lu et al. [19] explicitly use it to exclude races, via Segmented Thread-Sensitive Control Flow Graphs. This analysis is not justified w.r.t. a concrete semantics and is unsound on several litmus tests. They also describe mutexes held throughout descendant-thread execution, but give no analysis to detect this pattern; to our knowledge, ours is the first. Dynamic race-prediction techniques [8, 12, 31, 33] reason about ordering constraints induced by locks and other dependencies to determine which re-orderings of an observed execution are possible. This resembles our use of digests as synchronization histories to rule out parallel accesses, but the analysis problem differs substantially. Predictive analyses start from a single execution and seek to weaken its observed ordering without admitting infeasible re-orderings; our sound static analysis overapproximates all executions and must warn unless it can establish that the relevant accesses are ordered in every execution, not just those arising from re-orderings. The descendant-lockset construction establishes the same must-happen-before relationship that CP/WCP-style rules derive from lock synchronization — if a thread is known to acquire a specific mutex before another thread (in our case because the first thread is statically known to be an ancestor of the second and to hold the mutex when the descendant is created), then the release by the first thread must precede the acquire by the second thread. Unlike predictive analyses, which reason over a single trace, our analysis establishes this ordering soundly across all executions. Sulzmann and Thiemann [34] extend dynamic lockset reasoning with cross-thread critical sections, in which an event may be protected by an acquire–release pair executed by another thread when it must occur between them. This captures the same pattern as our creationLocksets: a mutex held by an ancestor throughout a descendant’s execution can protect accesses in the descendant, although it never acquires the mutex. Their analysis operates on observed executions and derives cross-thread critical sections from must-happen-before information; our contribution is a sound static abstraction establishing this protection across all executions using creation, join, thread-id, and lock-history information.

9

Conclusion and Future Work

Sound static race detection comes with strong guarantees; reducing false positives is crucial for usability. We built on digests, a framework refining threadmodular abstract interpretation, by distinguishing program points according to thread histories. While previous work cast existing techniques as digests to justify their soundness, we present novel digests for several interesting concurrency primitives that have received little to no attention in sound static race detection. Future work may apply our techniques to other concurrency bugs, such as deadlocks and termination.

Bibliography

[1] Baier, D., Beyer, D., Chien, P., Jankola, M., Kettl, M., Lee, N., Lemberger, T., Rosenfeld, M.L., Spiessl, M., Wachowitz, H., Wendler, P.: Cpachecker 2.3 with strategy selection - (competition contribution). In: Finkbeiner, B., Kovács, L. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 30th International Conference, TACAS 2024, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2024, Luxembourg City, Luxembourg, April 6-11, 2024, Proceedings, Part III, Lecture Notes in Computer Science, vol. 14572, pp. 359–364, Springer (2024), doi: 10.1007/978-3-031-57256-2_21, URL https://doi.org/10.1007/978-3-031-57256-2_21 [2] Butenhof, D.R.: Programming with POSIX threads. Addison-Wesley Professional (1993) [3] Christakis, M., Bird, C.: What developers want and need from program analysis: an empirical study. In: Lo, D., Apel, S., Khurshid, S. (eds.) Proceedings of the 31st IEEE/ACM International Conference on Automated Software Engineering, ASE 2016, Singapore, September 3-7, 2016, pp. 332–343, ACM (2016), doi: 10.1145/2970276.2970347, URL https: //doi.org/10.1145/2970276.2970347 [4] Cousot, P., Cousot, R.: Abstract interpretation: A unified lattice model for static analysis of programs by construction or approximation of fixpoints. In: POPL, pp. 238–252, ACM (1977), doi: 10.1145/512950.512973 [5] Dacı́k, T., Vojnar, T.: Racerf: Lightweight static data race detection for C code (experience paper). In: Aldrich, J., Silva, A. (eds.) 39th European Conference on Object-Oriented Programming, ECOOP 2025, Bergen, Norway, June 30 - July 2, 2025, LIPIcs, vol. 333, pp. 37:1–37:19, Schloss Dagstuhl - Leibniz-Zentrum für Informatik (2025), doi: 10.4230/LIPICS.ECOOP. 2025.37, URL https://doi.org/10.4230/LIPIcs.ECOOP.2025.37 [6] Das, M.M., Southern, G., Renau, J.: Section-based program analysis to reduce overhead of detecting unsynchronized thread communication. ACM Trans. Archit. Code Optim. 12(2), 23:23:1–23:23:26 (2015), doi: 10.1145/ 2766451, URL https://doi.org/10.1145/2766451 [7] Gadelha, M.Y.R., Ismail, H.I., Cordeiro, L.C.: Handling loops in bounded model checking of C programs via k-induction. Int. J. Softw. Tools Technol. Transf. 19(1), 97–114 (2017), doi: 10.1007/S10009-015-0407-9, URL https://doi.org/10.1007/s10009-015-0407-9 [8] Genç, K., Roemer, J., Xu, Y., Bond, M.D.: Dependence-aware, unbounded sound predictive race detection. Proceedings of the ACM on Programming Languages 3(OOPSLA), 1–30 (10 2019), doi: 10.1145/3360605, URL https://doi.org/10.1145/3360605 [9] Hobor, A., Gherghina, C.: Barriers in concurrent separation logic: Now with tool support! Log. Methods Comput. Sci. 8(2) (2012), doi: 10.2168/ LMCS-8(2:2)2012

Static Data Race Detection Off The Beaten Path

21

[10] Jeremiassen, T.E., Eggers, S.J.: Static analysis of barrier synchronization in explicitly parallel programs. In: Cosnard, M., Gao, G.R., Silberman, G.M. (eds.) Parallel Architectures and Compilation Techniques, Proceedings of the IFIP WG10.3 Working Conference on Parallel Architectures and Compilation Techniques, PACT’94, Montréal, Canada, 24-26 August, 1994, IFIP Transactions, vol. A-50, pp. 171–180, North-Holland (1994) [11] Johnson, B., Song, Y., Murphy-Hill, E.R., Bowdidge, R.W.: Why don’t software developers use static analysis tools to find bugs? In: Notkin, D., Cheng, B.H.C., Pohl, K. (eds.) 35th International Conference on Software Engineering, ICSE ’13, San Francisco, CA, USA, May 18-26, 2013, pp. 672– 681, IEEE Computer Society (2013), doi: 10.1109/ICSE.2013.6606613, URL https://doi.org/10.1109/ICSE.2013.6606613 [12] Kini, D., Mathur, U., Viswanathan, M.: Dynamic race prediction in linear time. ACM SIGPLAN Notices 52(6), 157–170 (6 2017), doi: 10.1145/ 3140587.3062374, URL https://doi.org/10.1145/3140587.3062374 [13] Klumpp, D., Dietsch, D., Heizmann, M., Schüssele, F., Ebbinghaus, M., Farzan, A., Podelski, A.: Ultimate gemcutter and the axes of generalization - (competition contribution). In: Fisman, D., Rosu, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 28th International Conference, TACAS 2022, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2022, Munich, Germany, April 2-7, 2022, Proceedings, Part II, Lecture Notes in Computer Science, vol. 13244, pp. 479–483, Springer (2022), doi: 10.1007/978-3-030-99527-0_ 35, URL https://doi.org/10.1007/978-3-030-99527-0_35 [14] Kokologiannakis, M., Vafeiadis, V.: BAM: Efficient Model Checking for Barriers. In: Echihabi, K., Meyer, R. (eds.) Networked Systems, vol. 12754, pp. 223–239, Springer International Publishing, Cham (2021), ISBN 9783-030-91013-6 978-3-030-91014-3, doi: 10.1007/978-3-030-91014-3_16, URL https://link.springer.com/10.1007/978-3-030-91014-3_16, series Title: Lecture Notes in Computer Science [15] Le, D.K., Chin, W.N., Teo, Y.M.: Verification of Static and Dynamic Barrier Synchronization Using Bounded Permissions. In: Hutchison, D., Kanade, T., Kittler, J., Kleinberg, J.M., Mattern, F., Mitchell, J.C., Naor, M., Nierstrasz, O., Pandu Rangan, C., Steffen, B., Sudan, M., Terzopoulos, D., Tygar, D., Vardi, M.Y., Weikum, G., Groves, L., Sun, J. (eds.) Formal Methods and Software Engineering, vol. 8144, pp. 231–248, Springer Berlin Heidelberg, Berlin, Heidelberg (2013), ISBN 978-3-642-41201-1 978-3-642-412028, doi: 10.1007/978-3-642-41202-8_16, URL http://link.springer. com/10.1007/978-3-642-41202-8_16, series Title: Lecture Notes in Computer Science [16] Le, Q.L., Raad, A., Villard, J., Berdine, J., Dreyer, D., O’Hearn, P.W.: Finding real bugs in big programs with incorrectness logic. Proc. ACM Program. Lang. 6(OOPSLA1), 1–27 (2022), doi: 10.1145/3527325 [17] de León, H.P., Furbach, F., Heljanko, K., Meyer, R.: Dartagnan: Bounded model checking for weak memory models (competition contribution). In: Biere, A., Parker, D. (eds.) Tools and Algorithms for the Construction

22

D. Bund, J. Erhard, M. Petter, and M. Schwarz

and Analysis of Systems - 26th International Conference, TACAS 2020, Held as Part of the European Joint Conferences on Theory and Practice of Software, ETAPS 2020, Dublin, Ireland, April 25-30, 2020, Proceedings, Part II, Lecture Notes in Computer Science, vol. 12079, pp. 378– 382, Springer (2020), doi: 10.1007/978-3-030-45237-7_24, URL https: //doi.org/10.1007/978-3-030-45237-7_24 [18] Lin, Y.: Static nonconcurrency analysis of OpenMP programs. In: Müller, M.S., Chapman, B.M., de Supinski, B.R., Malony, A.D., Voss, M. (eds.) OpenMP Shared Memory Parallel Programming - International Workshops, IWOMP 2005 and IWOMP 2006, Eugene, OR, USA, June 1-4, 2005, Reims, France, June 12-15, 2006. Proceedings, Lecture Notes in Computer Science, vol. 4315, pp. 36–50, Springer (2005), doi: 10.1007/978-3-540-68555-5_4 [19] Lu, F., Wang, X., Zeng, Q., Yuan, G., Bao, Y.: Segment-based may-happenin-parallel analysis for c programs. Concurrency and Computation: Practice and Experience 37(21-22), e70203 (2025), doi: 10.1002/cpe.70203 [20] Mauborgne, L., Rival, X.: Trace partitioning in abstract interpretation based static analyzers. In: Sagiv, M. (ed.) Programming Languages and Systems, pp. 5–20, Springer Berlin Heidelberg, Berlin, Heidelberg (2005), ISBN 978-3-540-31987-0 [21] Mittermayr, R., Blieberger, J.: Kronecker Algebra for Static Analysis of Barriers in Ada. In: Bertogna, M., Pinho, L.M., Quiñones, E. (eds.) Reliable Software Technologies — Ada-Europe 2016, vol. 9695, pp. 145– 159, Springer International Publishing, Cham (2016), ISBN 978-3-31939082-6 978-3-319-39083-3, doi: 10.1007/978-3-319-39083-3_10, URL http://link.springer.com/10.1007/978-3-319-39083-3_10, series Title: Lecture Notes in Computer Science [22] Murthy, K., Paul, S.R., Meel, K.S., Cogumbreiro, T., Mellor-Crummey, J.: Design and Verification of Distributed Phasers. In: Dutot, P.F., Trystram, D. (eds.) Euro-Par 2016: Parallel Processing, vol. 9833, pp. 405– 418, Springer International Publishing, Cham (2016), ISBN 978-3-31943658-6 978-3-319-43659-3, doi: 10.1007/978-3-319-43659-3_30, URL http://link.springer.com/10.1007/978-3-319-43659-3_30, series Title: Lecture Notes in Computer Science [23] Saan, S., Kocal, A.R., Petter, M., Holter, K., Erhard, J., Schwarz, M., Vojdani, V., Seidl, H.: Goblint: A portfolio for mixed flow-sensitive abstract interpretation - (competition contribution). In: Junges, S., Katz, G. (eds.) Tools and Algorithms for the Construction and Analysis of Systems - 32nd International Conference, TACAS 2026, Held as Part of the International Joint Conferences on Theory and Practice of Software, ETAPS 2026, Turin, Italy, April 11-16, 2026, Proceedings, Part II, Lecture Notes in Computer Science, vol. 16506, pp. 516–522, Springer (2026), doi: 10.1007/978-3-032-22749-2_26, URL https://doi.org/10.1007/ 978-3-032-22749-2_26 [24] Schwarz, M.: Thread-Modular Abstract Interpretation: The Local Perspective. Ph.D. thesis, Technical University of Munich (2025), URL https: //d-nb.info/137113345X/34

Static Data Race Detection Off The Beaten Path

23

[25] Schwarz, M., Erhard, J.: The digest framework: concurrency-sensitivity for abstract interpretation. International Journal on Software Tools for Technology Transfer (2024), ISSN 1433-2787, doi: 10.1007/ s10009-024-00773-y [26] Schwarz, M., Erhard, J.: Data race detection by digest-driven abstract interpretation. In: Chen, Y., Jensen, T.P., Lengál, O. (eds.) Verification, Model Checking, and Abstract Interpretation - 27th International Conference, VMCAI 2026, Rennes, France, January 12-13, 2026, Proceedings, pp. 309–334, Lecture Notes in Computer Science, Springer (2026), doi: 10.1007/978-3-032-15700-3_15, URL https://doi.org/10.1007/ 978-3-032-15700-3_15 [27] Schwarz, M., Saan, S., Seidl, H., Apinis, K., Erhard, J., Vojdani, V.: Improving thread-modular abstract interpretation. In: Dragoi, C., Mukherjee, S., Namjoshi, K.S. (eds.) Static Analysis - 28th International Symposium, SAS 2021, Chicago, IL, USA, October 17-19, 2021, Proceedings, Lecture Notes in Computer Science, vol. 12913, pp. 359–383, Springer (2021), doi: 10.1007/978-3-030-88806-0_18 [28] Schwarz, M., Saan, S., Seidl, H., Erhard, J., Vojdani, V.: Clustered relational thread-modular abstract interpretation with local traces. In: European Symposium on Programming, pp. 28–58, Springer (2023), doi: 10.1007/978-3-031-30044-8_2 [29] Seidl, H., Vojdani, V., Erhard, J., Schwarz, M.: Mixed flow-sensitive static analysis: Engineering modularity. In: Sampaio, A., Stoelinga, M. (eds.) Formal Methods - 27th International Symposium, FM 2026, Tokyo, Japan, May 18-22, 2026, Proceedings, Part II, Lecture Notes in Computer Science, vol. 16557, pp. 446–470, Springer (2026), doi: 10.1007/978-3-032-26220-2_ 22, URL https://doi.org/10.1007/978-3-032-26220-2_22 [30] Siegel, S.F., Zheng, M., Luo, Z., Zirkel, T.K., Marianiello, A.V., Edenhofner, J.G., Dwyer, M.B., Rogers, M.S.: CIVL: the concurrency intermediate verification language. In: Kern, J., Vetter, J.S. (eds.) Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2015, Austin, TX, USA, November 15-20, 2015, pp. 61:1– 61:12, ACM (2015), doi: 10.1145/2807591.2807635 [31] Smaragdakis, Y., Evans, J., Sadowski, C., Yi, J., Flanagan, C.: Sound predictive race detection in polynomial time. ACM SIGPLAN Notices 47(1), 387–400 (1 2012), doi: 10.1145/2103621.2103702, URL https: //doi.org/10.1145/2103621.2103702 [32] SonarSource SA: SonarSource rule RSPEC-5488 (2024), URL https:// rules.sonarsource.com/c/RSPEC-5488/ [33] Sulzmann, M., Stadtmüller, K.: Efficient, near complete, and often sound hybrid dynamic data race prediction. In: Proceedings of the 17th International Conference on Managed Programming Languages and Runtimes, p. 30–51, MPLR ’20, Association for Computing Machinery, New York, NY, USA (2020), ISBN 9781450388535, doi: 10.1145/3426182.3426185, URL https://doi.org/10.1145/3426182.3426185

24

D. Bund, J. Erhard, M. Petter, and M. Schwarz

[34] Sulzmann, M., Thiemann, P.: Cross-thread critical sections and efficient dynamic race prediction methods (2023), URL https://arxiv.org/abs/ 2307.09855 [35] Swain, B., Huang, J.: Towards incremental static race detection in OpenMP programs. In: Laguna, I., Rubio-González, C. (eds.) 2nd IEEE/ACM International Workshop on Software Correctness for HPC Applications, CORRECTNESS@SC 2018, Dallas, TX, USA, November 12, 2018, pp. 33–41, IEEE (2018), doi: 10.1109/CORRECTNESS.2018.00009 [36] Swain, B., Li, Y., Liu, P., Laguna, I., Georgakoudis, G., Huang, J.: Ompracer: a scalable and precise static race detector for OpenMP programs. In: Cuicchi, C., Qualters, I., Kramer, W.T. (eds.) Proceedings of the International Conference for High Performance Computing, Networking, Storage and Analysis, SC 2020, Virtual Event / Atlanta, Georgia, USA, November 9-19, 2020, p. 54, IEEE/ACM (2020), doi: 10.1109/SC41405.2020.00058 [37] Terauchi, T.: Checking race freedom via linear programming. In: Gupta, R., Amarasinghe, S.P. (eds.) Proceedings of the ACM SIGPLAN 2008 Conference on Programming Language Design and Implementation, Tucson, AZ, USA, June 7-13, 2008, pp. 1–10, ACM (2008), doi: 10.1145/1375581. 1375583

Static Data Race Detection Off The Beaten Path

A

25

Requirements on ||?e0 ,e1

Formally, we demand that a predicate ||?e0 ,e1 satisfies for all digests A0 , A1 : ∃t0 , t1 , t′ ∈ T : t0 ends in u0 ∧ αA t0 = A0 ∧ t1 ends in u1 ∧ αA t1 = A1 ∧ None ̸= J(u0 , act0 , u′0 )K(t0 , J(u1 , act1 , u′1 )K(t1 , t′ ))∧ None ̸= J(u1 , act1 , u′1 )K(t1 , J(u0 , act0 , u′0 )K(t0 , t′ )) =⇒ A0 ||?(u0 ,act0 ,v0 ),(u1 ,act1 ,v1 ) A1 = ⊤

The definition in terms of bi-directional digest compatibility is then given by A0 ||?(u0 ,act0 ,v0 ),(u1 ,act1 ,v1 ) A1 =  ♯ ♯ ′ ′  false if ¬∃A : None ̸= Ju0 , act0 KA (A0 , Ju1 , act1 KA (A1 , A ))∧ ♯ ♯ None ̸= Ju0 , act0 KA (A1 , Ju1 , act1 KA (A0 , A′ ))   ⊤ otherwise The soundness of this definition follows directly from the admissibility of the digest.

B

Proofs for Propositions 1 and 2

Recall Proposition 1 from Section 2.1: Proposition 5. Two accesses to a global variable g are racy in the intuitive sense if and only if at least one is a write and traces t0 and t1 ending in the respective CFG predecessors exist, s.t. they are bidirectionally trace compatible. Proof. More formally, in line with [26], define two accesses to be racy in the intuitive sense if they access the same memory, at least one is a write, and there exists a local trace in which they are unordered after disregarding the order induced by the accesses themselves. The proof is then a simplification of the proof of [26, Theorem 1], which uses atomicity mutexes to order accesses to globals. The existence of observing actions of arity n does not complicate the proof here, as it does not consider the reason some actions are ordered w.r.t. each other. ⊔ ⊓ Recall Proposition 2 from Section 2.2: Proposition 6. Refining a sound abstract interpretation of a concurrent program with an admissible digest yields a sound abstract interpretation. Proof. First, a version of the concrete semantics where the unknowns are split according to the digests is constructed. This refined concrete semantics is shown equivalent to the original concrete semantics, which is shown by giving a bijection between least solutions of either of the constraint systems. The property

26

D. Bund, J. Erhard, M. Petter, and M. Schwarz

is then established by fixpoint induction performing a case distinction based on the considered constraint. The proof is a (slight) generalization of the proof of Theorem 4 of Section 2.3 of the PhD thesis of Schwarz [24], to account for the higher arity of observing actions but no additional complications arise here. Then, from the soundness of the base analysis, the soundness of the refined analysis follows by checking that by concretizing a solution of the abstract refined analysis one obtains a solution of the refined concrete constraint system. This is done by verifying this property for each constraint. ⊔ ⊓ Technically, the admissibility of the lockset digest would also need to be reestablished for the additional considered actions, but as they return the digest unmodified, and pthread once and barriers do not affect sets of held locks, this is straightforward.

C

Details on & Extended Support for pthread once

Recall proposition Proposition 3 from Section 3. Proposition 7. The digest given in Section 3 is admissible, and its predicate ||? is sound. Proof. To verify admissibility, i.e., conditions (2) to (5), we first need to define αA t0 = (A0 , C0 ) where A0 is the set of control variables o for which startO(o) appears along the ego-lane of t0 , but endO(o) does not. C0 , on the other hand, is the set of control variables o for which endO(o) is backwards reachable by following program order edges →po , once order edges →oi , and thread creation edges →tc in reverse. This corresponds to those endO(o) actions that are either along the ego-lane of t0 , or along the ego-lane of one of its parents up to the point where the parent created the ego thread, or that the current thread has learned about by communicating through other control variables. This choice may seem complicated when contrasted with just considering all endO(o) actions that appear in the local trace, but is deliberate: in this way, information about control variables is not propagated along other pairs of observing/observable actions, improving performance of the analysis. We can then check conditions (2) to (5) by induction on the length of the trace. The definition of init♯A = {(∅, ∅)} in Figure 6 coincides with requirement (2), as in all initial traces, no startO(o) or endO(o) actions have been executed. We need to verify requirement (3) for all edges, which we recall is: ♯

ˆ Ju, actK (αA t0 , · · · , αA tk−1 ) map αA (JeK(t0 , · · · , tk−1 ))⊑ A where αA is mapped over the trace option returned by JeK(t0 , · · · , tk−1 ), and ˆ is the partial order on A opt with None as bottom and all other elements ⊑ incomparable.

Static Data Race Detection Off The Beaten Path

27

Let us first consider an edge e ≡ (u, Pos(ran(o)), v) in the trace. We have: ( None if o ̸∈ C ♯ J , Pos(ran(o))KA (A, C) = Some (A, C) otherwise Consider a trace t0 : – If JeK t0 = None, we have ˆ Ju, Pos(ran(o))K♯ (αA t0 ) map αA (JeK t0 ) = map αA None = None ⊑ A ˆ which holds as None is the bottom element of the partial order ⊑. – Consider now the case where JeK t0 = Some t1 and let αA t0 = (A0 , C0 ). • Consider the case where o ̸∈ C0 . Then, endO(o) does not appear in t0 : By construction, startO(o) appears in t0 as the guard can syntactically only appear between startO(o) and endO(o). All actions startO(o) and endO(o) as well as actions in between are totally ordered by →o and →po . Thus, if endO(o) appears anywhere in t0 it is backwards reachable by following program order edges →po , once order edges →oi , and thread creation edges →tc . As endO(o) does not appear in t0 , the code associated with o has not been executed, and thus JeK t0 = None, which is a contradiction. • It remains to consider the case where o ∈ C0 . Appending an action Pos(ran(o)) to the trace does not change the set of active or completed control variables, and thus αA t1 = (A0 , C0 ). Thus, we have: map αA (JeK t0 ) = map αA (Some t1 ) = Some (A0 , C0 ) ˆ Some (A0 , C0 ) = Ju, Pos(ran(o))K♯ (αA t0 ) ⊑ A Thus, the claim follows. The proofs proceed analogously for e ≡ (u, Neg(ran(o)), v), as well as for edges not involving control variables. Next, consider an edge e ≡ (u, startO(o), v). Since startO(o) observes either initO(o) or endO(o), its concrete semantics has two arguments. Let αA ti = (Ai , Ci ) for i ∈ {0, 1}. We have ( Some (A0 ∪ {o}, C0 ∪ C1 ) if o ∈ / A0 , ♯ J , startO(o)KA (A0 , C0 ) (A1 , C1 ) = None otherwise. Again, if JeK(t0 , t1 ) = None, requirement (3) follows immediately because None ˆ It therefore remains to consider JeK(t0 , t1 ) = Some t′ . is the least element of ⊑. In this case, o ∈ / A0 : otherwise, the ego-lane of t0 would contain an unmatched startO(o). A further startO(o) on the same lane cannot be supplied with a predecessor in the once order. The observable action supplying the unmatched start has already been consumed, while every later endO(o) is ordered after the new start. Adding the required once-order edge would therefore either violate its uniqueness requirement or create a cycle with program order. Hence, the concrete successor could not be a local trace, contradicting JeK(t0 , t1 ) = Some t′ .

28

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Appending the new action makes o active on the ego-lane and leaves the activity of every other control variable unchanged. Consequently, the active component of αA t′ is A0 ∪ {o}. Moreover, the new once-order edge makes every completed action that is backwards reachable in either input trace also backwards reachable in t′ , and it introduces no other endO action. Thus, its completed component is C0 ∪ C1 . We obtain map αA (JeK(t0 , t1 )) = Some (A0 ∪ {o}, C0 ∪ C1 ) ♯ ˆ ⊑ Some (A0 ∪ {o}, C0 ∪ C1 ) = J , startO(o)KA (A0 , C0 ) (A1 , C1 ). Consider now an edge e ≡ (u, endO(o), v). This action is non-observing, and its digest semantics is ♯

J , endO(o)KA (A0 , C0 ) = Some (A0 \ {o}, C0 ∪ {o}). If JeK(t0 ) = None, requirement (3) again follows from the minimality of None. Otherwise, let JeK(t0 ) = Some t′ and αA t0 = (A0 , C0 ). Appending endO(o) closes the section for o on the ego-lane, while leaving all other active sections unchanged. Hence, the active component of αA t′ is A0 \{o}. The appended action is itself backwards reachable from the maximal element of t′ , so o is completed; all previously completed control variables remain backwards reachable. Therefore, the completed component is C0 ∪ {o}, and map αA (JeK(t0 )) = Some (A0 \ {o}, C0 ∪ {o}) ♯ ˆ ⊑ Some (A0 \ {o}, C0 ∪ {o}) = J , endO(o)KA (A0 , C0 ). This concludes the proof for requirement (3). We next verify requirement (4), i.e., ˆ new♯A (αA t) u u1 map αA (new t u u1 ) ⊑ for every trace t and all program points u, u1 . Let αA t = (A0 , C0 ). By definition, new♯A (A0 , C0 ) u u1 = Some (∅, C0 ). If new t u u1 = None, the left-hand side of requirement (4) is None, so the claim follows from the minimality of None. Otherwise, let new t u u1 = Some t′ . The ego-lane of the newly created thread in t′ consists only of its initial configuration. In particular, it contains no unmatched startO(o) action, and the active component of αA t′ is therefore empty. The thread-creation edge makes exactly the part of the creating thread’s history available at the creation point backwards reachable from the new thread. Consequently, a endO(o) is backwards reachable in t′ if and only if it contributes o to C0 . Thus, αA t′ = (∅, C0 ), and we obtain map αA (new t u u1 ) = Some (∅, C0 ) ˆ ⊑ Some (∅, C0 ) = new♯A (αA t) u u1 .

Static Data Race Detection Off The Beaten Path

29

This proves requirement (3). Finally, requirement (5) demands that, for every digest (A0 , C0 ), ♯

Ju, x = create(u1 )KA (A0 , C0 ) ̸= None

=⇒

new♯A (A0 , C0 ) u u1 ̸= None.

This follows directly from the definition of new♯A : for every (A0 , C0 ) and all program points u, u1 , new♯A (A0 , C0 ) u u1 = Some (∅, C0 ) ̸= None. Thus, the conclusion of the implication holds independently of its premise, which proves requirement (5) and concludes the proof of admissibility. For the proof of soundness of ||? , we observe that actions startO(o) and endO(o) and the actions appearing in between in any local trace are totally ordered by →o and the program order →po . W.l.o.g., assume (A ∩ (A′ ∪ C ′ ) ̸= ∅) and that the considered access by thread with digest (A, C) is along an edge e. Consider t ∈ γA (A, C) and t′ ∈ γA (A′ , C ′ ). If o is in A and in A′ , for both traces to belong to the same execution, either t is a subtrace of t′ , or t′ is a subtrace of t, as endO(o) needs to occur before a second thread can execute startO(o). Thus, t and t′ cannot be bidirectionally trace-compatible. Now consider the case where o ∈ A ∩ C ′ . Then, in t′ , there is an edge Neg(ran(o)), meaning the code associated with o was actually run inside of t′ . For an access to occur with o ∈ A, Neg(ran(o)) needs to be contained in the ego-lane of t. As this holds for at most one thread in any execution, t and t′ can only be compatible if they coincide up to the execution of the access. Thus, t is a subtrace of t′ , and JeK(t0 , t1 ) = None and the traces are not bidirectionally compatible. ⊔ ⊓ Beyond supporting pthread once for checking for data races, one can also increase the precision of an analysis by only reading those values that globals may have after the code inside pthread once has been executed. A digest to help analyze this feature (Figure 10) may then track three pieces of information in a tuple (A, C, O): – Some set A of active control variables as in Section 3. – Some set C of completed control variables, i.e., control variables for which the associated fragment has surely been run. Unlike in Section 3, this is not only the case if endO(o) was called by the ego thread or one of its parents, but also when the ego thread incorporates an observable action where the control variable is completed. – Additionally, a map O tracking for each mutex a, for which of the control variables o the mutex a was unlocked while o was active. The interesting case is the right-hand side for acquiring a mutex a: In case the ego thread has observed that the mutex a was unlocked while some control variable o was active, but the trace ending in the unlock of a has neither observed this nor is the control variable currently active, there must have been a later unlock of a, where the control variable was active. Thus, no two traces with such digests can be compatible.

30

D. Bund, J. Erhard, M. Petter, and M. Schwarz

A = 2O × 2O × (S → 2O )

♯ J , lock(a)K A (A0 , C0 , O0 ) (A1 , C1 , O1 ) = ( None if O0 a ̸⊆ (C1 ∪ A1 ) Some (A0 , C0 ∪ C1 , O0 ∪ O1 ) otherwise

init♯A = {(∅, ∅, {a 7→ ∅ | a ∈ S})} new♯A (A, C, O) u u1 = Some (∅, C, O) ♯ J , Pos(ran(o))K A (A, C, O) = (

J , unlock(a)K♯A (A, C, O) = Some (A, C, O ⊕ {a 7→ O a ∪ A}) None if o ̸∈ C ♯ Some (A, C, O) otherwise J , actKA (A0 , C0 , O0 ) (A1 , C1 , O1 ) = ♯ Some (A0 , C0 ∪ C1 , O0 ∪ O1 ) (other observing) J , Neg(ran(o))K A (A, C, O) = ( None if o ∈ C J , actK♯ (A, C, O) = Some (A, C, O) (other non-observing) A Some (A, C, O) otherwise ( Some (A0 ∪ {o}, C0 ∪ C1 , O0 ∪ O1 ) None ♯ J , endO(o)KA (A, C, O) = Some (A \ {o}, C ∪ {o}, O)

J , startO(o)K♯A (A0 , C0 , O0 ) (A1 , C1 , O1 ) =

o ̸∈ A0 otherwise

Fig. 10. Right-hand sides for expressing pthread once as a refinement, where ∪ on maps is defined as the point-wise union of the right-hand sides.

Example 7. Consider again the program in Figure 5, and an analysis associating values of globals with mutexes that are always held when the global is accessed, refined with the digests from Figure 10. At the later lock(mdev ) in both of the threads, the only reaching digests of the ego threads are (∅, {o}, {mdev 7→ {o}}). Thus, only those unknowns associated with observable actions with a digest (A1 , C1 , O1 ) where o is either in A1 or C1 can be incorporated here. For all these unknowns, the value of g is known to not be null. Thus, the assertions can be shown in both threads. ⊔ ⊓

D

Details on Barriers

We first remark on the difference between barriers and signals. Remark 2. While the signalling mechanism of Pthreads at first glance seems similar to barriers of capacity one, the information that a call to signal wait(s) has returned cannot help exclude data races. Pthreads allows for spurious wakeups, so such a call may return even though s has not been signalled. We next turn to the soundness of using this digest for excluding races. Recall that the barrier digest is built on a digest A1 . We assume that A1 is admissible and that its predicate ||?A1 is sound. Recall that in Section 2.2 we have established that ||?A1 can be used to check whether arbitrary actions may-happen-in-parallel. We further assume that the base abstraction is insensitive to the newly introduced barrier record and check actions. That is, extending a trace by either action does not change its A1 abstraction, and the corresponding base right-hand sides are identity functions. As required for the generic thread IDs introduced in Section 2,

Static Data Race Detection Off The Beaten Path

31

πtid is constant along each concrete thread and unique(q) implies that at most one concrete thread in an execution has projected ID q. Recall the following proposition from Section 4: Proposition 8. Provided the digest A1 is admissible, and its predicate ||?A1 is sound, the digest given in Section 4 is admissible, and its predicate ||? sound. Proof. Even though the definition of the predicate ||? appears in the right-hand side of the digests, the proof can proceed step-by-step, first showing admissibility and turning to the soundness of ||? later. Let αA1 be the abstraction function of the base digest. We define the abstraction function for the product digest by αA t = (αA1 t, R(t), O(t)). Here, R(t) contains exactly those barriers b for which a barrier N record(b) action occurs on the ego-lane of t. For a projected thread ID q, the set O(t) q contains b if t contains a barrier N record(b) action performed by a thread whose base digest at that action projects to q. Thus, R describes records of the ego thread, whereas O also includes records learned from incorporated traces. We verify requirements (2) to (5). For requirement (2), an initial trace contains no barrier action. Therefore, R(t) = ∅ and O(t) is the everywhere-empty map for every t ∈ init. Its base component belongs to init♯A1 by admissibility of A1 . Consequently, { αA t | t ∈ init } = { (A, ∅, ∅) | A ∈ init♯A1 } = init♯A . We next verify requirement (3). As before, if a concrete right-hand side returns None, the requirement follows immediately because None is the least element ˆ In the following cases, we may therefore assume that the concrete operation of ⊑. succeeds. First, let e = (u, barrier N record(b), v),

JeK(t0 ) = Some t′ ,

and write αA t0 = (A0 , R0 , O0 ). The record action is appended to the ego-lane. Barrier actions do not affect the base digest, so the first component remains A0 . The new record adds b to R0 . It is performed by the ego thread, whose projected ID is πtid A0 , and therefore also adds b to the corresponding binding of O0 . No other binding changes. Hence, αA t′ = A0 , R0 ∪ {b},
O0 ⊕ {(πtid A0 ) 7→ (O0 (πtid A0 )) ∪ {b}} , ♯

which is exactly J , barrier N record(b)KA (A0 , R0 , O0 ). Now consider e = (u, barrier N check(b), v),

JeK(t0 , . . . , tN −1 ) = Some t′ ,

32

D. Bund, J. Erhard, M. Petter, and M. Schwarz

and let αA ti = (Ai , Ri , Oi ). Concrete success means that the N traces ending in the corresponding record action are distinct, mutually compatible, and can occur in parallel. Soundness of ||?A1 therefore gives Ai ||?A1 Aj = ⊤

for every i ̸= j.

It also implies the second check in the abstract right-hand side. To see this, fix i ̸= j and suppose that πtid Ai is unique. Every barrier record in Oj (πtid Ai ) was then performed by the unique ego thread represented by Ai . If such a record were not in Ri , tj would already contain a strict continuation of the ego-lane of ti . The two record actions supplied to the same barrier check could then not occur in parallel: combining the traces would either duplicate a barrier-order predecessor or create a causality cycle. This would contradict the assumed success of the concrete check. Therefore, unique(πtid Ai )

=⇒

Oj (πtid Ai ) ⊆ Ri .

Thus, the guard of the successful branch of the abstract right-hand side holds. The check action adds no barrier record to its ego-lane, so the resulting R component is R0 . It incorporates all input traces, and hence a record is available in the result exactly when it is available S in at least one input. Its observation N −1 map is consequently the pointwise union i=0 Oi . Finally, the check does not alter the base digest of the ego thread. We conclude that αA t′ = (A0 , R0 ,

N[ −1

Oi ),

i=0 ♯

which agrees with the successful branch of J , barrier N check(b)KA . It remains to consider an edge e = (u, act, v) for any other n-ary action. Let αA ti = (Ai , Ri , Oi ) and assume JeK(t0 , . . . , tn−1 ) = Some t′ . By requirement (3) for the base digest and the flat order on options, its abstract right-hand side returns precisely the base component A′ of t′ : ♯

Ju, actKA1 (A0 , . . . , An−1 ) = Some A′ . The action adds no barrier record to the ego-lane, so the second component remains R0 . All records incorporated from the argument traces are captured by the pointwise union of their observation maps. Therefore, αA t′ = (A′ , R0 ,

n−1 [

Oi ),

i=0

exactly as returned by the product right-hand side. This proves requirement (3) in all cases. For requirement (4), let αA t = (A0 , R0 , O0 ). If new t u u1 = None, the claim follows from the minimality of None. Otherwise, let new t u u1 = Some t′ . Requirement (4) for the base digest yields new♯A1 A0 u u1 = Some A′

with

αA1 t′ = A′ .

Static Data Race Detection Off The Beaten Path

33

The new thread’s ego-lane initially contains no barrier record, so its R component is empty. Through the creation edge, it inherits all records known at the creation point, and hence its observation map is O0 . It follows that αA t′ = (A′ , ∅, O0 ) = new♯A (A0 , R0 , O0 ) u u1 , establishing requirement (4). Finally, suppose the premise of requirement (5) holds: ♯

Ju, x = create(u1 )KA (A0 , R0 , O0 ) ̸= None.

By the definition of the product right-hand side, the corresponding base righthand side is also different from None. Requirement (5) for A1 then gives new♯A1 A0 u u1 = Some A′ for some A′ . By definition of the product operation, new♯A (A0 , R0 , O0 ) u u1 = Some (A′ , ∅, O0 ) ̸= None. This proves requirement (5), and hence the barrier digest is admissible. Let us now turn to the soundness of ||? : The first check is sound by soundness of ||?A1 . We show that the second argument for ⊓ returning false implies that the traces are not bi-directionally compatible. W.l.o.g., assume (unique (πtid A0 )∧O1 (πtid A0 ) ̸⊆ R0 ) and that the considered access by thread with digest (A0 , R0 , O0 ) is along an edge e. Consider t0 ∈ γA (A0 , R0 , O0 ) and t1 ∈ γA (A1 , R1 , O1 ). Then, trace t1 has observed an action performed by the ego-thread of t0 that itself is not part of t0 yet. Thus, a super-trace of t0 containing the access and the observed action is a subtrace of t1 . Thus, JeK(t0 , t1 ) = None and the claim follows. ⊔ ⊓

E

Digests for Descendant Lockset

A digest helping with analyzing the pattern described in Section 5 tracks the following information in a triple ((A, S), H, D): – A tuple (A, S) holding the value of the thread id digest A and the value of the lockset digest S – A map H, where each mutex m is mapped to the set of thread id s. This set includes only thread id s, in which m was locked. In Example 5, H holds the relevant information we need at the access to global in i1 . – A map D, where we map each thread id i to a set of mutexes. If m is included in the set, the conditions 2 and 3 listed in section 5. We then define the race check as: (A0 , S0 , H0 , D0 ) ||? (A1 , S1 , H1 , D1 ) = let i0 = πtid A0 in let i1 = πtid A1 in   (({i1 } ∪ must anc i1 ) ∩ may create A0 ̸= ∅ ∧      (∃iH1 ∈ TID, s ∈ S : iH1 ∈ H1 s ∧ s ∈ D0 i1 ∧ i0 ∈ must anc iH1 )) ∨  false if (({i0 } ∪ must anc i0 ) ∩ may create A1 ̸= ∅ ∧    (∃iH0 ∈ TID, s ∈ S : iH0 ∈ H0 s ∧ s ∈ D1 i0 ∧ i1 ∈ must anc iH0 ))    ⊤ otherwise

34

D. Bund, J. Erhard, M. Petter, and M. Schwarz

A = AT ×S × (S → 2TID ) × (TID → 2S ) ♯ new (A ((A, S), H, D) u u1 = Some ((A′ , S ′ ), H, {i 7→ S | i ∈ TID})

if new♯AT ×S (A, S) u u1 = Some (A′ , S ′ )

None otherwise init♯A = {((A, S), ∅, {i 7→ S | i ∈ TID}) | (A, S) ∈ init♯AT ×S } Ju,create u0 K♯A ((A, S), H, D) =  let Some Anew = new♯AT A u u0 in     let iego = πtid A in    let I ∗ = {i ∈ TID | π A ∈ ({i} ∪ must anc i)} in new ′

tid

if Ju, create u0 K♯AT A = Some A′

new

∗  let D = D ⊕ {i∗new 7→ S ∩ D i∗new | i∗new ∈ Inew , iego ∈ must anc i∗new } in     ′ ′  Some ((A , S), H, D )     None otherwise Ju,(lock(a)K♯A ((A0 , S0 ), H0 , D0 ) ((A1 , S1 ), H1 , D1 ) = Some ((A0 , S ′ ), H0 ⊕ {a 7→ (H0 a) ∪ {πtid A0 }}, D0 ) if Ju, lock(a)K♯AS S0 S1 = Some S ′ None otherwise Ju, unlock(a)K♯A ((A, S), H, D) = ′ let ( D = {i 7→ D i \ {a} | i ∈ TID} in Some ((A, S ′ ), H, D′ ) if Ju, unlock(a)K♯AS S = Some S ′ None otherwise ♯ J , actKA (((A0 , S0 ), H0 , D0 ), . . . , ((AN −1 , SN −1 ), HN −1 , DN −1 )) =  ♯ Some ((A′ , S ′ ), H0 , D0 ) if J , actKAT ×S ((A0 , S0 ), . . . , (AN −1 , SN −1 )) = 

  None

Some (A′ , S ′ ) otherwise

(other)

Fig. 11. Descendant lockset digest, where ⊕ denotes updating a map. Missing bindings map to the empty set.

Static Data Race Detection Off The Beaten Path

35

Example 8. Considering the program from Figure 8 again, the digests have the following interesting values at the accesses to global: – At the access in i1 , the H component has value {m 7→ {main, i1 }}. – At the access in main, the D component has value {i1 7→ {m}, i2 7→ {m}}. With these values and the may-race predicate given above, we can exclude the possibility of a data race. Proposition 9. Provided the digest AT ×S is admissible, the digest given above is admissible and its definition for ||? is sound. Proof. For proof of admissibility, we inductively verify that the digest fulfills (2) to (5). Let αB be the abstraction function for AT ×S and define αA t = (αB t, H(t), D(t)). The auxiliary components are defined inductively along the creation-extended ego lane of the local trace. For traces in init, H maps every mutex to ∅, while D maps every thread ID to S. Executing lock(a) in a thread with projected ID i adds i to H(a). A create action intersects D(i) with the current lockset for ∗ in Figure 11. Executing precisely the possible descendant IDs selected by Inew unlock(a) removes a from every entry of D. Other actions leave both components unchanged. A new thread inherits H from its creator and starts with a map mapping all thread id s to S for D. For requirement (2), an initial trace contains no lock, unlock, or creation action. Hence, for every t ∈ init, αA t = ((A, S), ∅, {i 7→ S | i ∈ TID}) ∈ init♯A where (A, S) ∈ init♯AT ×S . The converse inclusion follows from requirement (2) for the base digest, proving equality with the displayed init♯A . We verify requirement (3) by cases. A concrete result None is below every abstract result, so only successful concrete operations require consideration. Let e ≡ (u, create u0 , v), JeK(t) = Some t′ , and αA t = ((A, S), H, D). Base admissibility and flatness of the option order give ♯

Ju, create u0 KAT A = Some A′ ,

αB t′ = (A′ , S).

By requirement (5) for the thread-ID digest we have new♯AT A u u0 = Some Anew for some Anew . Thus, the pattern match defining Anew in the successful branch is total. By the definition of D, the new creation adds the current-lockset condition ∗ for exactly the IDs in the resulting Inew , so ∗ D′ = D ⊕ {i 7→ S ∩ D(i) | i ∈ Inew , πtid A ∈ must anc i}.

A create performs no lock, hence H is unchanged and αA t′ = ((A′ , S), H, D′ ), coinciding with the result of the right-hand side.

36

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Next, consider J(u, lock(a), v)K(t0 , t1 ) = Some t′ and let αA tk = ((Ak , Sk ), Hk , Dk ). ♯ The right-hand side of the base digest yield Ju, lock(a)KAS S0 = Some S ′ and leaves A0 unchanged. The action records that the ego thread, whose ID is πtid A0 , has locked a; it does not modify D. Therefore, αA t′ = ((A0 , S ′ ), H0 ⊕ {a 7→ H0 (a) ∪ {πtid A0 }}, D0 ), agreeing with the result of the right-hand side. For a successful unlock operation, J(u, unlock(a), v)K(t) = Some t′ with αA t = ♯ ((A, S), H, D), base admissibility yields Ju, unlock(a)KAS S = Some S ′ . This unlock invalidates the uninterrupted-holding condition for a for every potential descendant ID, while changing no H entry. Thus, αA t′ = ((A, S ′ ), H, {i 7→ D(i) \ {a} | i ∈ TID}), agreeing with the result of the right-hand side. For every other n-ary action, requirement (3) for the base digest and flatness give the exact successful base successor (A′ , S ′ ). Such an action changes neither auxiliary component by definition, so the product successor is ((A′ , S ′ ), H0 , D0 ), as specified by the “other” case in Figure 11. This proves requirement (3). For requirement (4), let αA t = ((A, S), H, D). It once again suffices to consider only the case where the edge succeeds in the concrete. For new t u u1 = Some t′ , base requirement (4) and flatness yield new♯AT ×S (A, S) u u1 = Some (A′ , S ′ ),

αB t′ = (A′ , S ′ ).

By definition, the child inherits H, has not itself established any creation constraint, and therefore starts with the everywhere-S map. Hence, αA t′ = ((A′ , S ′ ), H, {i 7→ S | i ∈ TID}), which coincides with the definition of new♯A . Finally, if the premise of requirement (5) holds for ((A, S), H, D), by requirements (3) and (5) makes new♯AT ×S (A, S) u u1 different from None. The definition of the product new-thread operation then returns Some ((A′ , S ′ ), H, {i 7→ S | i ∈ TID}) for the corresponding base result (A′ , S ′ ), proving requirement (5). Thus, the descendant-lockset digest is admissible. We now turn to the proof of soundness of ||? : W.l.o.g., assume the first disjunct of the false case holds. Consider two local traces t and t′ where t ∈ γA (A0 , S0 , H0 , D0 ) and t′ ∈ γA (A1 , S1 , H1 , D1 ). Since ({i1 } ∪ must anc i1 ) ∩ may create A0 ̸= ∅, t has observed at least one transitive creation of threads associated with i1 —the thread id at the end of t′ . As s ∈ D0 i1 , all of those creations happened while s was in the lockset and none of the creations is followed by unlock(s) in i0 . Since iH1 ∈ H1 s, t′ has observed lock(s) in iH1 . No matter which of the transitive creations in i0 described above resulted in the creation of the thread at the end of t′ —this lock happens after that creation, as i0 ∈ must anc iH1 . The

Static Data Race Detection Off The Beaten Path

37

lock must also happen after a succeeding unlock(s) following the creation in i0 , since s is in the lockset at that creation. Since no such unlock is included in t whereas the later lock is included in t′ , compatibility can hold only if t is a subtrace of t′ . Hence, the traces are not bidirectionally compatible. ⊔ ⊓

F

Digests for Creation Locksets

We propose the digest in Figure 12 to analyze the conditions given at the end of Section 6. Such a digest is a triple ((A, S, J), C, O): – A triple (A, S, J) representing the thread id and lockset digest introduced in Section 2.2, and the join digest by Schwarz and Erhard [25]. – A map C mapping each thread id i to a set of mutexes, where m is included if conditions 2 and 3 are satisfied. – A map O mapping each thread id i to a pair. In the digest of the ego thread, O i stores the C component and the set of may-created thread id s of the most recently observed sub-trace belonging to a thread represented by i. Such an observation occurs when the ego thread locks a mutex after that thread unlocks it. We use O to compare the lockset at a program point with inter-threaded mutex protections of other threads. To determine if two program points with the digests explained above may race, we can evaluate the following predicate: ((A0 , S0 , J0 ), C0 , O0 ) ||? ((A1 , S1 , J1 ), C1 , O1 ) = let i0 = πtid A0 in let  i1 = πtid A1 in ′  ) = O1 iO in (∃iO ∈ TID : iO ̸= i1 ∧ let (CO , IO    ′   C i ∩ S = ̸ ∅ ∧ ({i } ∪ must ̸= ∅) ∨ anc i0 ) ∩ IO O 0 1 0 false if ′ (∃iO ∈ TID : iO ̸= i0 ∧ let (CO , IO ) = O0 iO in   ′  CO i1 ∩ S0 ̸= ∅ ∧ ({i1 } ∪ must anc i1 ) ∩ IO ̸= ∅)    ⊤ otherwise Consider the first disjunct for the false case. It checks whether it can be shown that the access of thread i1 must happen after the access of thread i0 . Con′ cretely, O1 iO = (CO , IO ) means that i1 observed, through a lock it or one of its ancestors acquired, an action of a thread with thread id iO . The condition ′ ({i0 } ∪ must anc i0 ) ∩ IO ̸= ∅ establishes that this observation occurred after iO had created either i0 or one of its mandatory ancestors. If CO i0 ∩ S1 ̸= ∅ there is some mutex, say m, that is held at the access by i1 and that was held throughout the execution of i0 . Thus, we obtain that i0 or one of its mandatory ancestors must have been created before the access in i1 occurred and m was held throughout i0 ’s execution. As i0 ̸= i1 , for i1 to succeed in acquiring m, it must have been released, and thus i0 must have completed its execution before i1 ’s access. The second, gray disjunct checks the symmetric situation.

38

D. Bund, J. Erhard, M. Petter, and M. Schwarz

A = AT ×S×J × (TID → 2S ) × (TID → ((TID → 2S ) × 2TID )) new♯A ((A, S, J), C, O) u u1 = ′ let ( O = {i 7→ (∅, ∅) | i ∈ TID} in Some ((A′ , S ′ , J ′ ), ∅, O′ ) if new♯AT ×S×J (A, S, J) u u1 = Some (A′ , S ′ , J ′ ) None otherwise init♯A = {((A, S, J), ∅, {i 7→ (∅, ∅) | i ∈ TID}) | (A, S, J) ∈ init♯AT ×S×J } Ju,create u0 K♯A ((A, S, J), C, O) =  let Some Anew = new♯AT A u u0 in     let iego = πtid A in    let I ∗ = {i ∈ TID | π A ∈ ({i} ∪ must anc i)} in

new ∗ = C ⊕ {i∗new 7→ S ∩ C i∗new | i∗new ∈ Inew , iego ∈ must anc i∗new } in ′ ′

new ′

tid

if Ju, create u0 K♯AT A = Some A′

 let C      Some ((A , S, J), C , O)    None otherwise Ju, lock(a)K♯A ((A0 , S0 , J0 ), C0 , O0 ) ((A1 , S1 , J1 ), C1 , O1 ) = ′ let ( O = O0 ⊕ {πtid A1 7→ (C1 , may create A1 )} Some ((A0 , S ′ , J0 ), C0 , O′ ) if Ju, lock(a)K♯AS S0 = Some S ′ None otherwise Ju, unlock(a)K♯A ((A, S, J), C, O) = let iego = πtid A in let Irunning = {i ∈ TID | ∃icreated ∈ may create A : icreated ∈ {i} ∪ must anc i} \ J in ′ let ( C = C ⊕ {irunning 7→ C irunning \ {a} | irunning ∈ Irunning } in Some ((A, S ′ , J), C ′ , O) if Ju, unlock(a)K♯AS S = Some S ′ None otherwise J , actK♯A (((A0 , S0 , J0 ), C0 , O0 ), . . . , ((AN −1 , SN −1 , JN −1 ), CN −1 , ON −1 )) =  ♯ ′ ′ ′  Some ((A , S , J ), C0 , O0 ) if J , actKAT ×S×J ((A0 , S0 , J0 ), . . . , (AN −1 , SN −1 , JN −1 )) =   None

Some (A′ , S ′ , J ′ ) otherwise

(other)

Fig. 12. Creation lockset digest, where ⊕ denotes updating a map and missing bindings map to S.

Static Data Race Detection Off The Beaten Path

39

Example 9. Consider the program from Figure 9 again. At the access to g in i1 , the O component of the digest is {main 7→ ({work 7→ {m}, i1 7→ ∅}, {i1 , work })}, where missing bindings of the outer map default to (∅, ∅) and missing bindings of the inner map default to S. Together with S = {m}, this suffices to rule out a data race with any program point having thread id work . Proposition 10. Provided the product digest AT ×S×J is admissible, the digest given above is admissible and its definition for ||? is sound. Proof. Let αB be the abstraction function of the base product digest. Define αA t = (αB t, C(t), O(t)) inductively along the creation-extended ego lane of t. Initially, C maps every thread id to S (represented by the empty finite map), and O maps every thread ∗ with the current id to (∅, ∅). A create intersects the entries of C selected by Inew lockset. An unlock(a) removes a from the entries selected by Irunning . If a lock(a) observes a trace s ending in the matching unlock, it stores (C(s), may createAs ) in the O entry for πtid As , where αB s = (As , Ss , Js ). All other actions leave C and O unchanged. A new thread starts with the initial values of both maps. We verify (2) to (5). For requirement (2), an initial trace contains no creation, unlock, or observation. Hence αA t = ((A, S, J), ∅, {i 7→ (∅, ∅) | i ∈ TID}) for some (A, S, J) ∈ init♯AT ×S×J . Conversely, every initial base digest is represented by an initial trace by requirement (2) for the base digest. This proves equality with the definition of init♯A . For requirement (3), a concrete result None is below every abstract result, so it remains to consider successful concrete operations. First let e = (u, create u0 , v), JeK(t) = Some t′ , and αA t = ((A, S, J), C, O). Base admissibility and flatness of the option order give ♯

Ju, create u0 KAT A = Some A′ ,

αB t′ = (A′ , S, J).

Admissibility and the componentwise definition of the base product make the ∗ match new♯AT A u u0 = Some Anew total. Let Inew be the set induced by Anew in the right-hand side and let ∗ C ′ = C ⊕ {i 7→ S ∩ C i | i ∈ Inew , πtid A ∈ must anci}.

Exactly these entries acquire the current creation constraint; the create performs no observation. Thus αA t′ = ((A′ , S, J), C ′ , O), which is the result of the abstract create transfer.

40

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Next suppose J(u, lock(a), v)K(t0 , t1 ) = Some t′ , where t1 ends in the observed unlock(a), and write αA tk = ((Ak , Sk , Jk ), Ck , Ok )

(k ∈ {0, 1}). ♯

The componentwise base transfer and base admissibility yield Ju, lock(a)KAS S0 = Some S ′ and leave the ego thread’s A0 and J0 unchanged. The lock changes no creation constraint, and its mutex-order edge observes precisely t1 . Therefore, with O′ = O0 ⊕ {πtid A1 7→ (C1 , may createA1 )}, we have αA t′ = ((A0 , S ′ , J0 ), C0 , O′ ), exactly as specified by the abstract lock transfer. For a successful unlock(a), let αA t = ((A, S, J), C, O). Base admissibility ♯ gives Ju, unlock(a)KAS S = Some S ′ . The set Irunning = {i ∈ TID | ∃icreated ∈ may createA : icreated ∈ {i} ∪ must anci} \ J contains exactly the possible descendants not known to have been joined. Unlocking a invalidates the uninterrupted-holding condition for those entries and performs no observation. Hence, for C ′ = C ⊕ {i 7→ C i \ {a} | i ∈ Irunning }, we obtain αA t′ = ((A, S ′ , J), C ′ , O), the result of the abstract unlock transfer. Finally, for any other successful n-ary action, base admissibility and flatness give the exact base successor B ′ from the base digests B0 , . . . , Bn−1 . Such an action changes neither auxiliary component, so the successor is (B ′ , C0 , O0 ), agreeing with the “other” transfer. This proves requirement (3). For requirement (4), suppose αA t = (B, C, O) and new t u u1 = Some t′ . Base admissibility and flatness yield new♯AT ×S×J B u u1 = Some B ′ ,

αB t′ = B ′ .

A new thread has not created a descendant, invalidated a creation lockset, or observed another thread. Consequently αA t′ = (B ′ , ∅, {i 7→ (∅, ∅) | i ∈ TID}), precisely the result of new♯A . The unsuccessful concrete case follows from the minimality of None. Finally, suppose the premise of requirement (5) holds for (B, C, O). Then the corresponding base create transfer succeeds. Requirement (5) for the base product yields new♯AT ×S×J B u u1 = Some B ′ for some B ′ . The displayed definition of new♯A consequently returns Some (B ′ , ∅, {i 7→ (∅, ∅) | i ∈ TID}) ̸= None. This proves requirement (5) and hence admissibility.

Static Data Race Detection Off The Beaten Path

41

We now turn to the proof of soundness of ||? : W.l.o.g., assume the first disjunct of the false case holds. Consider t0 ∈ γA ((A0 , S0 , J0 ), C0 , O0 ) and t1 ∈ γA ((A1 , S1 , J1 ), C1 , O1 ). Consider some thread with id iO , from which the thread at the end of t1 ′ ′ ̸= ∅, threads has observed (CO , IO ) := O1 iO . Since ({i0 } ∪ must anc i0 ) ∩ IO associated with i0 have already been transitively created. Choose s ∈ CO i0 ∩ S1 . By the meaning of CO i0 , thread iO holds s throughout the execution of every relevant thread represented by i0 . At the same time, s ∈ S1 means that the ego thread represented by i1 holds s at the access in t1 . Since iO ̸= i1 , these are different threads. Mutual exclusion orders the corresponding critical sections by →s , so the accesses cannot be bidirectionally trace-compatible. ⊔ ⊓

G

Experimental Setup

G.1

Benchmark Subjects

Our benchmark sets follow the conventions of the SV-Comp software-verification competition. Each benchmark instance comprises source code together with at least one property to verify: – no-data-race , which evaluates to true if no data race occurs in any execution of the program; – unreach-call , which evaluates to true if the special function reach error() is unreachable in every execution of the program; and – other properties, which are not relevant to the benchmarks considered here. The possible verdicts are true, false, unknown, and error. An analyzer that cannot decide a property conclusively usually returns unknown. Because SV-Comp provides no direct way to specify invariants, we encode them using program guards and the unreach-call property. Although these benchmarks are formally unreach-call tests, they let us check whether an analyzer handles synchronization features correctly. We use a consistent naming scheme for the benchmark programs. Each filename contains four components separated by underscores. They identify, in order, the challenge (“b” for “barrier,” “cl” for “creation lockset,” “dl” for “descendant lockset,” and “o” for “once”), the property (“n” for no-data-race and “u” for unreach-call ), the expected verdict (“true” or “false”), and a number that uniquely identifies the benchmark. G.2

Soundness and Precision

For both no-data-race and unreach-call , we classify verdicts as follows: analysis verdict TRUE ground truth

FALSE

TRUE ✓ false positive FALSE false negative ✓

42

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Under this formulation, a false positive is a FALSE verdict when TRUE is expected and indicates imprecision. A false negative is a TRUE verdict when FALSE is expected and indicates unsoundness. Because abstract interpretation overapproximates program behavior, an abstract interpreter generally cannot substantiate a FALSE verdict when FALSE is expected and therefore usually returns UNKNOWN. G.3

Comparative Benchmark Baseline

We selected the baseline tools from SV-Comp participants that performed well in concurrent-program verification categories. For each tool, we used the parameters specified by its configuration for the relevant categories. RacerF is an abstract interpreter that supports only the no-data-race property, so we did not evaluate it on unreach-call . Tool

Version Configuration

Racerf ESBMC (base)

ESBMC (no-data-race) ESBMC (unreach-call) CPAChecker

U. Gemcutter Dartagnan

G.4

2.2 ./racerf-sv.py -machdep gcc x86 64 $FILE 7.7.0 ./esbmc --no-div-by-zero-check --force-malloc-success --state-hashing --add-symex-value-sets --no-align-check --k-step 2 --floatbv --unlimited-k-steps --no-vla-size-check $FILE --64 --no-por --context-bound 3 --witness-output witness.graphml --no-pointer-check --no-bounds-check --incremental-bmc --data-races-check --no-assertions --enable-unreachability-intrinsic 4.2.2 ./cpachecker --svcomp26 --heap 10000M --benchmark --timelimit 900 s --stats --spec $PROPERTY --64 $FILE 0.3.1 ./Ultimate.py --spec $PROPERTY --file $FILE --full-output --architecture 64bit 4.1.0 ./Dartagnan-SVCOMP.sh $PROPERTY $FILE

Benchmark Execution Times

We ran the benchmarks on a machine with a 2.5 GHz Intel Core i7-11700 CPU, 64 GB of RAM, and Ubuntu 26.04. Each tool invocation was limited to 5 minutes and 20 GB of RAM.

Static Data Race Detection Off The Beaten Path

Dartagnan

ESBMC

RacerF

UGemCutter

Goblint

b n false 1.c b n false 2.c b n false 3.c b n false 4.c b n false 5.c b n true 1.c b n true 2.c b n true 3.c b n true 4.c b n true 5.c b n true 6.c b n true 7.c b u false 1.i b u false 2.i b u false 3.i b u false 4.i b u false 5.i b u false 6.i b u true 1.i b u true 2.i b u true 3.i b u true 4.i b u true 5.i b u true 6.i b u true 7.i b u true 8.i cl n false 1.i cl n false 2.i cl n false 3.c cl n false 4.c cl n false 5.c cl n false 6.c cl n false 7.c cl n false 8.c cl n false 9.c cl n false 10.c cl n false 11.c cl n false 12.c cl n false 13.c dl n false 14.i dl n false 15.i dl n false 16.c dl n false 17.c dl n false 18.c dl n false 19.c dl n false 20.c dl n false 21.c dl n false 22.c dl n false 23.c dl n false 24.c dl n false 25.c cl n true 1.c cl n true 2.c cl n true 3.c cl n true 4.c cl n true 5.c dl n true 6.c dl n true 7.c

CPAchecker

Input File

lines of code

Table 4: Tool execution times (ms) per input file.

36 30 29 33 34 35 40 39 35 31 31 30 1420 1418 1431 1422 1417 1411 1415 1427 1429 1424 1425 1427 1427 1418 39 23 30 32 35 28 32 23 24 29 39 39 888 888 20 21 27 26 893 22 24 30 23 26 893 888 34 25 30 39 23 28

3013 2676 2530 2551 2867 2533 2532 2645 2486 2616 2342 2582 2983 2736 3696 2948 3037 2718 3051 3376 2841 2892 3005 2774 2902 3885 2483 2420 2594 2508 3506 2592 2626 2468 2590 2695 2823 2930 2761 2367 2382 2806 3216 2936 2912 2586 2468 2623 2486 3017 2527 2337 2431 2309 2361 2527 2248 2455

2144 2017 2152 2217 2134 2115 3275 2161 2423 2398 2239 2475 2040 1646 1655 1701 3195 1762 1684 1619 1667 3036 1677 1594 1687 1612 2336 3368 2456 2863 2527 2550 2587 2447 2666 2132 2633 3026 ∞ 3895 2923 2393 2282 2211 3663 2205 3647 2653 2246 2246 2408 2363 2446 3457 2580 2371 2196 2473

1337 1199 851 805 798 1316 2299 953 851 894 795 901 720 720 797 710 797 772 711 701 812 860 882 729 1112 706 1124 2148 845 1071 992 1613 1775 843 1079 1699 7174 3657 ∞ 1657 1531 1959 827 1077 945 848 871 8510 1839 818 13061 1432 5002 1067 1049 9480 824 982

2941 3371 2852 2754 2677 2656 2891 2851 2846 2708 2788 2812 1569 1577 3650 3519 3064 2998 2804 2931 2778 2621 2726 2120 2678 1501 1399 2543 3071 2648 2683 1867 1859 3100 3224 2855 3184 3405 3083 2851 3285 2010 2547 1857

11543 9471 8991 10669 9867 9235 9215 10709 8933 9389 9473 9133 11506 13664 13042 12700 12433 12139 12992 14886 13995 13357 12015 14324 13406 13195 9532 10176 10868 10238 10503 10024 9673 10829 10429 11228 10037 10191 10254 9486 8840 10196 10443 12272 10543 9936 9907 11235 9542 11450 9579 9468 9542 9703 9335 9301 10063 9567

82 71 65 66 64 65 74 93 59 56 65 59 53 53 76 62 51 47 46 50 56 84 81 59 52 46 73 65 61 59 60 88 64 51 55 60 60 62 65 48 71 68 90 63 55 54 54 57 54 59 64 61 61 54 65 89 54 62

Continued on next page

43

44

D. Bund, J. Erhard, M. Petter, and M. Schwarz

G.5

Input File

lines of code

CPAchecker

Dartagnan

ESBMC

RacerF

UGemCutter

Goblint

Table 4 continued from previous page

dl n true 8.c dl n true 9.c dl n true 10.i dl n true 11.i o n false 1.c o n false 2.c o n false 3.c o n false 4.c o n false 5.c o n false 6.c o n true 1.c o n true 2.c o n true 3.c o n true 4.c o n true 5.c o n true 6.c o n true 7.c o n true 8.c o n true 9.c o u false 1.i o u false 2.i o u false 3.i o u false 4.i o u false 5.i o u true 1.i o u true 2.i o u true 3.i o u true 4.i o u true 5.i o u true 6.i o u true 7.i o u true 8.i

28 23 889 28 26 47 59 30 35 28 34 63 29 28 41 40 48 27 27 938 926 924 925 928 930 1307 1302 1297 924 925 925 928

2260 2342 2477 2349 2856 2696 2731 2450 2442 2470 2903 2424 ∞ 2427 2349 2274 2512 2420 2428 2346 3504 2523 2743 2393 2328 2518 2752 2191 2350 2405 2397 2265

2152 2210 3555 2298 2581 2217 2264 2149 2187 2139 3598 2197 3171 3590 2174 2171 3876 2185 2125 1669 2796 2232 2099 1741 1758 2400 2192 1730 1652 1832 1731 1786

1440 970 869 898 787 1065 796 841 868 842 851 905 ∞ 944 840 881 1985 949 1042 752 768 1445 894 755 888 1007 852 1691 794 818 1075 793

2547 2843 1632 1546 1955 3359 2742 1768 2627 1788 2723 2936 2874 3066 2860 2947 2996 2904 1747 -

9702 9225 8650 9943 10821 9970 11350 9740 9984 9960 9789 9641 10716 9132 9391 9371 10592 10061 10613 12889 11322 11151 13314 11400 12621 16589 11251 13574 12891 12031 12693 12433

52 59 49 47 55 61 62 57 57 60 68 74 61 60 59 61 74 56 79 55 65 46 54 53 48 60 47 72 50 75 54 45

Soundness

To assess soundness, we use no-data-race and unreach-call benchmarks whose expected verdict is FALSE and compare each tool’s result with the expected verdict. A TRUE verdict in these cases misses a data race and is therefore a false negative; a single such verdict demonstrates unsound behavior. A FALSE or UNKNOWN verdict is consistent with soundness, but an UNKNOWN verdict does not establish that the property is false. Dartagnan and Ultimate Gemcutter recognize occurrences of barriers and pthread once but return ERROR and UNKNOWN, respectively. These inconclusive results provide no evidence of unsoundness or precision. RacerF does not support unreach-call and is therefore not evaluated for that property. Because Goblint is an overapproximating abstract interpreter, it returns UNKNOWN, rather than FALSE, for the false unreach-call properties. It could nevertheless return TRUE; such a result would be a false negative. Benchmark Results

Static Data Race Detection Off The Beaten Path

45

Table 5: Unsoundness experiment: TRUE verdicts for no-data-race or unreach-call when FALSE is expected are considered missed data races, and indicate unsound behaviour for this tool in this test. Input File

CPAchecker

Dartagnan

ESBMC

RacerF

UGemCutter

Goblint

b n false 1.c b n false 2.c b n false 3.c b n false 4.c b n false 5.c b u false 1.i b u false 2.i b u false 3.i b u false 4.i b u false 5.i b u false 6.i cl n false 1.i cl n false 2.i cl n false 3.c cl n false 4.c cl n false 5.c cl n false 6.c cl n false 7.c cl n false 8.c cl n false 9.c cl n false 10.c cl n false 11.c cl n false 12.c cl n false 13.c dl n false 14.i dl n false 15.i dl n false 16.c dl n false 17.c dl n false 18.c dl n false 19.c dl n false 20.c dl n false 21.c dl n false 22.c dl n false 23.c dl n false 24.c dl n false 25.c o n false 1.c o n false 2.c o n false 3.c o n false 4.c o n false 5.c o n false 6.c o u false 1.i o u false 2.i o u false 3.i o u false 4.i o u false 5.i

FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE TRUE TRUE FALSE FALSE UNKNOWN UNKNOWN FALSE FALSE FALSE FALSE FALSE FALSE FALSE TRUE TRUE FALSE FALSE FALSE FALSE UNKNOWN UNKNOWN FALSE FALSE FALSE UNKNOWN TRUE TRUE TRUE TRUE TRUE TRUE TRUE FALSE FALSE TRUE TRUE

ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR TRUE TRUE FALSE FALSE FALSE TRUE FALSE FALSE FALSE FALSE FALSE FALSE UNKNOWN TRUE TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR

FALSE FALSE FALSE FALSE FALSE ERROR ERROR ERROR ERROR ERROR ERROR TRUE TRUE FALSE FALSE FALSE TRUE TRUE FALSE FALSE FALSE TRUE FALSE UNKNOWN TRUE TRUE FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE FALSE ERROR TRUE TRUE TRUE TRUE TRUE TRUE ERROR ERROR ERROR ERROR ERROR

FALSE FALSE FALSE FALSE FALSE ERROR ERROR FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE TRUE FALSE ERROR ERROR FALSE FALSE FALSE FALSE TRUE TRUE FALSE FALSE FALSE FALSE TRUE FALSE FALSE TRUE FALSE TRUE -

UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN TRUE TRUE UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN TRUE TRUE UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN

UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN

13 0 9 2 2

6 0 0 3 3

14 0 6 5 3

6 0 3 1 2

4 0 0 2 2

0 0 0 0 0

# false negatives barriers once creationLockset descendantLockset

Example benchmarks indicating unsound behavior To illustrate the unsoundness we found, we present compact benchmarks that the corresponding tools report as data-race-free even though they contain a data race.

46

D. Bund, J. Erhard, M. Petter, and M. Schwarz

Assertions provide another way to expose unsound behavior. In SV-Comp, assertions are typically encoded using the unreach-call property, which can also reveal false negatives, as one of the examples below shows. – Racerf reports this program as data-race-free: // expected verdict: no-data-race false #include <pthread.h> #include <stdio.h> #include <assert.h> int g = 0; pthread_once_t once = PTHREAD_ONCE_INIT; void fun() { g++; // RACE } void *f(void *p){ fun(); } pthread_t id1; int main(void) { pthread_t id; pthread_create(&id1, NULL, f, NULL); pthread_once(&once, fun); return 0; }

– CPAChecker reports this file as data-race-free: // expected verdict: no-data-race false extern int __VERIFIER_nondet_int(); #include <pthread.h> int global = 0; pthread_mutex_t mutex = PTHREAD_MUTEX_INITIALIZER; pthread_t id1, id2; void *t1(void *arg) { pthread_mutex_lock(&mutex); global++; // RACE! pthread_mutex_unlock(&mutex); return NULL; } // t2 is not protected by mutex locked in main thread, // joining may not happen before unlock void *t2(void *arg) { global++; // RACE! return NULL; } int main(void) { pthread_create(&id1, NULL, t1, NULL); pthread_mutex_lock(&mutex); pthread_create(&id2, NULL, t2, NULL); int maybe = __VERIFIER_nondet_int(); if (maybe) { pthread_join(id2, NULL); } pthread_mutex_unlock(&mutex); return 0; }

Static Data Race Detection Off The Beaten Path

47

– ESBMC and CPAChecker report that the error state in this file is unreachable: // expected verdict: unreach-call false #include <pthread.h> #include <stdio.h> #include <assert.h> extern void abort(void); void reach_error() { assert(0); } // expected: unreach-call is false #define __VERIFIER_assert(cond) { if((cond)) { reach_error(); abort(); } } int g = 0; pthread_once_t once = PTHREAD_ONCE_INIT; void fun() { g++; } int main(void) { pthread_t id; pthread_once(&once, fun); pthread_once(&once, fun); __VERIFIER_assert(g==1); // g==1 is true here -> reach_error() is reached return 0; }

G.6

Precision

To assess precision, we use no-data-race and unreach-call benchmarks whose expected verdict is TRUE and compare each tool’s result with the expected verdict. A FALSE verdict in these cases is a false positive. Dartagnan and Ultimate Gemcutter recognize occurrences of barriers and pthread once but return ERROR and UNKNOWN, respectively. Neither result demonstrates that the tool can verify the property. RacerF does not support unreach-call and is therefore not evaluated for that property. Benchmark Results Table 6: Precision experiment: FALSE verdicts for no-data-race or unreach-call when TRUE is expected are false positives. Input File

CPAchecker

Dartagnan

ESBMC

RacerF

UGemCutter

Goblint

b n true 1.c b n true 2.c b n true 3.c b n true 4.c b n true 5.c b n true 6.c b n true 7.c

FALSE FALSE FALSE TRUE TRUE TRUE FALSE

ERROR ERROR ERROR ERROR ERROR ERROR ERROR

FALSE FALSE FALSE TRUE TRUE TRUE FALSE

FALSE FALSE FALSE FALSE FALSE FALSE FALSE

UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN

TRUE TRUE TRUE TRUE TRUE TRUE TRUE

Continued on next page

48

D. Bund, J. Erhard, M. Petter, and M. Schwarz Table 6 continued from previous page

Input File

CPAchecker

Dartagnan

ESBMC

RacerF

UGemCutter

Goblint

b u true 1.i b u true 2.i b u true 3.i b u true 4.i b u true 5.i b u true 6.i b u true 7.i b u true 8.i cl n true 1.c cl n true 2.c cl n true 3.c cl n true 4.c cl n true 5.c dl n true 6.c dl n true 7.c dl n true 8.c dl n true 9.c dl n true 10.i dl n true 11.i o n true 1.c o n true 2.c o n true 3.c o n true 4.c o n true 5.c o n true 6.c o n true 7.c o n true 8.c o n true 9.c o u true 1.i o u true 2.i o u true 3.i o u true 4.i o u true 5.i o u true 6.i o u true 7.i o u true 8.i

FALSE FALSE FALSE FALSE FALSE FALSE FALSE FALSE TRUE TRUE TRUE TRUE FALSE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE UNKNOWN TRUE TRUE TRUE UNKNOWN TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE

ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR TRUE TRUE TRUE TRUE ERROR TRUE TRUE TRUE TRUE TRUE TRUE ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR

ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE UNKNOWN TRUE TRUE TRUE TRUE TRUE TRUE ERROR ERROR ERROR ERROR ERROR ERROR ERROR ERROR

FALSE TRUE FALSE FALSE TRUE FALSE TRUE FALSE FALSE ERROR ERROR FALSE FALSE FALSE FALSE FALSE TRUE FALSE FALSE TRUE -

UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN TRUE TRUE UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN UNKNOWN

TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE TRUE

13 12 0 1 0

0 0 0 0 0

4 4 0 0 0

20 7 7 3 3

0 0 0 0 0

0 0 0 0 0

# false positives barriers once creationLockset descendantLockset

Example benchmarks indicating imprecise behavior To demonstrate the kinds of imprecise behavior we found, we present compact benchmarks that some analyzers report as containing a data race but that are actually data-race-free. The following is a representative barrier example: // expected verdict: no-data-race true #include<pthread.h> #include<stdio.h> #include<unistd.h> extern int __VERIFIER_nondet_int(); int g; pthread_barrier_t barrier;

Static Data Race Detection Off The Beaten Path void* f1(void* ptr) { g = 2; // NORACE pthread_barrier_wait(&barrier); return NULL; } int main(int argc, char const *argv[]) { int top = __VERIFIER_nondet_int(); int i = 0; pthread_barrier_init(&barrier, NULL, 2); pthread_t t1; pthread_create(&t1,NULL,f1,NULL); pthread_barrier_wait(&barrier); g = 3; //NORACE return 0; }

49

Related documents

• AutoTrans: AI-Assisted Automatic Translation of Security Assertions for RISC-V Processors#996974
• Cutting Corners on Uncertainty: Zonotope Abstractions for Stream-based Runtime Monitoring#629899
• Cutting Corners on Uncertainty: Zonotope Abstractions for Stream-based Runtime Monitoring#628037
• FSNIC: A Low-Latency Flow-Based Intrusion Detection Architecture for FPGA SmartNICs#1110726
• obliv-clang: Real-World Oblivious Programming in C++#280119