REINS: Agent-guided Thread Scheduling for Concurrency Bug Detection and Reproduction

REINS: AGENT- GUIDED T HREAD S CHEDULING FOR C ONCURRENCY B UG D ETECTION AND R EPRODUCTION

arXiv:2610.13421v1 [cs.SE] 9 Oct 2026

Yu Zhang The University of Queensland yu.zhang3@uq.edu.au

Corina S. Pasareanu Carnegie Mellon University pcorina@andrew.cmu.edu

Guowei Yang The University of Queensland guowei.yang@uq.edu.au

A BSTRACT Concurrency bugs manifest only under specific thread interleavings, making them hard to detect and reproduce. Existing controlled concurrency testing techniques take over thread scheduling to explore the interleaving space. As the space grows rapidly with program scale, finding interleavings that can trigger bugs within a limited budget remains challenging. The program’s concurrency semantics can reveal which variable accesses and synchronization operations under specific interleavings lead to unexpected program behavior, and thus help focus the exploration on bug-relevant interleavings. However, prior techniques have not fully exploited such semantic information. In this paper, we present R EINS, an agentic approach for detecting and reproducing concurrency bugs. At its core, R EINS guides thread scheduling with the agent’s reasoning about the concurrency semantics and known concurrency bug patterns. R EINS starts with runtime observations and combines them with static information to reason about the program’s concurrency behavior and formulate hypotheses about potential bugs. A hypothesis translates into a set of constraints on event orders and variable states, guiding a controlled scheduler toward interleavings likely to trigger the bug. R EINS draws conclusions from the execution results and keeps refining the constraints until the bug is triggered or the hypothesis is refuted. Compared with existing techniques on three public benchmarks, R EINS detects more bugs within the same time budget. Furthermore, R EINS found six previously unknown concurrency bugs in real-world projects, three of which have been confirmed by the developers. Keywords Concurrency Testing, LLM Agent, Detection, Reproduction

1

Introduction

Concurrency bugs are notoriously difficult to detect and reproduce [34, 44]. Due to the non-determinism of thread scheduling, they may manifest only under specific thread interleavings, making them difficult to expose during testing. Once triggered in production, they can lead to severe consequences, such as program crashes, data corruption, and security vulnerabilities [27]. Traditional stress testing, which relies on massive repeated executions and random perturbations, struggles to expose concurrency bugs in the vast thread-interleaving space [13, 34]. Controlled concurrency testing (CCT) takes over thread scheduling to make the exploration and reproduction of interleavings controllable, and has therefore become one of the prevailing approaches to concurrency bug detection and reproduction. CCT mainly proceeds through systematic enumeration [33, 34, 14] or randomized sampling with probabilistic guarantees [4, 54]. Recent work further improves the scheduling strategies, such as periodical scheduling [48] and selectively uniform sampling [55], or introduces ideas from reinforcement learning [32] and greybox fuzzing [49] to guide scheduling decisions. Despite these advances, bugs with narrow triggering windows and specific state preconditions remain difficult to expose within a limited budget. A key limitation of existing approaches is their insufficient exploitation of concurrency semantics of the program, e.g., which combinations of accesses are dangerous under the program logic, and in what state the program must be for a bug to be triggered. Such information is hard to obtain at the schedule level where these approaches operate. Recently, LLM-based agents have been applied to a wide range of software testing tasks [46, 56, 37, 47, 6], demonstrating strong capabilities in program comprehension and reasoning. These advances motivate us to investigate whether an agent’s reasoning about concurrency semantics can guide thread scheduling to more effectively trigger concurrency bugs.

Zhang et al.

However, effectively applying LLM agents to concurrency testing presents several key challenges, which we summarize as follows. C1: Incomplete understanding of concurrency semantics. LLM agents struggle to comprehend the concurrency semantics [19, 8], especially in large programs where a concurrency bug often spans multiple threads, functions, and files. Constrained by their context, the agents may not be able to piece together a reliable global view and locate bug-relevant operations in massive code bases. C2: The gap between concurrency semantics and thread scheduling. The agent reasons at the level of program semantics, focusing on the roles of variables and operations and on which thread interactions may lead to unexpected behavior. On the other hand, the scheduler must decide which thread to run next at every scheduling point during execution, and a single run may involve thousands of such points. Requiring the agent to make every scheduling decision is impractical, while its high-level semantic reasoning cannot be directly translated into concrete thread choices at individual scheduling points. C3: Unreliable agent output. The agent may produce plausible yet incorrect reasoning [45, 20], and may even hallucinate variables and code locations that do not exist, so its claims do not directly constitute evidence. In this paper, we propose R EINS, an agentic approach that addresses the above challenges for detecting and reproducing concurrency bugs in shared-memory multithreaded programs. The key insight of R EINS is to turn the agent’s reasoning about the concurrency semantics into constraints that the scheduler recognizes and enforces, thereby guiding thread scheduling toward the interleavings that are likely to trigger bugs, while the results of the controlled executions in turn serve as the evidence to refine the agent’s hypotheses. Specifically, R EINS introduces the following features to address the three challenges. For C1, R EINS starts from the shared-variable accesses observed in real executions. They reflect the actual interactions between threads and, although covering limited execution behavior, they help the agent to initially locate the key variables and operations. Starting from runtime information, the agent selectively examines relevant source code and queries the corresponding calling contexts and path conditions through static analysis to supplement information not captured by runtime observations. This enables the agent to reason about concurrency semantics without exhaustively exploring a large codebase. Based on this reasoning, the agent formulates bug hypotheses, each characterizing the program interactions that may lead to a specific concurrency bug pattern and its resulting failure. For C2, R EINS bridges the agent’s reasoning and the scheduler’s execution with the schedule plan. A schedule plan is a set of constraints on event orders and variable states, involving only the few key events and variables required to trigger a bug, which is the granularity the agent can express precisely at the semantic level. The agent derives the constraints from a hypothesis and writes them into a plan for the scheduler to execute. The scheduler controls the execution according to the plan at the scheduling points relevant to the constraints, and decides the rest at random. For C3, R EINS checks the agent’s output and takes execution results as evidence. The events and variables in a plan proposed by the agent are validated against the program before the plan is executed by the controlled scheduler. The conclusions of R EINS rest on real executions. For an execution that triggers the bug, its scheduling trace is recorded so that the bug can be deterministically replayed. For the executions that do not trigger the bug, the results distinguish whether the interleaving did not happen as planned or happened without the expected failure, and the agent then revises the plan or the hypothesis accordingly and iterates with subsequent executions. R EINS proceeds iteratively through three phases: comprehend, attempt, and assess. The comprehend phase builds the understanding of the concurrency semantics of the program and proposes a set of bug hypotheses as candidates. The attempt phase derives schedule plans for the candidates and executes them to trigger the hypothesized bugs. The assess phase analyzes the results, propagates conclusions to related candidates, and decides whether the next iteration returns to the comprehend phase for further collection or moves on to the attempt phase for the remaining candidates. R EINS continues until all candidates are settled or the time budget is exhausted. We evaluate R EINS on three public benchmarks [43, 5, 26], and compare it with representative controlled scheduling techniques [49, 55, 4, 44]. R EINS detected more bugs than all baselines across the three benchmarks. In particular, on the largest benchmark, RaceBench [26], R EINS detected 38 more bugs than the best-performing baseline [55] within the same time budget. In addition, on two real-world projects, R EINS detected six previously unknown concurrency bugs, three of which have been confirmed by their developers. In summary, this paper makes the following contributions: • We propose agent-guided thread scheduling, an approach that leverages the agent’s reasoning about the concurrency semantics to guide controlled scheduling toward bug-relevant schedules. • We design and implement R EINS, an agentic system for detecting and reproducing concurrency bugs, which integrates agent reasoning with controlled scheduling and iterates through the comprehend, attempt, and assess phases. • We evaluate R EINS against existing techniques on public benchmarks, where it detects more bugs within the same time budget, demonstrating its effectiveness. R EINS further identifies six previously unknown bugs in real-world projects. 2

Zhang et al.

1 2 3 4 5 6 7 8 9 10 11 12 13 14 15 16 17 18 19 20 21 22 23 24 25 26 27 28

Mutex mutatorsMutex_; ThreadSafeCodeBlockMap map; mozilla::Atomic<bool> CodeExists(false); bool RegisterCodeBlock(const CodeBlock* cs) { bool result; { LockGuard<Mutex> lock(mutatorsMutex_); result = map.insert(cs); } if (result) CodeExists = true; return result; } void UnregisterCodeBlock(const CodeBlock* cs) { size_t newCount; { LockGuard<Mutex> lock(mutatorsMutex_); map.remove(cs); newCount = map.length(); } if (newCount == 0) CodeExists = false; } T MemoryRead(uintptr_t addr) { if (CodeExists) {

Thread main loop { m = compile(); // calls RegisterCodeBlock

// calls RegisterCodeBlock

… drop(m); gc();

… loop { try { w.load(oob); } // calls MemoryRead catch (RuntimeError) {…}

// calls UnregisterCodeBlock

} } }

main

worker

} return *(T*)addr;

map

CodeExists

∅

true

≠∅

true

≠∅

true

≠∅

false

≠∅

false

gc() → UnregisterCodeBlock(X) when X is the only block left in map

