Paper deep dive
From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs
Kaiwen Zhang, Guanjun Liu
Intelligence
Status: succeeded | Model: Gemma-4-26B-A4B | Prompt: intel-v1 | Confidence: 90%
Last extracted: 7/25/2026, 1:18:16 AM
Summary
The paper introduces SyncPetri, a methodology for generating executable Rust tests for concurrent stateful APIs using Petri nets to guide Large Language Models (LLMs). It separates semantic intent (defined by Petri nets representing resource flow, lifecycle, and concurrency) from code realization (handled by LLMs). The approach uses a local-faithfulness contract, structural repair loops, and a layered semantic oracle to ensure generated tests are semantically faithful, handle deep states and race conditions, and distinguish between synthesis failures and actual API bugs.
Entities (11)
Relation Signals (10)
SyncPetri → targets → Rust
confidence 99% · test generation over concurrent stateful Rust APIs.
SyncPetri → uses → Petri Net
confidence 95% · We present a Petri-net-guided methodology for test generation over concurrent stateful Rust APIs.
SyncPetri → employs → Layered Semantic Oracle
confidence 92% · A layered semantic oracle then distinguishes synthesis failures from violations of the target API's expected behavior.
SyncPetri → uses → Large Language Model
confidence 92% · uses these scenarios as a constrained intermediate representation for LLM-based code synthesis.
SyncPetri → appliedto → tokio::sync
confidence 90% · instantiate the full workflow on tokio::sync-style APIs.
SyncPetri → employs → Local-Faithfulness Contract
confidence 90% · A local-faithfulness contract and structural repair loop preserve the modeled intent during concretization
Petri Net → represents → mpsc channel
confidence 88% · The method represents API resources... as colored tokens and transitions... mpsc channels expose senders, receivers...
Layered Semantic Oracle → detects → ConcretizationError
confidence 85% · If an LLM error... the run is flagged as a ConcretizationError
Cypher Suggestions (0)
No Cypher suggestions yet.
Abstract
Abstract:Concurrent stateful library APIs expose behavior through evolving resource ownership, lifecycle states, and competing interleavings. Large language models can synthesize executable Rust tests, but their outputs often violate API preconditions, remain shallow, or reduce concurrency to accidental sequential traces. Conversely, model-based and systematic testing techniques provide semantic control but commonly require substantial handwritten code to turn abstract scenarios into executable tests. This paper addresses the gap between formal scenario design and low-cost test concretization. We present a Petri-net-guided methodology for test generation over concurrent stateful Rust APIs. The method represents API resources, lifecycle conditions, and causal dependencies as colored tokens and transitions; derives legal deep-state, near-legal, and partial-order concurrent scenarios; and uses these scenarios as a constrained intermediate representation for LLM-based code synthesis. A local-faithfulness contract and structural repair loop preserve the modeled intent during concretization, while Petri-guided schedule shaping prioritizes high-conflict concurrency skeletons for systematic exploration. A layered semantic oracle then distinguishes synthesis failures from violations of the target API's expected behavior.
Tags
Links
- Source: https://arxiv.org/abs/2607.21530v1
- Canonical: https://arxiv.org/abs/2607.21530v1
Trouble viewing inline? Open PDF directly →
Full Text
52,586 characters extracted from source content.
Expand or collapse full text
From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs Kaiwen Zhang, Guanjun Liu Tongji UniversityShanghai,China zhangkw@tongji.edu.cn Abstract. Concurrent stateful library APIs expose behavior through evolving resource ownership, lifecycle states, and competing interleavings. Large language models can synthesize executable Rust tests, but their outputs often violate API preconditions, remain shallow, or reduce concurrency to accidental sequential traces. Conversely, model-based and systematic testing techniques provide semantic control but commonly require substantial handwritten code to turn abstract scenarios into executable tests. This paper addresses the gap between formal scenario design and low-cost test concretization. We present a Petri-net-guided methodology for test generation over concurrent stateful Rust APIs. The method represents API resources, lifecycle conditions, and causal dependencies as colored tokens and transitions; derives legal deep-state, near-legal, and partial-order concurrent scenarios; and uses these scenarios as a constrained intermediate representation for LLM-based code synthesis. A local-faithfulness contract and structural repair loop preserve the modeled intent during concretization, while Petri-guided schedule shaping prioritizes high-conflict concurrency skeletons for systematic exploration. A layered semantic oracle then distinguishes synthesis failures from violations of the target API’s expected behavior. We implement a prototype for Rust concurrency libraries and define an evaluation protocol that examines executability, structural fidelity, deep-state reachability, boundary-failure yield, and conflict coverage. The central methodological principle is to separate responsibilities: the Petri net specifies semantic intent, resource flow, reachability, conflict, and bug-relevant mutations, whereas the LLM realizes library-specific syntax, task scaffolding, and assertions. This design provides a concrete basis for studying whether formal resource-flow models can make LLM-generated concurrency tests more faithful, stateful, and diagnostically useful. Petri nets, large language models, Rust, concurrency testing, stateful API testing, test generation †copyright: none†ccs: Software and its engineering Software testing and debugging†ccs: Software and its engineering Formal software verification†ccs: Software and its engineering Software reliability 1. Introduction Many Rust library APIs are not isolated function interfaces. They expose handles, permits, closures, buffered state, and task-level interaction patterns whose behavior depends on prior operations and competing schedules. In this setting, Rust’s type system removes broad classes of memory errors, but it does not prove that a library respects its higher-level protocol. The bugs that remain are semantic faults: a stale capability is still accepted, a close operation invalidates the wrong behavior, a buffered value is lost, or a test hangs only after a specific interleaving reaches a deep state. These APIs are difficult to test for three coupled reasons. First, interesting behaviors are strongly stateful: many failure modes appear only after a legal prefix establishes a nontrivial resource configuration. Second, the prefix itself must be semantically disciplined; otherwise later observations are meaningless because the test never exercised a valid protocol state. Third, concurrency matters at the level of partial order rather than raw length. A long sequence is not useful if it accidentally serializes the very race that should have been exposed. Existing approaches each cover only part of this space. Model-based and dependency-aware testing can describe legal states, resource flow, and boundary conditions, but converting those abstractions into executable Rust tests still demands substantial handwritten scaffolding, task orchestration, and API-specific assertions. Direct LLM prompting reduces that coding burden, but it also pushes semantic responsibility back into the model. In practice, the LLM may invent events, violate enablement conditions, confuse reserved capabilities with fresh ones, weaken assertions, or flatten concurrent behavior into a convenient sequential trace. Our position in this paper is intentionally narrower. We do not ask the LLM to discover concurrency semantics from scratch, and we do not claim to eliminate modeling effort. Instead, we use a Petri-net model to encode resource multiplicity, causality, conflict, and near-legal boundary cases, then use the LLM only to realize model-produced scenarios as executable Rust code. The scheduler still explores runtime interleavings, and API-specific invariants still need to be authored. The point is to separate responsibilities so that semantic intent stays outside the LLM while code realization stays inexpensive. This tradeoff fits concurrent stateful Rust APIs especially well. A Petri net can represent senders, receivers, permits, capacity, buffered messages, and observation obligations as tokens, and it can express the precise conflicts and causal dependencies that make a test diagnostically useful. Once that structure is explicit, the LLM can do what it is relatively good at: writing target-specific setup, task creation, assertions, and cleanup. The key design rule is simple: the model writes meaning, the LLM writes code. The price of this design is also clear. SyncPetri requires manually authored resource models, adapters, and scenario invariants, and its schedule shaping improves harness selection above tools such as Loom rather than replacing their internal search. We state these limitations up front because they define the appropriate contribution: not fully automatic concurrency verification, but a testing architecture that trades some modeling effort for stronger semantic control over generated tests. Concretely, SyncPetri synthesizes legal deep-state traces, near-legal boundary probes, and partial-order concurrent scenarios from a colored Petri net; concretizes them through a constrained prompt and structural repair loop; and judges the resulting executions with a layered oracle that separates concretization failure from semantic failure. The result is a testing pipeline designed for concurrent Rust APIs whose hard bugs live in resource protocols rather than in isolated function outputs. We make five contributions: • We formalize concurrent stateful Rust API testing as Petri-net-guided scenario synthesis over resource-carrying transitions. • We define an adapter schema and a local-faithfulness contract that connects abstract Petri-net steps to concrete Rust executions. • We define a scenario representation that unifies legal reachability, near-legal boundary mutation, and partial-order concurrency. • We present a constrained concretization loop and a multi-layer oracle that distinguish generation failure from semantic failure. • We propose a Petri-guided schedule shaping method for Loom-compatible harnesses and instantiate the full workflow on tokio::sync-style APIs. 2. Problem Setting and Running Example We target APIs with three fundamental properties: 1) Statefulness: The outcome or validity of an operation depends heavily on the internal abstract resource state of the system. 2) Resource sensitivity: Operations directly manipulate capabilities—consuming, producing, splitting, merging, or invalidating handles, permits, buffered data, or access tokens. 3) Concurrency exposure: Multiple distinct tasks or handles interact simultaneously, meaning distinct execution schedules can yield entirely different observable outcomes. This covers a useful slice of Rust libraries. In tokio::sync, for example, mpsc channels expose senders, receivers, permits, buffering, and closure; watch exposes latest-value semantics and observed states; broadcast exposes lagging receivers and replay boundaries; and Semaphore exposes acquisition, release, and closure behavior (Tokio Contributors, 2026c, e, b, d). These APIs are small enough to test locally but rich enough to require genuine semantic orchestration. Table 1 shows a compact abstraction for a running mpsc example. Table 1. Example Petri-net places for a bounded mpsc. Place Meaning LiveSender(s) Sender handle s exists and may initiate send-side operations. LiveReceiver(r) Receiver handle r exists and may receive or close. Open(c) Channel c accepts ordinary sends. Closed(c) Channel c has been closed from the receive side. Permit(s,c) Sender s holds a reserved permit on channel c. Cap(c,n) Channel c has n unreserved buffer slots. Buf(c,n) Abstract buffered-item count for channel c. Obs(x) Runtime observation token emitted by instrumentation. The research problem is therefore: How can we synthesize semantically meaningful concurrent test scenarios from a Petri-net model of a Rust API, concretize those scenarios into executable Rust code with an LLM, and judge whether the resulting execution preserves or violates the intended API semantics? 2.1. Bug Model We target semantic faults that escape Rust’s type system and strict memory-safety checks. We classify these faults into four core families: • preB_ pre (Precondition Enforcement): An operation incorrectly succeeds even though its abstract prerequisite condition is violated (e.g., sending into a closed channel). • stateB_ state (Post-State Inconsistency): Resource accounting, ownership transfer, or cleanup logic diverges from the specification after an operation executes. • raceB_ race (Race Sensitivity): A schedule-dependent interleaving exposes an observation sequence or state variation that the high-level protocol strictly forbids. • liveB_ live (Liveness and Blocking): The implementation suffers from permanent blocking, dropped wake-ups, or a failure to terminate after reaching a terminal protocol state. For tokio::sync APIs, these categories correspond to concrete fault shapes such as send-after-close success, stale-handle acceptance, lost notification after value update, inconsistent permit accounting, or non-terminating close races. This bug model serves as the ground truth for our seeded mutant evaluation. 2.2. Running Example and Baseline Pitfalls We motivate the SyncPetri workflow using a capacity-one Tokio MPSC channel. The setup involves a receiver R0R_0, an ordinary sender SpS_p used to reserve capacity, and an independent sender SbS_b acting as a boundary probe. The core semantic invariant of interest involves a subtle asynchronous contract: closing the receiver must immediately reject new ordinary send operations, yet any pre-existing Permit or OwnedPermit successfully acquired prior to closure remains valid and must be allowed to commit its message to the buffer (Tokio Contributors, 2026c). The receiver is then obligated to drain this outstanding message before final termination. This nuanced lifecycle contract creates several plausible semantic faults: an implementation might erroneously drop the message backed by the outstanding permit upon closure, reject the valid permit commit, or hang indefinitely due to internal desynchronization between close flags and permit counters. Traditional testing paradigms struggle to isolate this behavior. A purely random concurrency fuzzer is highly unlikely to generate the exact interleaved sequence required to hit this deep state (reserving capacity, racing a close with a commit, and then validating the residual drain). Conversely, a pure prompt-only LLM routinely suffers from two opposing failures: it either collapses the concurrent execution into a simplified sequential trace that entirely misses the race, or it hallucinates a strict sequential rule (e.g., assuming all operations fail post-close), thereby generating incorrect test assertions that mismatch the API’s actual contract. Step 1: Resource Model and Deep State. Initially, the abstract initial marking M0M_0 contains two live sender capabilities, one live receiver, an open-channel token, and one capacity token. The first modeled event explicitly targets a deep state by reserving capacity: e1=(Sp)→P0.e_1= reserveOwned(S_p)→ P_0. The resulting marking moves the net into a distinct configuration containing Permit(P0,c) Permit(P_0,c) and Cap(c,0) Cap(c,0). This represents the deep state of interest: the channel possesses an outstanding, isolated send capability (P0P_0) distinct from an ordinary open sender or a simple buffered item. Crucially, the model dictates that the permit-commit transition consumes P0P_0 without requiring Open(c) Open(c), while ordinary sends still depend on both Open(c) Open(c) and free capacity. Step 2: Scenarios. From this marking, SyncPetri builds a partial-order graph over E=e1,…,e7E=\e_1,…,e_7\ with the following labels: e1 e_1 :(Sp)→P0, : reserveOwned(S_p)→ P_0, e2 e_2 :(T1,P0), : spawn(T_1,P_0), e3 e_3 :(P0,m1), : permitSend(P_0,m_1), e4 e_4 :(R0), : close(R_0), e5 e_5 :(R0)→m1, : recv(R_0)→ m_1, e6 e_6 :(Sb,m2), : trySend(S_b,m_2), e7 e_7 :(R0). : recvEnd(R_0). Rather than fixing a rigid, linear trace, only necessary causal dependencies are captured in ≺ : e1≺e2≺e3,e1≺e4,e3≺e5,e4≺e5≺e6≺e7. gatherede_1 e_2 e_3, e_1 e_4,\\ e_3 e_5, e_4 e_5 e_6 e_7. gathered Events e3e_3 and e4e_4 are causally independent but compete for overlapping resource fields, and are thus flagged as an explicit race pair: (e3,e4)∈#(e_3,e_4)∈\#. This partial order safely encapsulates two valid interleavings: commit-before-close and close-before-commit. Event e6e_6 acts as a near-legal boundary probe; following e5e_5, the channel’s capacity is free but its state remains closed, meaning e6e_6 violates exactly one enablement condition (Open(c) Open(c)). The expected observations are mapped as set-valued allowed classes: Φe3 _e_3 =, =\ SendOk\, Φe5 _e_5 =(m1), =\ Msg(m_1)\, Φe6 _e_6 =, =\ ClosedLike\, Φe7 _e_7 =. =\ End\. Table 2. SyncPetri Responsibilities Division and Artifacts for the Motivating Example. Stage Model intent Realization Scenario 7 typed events, causal edges ≺ , conflict pair (e3,e4)(e_3,e_4) Immutable JSON prompt constraints. Code Resource bindings, outcome classes Φ , banned edits LLM generates tasks, scopes, adapters, and assertions. Schedule Frontier prioritized by uncovered conflicts Two shaped execution harnesses. Oracle str∧out∧inv∧liveO_str _out _inv _live Separates synthesis failures from API bugs. Step 3: Constrained LLM Concretization. The structural graph is serialized into a highly constrained data prompt rather than a loose text description. The prompt provides explicit resource mappings, edge dependencies, and allowable outcome envelopes. To bridge the gap between abstract events and executable tasks, the framework derives execution scaffolding from the conflict relation. Because (e3,e4)∈#(e_3,e_4)∈\# is an active concurrency pair, the prompt requires explicit readiness, release, and completion handshakes rather than letting the model serialize the actions. Listing 1 illustrates the resulting code artifact. The LLM remains free to handle target-specific syntax and variable scoping but cannot strip the structural instrumentation markers (mark). Listing 1: Schematic generated harness for the motivating scenario. ⬇ let (sp, sb, mut r0) = bounded_with_clone(1); let p0 = mark(e1, || reserve_owned(sp)); let gate = deterministic_handshake(); let child = mark(e2, || spawn(move || gate.ready(); gate.wait_release(); mark(e3, || p0.send(m1)) )); gate.wait_ready(); gate.release(); mark(e4, || r0.close()); join_bounded(child); assert_msg(mark(e5, || recv(&mut r0)), m1); assert_closed(mark(e6, || sb.try_send(boundary_msg))); assert_end(mark(e7, || recv_bounded(&mut r0))); Step 4: Petri-Guided Schedule Exploration. The synthesized event graph induces two macro harnesses: h h_commit =[e1,e2,e3,e4,e5,e6,e7], =[e_1,e_2,e_3,e_4,e_5,e_6,e_7], h h_close =[e1,e2,e4,e3,e5,e6,e7]. =[e_1,e_2,e_4,e_3,e_5,e_6,e_7]. The generated handshakes guarantee that the deep state P0P_0 is established before the race window opens. A deterministic scheduler adapter (or Loom) then enumerates only the micro-interleavings inside that window. This division of labor lets the Petri-net model select the macro-concurrency surface while the runtime scheduler explores local execution choices. Step 5: Oracle Decision and Report. On a compliant implementation, either linearization may occur at runtime. Regardless of whether e3e_3 or e4e_4 executes first, e3e_3 must yield SendOk, e5e_5 must observe m1m_1, and the post-close boundary check e6e_6 must evaluate to ClosedLike. The layered oracle first invokes the structural checker (strO_str) to verify that all seven runtime markers executed in a sequence that satisfies ≺ . If an LLM error or compiler optimization reordered or bypassed a marker, the run is flagged as a ConcretizationError and pruned. If strO_str passes but the library returns an unmapped observation class (e.g., if a mutant rejects the outstanding permit during a close-first interleaving), the system registers a true SemanticFailure. The resulting diagnostic profile is recorded as: =(pc,SemanticFailure,,τ⋆,h). Report=(S_pc, SemanticFailure,\out\,τ ,h_close). This structured output ensures that hundreds of identical low-level scheduler interleavings that expose the exact same root bug are seamlessly de-duplicated into a single actionable report. 3. Formal Model 3.1. API Abstraction and Colored Petri Net We begin with a lightweight API abstraction A=(R,O,Σ,Ω),A=(R,O, , ), where R is a set of resource sorts, O is a set of operation names, Σ maps each operation to typed arguments and result classes, and Ω is a set of observation classes used by the runtime oracle. The API abstraction is compiled into a colored Petri net NA=(P,T,F,χ,λ,g,u,M0).N_A=(P,T,F,χ,λ,g,u,M_0). where P is a finite set of places, T is a finite set of transitions, F⊆(P×T)∪(T×P)F (P× T)∪(T× P) is the flow relation, χ maps each place to a token color domain, λ:T→Oλ:T→ O labels transitions with API or harness operations, gtg_t is a guard predicate for each transition t, utu_t is a token-update function for each transition t, M0M_0 is the initial marking. Let It(p)I_t(p) and Ot(p)O_t(p) denote the input and output token multisets of transition t at place p. A transition is enabled under marking M iff (M,t)⇔gt(M)=true∧∀p∈P,It(p)⊆M(p). enabled(M,t) g_t(M)= true\; \;∀ p∈ P,\;I_t(p) M(p). If (M,t) enabled(M,t) holds, firing t yields a new marking M′M defined by M′=ut((M−It)+Ot).M =u_t ((M-I_t)+O_t ). We write M→M′M tM for one firing step and M0→t1⋯tkMkM_0 t_1·s t_kM_k for a finite firing sequence. The reachability set is (NA)=M∣∃π,M0→M. Reach(N_A)=\M ∃π,\;M_0 πM\. The practical purpose of the net is not only to reject impossible calls. It records how resources move, which operations compete for them, and which events are causally independent. 3.2. Adapter Schema and Local Faithfulness The Petri net is abstract, but the test oracle runs over concrete Rust executions. We therefore associate each target library domain d with an adapter schema Ad=(,,,,,,Γ,ρd).A_d=( Ctor, Step, Spawn, Mark, Assert, Cleanup, , _d). Here Ctor constructs the initial runtime objects, Step maps a modeled transition to a concrete Rust operation, Spawn packages spawnable event groups into tasks, Mark emits event markers, Assert instantiates concrete checks, Cleanup bounds teardown, Γ maps concrete results to observation classes in Ω , and ρd _d abstracts a concrete runtime state to a Petri-net marking. We do not require a full bisimulation between implementation and model. The methodological requirement is a local faithfulness contract at modeled event boundaries. For an event e with η(e)=tη(e)=t, let d(t,σ,β(e))↝(σ′,o) Step_d(t,σ,β(e)) (σ ,o) denote one concrete adapter step from runtime state σ to σ′σ with raw observation o, and let Ωtok,Ωterr⊆Ω _t^ok, _t^err denote the modeled success and error observation classes of t. For legal steps, we require ρd(σ)=M∧M→M′⟹ _d(σ)=M M tM ∃σ′,o.d(t,σ,β(e))↝(σ′,o) ∃σ ,o.\; Step_d(t,σ,β(e)) (σ ,o) ∧ρd(σ′)=M′∧Γ(o)∈Ωtok. _d(σ )=M (o)∈ _t^ok. For near-legal steps, we require that a single-precondition violation maps to an explicit error-class outcome: ρd(σ)=M∧ _d(σ)=M |ΔF(M,t)|+|ΔG(M,t)|=1 | _F(M,t)|+| _G(M,t)|=1 ⟹ ∃σ′,o.d(t,σ,β(e))↝(σ′,o) ∃σ ,o.\; Step_d(t,σ,β(e)) (σ ,o) ∧Γ(o)∈Ωterr. (o)∈ _t^err. This contract is intentionally lightweight. It requires the adapter to preserve the meaning of modeled steps and boundary failures without demanding that every internal library state be exposed or reconstructed. 3.3. Reusable Transition Schemas To avoid making each Petri net a one-off artifact, we model concurrent Rust APIs with a small library of reusable transition schemas. A schema is a tuple θ=(Pθin,Pθout,gθ,uθ,Ωθ),θ= (P^in_θ,P^out_θ,g_θ,u_θ, _θ ), consisting of typed input places, typed output places, a guard, a token-update rule, and the observation classes attached to the step. Instantiating a schema only requires binding symbolic place names and resource identifiers. Four schemas are especially common in tokio::sync APIs: θclone:LiveHandle(x)→LiveHandle(x)+LiveHandle(x′),θreserve:LiveSender(s)+Open(c)+Cap(c,n)→LiveSender(s)+Permit(s,c)+Cap(c,n−1),θclose:LiveReceiver(r)+Open(c)→LiveReceiver(r)+Closed(c),θconsume:LiveReceiver(r)+Buf(c,n)→LiveReceiver(r)+Buf(c,n−1)+Obs(). array[]@l@ _clone:\\ 18.49988pt LiveHandle(x)→ LiveHandle(x)+ LiveHandle(x ),\\[2.0pt] _reserve:\\ 18.49988pt LiveSender(s)+ Open(c)+ Cap(c,n)\\ 18.49988pt→ LiveSender(s)+ Permit(s,c)+ Cap(c,n\!-\!1),\\[2.0pt] _close:\\ 18.49988pt LiveReceiver(r)+ Open(c)→ LiveReceiver(r)+ Closed(c),\\[2.0pt] _consume:\\ 18.49988pt LiveReceiver(r)+ Buf(c,n)\\ 18.49988pt→ LiveReceiver(r)+ Buf(c,n\!-\!1)\\ 18.49988pt+ Obs( RecvOk). array The guards on θreserve _reserve and θconsume _consume additionally require n>0n>0. Near-legal mutations then arise naturally by violating exactly one of these guard or token conditions, such as attempting θreserve _reserve when the channel is closed or capacity is exhausted. These schemas transfer across the target API family. In mpsc, θreserve _reserve models permit acquisition; in Semaphore, the same schema models acquisition over capacity tokens; in watch, θconsume _consume becomes observation of an unseen update; and in broadcast, it becomes lag-sensitive receive with a richer outcome-class mapping. The point is methodological: the Petri model is not handwritten from scratch for every call sequence, but assembled from resource-transition idioms that recur across concurrent Rust libraries. 3.4. Scenario Semantics An abstract scenario is a tuple =(E,≺,#,η,β,Φ),S=(E, ,\#,η,β, ), where E is a finite event set, ≺⊆E×E \; E× E is a strict partial order, #⊆E×E\#\; E× E is a symmetric conflict relation, η:E→Tη:E→ T maps events to Petri-net transitions, β binds symbolic resources and payloads to event parameters, Φ contains expected outcome predicates and global invariants. A linearization of S is any bijective sequence over E that respects ≺ . We write ()=π∣π is a linearization of (E,≺). Lin(S)=\π π is a linearization of (E, )\. The executable semantics of a scenario under net NAN_A is (,NA)=π∈()∣M0→η(π)M for some M, Exec(S,N_A)=\π∈ Lin(S) M_0 η(π)M for some M\, where η(π)η(π) lifts η pointwise from events to transition sequences. A scenario is legal iff (,NA)≠∅ Exec(S,N_A)≠ . Equivalently, at least one linearization e1,…,ene_1,…,e_n satisfies M0→η(e1)⋯η(en)MnM_0 η(e_1)·sη(e_n)M_n. To formalize boundary mutation, let ΔF(M,t)=p∈P∣It(p)⊈M(p) _F(M,t)=\p∈ P I_t(p) M(p)\, and assume the guard of t is written as gt=q1∧q2∧⋯∧qrg_t=q_1 q_2 ·s q_r. Let ΔG(M,t)=qj∣qj(M)=false, 1≤j≤r _G(M,t)=\q_j q_j(M)= false,\;1≤ j≤ r\, so that missing tokens and violated atomic guards are counted separately. A disabled transition t is near-legal at M if |ΔF(M,t)|+|ΔG(M,t)|=1| _F(M,t)|+| _G(M,t)|=1. This definition captures the specific kind of semantic boundary case we want: a trace that is almost enabled, but violates exactly one precondition. The conflict relation #\# records pairs of events that should be scheduled adversarially because they compete for a token class, touch the same linear resource, or correspond to user-declared race pairs. The partial order ≺ records only necessary causality, not a fully committed thread schedule. For concurrent scenarios, Φ is set-valued rather than schedule-singleton. If incomparable events can race, the allowed outcome class for event e may be Φe=⋃π∈(,NA)Φeπ, _e= _π∈ Exec(S,N_A) _e^π, where Φeπ _e^π is the modeled observation class of e under linearization π. This lets the oracle accept multiple race-permitted outcomes while still rejecting classes that no legal linearization admits. 4. Scenario Synthesis 4.1. Three Scenario Families SyncPetri synthesizes three classes of scenarios from the same Petri-net model. The classes can be used independently or composed: in Section 2.2, a partial-order legal core is followed by a near-legal boundary probe. These are fully enabled traces selected to reach semantically uncommon markings rather than merely long traces. We assign a heuristic score (π)=αU(Mk)+βC(π)+γX(π), Depth(π)=α U(M_k)+β C(π)+γ X(π), where π is a legal trace ending at marking MkM_k, U(Mk)U(M_k) is a marking-novelty term, C(π)C(π) measures structural coverage (for example, distinct transition or place classes), and X(π)X(π) measures conflict exposure induced by the trace. These consist of a legal prefix followed by one near-legal event. They target boundary checks, stale-resource handling, and error propagation without collapsing into meaningless invalid sequences. These begin as legal event sets, but independent steps are left unordered. The output is therefore a DAG of causality plus a conflict relation, not a single linear schedule. 4.2. Generation Algorithm Algorithm 1 Petri-net scenario synthesis 1:net NAN_A, family f, length bound L 2:abstract scenario S 3:M←M0M← M_0, E←[]E←[\,], ≺←∅ ← , #←∅\#← 4:for i=1i=1 to L do 5: Cen←t∈T∣(M,t)C_en←\t∈ T enabled(M,t)\ 6: Cnear←t∈T∣|ΔF(M,t)|+|ΔG(M,t)|=1C_near←\t∈ T | _F(M,t)|+| _G(M,t)|=1\ 7: if f=NearLegalf= NearLegal and i is the mutation point then 8: choose t⋆t from CnearC_near 9: append boundary event eie_i with η(ei)=t⋆η(e_i)=t 10: break 11: else 12: choose t⋆t from CenC_en maximizing Depth 13: append legal event eie_i with η(ei)=t⋆η(e_i)=t 14: add causal edges induced by token production and consumption 15: add conflict edges induced by shared resources 16: fire t⋆t and update M 17: end if 18:end for 19:if f=PartialOrderf= PartialOrder then 20: remove unnecessary order edges while preserving causality 21:end if 22:return =(E,≺,#,η,β,Φ)S=(E, ,\#,η,β, ) The Algorithm 1 is intentionally model-centric. The choice of which event should happen next is driven by reachability and conflict structure, not by code-generation convenience. In practice, near-legal mutation is not inserted uniformly. After a legal prefix reaches marking M, we score candidate boundary events by (M,t)= MutScore(M,t)= w1[|ΔF(M,t)|+|ΔG(M,t)|=1] w_11[| _F(M,t)|+| _G(M,t)|=1] +w2(M,t)+w3(M,t), +w_2 Stale(M,t)+w_3 ConflictCtx(M,t), where Stale rewards operations that reuse recently invalidated resources and ConflictCtx rewards mutations placed near a high-conflict frontier. This focuses budget on the kinds of boundary mistakes that concurrent libraries commonly mishandle. 5. LLM Concretization 5.1. Prompt Contract The LLM receives a typed prompt assembled from the scenario tuple and API adapter schema: P(,Ad)=(,,,,,,,).P(S,A_d)=( Hdr, Res, Ev, Ord, Conf, Obs, Out, Ban). The fields encode resource declarations, typed events, order edges, concurrency hints, expected observation classes, and banned behaviors such as invented semantic events or weakened assertions. A representative prompt fragment is shown in Listing 2. Listing 2: Constrained prompt fragment for concretization. ⬇ scenario_id: mpsc_permit_close target_api: tokio::sync::mpsc resources: permit_sender: Sp boundary_sender: Sb receiver: R0 events: - e1: reserve_owned Sp -> P0 - e2: spawn T1 with P0 - e3: permit_send P0 m1 - e4: close R0 - e5: recv R0 -> m1 - e6: try_send Sb boundary_msg - e7: recv_end R0 order: - e1 < e2 < e3 - e1 < e4 - e3 < e5 - e4 < e5 < e6 < e7 concurrent: - (e3, e4) expected: - class(out(e3)) in SendOk - class(out(e6)) in ClosedLike - class(out(e7)) in End output_contract: - emit one marker before each modeled event - preserve all order constraints - return Rust test code only The LLM output is represented as Y=(c,μ,a)Y=(c,μ,a) where c is Rust test code, μ maps scenario events to emitted runtime markers, and a is a set of generated assertions. We accept a generated artifact for execution only if (Y,)⇔ WellFormed(Y,S) (c) Compiles(c) ∧∀e∈E,μ(e)↓ ∀ e∈ E,\;μ(e) ∧(Y,E). NoInventedEvents(Y,E). This is a static admission filter; the structural oracle later checks whether the runtime trace actually respects the intended partial order. For evaluation, we also use a partial structural-fidelity score. Let h⋆h be a maximum-cardinality order-preserving partial matching from scenario events to emitted markers. We define (,τ)=|dom(h⋆)||E|. Fid(S,τ)= | dom(h )||E|. This allows tool to measure how much of the intended structure survives concretization even when the full structural oracle fails. The crucial rule is that the LLM may choose syntax, helper names, and local scaffolding, but it may not invent new semantic events, relax order constraints, or redefine the expected outcome classes. 5.2. Concretization and Repair Loop We require a generated test to compile and to expose the marker structure needed by the runtime oracle. Algorithm 2 gives the loop. This loop is deliberately strict because successful compilation alone is insufficient to prove that the scenario has been correctly concretized. Algorithm 2 Concretization with structural repair 1:scenario S, adapter schema AdA_d, LLM L, retry bound R 2:faithful test artifact or failure 3:for r=1r=1 to R do 4: build prompt P(,Ad)P(S,A_d) 5: Y←L(P)Y← L(P) 6: if Y.cY.c fails to compile then 7: feed compiler diagnostics back to L 8: continue 9: end if 10: if marker coverage is incomplete then 11: feed structural diagnostics back to L 12: continue 13: end if 14: return Y 15:end for 16:return Fail 6. Petri-Guided Schedule Exploration The scenario tuple already tells us which events are causally constrained and which pairs are in semantic conflict. We use that information to shape schedule exploration rather than treating all harness variants as equally important. For a prefix ρ⊆Eρ E, define the ready frontier as (ρ)=e∈E∖ρ∣∀e′≺e,e′∈ρ. frontier_S(ρ)=\e∈ E ρ ∀ e e,\;e ∈ρ\. For any ready event e, we define a conflict-first priority ρ(e)= prio_ρ(e)= α∑e′∈(ρ)∖e[(e,e′)∈#] α _e ∈ frontier_S(ρ) \e\1[(e,e )∈\#] +β(e)−γ(ρ,e), +β\, Rare(e)-γ\, Seen(ρ,e), where (e) Rare(e) rewards uncommon transition classes and Seen penalizes already explored prefixes. A partial-order scenario also induces a task skeleton K=(Vtask,Espawn,Econf),K_S=(V_task,E_spawn,E_conf), where VtaskV_task partitions events by task ownership, EspawnE_spawn records spawn-parent relations, and Econf=(ei,ej)∣ei∥ej∧(ei,ej)∈#E_conf=\(e_i,e_j) e_i e_j (e_i,e_j)∈\#\ collects incomparable conflict pairs. A concrete harness variant chooses task creation order, barrier placement, and explicit yield points around selected pairs in EconfE_conf. We do not need to modify Loom internals to use this signal. Instead, we generate a small set of schedule-shaping harness variants that prioritize different high-conflict frontier choices, then run each variant under Loom when a Loom-compatible harness exists. For APIs where direct Loom integration is unavailable, the same schedule-shaping variants can be executed under a deterministic scheduler wrapper. The improvement is therefore above Loom rather than inside Loom: the Petri net chooses which concurrency skeletons deserve schedule budget. Algorithm 3 Petri-guided schedule shaping 1:partial-order scenario S, variant budget K 2:harness variants H 3:H←∅H← 4:for j=1j=1 to K do 5: ρ←∅ρ← , hj←[]h_j←[\,] 6: while ρ≠Eρ≠ E do 7: F←(ρ)F← frontier_S(ρ) 8: choose e⋆∈Fe ∈ F maximizing ρ(e) prio_ρ(e) 9: append e⋆e to hjh_j 10: insert yield/barrier hooks around conflicting incomparable pairs 11: ρ←ρ∪e⋆ρ←ρ∪\e \ 12: end while 13: add hjh_j to H 14:end for 15:return H Let (h) YieldPts(h) denote the conflict pairs that a harness variant h explicitly exposes with barriers or yields, and let Cj−1C_j-1 be the set already covered by earlier variants. We can then rank candidate variants by uncovered conflict gain: hj=argmaxh∈ℋ()∑(e,e′)∈(h)∖Cj−1w(e,e′).h_j= _h (S) _(e,e )∈ YieldPts(h) C_j-1w(e,e ). This gives a concrete methodological improvement over naive schedule enumeration: Loom still explores schedules within each harness, but the Petri layer decides which harnesses deserve schedule budget by maximizing semantically meaningful conflict coverage first. 7. Multi-Layer Semantic Oracle The execution harness records a trace τ=((m1,o1),(m2,o2),…,(mk,ok)),τ= ((m_1,o_1),(m_2,o_2),…,(m_k,o_k) ), where each mim_i is an emitted marker and each oio_i is the corresponding local observation or return class. We define the oracle as a conjunction of four layers: (,τ)=str∧out∧inv∧live.O(S,τ)=O_str _out _inv _live. Structural oracle. str(,τ)=1O_str(S,τ)=1 iff there exists an injective matching h:E→1,…,kh:E→\1,…,k\ such that: (1) the marker at position h(e)h(e) corresponds to event e; (2) if ei≺eje_i e_j, then h(ei)<h(ej)h(e_i)<h(e_j). If str=0O_str=0, the test is treated as a concretization failure rather than an API bug. Outcome oracle. Each event e may carry an allowed set of observation classes Φe _e. Then out(,τ)=1O_out(S,τ)=1 iff for every matched event e, the observed class at h(e)h(e) belongs to Φe _e. This allows the oracle to express sets of admissible concurrent outcomes rather than brittle single-value expectations. Invariant oracle. Let Ψ be the set of global scenario invariants. Then inv(,τ)=1O_inv(S,τ)=1 iff every invariant in Ψ holds over the observed execution summary. Typical examples include resource conservation, absence of ghost messages, bounded buffer counts, or monotonic closure state. Liveness oracle. live(,τ)=1O_live(S,τ)=1 iff the run terminates within a bound and no task expected to complete remains permanently blocked. This matters because many concurrency faults manifest as hangs rather than wrong return values. Let sem=out∧inv∧liveO_sem=O_out _inv _live. We classify outcomes by (,τ)=ConcretizationErrorif str=0,SemanticFailureif str=1∧sem=0,Passotherwise. Class(S,τ)= aligned & ConcretizationError&&if O_str=0,\\ & SemanticFailure&&if O_str=1 _sem=0,\\ & Pass&&otherwise. aligned This decision rule is operationally important: only the second case becomes a bug candidate. Table 3 summarizes the role of each layer. Table 3. Semantic oracle layers. Layer Checks Failure signal Structural Marker coverage and order preservation LLM omitted an event or reordered a required edge Outcome Return/error class membership A close-after-send boundary event unexpectedly succeeds Invariant Scenario-level semantic properties Buffered count becomes inconsistent with sends and receives Liveness Bounded completion and join behavior Test hangs after a race that should terminate This separation is important. It prevents the system from confusing a bad generated test with a bad library behavior. Soundness intuition. Assume that (1) the adapter AdA_d is locally faithful, (2) marker μ(e)μ(e) is emitted immediately before the concrete step for e, and (3) helper code emits no spurious modeled markers. If str(,τ)=1,O_str(S,τ)=1, then τ contains a matched subsequence with the same order as some π∈(,NA)π∈ Exec(S,N_A). In other words, the runtime trace refines a modeled linearization of the intended scenario up to unmodeled helper steps. Under this assumption, a semantic-oracle failure points to API behavior under the concretized scenario rather than to missing events or reordered scaffolding. Failure report. When a run fails, the system reports =(,,Lf,τ⋆,hj), Report=(S, Class,L_f,τ ,h_j), where Lf⊆out,inv,liveL_f \out,inv,live\ is the set of failed oracle layers, τ⋆τ is the matched event subsequence, and hjh_j is the harness variant that exposed the behavior. This report structure matters in practice because it supports triage, de-duplication, and prompt repair without collapsing all failures into a single undifferentiated bug bucket. 8. Evaluation and Results This section reports a preliminary evaluation of the reviewed MPSC running example. The goal is not a large benchmark, but a paper-level check that the current prototype can carry one manually modeled CPN and one reviewed ScenarioBlueprint all the way to executable Tokio code, and that the resulting runtime trace agrees with the model-derived oracle. 8.1. Subjects and Setup The evaluated subject is a bounded Tokio MPSC channel with capacity one. The reviewed scenario contains seven events and exactly two legal linearizations: ⬇ e3_before_e4: e1 e2 e3 e4 e5 e6 e7 e4_before_e3: e1 e2 e4 e3 e5 e6 e7 The repaired generated source compiles, executes both legal schedules inside one Tokio test, and emits 14 JSONL records per run. We evaluate the same source three times with the generic artifact-driven evaluator; all three runs pass and the evaluator reports no findings. Table 4. Current MPSC prototype evidence. Property Result Compilation passed Legal schedules 2 Runtime executions 3 Records per execution 14 Evaluator findings none 8.2. RQ1: Can the artifact-constrained prompt produce executable Tokio code? The generated test compiles under the recorded toolchain and runs to completion under the generic evaluator. This is the first requirement for the pipeline: the prompt and generation contract are strong enough to produce a real Tokio test rather than a sketch or pseudo-code fragment. The same source also carries the scenario labels, the expected observations, and the runtime evidence points that the evaluator consumes. For this MPSC example, those ingredients were sufficient to obtain three successful executions without any MPSC-specific checker in the evaluation crate. 8.3. RQ2: Does the generated runner preserve schedule-sensitive structure? The scenario distinguishes two legal linearizations by the relative order of e3 and e4, and the runner preserves that distinction in the runtime trace. Each execution emits the same 14 records, split evenly across the two schedules, and the evaluator confirms that the observed record order matches the artifact oracle. This matters because the example is not merely “some test that passes.” It is a small schedule family whose legal orders remain visible in the final trace. That is the concrete structural property the prototype is meant to preserve. 8.4. RQ3: Can feedback repair recover from a concrete mismatch without changing the scenario? The repaired source used here is the result of a bounded runtime-feedback repair. The repair adjusted the emitted operation labels to the exact Scenario strings, while preserving the same schedules, the same observable behavior, and the same record count. In other words, repair fixed the contract mismatch rather than rewriting the test into a different one. This is the relevant form of repair for the current prototype: the generated code may change its surface syntax and evidence plumbing, but it should not silently change the modeled scenario or weaken the oracle. 8.5. RQ4: Is the artifact boundary strict enough to isolate the generic pipeline from the subject-specific model? The generic LLM and evaluator layers consume the portable artifact, not handwritten MPSC logic. The subject-specific semantics live in the family crate: the reviewed CPN, the reviewed scenario, and the runtime observation contract. The generic pipeline then compiles the generated source, executes it, and checks the emitted JSONL records against the artifact-derived oracle. The limitation is scope. This is still a preliminary evaluation on one running example, not a large-scale mutation study or a schedule-budget benchmark. The result supports feasibility, not statistical superiority. 8.6. Threats to Validity The main threat is scale. The current evaluation covers one reviewed MPSC subject and one repaired generated runner. It does not yet include a mutant corpus, a pure prompt baseline, or a schedule-exploration comparison. Even so, the available evidence is enough for an arXiv submission that claims a working prototype and a validated artifact boundary, rather than a completed benchmark. 9. Related Work Model-based testing with Petri nets. Petri nets have long been used for formal modeling, reachability reasoning, and test derivation in stateful systems (Murata, 1989; Manral, 2015). That line of work establishes why token-based models are useful: they express multiplicity, causality, and conflict more naturally than flat state machines. Our setting adds a missing concretization problem. The output must not stop at an abstract trace; it must become a compilable Rust test with tasks, ownership moves, time bounds, and executable assertions. SyncPetri therefore uses the Petri net as a semantic intermediate representation rather than as the whole testing engine. Stateful API testing and deep-state exploration. REST-ler showed that dependency-aware generation is necessary for stateful APIs because naive request composition rarely reaches meaningful deep states (Atlidakis et al., 2018). StateAFL and later stateful greybox work likewise argue that failures often emerge only after the system enters semantically distinct states (Natella, 2021; Ba et al., 2022). We share that motivation, but the target and abstraction differ. Those systems focus on network-facing or protocol-facing interfaces, whereas SyncPetri targets in-process Rust library APIs whose hard behaviors depend on resource ownership, handle invalidation, reserved capabilities, and schedule-sensitive partial orders. Our near-legal scenarios also aim at semantic boundaries defined by the model, rather than at arbitrary invalid inputs. LLM-based test generation. TitanFuzz and Fuzz4All showed that LLMs can generate diverse tests and programs in domains where manual generators are costly (Deng et al., 2022; Xia et al., 2023). CoverUp further showed that external feedback and structure remain important even for strong models (Pizzorno and Berger, 2024). SyncPetri adopts that lesson but changes the guidance signal. Instead of relying on open-ended prompting or coverage alone, we provide a typed event graph with resource bindings, order constraints, admissible outcome classes, and banned semantic edits, then judge the result with a structural oracle. The contribution is therefore not simply to use an LLM for testing, but to restrict the LLM to code realization while keeping semantic intent outside the model. Systematic concurrency exploration. Loom provides controlled schedule exploration for Rust concurrent code (Tokio Contributors, 2026a). Our work is complementary rather than competitive. Loom explores micro-interleavings inside a harness; SyncPetri tries to make that harness semantically meaningful in the first place by extracting race windows and conflict pairs from the resource model. The schedule-shaping component therefore operates above the scheduler: it prioritizes which concurrency skeletons deserve exploration budget, but it does not modify the scheduler’s internal search algorithm. Positioning. Across these lines of work, the missing combination is a model-driven route from resource-aware concurrency semantics to executable Rust tests without delegating the semantic oracle to the LLM. SyncPetri occupies that space by combining Petri-net scenario synthesis, constrained concretization, schedule-aware harness construction, and layered runtime judgment in one testing workflow. 10. Conclusion This paper presented SyncPetri, a Petri-net-constrained architecture for LLM-based test generation over concurrent stateful Rust APIs. The main thesis is that model structure should control semantics, boundary mutation, and concurrency exposure, while the LLM should only control executable realization. To support that thesis, we formalized the target domain, defined a scenario language, specified concretization and repair loops, proposed Petri-guided schedule shaping, and introduced a multi-layer semantic oracle. Together, these pieces form a main-track-sized methodology: not merely a sketch that Petri nets and LLMs can be combined, but a concrete design for how they should be combined in a test-generation system. References V. Atlidakis, P. Godefroid, and M. Polishchuk (2018) REST-ler: automatic intelligent REST API fuzzing. External Links: 1806.09739, Link Cited by: §9. J. Ba, M. Böhme, Z. Mirzamomen, and A. Roychoudhury (2022) Stateful greybox fuzzing. External Links: 2204.02545, Link Cited by: §9. Y. Deng, C. S. Xia, H. Peng, C. Yang, and L. Zhang (2022) Large language models are zero-shot fuzzers: fuzzing deep-learning libraries via large language models. External Links: 2212.14834, Link Cited by: §9. J. Manral (2015) Automated test case generation using petri nets. External Links: 1509.08401, Link Cited by: §9. T. Murata (1989) Petri nets: properties, analysis and applications. Proceedings of the IEEE 77 (4), p. 541–580. External Links: Document Cited by: §9. R. Natella (2021) StateAFL: greybox fuzzing for stateful network servers. External Links: 2110.06253, Link Cited by: §9. J. A. Pizzorno and E. D. Berger (2024) CoverUp: coverage-guided LLM-based test generation. External Links: 2403.16218, Link Cited by: §9. Tokio Contributors (2026a) loom. Note: https://docs.rs/loom/latest/loom/Accessed 2026-07-16 Cited by: §9. Tokio Contributors (2026b) tokio::sync::broadcast. Note: https://docs.rs/tokio/latest/tokio/sync/broadcast/Accessed 2026-07-16 Cited by: §2. Tokio Contributors (2026c) tokio::sync::mpsc. Note: https://docs.rs/tokio/latest/tokio/sync/mpsc/Accessed 2026-07-16 Cited by: §2.2, §2. Tokio Contributors (2026d) tokio::sync::Semaphore. Note: https://docs.rs/tokio/latest/tokio/sync/struct.Semaphore.htmlAccessed 2026-07-16 Cited by: §2. Tokio Contributors (2026e) tokio::sync::watch. Note: https://docs.rs/tokio/latest/tokio/sync/watch/Accessed 2026-07-16 Cited by: §2. C. S. Xia, M. Paltenghi, J. L. Tian, M. Pradel, and L. Zhang (2023) Fuzz4All: universal fuzzing with large language models. External Links: 2308.04748, Link Cited by: §9.