From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs

Source: arXiv:2607.21530 · Published 2026-07-23 · By Kaiwen Zhang, Guanjun Liu

TL;DR

This paper addresses the challenge of generating semantically meaningful, executable concurrency tests for stateful Rust library APIs, which expose complex resource ownership and lifecycle behaviors under concurrent interleavings. Large language models (LLMs) can generate Rust test code but tend to violate API preconditions or produce shallow sequential traces that miss concurrency bugs. Conversely, existing model-based testing approaches provide semantic control but require heavy handwritten scaffolding to turn abstract scenarios into executable tests. The authors propose SyncPetri, a methodology combining colored Petri nets to formally model resource flow, lifecycle states, and concurrency conflicts with LLM-driven concretization of these models into Rust test code. Petri nets specify deep-state legal and near-legal scenarios as constrained partial orders, while an LLM generates the concrete syntax and test scaffolding under strict prompt contracts and repair loops. A layered semantic oracle then distinguishes test synthesis failures from true API misbehaviors.

SyncPetri was instantiated on tokio::sync-style concurrency libraries, modeling resource-sensitive APIs such as bounded MPSC channels with subtle async contracts. Their evaluation on a hand-modeled MPSC prototype demonstrated that SyncPetri can generate tests with perfect structural fidelity and coverage of deep-state concurrent interleavings that expose semantic faults missed by naive fuzzing or pure LLM prompting. By separating semantic intent (in Petri nets) from low-cost code generation (via LLMs), SyncPetri achieves stronger semantic correctness and concurrency exploration without requiring the model to capture full implementation details. This work suggests a practical tradeoff favoring lightweight modeling plus constrained LLM synthesis for testing complex concurrent Rust APIs.

Key findings

• SyncPetri successfully synthesizes legal deep-state concurrent test scenarios from colored Petri nets representing resource flow and concurrency conflicts with perfect structural fidelity (Fid=100%) in evaluated MPSC prototype.
• The framework produces two legal linearizations that capture subtle interleavings related to permit commit and receiver close order in MPSC with capacity one, exposing semantic boundary violations.
• Layered semantic oracle separates concretization errors from semantic failures, improving diagnosis and reducing false bug reports from malformed LLM outputs.
• Petri-guided schedule shaping prioritizes harness variants exposing semantic conflicts, improving concurrency coverage over naive or random fuzzing techniques.
• Constrained LLM prompts enforce explicit concurrency scaffolding and marker emission, preventing hallucinated events or relaxed API precondition violations during test generation.
• Adaptation schemas generalize reusable transition models (clone, reserve, close, consume) across multiple tokio::sync APIs, reducing modeling cost.
• The prototype evaluation included 3 runtime executions and 14 recorded markers per execution, confirming the approach’s feasibility and structural fidelity.
• Near-legal boundary mutations generated by SyncPetri target single precondition violations to probe API robustness at semantic limits.

Threat model

The adversary is a testing framework tasked with generating concurrent Rust tests that expose semantic API bugs related to resource states and concurrency races. It cannot alter the Petri-net model or Rust API implementation but aims to discover violations such as precondition breaches, stale capability use, race-sensitive invalid states, or liveness failures by exploring legal and near-legal event sequences and interleavings. The model assumes Rust’s memory safety guarantees but focuses on higher-level semantic protocol bugs.

Methodology — deep read

1. Threat Model & Assumptions: The adversary considered is the testing framework itself, challenged to generate test sequences exposing semantic protocol bugs in concurrent Rust APIs. Assumptions include correct Rust memory safety, with focus on semantic faults beyond type safety (e.g., stale handles, lost notifications, race sensitivity, liveness bugs). The system assumes the target API designer provides a formal resource model as a colored Petri net and adapter schema linking model steps to concrete Rust operations. The adversary cannot modify the model or implementation but tries to expose subtle logical errors through concurrency interleavings.

2. Data: The approach operates on formal Petri-net models describing API resource places (e.g., senders, receivers, buffer slots), transitions representing API operations (send, receive, close), associated guards, and token color updates. Scenario synthesis produces event sets with partial orders and conflict relations, along with expected outcome classes for each event. The concrete example focuses on the tokio::sync MPSC channel with capacity one. Data splits or scalability tests are not detailed.

3. Architecture / Algorithm: The core architecture couples three components: (1) Petri-net scenario synthesis (Algorithm 1) that generates legal, near-legal, and partial-order concurrent event scenarios based on token reachability and conflict scoring heuristics; (2) LLM concretization constrained by a typed JSON prompt encoding the scenario plus typed resource bindings, concurrency edge relations, banned behaviors, and expected outputs; the LLM outputs Rust test code with event markers, scaffolding, assertions, and synchronized handshakes to preserve concurrency semantics; a structural repair loop (Algorithm 2) rejects incomplete or misordered marker usage and retries LLM generation with feedback; (3) Petri-guided schedule shaping (Algorithm 3) that generates multiple harness variants prioritized for conflict coverage, feeding these into the Loom scheduler or a deterministic runtime adapter for interleaving exploration.

Reusable transition schemas model common API idioms (clone, reserve, close, consume) to assemble Petri nets from composable building blocks rather than bespoke nets per API.

4. Training Regime: Not applicable—no ML training is performed. LLMs are prompted at generation time via structured JSON inputs and constrained output contracts enforcing syntactic and semantic properties.