e₁ ⟨main, W(map)@ℓ17⟩ e₂ ⟨main, R(map)@ℓ18⟩

newCount = 0; unlocked at ℓ19; ℓ20 pending

compile() → RegisterCodeBlock(Y) insert Y into map, then set CodeExists

e₃ ⟨worker, W(map)@ℓ8⟩ e₄ ⟨worker, W(CodeExists)@ℓ10⟩ w.load(oob) → MemoryRead(a) e₅ ⟨worker, R(CodeExists)@ℓ23⟩ reads true → ℓ25 trap, caught ✓

// an out-of-bounds wasm access must trap

if (IsWasmOutOfBounds(addr)) throw RuntimeError();

Thread worker loop { w = compile();

writes false from the old newCount

e₆ ⟨main, W(CodeExists)@ℓ20⟩

}

w.load(oob) → MemoryRead(a) e₇ ⟨worker, R(CodeExists)@ℓ23⟩ reads false → ℓ27 raw read → SIGSEGV ✗

(a)

(b)

Figure 1: An atomicity violation from Mozilla SpiderMonkey that ends in a crash on an out-of-bounds access. CodeExists caches whether map is non-empty, but the two are not updated atomically. (a) The simplified key code snippet. (b) The thread interleaving that triggers the bug, with red marking the states where map and CodeExists disagree.

2

Overview

In this section, we first use a motivating example to illustrate why concurrency bugs are difficult to trigger, and then provide an overview of how R EINS guides thread scheduling to detect such bugs. Motivating Example. Figure 1 shows an atomicity violation from Mozilla SpiderMonkey [31], the JavaScript and WebAssembly (wasm) engine of Firefox. An out-of-bounds wasm memory access must be turned into a RuntimeError that JavaScript can catch, rather than crashing the process. SpiderMonkey records the current wasm code blocks in a lock-protected map, caches whether map is non-empty in the atomic flag CodeExists, and performs the bounds check in MemoryRead only when CodeExists is true (lines 23–25). Critically, a false CodeExists while map is non-empty causes MemoryRead to skip the required bounds check. However, UnregisterCodeBlock computes the remaining count while holding the lock but updates CodeExists only after releasing it (lines 16–20). As shown in Figure 1(b), the main thread removes the last code block and observes newCount = 0 (e1 , e2 ), but is delayed before updating the flag. Meanwhile, the worker thread registers a new code block and sets CodeExists to true (e3 , e4 ), restoring a consistent state in which map ̸= ∅ and CodeExists = true. Its first out-of-bounds access is therefore correctly trapped (e5 ). The main thread then resumes and writes CodeExists = false based on its stale newCount (e6 ), overwriting the worker’s update and leaving map ̸= ∅ while CodeExists = false. A subsequent out-of-bounds access by the worker reads this false flag, skips the bounds check, and directly accesses the invalid address (e7 ), resulting in SIGSEGV. Triggering this bug requires several ordering constraints to hold at once. The main thread must be delayed between observing newCount = 0 and writing the flag, the worker must complete a registration within this interval, and its subsequent out-of-bounds access must occur before any later registration corrects the flag. Such opportunities are rare. The window opens only when the last code block is unregistered, and it lasts only a single statement, during which the worker must happen to complete a registration. Such an interleaving is therefore unlikely to arise under natural scheduling and calls for explicit control over thread execution. Controlled Scheduling. Controlled concurrency testing [33, 34, 14, 4, 54] takes over thread scheduling by inserting scheduling points at key operations, such as shared-memory accesses and synchronization primitives, where the scheduler selects a runnable thread to execute. An execution is thus represented by a sequence of scheduling decisions, which can be recorded to deterministically reproduce a bug-triggering execution. Such techniques can cover the buggy interleaving in Figure 1 in theory. However, real-world programs contain numerous scheduling points, and the scheduler does not know which decisions are relevant to the bug, so reaching the target interleaving remains challenging for bugs with narrow triggering windows and multiple ordering constraints. 3

Zhang et al.

Global State Tools

SCOPE

SHARED_ACCESS

CANDIDATES

ATTEMPTS

[SearchCode] [InstrumentTarget] [RunTarget] [AnalyzeStaticInfo] [AnalyzeSharedAccess] [AnalyzeExecution]

Δtotal

Comprehend

Attempt

Assess

propose bug hypotheses from runtime observations and static program information

guide thread scheduling to confirm or refute hypotheses

analyze the execution results of the current round and decide the next step

Scope measurement

Subagent dispatch

Batch selection for each candidate

Result propagation

Δsub

Runtime observation Program Static inspection Hypothesis proposal

Plan

Examine

propose a schedule plan to trigger the hypothesized bug

execute the plan and analyze results to revise or conclude

≤ p plan versions

≤ q runs per plan

Attribution analysis Final Report Coverage review Decision

after all subagents finish

Result collection further collection

next batch

Figure 2: Overview of R EINS. The agent runs in three phases within a total time limit ∆total , and each subagent runs within a time limit ∆sub , with at most p plan versions and q runs per plan.

Agent-guided Thread Scheduling. Triggering the bug in Figure 1 depends on only a few scheduling decisions, yet nothing at the schedule level tells them apart from the numerous others. R EINS combines runtime observations and static information to help the agent propose a bug hypothesis: CodeExists is updated outside the lock and may overwrite the true just set by another thread with false, which in turn lets an out-of-bounds access skip the check and crash. From the hypothesis, R EINS further derives the event orders and variable states required to trigger the bug. In terms of order, the worker must complete a registration (e4 ) and enter its memory-access loop (e5 ) before the main thread writes the stale false (e6 ), and the worker must then perform another out-of-bounds access (e7 ), so that e7 reads the false written by e6 rather than a true corrected by a later registration. In terms of variable state, CodeExists must be true when e6 occurs, so that e6 overwrites the valid value just set by e4 , the inconsistent state with map non-empty and CodeExists false arises, and e7 skips the check and crashes. These requirements are expressed as constraints for the scheduler, which prioritizes or delays threads at the relevant scheduling points to satisfy them and decides the remaining points at random. The execution results feed back whether the intended interleaving is reached and whether the bug is triggered, and the agent refines the constraints or revises the hypothesis accordingly. Figure 2 shows the workflow of R EINS, driven by a lead LLM agent1 that iterates in rounds through the comprehend, attempt, and assess phases. The first round starts from the comprehend phase, which proposes bug hypotheses as candidates. In the attempt phase, the agent dispatches a subagent for each selected candidate to propose and execute plans. Every round ends with the assess phase, which consolidates the results of the round and decides which phase the next round starts from. We formalize the related notions in Section 3 and detail R EINS in Section 4.

3

Preliminary

In this section, we introduce the foundational notions and relevant definitions. Basic Notions. We use the symbol P to denote the target concurrent program, the symbol c to denote a source file in P , and ℓ to denote the line number in source code. The symbols F (f ∈ F ) and V (v ∈ V ) denote the set of functions and the set of variables, respectively, and T (t ∈ T ) denotes the set of threads spawned during execution. A variable access site τ = op(v)@c:ℓ denotes a read or write operation op ∈ {R, W} on variable v at line ℓ of source file c. An event e = ⟨t, τ ⟩ represents thread t performing the access τ during execution. Definition 1. The observed access summary of a variable v is σv = ⟨v, [⟨e1 , L1 ⟩, ⟨e2 , L2 ⟩, . . .]⟩, which records the events on v in the order observed over a set of executions, where Li is the set of locks held by thread t when the event ei = ⟨t, τ ⟩ occurs. Definition 2. A bug hypothesis is a conjecture proposed by the agent about a potential concurrency bug, denoted as h = ⟨Vh , Th , δ⟩, where Vh is the set of variables involved, Th is the set of access sites on which the hypothesis rests, and δ is a natural-language description of the hypothesis, i.e., which accesses interleave in which way to go wrong, and its expected failure. 1

Unless otherwise stated, “the agent” in the rest of the paper refers to the lead agent.

4

Zhang et al.

Definition 3. A schedule plan consists of a set of constraints, denoted as π = ⟨S, Φ⟩, where S = [e1 ≺ e2 ≺ · · · ≺ en ] is a sequence of ordering constraints, each e ≺ e′ requiring that event e occur before event eV′ ; and Φ = {(e, ϕ)} is a set of state constraints, each pair (e, ϕ) requiring that ϕ hold when event e occurs, where ϕ = i φ(vi ) is a conjunction of predicates, each φ(vi ) restricting the value of an involved variable vi . Example 1. For the bug in Figure 1(a), the schedule plan that eventually triggers the bug is S = [e4 ≺ e5 ≺ e6 ≺ e7 ] and Φ = {(e6 , CodeExists = true)}, with events as labeled in Figure 1(b). The ordering constraints require the four events to occur in sequence, and the state constraint requires CodeExists to be true when e6 occurs. Definition 4. The execution result of a single run of a schedule plan π is a tuple x = ⟨ϵ, κS , κΦ , θ, γ⟩. The termination result of the run is denoted by ϵ ∈ {normal, triggered, timeout, other}, indicating that the run exits normally, triggers the expected bug, times out without triggering it, or fails for a reason other than the expected bug. The symbol κS ∈ {0, . . . , n} is the length of the prefix of S = [e1 ≺ · · · ≺ en ] satisfied in order, i.e., e1 , . . . , eκS occur in the planned order while eκS +1 does not, with κS = n meaning all are satisfied. Similarly, κΦ ⊆ Φ is the set of state constraints (e, ϕ) whose ϕ never holds when e is ready to occur, being ∅ if all state constraints are satisfied. If κS = n and κΦ = ∅, the run is engaged as planned. The scheduling trace of the run is denoted by θ : {1, 2, . . .} → T , mapping the i-th scheduling point to the thread θ(i) ∈ T chosen to execute there, which allows the run to be deterministically replayed. The new coverage of the run is denoted by γ = ⟨Cγ , Tγ ⟩, where Cγ is the set of source files and Tγ the set of access sites reached in this run but not observed before. Executing π multiple times yields the result sequence Xπ = [x1 , x2 , . . .], whose aggregation X̂π summarizes the number of runs and engaged runs, the count of each ϵ, the distributions of κS and κΦ , the scheduling trace θ of a triggering run, and the merged γ. Problem Statement. Given a shared-memory multithreaded program P with its test entries and inputs, we aim to detect and reproduce concurrency bugs in P within a time budget ∆total through agent-guided thread scheduling. This work targets the common concurrency bug patterns [27, 38], including data races, atomicity violations, order violations, and deadlocks, that lead to observable execution failures, such as crashes, assertion failures, and hangs. Silent concurrency errors that produce wrong results while the program terminates normally are not considered currently.

4

Methodology

In this section, we introduce R EINS in detail. As shown in Figure 2, R EINS takes the target program as input and proceeds in rounds through three phases within the time budget ∆total , maintaining a set of global states and equipped with several tools. Each round verifies a batch of candidates, dispatching one subagent per candidate. A subagent works within a time limit ∆sub , proposing at most p plan versions and running each version at most q times. At the end, R EINS generates a final report of the detected bugs, each with its scheduling trace θ for reproduction. We first introduce the global states and the execution infrastructure, and then describe the three phases in turn. 4.1

Global States and Execution Infrastructure

Throughout the process, R EINS maintains four global states and provides the agent with an execution infrastructure of tools and a controlled scheduler. We describe them as follows. Global States. The four global states are shown at the top of Figure 2. SCOPE records the set of source files {c} reached during execution, measured initially in the comprehend phase and extended in the attempt phase with newly reached files. SHARED_ACCESS records the observed access summaries {σv } of all shared variables, initially collected in the comprehend phase and extended in the attempt phase as new access sites or events are observed. CANDIDATES records all bug hypotheses proposed by the agent as candidates, i.e., a set of triples ⟨h, status, settledBy⟩. Each candidate is tagged with a status: pending for candidates not yet verified, succeeded for those triggered, refuted for those shown by evidence not to be bugs, and uncertain for those tried but neither triggered nor refuted. The field settledBy records whether the status is settled by the candidate’s own attempts (own) or by a related candidate (related), and is initialized to ⊥. ATTEMPTS records the attempts on each candidate as a map h 7→ [⟨round , A⟩, . . .], where each attempt is made in one round and A = [⟨π1 , X̂π1 ⟩, ⟨π2 , X̂π2 ⟩, . . .] is the sequence of schedule plans tried in that round with their aggregated execution results. Tools. Table 1 lists the six tools in R EINS. [SearchCode] retrieves source code by function name, regular expression, or file and line range. [InstrumentTarget] instruments the variable access sites in the target with a unified probe macro and compiles it into two binaries, covering all sites in SCOPE by default or a specified subset on request. In the recorder binary, the probe records the executing thread, the access site, and the lock set held at that moment. In the scheduler binary, the probe yields control to the scheduler so that each site becomes a scheduling point. [RunTarget] runs the target in four modes. The natural mode runs the program as is. The collect mode runs the recorder binary and collects the access traces. The control mode first validates whether the variables and locations in 5

Zhang et al.

Table 1: Tools in R EINS. Tool

Description

[SearchCode] [InstrumentTarget] [RunTarget] [AnalyzeStaticInfo] [AnalyzeSharedAccess] [AnalyzeExecution]

Search source code by name, pattern, or location Instrument and build binaries for recording or scheduling: recorder | scheduler Run the target in one of the modes: natural | collect | control | replay Static analysis for the requested information: callGraph | pathCond | sharedVar Build SHARED_ACCESS and analyze access profiles and conflicting pairs Aggregate the execution results of a plan

Algorithm 1: Scheduling decision of the controlled scheduler in the control mode. Input: plan π = ⟨S, Φ⟩; runnable threads Trdy ; the length s of the satisfied prefix of S Output: the next thread t∗ to run 1 partition Trdy into Tnext , Theld , and Tfree ; 2 if Tnext ̸= ∅ then 3 t∗ ← a thread in Tnext ; s ← s + 1; 4 else 5 if Tfree ̸= ∅ then 6 t∗ ← a thread drawn from Tfree at random; 7 else 8 t∗ ← a thread forcibly released from Theld , not advancing s; if s has not advanced within a timeout then abandon the remaining constraints; ∗ ∗ 11 append t to θ; return t ; 9

10

a given plan π actually exist. A valid plan is executed by running the scheduler binary under the controlled scheduler, and an invalid one is returned with the reason. The replay mode deterministically replays a run under the controlled scheduler according to a given θ. [AnalyzeStaticInfo] performs static analysis on the Clang AST. The callGraph mode returns the callers and callees of a function and the call chains reaching a site. The pathCond mode extracts the branch conditions dominating an access site, and the sharedVar mode identifies the shared variables and their access sites. [AnalyzeSharedAccess] analyzes the accesses collected at runtime. It first identifies the shared variables from the traces, i.e., the variables accessed by multiple threads, and aggregates their accesses into SHARED_ACCESS. It then reports how many threads and sites access each variable, and identifies the conflicting access pairs on a given variable, where two accesses form a pair if they come from different threads with at least one write, hold no common lock, and are not ordered by thread creation or join, together with the number of executions in which each condition holds and the distribution of their observed orders. [AnalyzeExecution] aggregates the execution results Xπ of all runs of a plan into X̂π . Controlled Scheduler. The control and replay modes of [RunTarget] run on top of the controlled scheduler, a serializing scheduler that we implement following Coyote’s approach [1, 11]. The scheduler takes the instrumented variable accesses and the intercepted synchronization operations as scheduling points. A thread hands control to the scheduler on reaching a scheduling point, and only one thread runs at any moment. The control mode drives the execution to satisfy the plan π. Let s denote the length of the satisfied prefix of S = [e1 ≺ · · · ≺ en ], so the scheduler waits for the next event es+1 and releases it only when its state constraint ϕs+1 in Φ holds, or immediately if Φ pairs no constraint with es+1 . At each scheduling point, the scheduler decides following Algorithm 1. The paused threads, each about to perform one event, are partitioned into three classes. A thread in Tnext is about to perform es+1 with ϕs+1 holding, and releasing it advances s. A thread in Theld is suspended, as its event comes after es+1 in S, or is es+1 while ϕs+1 does not yet hold, or would change the state of a variable in ϕs+1 once ϕs+1 holds and before es+1 occurs. The remaining threads irrelevant to the current constraints belong to Tfree and are scheduled at random. When only suspended threads remain or s has not advanced within a timeout, the scheduler forcibly releases a thread or abandons the remaining constraints, and such forced steps do not advance s. A run is therefore biased toward satisfying π rather than guaranteed to, and κS and κΦ record how the constraints are actually satisfied in the run, while θ records the scheduling decision at each scheduling point. The replay mode releases threads point by point according to θ and thus deterministically reproduces the recorded run. 6

Zhang et al.

4.2

Comprehend: Hypothesizing from Runtime Observations and Static Information

The comprehend phase proposes hypotheses of potential concurrency bugs by combining runtime observations with static program information, and proceeds in four steps. Scope measurement. The agent first calls [RunTarget] to run the program in natural mode, collects the reached source files, and writes them into SCOPE as the initial scope. Runtime observation. The agent calls [InstrumentTarget] to instrument the files in SCOPE, then calls [RunTarget] in collect mode to collect the variable access traces at runtime, and calls [AnalyzeSharedAccess] to populate SHARED_ACCESS. From the access profile of each variable, the agent picks the variables of interest, such as those accessed by multiple threads at multiple sites, examines their conflicting access pairs, and judges which pairs serve as clues. Static inspection. Following the runtime clues, the agent reads the relevant source code via [SearchCode] and calls [AnalyzeStaticInfo] when needed for call relations and path conditions. Combining the dynamic and static information, the agent reasons about the concurrency semantics: the role of each thread, the state and synchronization operations related to the key shared variables, whether the orders between their accesses are protected, and which reachable code regions remain unexecuted. On this basis, drawing on its knowledge of known concurrency bug patterns, the agent judges which interleavings may break the expected program behavior and with what consequences. Hypothesis proposal. Based on the above analysis and reasoning, the agent proposes a set of bug hypotheses, each of which is written into CANDIDATES as ⟨h, pending, ⊥⟩. Example 2. For the program in Figure 1, the observed access summary σCodeExists of the shared variable CodeExists records the events e4 , e5 , and e6 , all with an empty lock set, and σmap records e1 , e2 , and e3 , all with the lock set {mutatorsMutex_}. Through [AnalyzeSharedAccess], the agent obtains the conflicting access pair on CodeExists, namely ⟨worker, W(CodeExists)@ℓ10⟩ and ⟨main, W(CodeExists)@ℓ20⟩, where the source file c of the variable access sites is omitted for brevity. Reading the source code further, the agent understands that CodeExists caches whether map is non-empty, is updated in a different critical section from map, and decides whether MemoryRead performs the bounds check. The agent thus proposes the hypothesis h with Vh = {CodeExists, map}, Th = {W(CodeExists)@ℓ10, W(CodeExists)@ℓ20, R(CodeExists)@ℓ23, W(map)@ℓ8, W(map)@ℓ17, R(map)@ℓ18} and δ: if a registration occurs between the computation of newCount and the write to CodeExists in UnregisterCodeBlock, the written false overwrites the just-published true, and a subsequent out-of-bounds access skips the bounds check and crashes. 4.3