5. Evaluation Protocol: Evaluation uses a single hand-modeled MPSC Rust library scenario with 7 events and two legal linearizations exemplifying concurrency races around permit usage and receiver closure. Metrics include compilation success, execution runs, recorded event markers, structural fidelity scores between scenario events and emitted markers, and semantic oracle verdicts evaluating correctness, boundary violation detection, and liveness. There are no cross-validation folds or distribution shifts tested. The baseline consists of typical LLM prompting approaches and random concurrency fuzzing discussed qualitatively.

6. Reproducibility: The paper mentions a prototype implementation integrating Petri net modeling, prompt construction, LLM calls, and runtime oracle checks. It does not state if code or datasets are publicly released. The described approach relies on manually crafted Petri nets and adapter schemas.

Example Walkthrough: The motivating example models a bounded MPSC channel with capacity one, including sender permits and receiver handles. The Petri net encodes states such as LiveSender, Open channel, Permit possession, and buffer counts. SyncPetri synthesizes a scenario with events representing reserving a permit, spawning a task to commit the permit-send, closing the receiver, receiving a message, and boundary probes with try_send after close. The LLM is prompted with detailed JSON describing resource bindings, event order constraints, concurrency conflict pairs, and expected output classes. It generates Rust test code with explicit marker calls before each modeled event and synchronization handshakes to preserve concurrency semantics. The harness variants execute alternative linearizations (commit-before-close and close-before-commit) under Loom to explore interleavings. The four-layer oracle validates structural event order, output classes, global invariants, and liveness, distinguishing concretization failures (e.g., missing or reordered markers) from true semantic failures (e.g., sending allowed after close). The framework successfully avoids pitfalls of naive fuzzing or unconstrained LLM prompting that collapse concurrency or omit crucial races.

Technical innovations

• A Petri-net-guided scenario synthesis method that encodes resource flow, lifecycle, and concurrency conflicts as colored tokens and transitions to generate legal, near-legal, and partial-order event scenarios.
• A constrained LLM prompt design coupled with a structural repair loop enforcing local faithfulness contracts and blocking semantic event invention during test concretization.
• A layered semantic oracle combining structural, outcome, invariant, and liveness checks to differentiate concretization errors from true semantic bugs.
• A Petri-guided schedule shaping algorithm that prioritizes execution harness variants exposing maximal uncovered concurrency conflicts for systematic exploration.

Datasets

• MPSC prototype scenario — 7 events, 2 legal linearizations — manually modeled from tokio::sync::mpsc (not publicly released)

Baselines vs proposed

• Naive random concurrency fuzzing: unlikely to reach deep resource states or expose race-sensitive semantic bugs versus SyncPetri: reliably generates deep-state legal scenarios with concurrency conflicts captured
• Direct LLM prompting without Petri constraints: often collapses concurrency to sequential traces or hallucinates incorrect precondition enforcement versus SyncPetri: enforces strict order and concurrency constraints leading to faithful concurrent tests
• Loom baseline schedule exploration: uniform harness enumeration versus Petri-guided schedule shaping: prioritizes high-conflict harnesses improving semantic bug exposure efficiency

Limitations

• Requires manual construction of Petri-net resource models and adapter schemas, limiting fully automatic applicability.
• Evaluated only on a small prototype MPSC library scenario with 7 events and limited concurrency complexity.
• Does not fully integrate or replace underlying concurrency schedulers like Loom but shapes harness selection above them.
• No evaluation on distribution shifts, unseen APIs, or large-scale benchmark datasets reported.
• No adversarial evaluation against malicious LLM outputs beyond structural checks.
• Liveness oracle deployment may be sensitive to fixed runtime bounds and may miss rare deadlocks.

Open questions / follow-ons

• How well does the approach scale to larger Rust concurrency APIs with more complex state and resource interactions?
• Can the Petri-net resource and adapter schemas be learned or semi-automated to reduce manual modeling effort?
• What is the impact of using more advanced or fine-tuned LLMs on concretization fidelity and repair convergence?
• How effective is the approach when combined with more sophisticated concurrency schedulers or model checkers beyond Loom?

Why it matters for bot defense

This work is highly relevant for bot-defense engineers and CAPTCHA practitioners interested in robust testing of concurrent stateful APIs exposed to untrusted or adversarial inputs, as it offers a structured methodology to generate semantically faithful, executable concurrent tests that expose subtle race conditions and protocol violations often missed by naive fuzzing or unconstrained LLM generation. The separation of semantic modeling (resource flow, conflict) from syntactic concretization (via constrained LLM prompts) is a valuable design pattern when building automated test pipelines for complex concurrent services. Additionally, the multi-layer oracle’s capacity to distinguish test synthesis failures from actual API bugs can improve diagnostic accuracy in automated testing regimes. Implementers should note the manual modeling cost and prototype scope, but adopting Petri-net-guided scenario synthesis could improve reliability and coverage of concurrency test harnesses in cutting-edge Rust-based microservices or proxy implementations that protect backend CAPTCHA verification logic.

Cite

@article{arxiv2607_21530,
  title={ From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs },
  author={ Kaiwen Zhang and Guanjun Liu },
  journal={arXiv preprint arXiv:2607.21530},
  year={ 2026 },
  url={https://arxiv.org/abs/2607.21530}
}

Read the full paper

• arXiv:2607.21530 (abstract)
• arXiv:2607.21530 (PDF)