Attempt: Guiding Thread Scheduling to Confirm or Refute Bug Hypotheses

The attempt phase confirms the hypothesis of each candidate by guiding thread scheduling to trigger the described bug, or refutes it with code and execution evidence, in the following steps. Batch selection. The agent selects a batch for this round from the pending or uncertain candidates in CANDIDATES. Considering the strength of evidence of each candidate, the number of remaining candidates, and the diversity within the batch, the agent picks the candidates most likely to be triggered, and the batch size is also decided by the agent. Subagent dispatch. The agent dispatches one subagent for each selected candidate, passing the hypothesis h of the candidate, the existing attempts on h in ATTEMPTS if the candidate has been dispatched in previous rounds but remains uncertain, and the budget of the subagent, i.e., at most p plan versions, at most q runs per plan, and the time limit ∆sub . The output of the subagent is all plans tried in the round with their aggregated execution results, i.e., [⟨π1 , X̂π1 ⟩, ⟨π2 , X̂π2 ⟩, . . .]. The subagent can use [SearchCode], [AnalyzeStaticInfo], [AnalyzeSharedAccess], [RunTarget], and [AnalyzeExecution], and can read SCOPE and SHARED_ACCESS. Inside a subagent, the work proceeds in two phases, which alternate until the bug is triggered, refuting evidence is found, or the budget of the subagent is exhausted. • Plan. Based on the hypothesis h = ⟨Vh , Th , δ⟩ of the candidate, the subagent works out under what thread schedule the bug described in δ can be triggered, calling [SearchCode], [AnalyzeStaticInfo], and [AnalyzeSharedAccess] when needed. The inference is turned into two kinds of requirements: which events must occur in which order, and whether the relevant variables must be in particular states, corresponding to ordering constraints and state constraints respectively, which form the plan π = ⟨S, Φ⟩. • Examine. The subagent submits π to [RunTarget] in control mode. The plan is first validated. One that fails is returned for revision and resubmitted without counting toward the p plan versions, and a validated one counts as one version, with at most p versions in total. The controlled scheduler executes each version for at most q runs, and stops early once a run triggers the hypothesized bug. Then the subagent calls 7

Zhang et al.

[AnalyzeExecution] to aggregate the results Xπ of all runs into X̂π , and judges the outcome in three cases. If some run is engaged as planned with ϵ = triggered, the bug is triggered. If some run is engaged but ϵ ̸= triggered, the interleaving occurred without the expected consequence; the subagent then analyzes whether a constraint is missing or whether no bug exists there. If no run is engaged, the subagent locates the stall from X̂π and adjusts the corresponding constraint. In the latter two cases, the subagent returns to the plan phase and proposes a new version until the bug is triggered, refuting evidence is found, or p or ∆sub is reached. Result collection. After each subagent returns, the agent updates the status of the candidate in CANDIDATES according to the returned results, attaching the scheduling trace θ for a succeeded candidate. The agent then writes the attempt ⟨round , A⟩ into ATTEMPTS, and adds any new coverage γ reported in the execution results to SCOPE and SHARED_ACCESS. Example 3. For h in Example 2, the subagent derives from δ that the overwrite must follow the worker’s publication, and first proposes π1 with S = [e4 ≺ e6 ] and Φ = ∅. In X̂π1 , every run is engaged yet ends with ϵ = normal. The subagent reasons that the main thread overwrites before the worker enters wasm execution, and the next scheduling point is its next registration, which repairs CodeExists before any read observes it. The subagent then proposes π2 with S = [e4 ≺ e5 ≺ e6 ≺ e7 ] and Φ = {(e6 , CodeExists = true)}. A run of π2 is engaged as planned with ϵ = triggered. The candidate is updated in CANDIDATES as ⟨h, succeeded, own⟩ with θ attached for reproduction, and this round’s attempt of h, [⟨π1 , X̂π1 ⟩, ⟨π2 , X̂π2 ⟩], is appended to ATTEMPTS. 4.4

Assess: Analyzing Results to Steer the Next Round or Conclude

After all subagents of a round return, R EINS enters the assess phase, analyzes the results of the round as a whole, and accordingly steers the next round or concludes, in the following steps. Result propagation. The agent checks whether the conclusions of this round have implications for the pending or uncertain candidates. Evidence refuting one candidate may also refute those resting on the same mechanism or variable, and executing one candidate may trigger the bug of another. The agent accordingly updates the status of such candidates and marks their settledBy as related. Attribution analysis. The agent analyzes why the candidates of this round succeed or fail. For the triggered candidates, it summarizes what their hypotheses have in common to infer the likely bug patterns in this program. For the untriggered ones, it distinguishes whether the plans are not engaged or engaged but not crashed to infer why. The patterns of success then bias the batch selection and hypothesis proposal of the next round toward similar candidates and mechanisms, and the causes of failure are passed as hints to the subagents dispatched next. Coverage review. For the files Cγ and sites Tγ newly added to SCOPE and SHARED_ACCESS in the attempt phase, the agent inspects their source and static information, and judges whether the files deserve instrumentation and collection and whether the sites deserve hypothesis proposal. Decision. The agent then decides where the next round starts: from the comprehend phase if the coverage review finds new files or sites worth analyzing, or from the attempt phase if pending or uncertain candidates remain. If all candidates are settled, the whole process ends.

5

Evaluation

To evaluate R EINS, we consider the following research questions: RQ1 How does R EINS perform compared with existing controlled scheduling techniques? RQ2 Can R EINS detect concurrency bugs in real-world projects? RQ3 How do the key designs of R EINS contribute to its effectiveness? 5.1

Experimental Setup

Implementation. R EINS is implemented on top of the Claude Agent SDK [2]. The six tools described in Section 4.1 are exposed to the agents through an MCP server. The lead agent and the subagents are each driven by a skill: the skill of the lead agent describes the three-phase workflow in Sections 4.2–4.4, and the skill of the subagent describes how to propose and examine plans for a single candidate in the attempt phase (Section 4.3). A subagent is spawned by the lead agent as a separate session that shares the same output directory with the lead agent but has its own context and wall clock, and we set the subagents within a round to be dispatched sequentially. We use Claude Sonnet 4.6 as the 8

Zhang et al.

6

5

8

9

17

4

6

5

8

9

not detected

17

not detected

Time to first trigger (s)

Schedules to first trigger

4

105 104 103 102 101

104 103 102 101 100 10−1

100 S IN

RE

RW

SU

F

RF

T-3

PC

0 T-1 PC

S IN

RW

RE

(a)

RW

SU

F

RF

T-3

PC

0 T-1

PC

RW

(b)

Figure 3: Distribution of the number of schedules (a) and the time (b) to the first trigger on SCTBench and ConVul. Each dot corresponds to one program, and horizontal bars mark the medians over the detected programs; hollow circles in the shaded band, with counts aside, denote the programs not detected within the time budget, and in (b) the lower edge of the band coincides with the budget.

default model. The per-phase parameters are set uniformly as follows: in the comprehend phase, the trace collection in collect mode executes each target 10 times; in the attempt phase, the budget of a subagent is at most p = 5 plan versions, at most q = 50 runs per plan, and a time limit ∆sub of 30 minutes. The total time budget ∆total is set to 5 hours per target throughout the evaluation. Environment. All experiments are conducted on a machine with a 64-core AMD Ryzen Threadripper PRO 7985WX CPU and 512 GB of memory, running Ubuntu 24.04 LTS. 5.2

RQ1: Comparison with Existing Techniques

To answer RQ1, we compare R EINS with representative controlled scheduling techniques on three publicly available benchmarks of concurrent programs, and evaluate its effectiveness and efficiency. Benchmark. The three benchmarks are SCTBench, ConVul, and RaceBench. SCTBench [43, 39] comprises buggy pthread programs drawn from test suites of prior concurrency testing and verification work, and we adopt the curated version [48] of 42 programs. Each program contains a single known bug that manifests as an assertion violation, crash, or hang, and the bugs cover data races, atomicity violations, order violations, and deadlocks. Most programs are under 2 kLOC, and a few link against real-world projects of tens of thousands of lines. ConVul [5, 10] consists of 10 bugs extracted from concurrency-related CVEs into single-file programs of under 300 LOC, mostly data races that lead to memory errors such as use-after-free, null-pointer dereference, and double-free. RaceBench [26] is an injected concurrency-bug benchmark with built-in assertion oracles, consisting of 15 multi-file programs from PARSEC and SPLASH-2 of about 3 to 26 kLOC. Each program has five variants, and each variant is injected with 20 bugs covering data races, atomicity violations, and order violations, all observable as crashes once triggered. Baseline. Among the advanced controlled scheduling techniques [48, 24, 53, 55, 49], we select the state-of-the-art SURW [55] and RFF [49] as the baselines. In addition, since the scheduler of R EINS decides the scheduling points beyond the plans at random, we also include the classic randomized algorithms probabilistic concurrency testing [4] with depth d=3 and d=10 (denoted PCT-3 and PCT-10) and random walk (RW) [44]. We use the public implementations of SURW and RFF, and reimplement the PCT-3, PCT-10, and RW algorithms on the same scheduler as R EINS. Comparison Results. We first evaluate on the 52 programs from SCTBench and ConVul, where each program contains a single bug, and a program is counted as a detection failure if no bug is triggered within ∆total . Following existing work [49, 55], we measure the number of schedules executed until the bug is first triggered2 . Considering that the tools differ in the granularity of scheduling points and the cost of a single execution, we also report the wall-clock time to the first trigger, as well as the token consumption of R EINS. 2

For R EINS, the number of schedules counts only the executions under the controlled scheduler in the attempt phase.

9

Zhang et al.

Table 2: Results on RaceBench. Each row is a base program with five variants, each injected with 20 bugs (max. 100 per program). kLOC is the average size of the five variants, and each tool column reports the number of distinct injected bugs detected within the time budget. The best result of each row is in bold. Program kLOC R EINS SURW RFF PCT-3 PCT-10 RW blackscholes streamcluster water_nsquared canneal water_spatial dedup fluidanimate pigz cholesky bodytrack raytrace ferret raytrace2 volrend x264

3.0 3.1 4.0 4.1 4.6 4.8 5.1 7.2 8.3 8.4 10.2 11.2 11.4 15.2 26.3

19 59 17 52 67 57 56 75 65 50 36 66 48 34 68

32 59 11 55 41 58 55 76 54 38 60 67 49 31 45

24 40 20 51 49 50 38 61 43 30 43 80 33 23 60

23 31 9 19 23 22 41 59 32 24 24 41 24 16 25

25 43 12 27 33 24 46 62 38 26 24 54 24 17 34

Total (max. 1,500)

–

769

731

645

413

489 439

10 44 13 29 33 33 27 59 36 30 20 37 25 13 30

In terms of detection, R EINS detects 48 out of the 52 programs, while SURW, RFF, PCT-3, PCT-10, and RW detect 46, 47, 44, 43, and 35, respectively. The four programs missed by R EINS are also missed by all the baselines, and the one additionally missed by RFF is due to its instrumentation not supporting the program. Figure 3(a) shows that all the detections of R EINS are completed within about 100 schedules, whereas the baselines exhibit long tails of 103 to 104 schedules on hard programs. Figure 3(b) shows that R EINS is two to three orders of magnitude more expensive than the baselines in time due to the reasoning of the agent, with a median time to the first trigger of about 7 minutes and a maximum of 29 minutes, and its token consumption ranges from 386k/6k to 4.1M/68k input/output tokens per program. Overall, on these two benchmarks, R EINS shows no significant advantage in detection, but the agent guidance brings no degradation, and the far fewer schedules indicate that the constraints derived from the hypotheses do narrow the scheduler down to the interleavings likely to trigger the bug. We further evaluate on RaceBench, which consists of larger programs. Each program variant is treated as a target and contains multiple injected bugs, and we count the distinct injected bugs triggered within ∆total . All tools use the seed input provided by RaceBench, and the triggered bugs are configured not to abort the process on subsequent triggers so that the remaining bugs can be further explored. For R EINS, since the injected bugs of RaceBench leave recognizable traces in the source code, such as numbered state variables and trigger functions, we mechanically anonymize these traces by renaming the relevant identifiers and removing the injection markers without changing any program instruction, to prevent the agent from locating the injected bugs directly. Table 2 and Figure 4 present the per-program detection and the cumulative detection over time. Among the 1,500 injected bugs of the 75 targets, R EINS detects 769 bugs, the highest among all the tools and 38 more than the best baseline SURW with 731. In terms of the time trend, PCT and RW saturate within about one hour, as random scheduling quickly covers the shallow interleavings. R EINS detects no bug in the first five minutes due to the collection and analysis in the comprehend phase, then grows rapidly, surpasses SURW between 60 and 90 minutes, and keeps growing until the budget runs out. The end-to-end wall time of R EINS ranges from 84 minutes to 5 hours, and the token consumption ranges from 5.7M/68k to 153.1M/912k input/output tokens per target. Compared with SURW and RFF, R EINS performs worse on programs raytrace, blackscholes, and ferret. The untriggered bugs share a common characteristic that the triggering requires the state variables to hold specific values. These values rarely appear at runtime and can only be produced through a large number of interleavings and even the interleavings inside a statement. During the scheduled execution, R EINS waits for the values to appear or guides a limited number of interleavings rather than precisely controlling every step of the value accumulation, and its source-level instrumentation misses some interleaving points inside a statement, so the values can hardly appear within the schedule budget of a single plan. As a result, even though the agent correctly understands the triggering conditions, it fails to trigger these bugs. SURW and RFF instrument at the binary level, which allows thread switches inside a statement, and they sample interleavings with a large number of executions, so they can reach these values instead. For R EINS, instrumenting the 10

Zhang et al.

Rᴇɪɴs

SURW

RFF

PCT-3

PCT-10

RW

Number of bugs

800

600

400

200

0 0.5

1

5

15

30

60

120

300

Time (minutes)

Figure 4: Cumulative number of injected bugs on RaceBench detected over time, summed over the 75 targets.

scheduler at a finer granularity or employing a solver to compute the paths to the target values is a feasible improvement. In addition, all the tools find no more than about 51% of the 1,500 injected bugs within the 5-hour budget, which comes from two aspects. The first is the test input. RaceBench provides one seed input for each program variant and a separate mutated input that triggers each of the 20 injected bugs. Switching inputs per bug requires dividing the execution budget among multiple inputs with no consistent allocation across tools, and some tools perform additional processing for each input, for example the per-input dynamic preprocessing of RFF over 20 inputs on the variants of cholesky costs time comparable to the whole budget. We therefore uniformly use the seed input, but some injected bugs can only be triggered with the specific data in their mutated inputs, which imposes a common ceiling on the detection of all tools. The second is the time budget. Considering the token cost of R EINS, we set ∆total to 5 hours, while the curves of R EINS, SURW, and RFF are still rising at the end of the budget. In particular, some programs run slowly after instrumentation, and the schedules SURW completes within the budget are far fewer than the 10,000 schedules per target used in its original evaluation. Answer to RQ1: Compared with existing controlled scheduling techniques on the three benchmarks, R EINS detects more concurrency bugs. 5.3

RQ2: Bug Finding in Real-world Projects

We further apply R EINS to real-world concurrent projects to evaluate its effectiveness. Target Projects. We select the target projects by tracing the real bugs and base programs in the three benchmarks back to their upstream projects and keeping those still actively maintained, which yields two Mozilla projects, NSPR [30] and SpiderMonkey [31]. NSPR (Netscape Portable Runtime) is Mozilla’s cross-platform system runtime library providing threads, synchronization primitives, and I/O abstractions, with about 136 kLOC. SpiderMonkey is Mozilla’s JavaScript/WebAssembly runtime featuring JIT compilation and garbage collection, which makes heavy use of multithreading internally and has about 1,214 kLOC. Bug Findings. R EINS detects bugs with given test cases and inputs as program entries. In total, R EINS finds six previously unknown concurrency bugs in the two projects, all of which have been reported to the developers via Bugzilla [29]. The test cases and detailed bug descriptions are available in our artifact. Table 3 lists the bugs with aliases assigned in this paper and the scale of code executed in each detection. At the time of writing, the three SpiderMonkey bugs have all been confirmed and fixed by the core developers of the corresponding components. Most of these bugs depend on both specific state preconditions and access orders and are thus hardly triggered in natural runs, and the agent triggers them by guiding the scheduling from its reasoning about the concurrency semantics. The six bugs cover atomicity violations, a deadlock, and data races. Bug 1 is an atomicity violation, where an unlocked read-modify-write on a shared word races with other writers, so that an interrupt request is lost, the waiting thread is never woken up, and the program hangs. Bug 2 is a deadlock, where the thread joining the pool and the timer thread acquire the job-queue lock and the timer-queue lock in opposite orders and wait for each other. Bug 3 is an atomicity 11

Zhang et al.

Table 3: Concurrency bugs found by R EINS in real-world projects. AV, DL, and DR denote atomicity violation, deadlock, and data race, respectively. Files and LOC denote the number of source files and lines of code actually executed in the detection run. ID Name Project Type Files LOC Status 1 2 3 4 5 6

thread-state pool-join waitgroup-enum rope-flatten atom-bitmap wasm-codeblock

NSPR NSPR NSPR SpiderMonkey / GC SpiderMonkey / GC SpiderMonkey / Wasm

AV DL AV DR DR AV

31 35 34 737 829 909

27k 31k 30k 616k 709k 803k

Reported Reported Reported Fixed Fixed Fixed

violation, where the enumeration of a wait group caches the base address of the hash table outside the lock while another thread expands the table under the lock and frees the old one, so that the enumeration dereferences freed memory and crashes. Bug 4 is a data race, where the main thread overwrites a child slot of a rope string with a parent pointer while flattening it, and the concurrent marking thread reads the slot as a child to mark, crashing on an invalid pointer. Bug 5 is a data race, where the main thread inserts into the hash table behind a zone’s atom marking bitmap and rehashes it, while the concurrent marking thread looks up the same table and reads an inconsistent or freed table, leading to a crash. Bug 6 is another atomicity violation, where two updates that should be performed together are split into two critical sections, and their interleaving leaves a flag stale, so that a wasm out-of-bounds access crashes the process directly instead of being turned into a controlled runtime error. The motivating example in Section 2 is a simplified version of this bug. Answer to RQ2: R EINS finds six previously unknown concurrency bugs, three of which have been confirmed by the developers, demonstrating its effectiveness in practice. 5.4

RQ3: Analysis of Key Designs in R EINS

We evaluate the key designs of R EINS from three aspects: the role of the runtime observation and static inspection in helping the agent understand the concurrency semantics, the effect of the schedule plans on the controlled scheduler, and the contribution of the iterative mechanisms. We use the five variants of x264 in RaceBench as the targets, with the same setup as in Section 5.2. Runtime Observation and Static Inspection. To evaluate the two designs in the comprehend phase, we construct two ablation variants. w/o Runtime removes the runtime observation, so that the agent proposes candidates by reading the source code and invoking static analysis, without the observed access summaries as clues. w/o Static removes the static inspection, so that the agent proposes candidates directly from the collected shared accesses and conflicting access pairs without reading the source code or invoking static analysis. In addition, we evaluate General Agent as a baseline, a vanilla agent on the Claude Agent SDK that has only the format of schedule plans and the controlled scheduler as the execution infrastructure, and detects bugs on its own by reading the source code and analyzing the program. Table 4 reports the total numbers of detected bugs, proposed candidates, and dispatched subagents over the five variants, as well as the dispatch effectiveness and the average time and token cost. In the attempt phase, a subagent is dispatched for each selected candidate to examine it by execution, which we call a dispatch, while some candidates are settled directly in the assess phase. A dispatch is effective if the subagent triggers at least one bug with its plans, and Disp. Eff. is the fraction of effective dispatches. The full R EINS detects the most bugs. The two ablation variants propose and dispatch similar numbers of candidates to R EINS, so their gaps mainly lie in the quality of the hypotheses. w/o Runtime drops the most. Without runtime clues, the agent has to search the code blindly for shared variables, which raises the token consumption, and its candidates largely deviate from the actually executed paths, reducing the effectiveness from 17.6% to 6.6%. Their plans often stall at events that never occur, so the subagents end early once they confirm from the code that these events are unreachable under the given input, and the refuting evidence settles the related candidates through result propagation. As a result, all candidates are settled after 182 minutes on average, before the budget runs out. Its detection is even lower than that of General Agent, which has no candidate mechanism, is free to change its exploration direction, and uses up the whole budget. For w/o Static, the candidates come from the observed conflicting access pairs, many of which are benign races, so its effectiveness decreases to 11.8%. The full R EINS rules out such pairs by static inspection in the comprehend phase, whereas w/o Static defers this judgment to each subagent, which examines its pair by reading the code, invoking static analysis, or executing it. This raises the cost of each dispatch, so the token consumption nearly doubles and the 12

Zhang et al.

Table 4: Results of R EINS and the compared configurations on the five variants of x264. #Bugs (max. 100), #Cand., and #Disp. are the total numbers of detected bugs, proposed candidates, and dispatched subagents; Disp. Eff. is the fraction of dispatched subagents that trigger at least one bug; Avg. Time and Avg. Token are the average time and input/output token consumption per target. #Bugs #Cand. #Disp. Disp. Eff. Avg. Time Avg. Token R EINS w/o Runtime w/o Static General Agent RW

68 41 56 46 30

453 397 389 – –

159 137 153 – –

6-20

21-50

Total

v1

36

7

2

45

v2

11

3

2

16

v3

0

0

2

2

v4

3

1

0

4

v5

1

0

0

30

Detected bugs

Plan version

Executions at first trigger 1-5

17.6% 6.6% 11.8% – –

240 min 182 min 297 min 300 min 300 min

62.5M/526k 79.4M/603k 118.4M/981k 72.2M/156k –

27 19

20

11

10

8 3

0

1

R1

(a)

R2

R3

R4

R5

R6

R7

R8

R9

(b)

Figure 5: Iteration in R EINS on the five variants of x264. (a) Distribution of the 68 triggered bugs over the plan version and the number of executions at the first trigger. (b) Number of bugs detected in each round, summed over the five targets by round number, where x264_1 to x264_5 run 8, 7, 3, 9, and 3 rounds, respectively.

runs take nearly the whole budget. General Agent consumes the fewest output tokens but detects only 68% of the bugs of R EINS, since its unstructured exploration is slow and shallow. Note that even the full R EINS has an effectiveness of only 17.6%, but the dispatches that trigger no bug are not wasted, as a refuted candidate rules out a class of possible bugs, and the execution results are used for result propagation and attribution analysis to guide later rounds. Schedule Plans. The schedule plans bridge the agent’s reasoning and the scheduler’s execution, as the scheduler follows them at the relevant scheduling points and keeps the rest random. We therefore compare the agent-guided configurations against RW, which runs on the same scheduler without guidance. As shown in Table 4, all the agentguided configurations detect more bugs than RW, and the full R EINS more than doubles the detection of RW while covering all of its bugs. The plans thus effectively direct the scheduler toward bug-triggering interleavings. Iterative Mechanisms. The iterative mechanisms feed the execution results back into subsequent attempts at two levels. Within the attempt phase, a subagent revises its plan according to the execution results for at most p versions. Across rounds, the assess phase consolidates the results of a round to steer the next one. As shown in Figure 5(a), among the 68 bugs, 45 are triggered by the first plan version and 23 by a version revised according to the execution results. Meanwhile, 91% of the bugs are triggered within the first 20 executions of a version, and the fourth and fifth versions contribute only 5 in total. Thus, once the plan captures the required interleaving, little scheduling exploration is needed, and the budget of p = 5 versions and q = 50 executions is sufficient. As shown in Figure 5(b), 27 bugs are triggered in the first round and the remaining 41 in later rounds, owing to the maintenance of the candidate pool by the assess phase. The five targets produce 453 candidates in total, far more than a single round can verify, and only 159 of them are dispatched (Table 4). The assess phase selects the candidates most worth verifying in the next round according to the attribution of the current results, and settles some directly by result propagation. It also expands the pool in two ways, either returning to the comprehend phase to instrument and collect the newly reached files, or directly proposing new hypotheses on the previously accumulated sites. Both occur on x264, each sharply expanding the pool, and these candidates enter verification only through the iteration. 13

Zhang et al.

Answer to RQ3: Runtime observation and static inspection jointly help the agent build the semantic understanding, the schedule plans direct the scheduling and thus improve detection, and the iteration within an attempt and across rounds yields more detections.

6

Discussion

Cost and Efficiency. The time cost of R EINS mainly comes from the reasoning of the agent, and about 87% of the wall time is spent in the subagents. To keep the same execution parallelism on the controlled scheduler as the baselines and to stay within the usage limits of the model service, the subagents within a round are executed sequentially in our experiments; however, parallel execution is possible and it would significantly reduce the wall time. As for the token cost, about 90% of the input tokens reported in the evaluation are prompt cache reads, which are priced far below regular input tokens, and the subagents, whose tasks are simpler than those of the lead agent, can be driven by cheaper models. In addition, R EINS can be combined with traditional techniques, letting cheap random scheduling pick up the shallow bugs first and leaving the hard ones to the agent, as supported by the finding in Section 5.4 that all 30 bugs detected by RW are included in the 68 bugs of R EINS. In future work, we will explore these ideas to improve the efficiency of R EINS while retaining its detection capability. Threats to Validity. The randomness of LLM outputs is the main threat, as the hypotheses and plans generated by the agent may differ across runs. Due to the high cost of each run, each tool and configuration is run once, and the agent uses a single model. Our evaluation on 127 targets with more than 1,500 bugs mitigates this risk, as the conclusions are drawn from the overall results rather than from individual targets. Data leakage is another concern. The injected bugs in RaceBench leave traces in the source code, which we anonymize to prevent the agent from locating the bugs directly. The benchmark code may appear in the training corpus of the model, but memorization at most helps locate suspicious code and cannot replace constructing a replayable schedule that triggers the bug. General Agent with the same model detects far fewer bugs than R EINS, indicating that the detection depends mainly on the workflow design rather than pure memorization. In addition, the previously unknown bugs found in real-world projects are free from data leakage. Regarding the comparison with the baselines, the original papers of some baselines use the number of schedules as the budget, whereas we evaluate all tools under the same time budget, so our results are not directly comparable with those reported in the original papers, while the comparison under the same budget remains valid. Limitations. First, like other CCT techniques, R EINS detects bugs only in the code reached by the given test entries and inputs. Second, the current implementation supports C/C++ programs with shared-memory multithreading, and extending it to other languages or concurrency models requires adapting the instrumentation and scheduling layers. Third, R EINS detects only the bugs that manifest as crashes, assertion failures, or hangs, and those with silent symptoms such as data corruption require additional oracles.

7

Related Work

Concurrency Testing. Many program analysis [36, 3, 7, 15, 41, 57], verification [24, 17, 9], and testing [13, 52, 44] techniques have been proposed for concurrency bug detection and reproduction. In this work, we mainly focus on controlled scheduling techniques. Controlled concurrency testing explores the interleaving space systematically or randomly. Systematic concurrency testing stems from stateless model checking [18, 16, 24] and enumerates the interleaving space under certain bounds, such as the preemption bound [33, 34] and the delay bound [14], while P ERIOD [48] divides the execution into periods and explores their interleavings guided by the execution history. Randomized concurrency testing, represented by the random priority scheduling of PCT [4], samples the interleaving space randomly with a probabilistic guarantee of triggering bugs. QL [32] learns scheduling decisions from past executions with Q-learning to bias the scheduler toward bug-exposing choices. RFF [49] applies greybox fuzzing, partitioning the search space by the reads-from relation of executions and pruning the covered partitions to steer exploration toward the under-explored ones. SURW [55] targets the interleaving uniformity missed by prior randomized algorithms and samples interleavings uniformly over a selected subset of events. These techniques decide the schedules from bounds, probabilities, or execution signals at the level of events and executions, whereas R EINS guides thread scheduling with the agent’s reasoning about the program semantics. In addition, there exist some studies that combine predictive analysis with active thread scheduling to detect bugs of specific patterns, known as active testing [21]. These studies predefine an interleaving pattern for each type of bug, predict its potential instances composed of a few program events with their order or dependencies, and actively schedule threads to trigger them. For example, R ACE F UZZER [40] detects data races with potentially racing statement pairs, CT RIGGER [35] detects atomicity violations with unserializable interleavings of two local accesses and one remote access, and D EADLOCK F UZZER [22] detects deadlocks with potential cycles of lock dependencies. M APLE [53] further generalizes these patterns into idioms 14

Zhang et al.

of one or two inter-thread dependencies and exposes their untested instances by active scheduling. By comparison, R EINS is not limited to any specific or predefined interleaving pattern. Its hypotheses describe the thread interactions that may go wrong based on the program semantics, its schedule plans constrain a variable number of events and can carry conditions on program states, and the execution results are fed back to subsequent attempts to revise the plans or hypotheses. LLM Agents for Software Testing. LLMs and agents have recently been applied to a wide range of software testing tasks [46], such as unit test case generation [47], test oracle generation [12], test input generation [50, 51, 56], and bug analysis [23, 25, 37, 42]. Recent work couples the agent with program analysis and dynamic validation in an iterative loop, such as L OCUS [56] synthesizing progress predicates for directed fuzzing, C ONCO LLM IC [28] performing symbolization and constraint solving in natural language for concolic testing, and K-R EPRO [37] and P O CG EN [42] generating and validating PoCs for vulnerability reproduction. On the concurrency side, S LYP [25] uses a ReAct-style agent with binary-exploration and debugging tools to locate race-induced memory corruption in COTS binaries and synthesizes concurrent-invocation PoCs that are validated by native execution, whereas R EINS triggers bugs by taking over and guiding thread scheduling. C ON C OV U P [6] generates multithreaded test drivers for concurrency testing with multiple collaborating agents, identifying conflicting shared-memory access pairs through static analysis and deducing the inputs to reach them to improve the coverage of shared-memory access pairs. It focuses on test driver generation, while R EINS focuses on scheduling control over the covered code, making the two complementary.

8

Conclusion

This paper presents agent-guided thread scheduling and implements it in R EINS, which detects more bugs than existing controlled scheduling techniques on three public benchmarks and finds six previously unknown concurrency bugs in two real-world projects. These results demonstrate that the agent’s reasoning about the concurrency semantics can guide thread scheduling to trigger concurrency bugs more effectively.

Data Availability The source code and experimental data are available at https://anonymous.4open.science/r/ Reins-artifact/.

References [1] Udit Agarwal, Pantazis Deligiannis, Cheng Huang, Kumseok Jung, Akash Lal, Immad Naseer, Matthew Parkinson, Arun Thangamani, Jyothi Vedurada, and Yunpeng Xiao. Nekara: Generalized concurrency testing. In 2021 36th IEEE/ACM International Conference on Automated Software Engineering (ASE), pages 679–691. IEEE, 2021. [2] Anthropic. Claude agent SDK. https://docs.claude.com/en/api/agent-sdk/overview, 2026. Accessed 2026-07. [3] Sam Blackshear, Nikos Gorogiannis, Peter W O’Hearn, and Ilya Sergey. Racerd: compositional static race detection. Proceedings of the ACM on Programming Languages, 2(OOPSLA):1–28, 2018. [4] Sebastian Burckhardt, Pravesh Kothari, Madanlal Musuvathi, and Santosh Nagarakatte. A randomized scheduler with probabilistic guarantees of finding bugs. In Proceedings of the 15th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 167–178, 2010. [5] Yan Cai, Biyun Zhu, Ruijie Meng, Hao Yun, Liang He, Purui Su, and Bin Liang. Detecting concurrency memory corruption vulnerabilities. In Proceedings of the 2019 27th ACM Joint Meeting on European Software Engineering Conference and Symposium on the Foundations of Software Engineering, pages 706–717, 2019. [6] Yuandao Cai, Shuhao Fu, Wensheng Tang, Cheng Wen, Shengchao Qin, and Charles Zhang. Concovup: Effective agent-based test driver generation for concurrency testing. arXiv preprint arXiv:2605.09573, 2026. [7] Yuandao Cai, Peisen Yao, and Charles Zhang. Canary: practical static detection of inter-thread value-flow bugs. In Proceedings of the 42nd ACM SIGPLAN International Conference on Programming Language Design and Implementation, pages 1126–1140, 2021. [8] Le Chen, Xianzhong Ding, Murali Emani, Tristan Vanderbruggen, Pei-Hung Lin, and Chunhua Liao. Data race detection using large language models. In Proceedings of the SC’23 Workshops of the International Conference on High Performance Computing, Network, Storage, and Analysis, pages 215–223, 2023. 15

Zhang et al.

[9] Edmund Clarke, Daniel Kroening, and Flavio Lerda. A tool for checking ansi-c programs. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 168–176. Springer, 2004. [10] ConVul CVE dataset. ConVul CVE dataset. https://github.com/mryancai/ConVul, 2019. Accessed 2026-07. [11] Pantazis Deligiannis, Aditya Senthilnathan, Fahad Nayyar, Chris Lovett, and Akash Lal. Industrial-strength controlled concurrency testing for C# programs with Coyote. In International Conference on Tools and Algorithms for the Construction and Analysis of Systems, pages 433–452. Springer, 2023. [12] Elizabeth Dinella, Gabriel Ryan, Todd Mytkowicz, and Shuvendu K Lahiri. Toga: A neural method for test oracle generation. In Proceedings of the 44th International Conference on Software Engineering, pages 2130–2141, 2022. [13] Orit Edelstein, Eitan Farchi, Yarden Nir, Gil Ratsaby, and Shmuel Ur. Multithreaded java program test generation. IBM Systems Journal, 41(1):111–125, 2002. [14] Michael Emmi, Shaz Qadeer, and Zvonimir Rakamarić. Delay-bounded scheduling. In Proceedings of the 38th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 411–422, 2011. [15] Cormac Flanagan and Stephen N Freund. Fasttrack: efficient and precise dynamic race detection. ACM SIGPLAN Notices, 44(6):121–133, 2009. [16] Cormac Flanagan and Patrice Godefroid. Dynamic partial-order reduction for model checking software. In Proceedings of the 32nd ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 110–121, 2005. [17] Patrice Godefroid. Partial-Order Methods for the Verification of Concurrent Systems: An Approach to the State-Explosion Problem, volume 1032 of Lecture Notes in Computer Science. Springer, Berlin, Germany, 1996. [18] Patrice Godefroid. Model checking for programming languages using VeriSoft. In Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), pages 174–186, 1997. [19] Jue Huang, Tarek Mahmud, Corina Pasareanu, and Guowei Yang. Concur: Benchmarking llms for concurrent code generation. arXiv preprint arXiv:2603.03683, 2026. [20] Lei Huang, Weijiang Yu, Weitao Ma, Weihong Zhong, Zhangyin Feng, Haotian Wang, Qianglong Chen, Weihua Peng, Xiaocheng Feng, Bing Qin, and Ting Liu. A survey on hallucination in Large Language Models: Principles, taxonomy, challenges, and open questions. ACM Transactions on Information Systems, 43(2):1–55, 2025. [21] Pallavi Joshi, Mayur Naik, Chang-Seo Park, and Koushik Sen. Calfuzzer: An extensible active testing framework for concurrent programs. In International Conference on Computer Aided Verification, pages 675–681. Springer, 2009. [22] Pallavi Joshi, Chang-Seo Park, Koushik Sen, and Mayur Naik. A randomized dynamic program analysis technique for detecting real deadlocks. ACM SIGPLAN Notices, 44(6):110–120, 2009. [23] Sungmin Kang, Juyeon Yoon, and Shin Yoo. Large language models are few-shot testers: Exploring llm-based general bug reproduction. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), pages 2312–2323. IEEE, 2023. [24] Michalis Kokologiannakis and Viktor Vafeiadis. GenMC: A model checker for weak memory models. In Proceedings of the International Conference on Computer Aided Verification (CAV), pages 427–440, Cham, Switzerland, 2021. Springer. [25] Hwiwon Lee, Jongseong Kim, and Lingming Zhang. Agentic vulnerability reasoning on cots binaries. arXiv preprint arXiv:2605.05000, 2026. [26] Jiashuo Liang, Ming Yuan, Zhanzhao Ding, Siqi Ma, Xinhui Han, and Chao Zhang. Racebench: A triggerable and observable concurrency bug benchmark. In Proceedings of the 2023 ACM Asia Conference on Computer and Communications Security, pages 415–428, 2023. [27] Shan Lu, Soyeon Park, Eunsoo Seo, and Yuanyuan Zhou. Learning from mistakes: A comprehensive study on real world concurrency bug characteristics. In Proceedings of the 13th International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), pages 329–339, 2008. [28] Zhengxiong Luo, Huan Zhao, Dylan Wolff, Cristian Cadar, and Abhik Roychoudhury. Agentic concolic execution. In 2026 IEEE Symposium on Security and Privacy (SP), pages 1673–1691. IEEE, 2026. [29] Mozilla. Bugzilla. https://bugzilla.mozilla.org/, 2026. Accessed 2026-07. [30] Mozilla. NSPR: Netscape portable runtime. https://firefox-source-docs.mozilla.org/nspr/index. html, 2026. Accessed 2026-07. 16

Zhang et al.

[31] Mozilla. SpiderMonkey: Mozilla’s JavaScript and WebAssembly engine. https://spidermonkey.dev/, 2026. Accessed 2026-07. [32] Suvam Mukherjee, Pantazis Deligiannis, Arpita Biswas, and Akash Lal. Learning-based controlled concurrency testing. Proceedings of the ACM on Programming Languages, 4(OOPSLA):1–31, 2020. [33] Madanlal Musuvathi and Shaz Qadeer. Iterative context bounding for systematic testing of multithreaded programs. In Proceedings of the 28th ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), pages 446–455, 2007. [34] Madanlal Musuvathi, Shaz Qadeer, Thomas Ball, Gerard Basler, Piramanayagam Arumuga Nainar, and Iulian Neamtiu. Finding and reproducing Heisenbugs in concurrent programs. In Proceedings of the 8th USENIX Symposium on Operating Systems Design and Implementation (OSDI), pages 267–280, 2008. [35] Soyeon Park, Shan Lu, and Yuanyuan Zhou. Ctrigger: exposing atomicity violation bugs from their hiding places. In Proceedings of the 14th International Conference on Architectural Support for Programming Languages and Operating Systems, pages 25–36, 2009. [36] Polyvios Pratikakis, Jeffrey S Foster, and Michael Hicks. Locksmith: Practical static race detection for c. ACM Transactions on Programming Languages and Systems (TOPLAS), 33(1):1–55, 2011. [37] Juefei Pu, Xingyu Li, Zhengchuan Liang, Jonathan Cox, Yifan Wu, Kareem Shehada, Arrdya Srivastav, and Zhiyun Qian. Patch-to-poc: A systematic study of agentic llm systems for linux kernel n-day reproduction. arXiv preprint arXiv:2602.07287, 2026. [38] Stefan Savage, Michael Burrows, Greg Nelson, Patrick Sobalvarro, and Thomas Anderson. Eraser: A dynamic data race detector for multithreaded programs. ACM Transactions on Computer Systems (TOCS), 15(4):391–411, 1997. [39] SCTBench. SCTBench: a set of C/C++ pthread benchmarks for evaluating concurrency testing techniques. https://github.com/mc-imperial/sctbench, 2016. Accessed 2026-07. [40] Koushik Sen. Race directed random testing of concurrent programs. In Proceedings of the 29th ACM SIGPLAN Conference on Programming Language Design and Implementation, pages 11–21, 2008. [41] Konstantin Serebryany and Timur Iskhodzhanov. Threadsanitizer: data race detection in practice. In Proceedings of the workshop on binary instrumentation and applications, pages 62–71, 2009. [42] Deniz Simsek, Aryaz Eghbali, and Michael Pradel. Pocgen: Generating proof-of-concept exploits for vulnerabilities in npm packages. Proceedings of the ACM on Software Engineering, 3(FSE):3887–3908, 2026. [43] Paul Thomson, Alastair F Donaldson, and Adam Betts. Concurrency testing using schedule bounding: An empirical study. In Proceedings of the 19th ACM SIGPLAN Symposium on Principles and Practice of Parallel Programming, pages 15–28, 2014. [44] Paul Thomson, Alastair F. Donaldson, and Adam Betts. Concurrency testing using controlled schedulers: An empirical study. ACM Transactions on Parallel Computing, 2(4), 2016. [45] Miles Turpin, Julian Michael, Ethan Perez, and Samuel Bowman. Language models don’t always say what they think: Unfaithful explanations in chain-of-thought prompting. Advances in Neural Information Processing Systems, 36:74952–74965, 2023. [46] Junjie Wang, Yuchao Huang, Chunyang Chen, Zhe Liu, Song Wang, and Qing Wang. Software testing with large language models: Survey, landscape, and vision. IEEE Transactions on Software Engineering, 50(4):911–936, 2024. [47] Zejun Wang, Kaibo Liu, Ge Li, and Zhi Jin. Hits: High-coverage llm-based unit test generation via method slicing. In Proceedings of the 39th IEEE/ACM International Conference on Automated Software Engineering, pages 1258–1268, 2024. [48] Cheng Wen, Mengda He, Bohao Wu, Zhiwu Xu, and Shengchao Qin. Controlled concurrency testing via periodical scheduling. In Proceedings of the 44th International Conference on Software Engineering (ICSE), pages 474–486, 2022. [49] Dylan Wolff, Zheng Shi, Gregory J Duck, Umang Mathur, and Abhik Roychoudhury. Greybox fuzzing for concurrency testing. In Proceedings of the 29th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 2, pages 482–498, 2024. [50] Chunqiu Steven Xia, Matteo Paltenghi, Jia Le Tian, Michael Pradel, and Lingming Zhang. Fuzz4all: Universal fuzzing with large language models. In Proceedings of the IEEE/ACM 46th International Conference on Software Engineering, pages 1–13, 2024. 17

Zhang et al.

[51] Hanxiang Xu, Wei Ma, Ting Zhou, Yanjie Zhao, Kai Chen, Qiang Hu, Yang Liu, and Haoyu Wang. Ckgfuzzer: Llm-based fuzz driver generation enhanced by code knowledge graph. In 2025 IEEE/ACM 47th International Conference on Software Engineering: Companion Proceedings (ICSE-Companion), pages 243–254. IEEE, 2025. [52] Meng Xu, Sanidhya Kashyap, Hanqing Zhao, and Taesoo Kim. Krace: Data race fuzzing for kernel file systems. In 2020 IEEE Symposium on Security and Privacy (SP), pages 1643–1660. IEEE, 2020. [53] Jie Yu, Satish Narayanasamy, Cristiano Pereira, and Gilles Pokam. Maple: A coverage-driven testing tool for multithreaded programs. In Proceedings of the ACM International Conference on Object Oriented Programming Systems Languages and Applications (OOPSLA), pages 485–502, 2012. [54] Xinhao Yuan, Junfeng Yang, and Ronghui Gu. Partial order aware concurrency sampling. In Proceedings of the International Conference on Computer Aided Verification (CAV), pages 317–335, Cham, Switzerland, 2018. Springer. [55] Huan Zhao, Dylan Wolff, Umang Mathur, and Abhik Roychoudhury. Selectively uniform concurrency testing. In Proceedings of the 30th ACM International Conference on Architectural Support for Programming Languages and Operating Systems, Volume 1, pages 1003–1019, 2025. [56] Jie Zhu, Chihao Shen, Ziyang Li, Jiahao Yu, Yizheng Chen, and Kexin Pei. Locus: Agentic predicate synthesis for directed fuzzing. In Proceedings of the 2026 IEEE/ACM 48th International Conference on Software Engineering, pages 992–1005, 2026. [57] Shihao Zhu, Yuqi Guo, Long Zhang, and Yan Cai. Tolerate control-flow changes for sound data race prediction. In 2023 IEEE/ACM 45th International Conference on Software Engineering (ICSE), pages 1342–1354. IEEE, 2023.

18

Related documents

• REINS: Agent-guided Thread Scheduling for Concurrency Bug Detection and Reproduction#1297773
• Robustness Analysis of Agentic AI to Inconsistent and Incomplete Tool Responses#793895
• Robustness Analysis of Agentic AI to Inconsistent and Incomplete Tool Responses#789876
• Scalable, Intelligent Verification and Validation of Concurrent and Distributed Systems (ScaIVeri) (Track Summary)#1360658
• WebCQ: Cooperative Multi-Agent Deep Reinforcement Learning for Scalable Web GUI Testing#300008