从资源流到可执行测试：Petri 网指导的并发有状态 Rust API 大语言模型测试生成

从资源流到可执行测试：Petri 网指导的并发有状态 Rust API 大语言模型测试生成（中文全译）

翻译说明：本文是 arXiv 论文 From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs（arXiv:2607.21530）的中文全译，由智测团队翻译。原作者：Kaiwen Zhang、Guanjun Liu（同济大学）。原文以 CC BY 4.0 许可发布。译文保留原文全部章节、数据与结论；参考文献列表从略。

摘要

并发有状态库 API 通过不断演变的资源所有权、生命周期状态和竞争的交错执行来暴露其行为。大型语言模型可以合成可执行的 Rust 测试，但其输出常常违反 API 前置条件、保持浅层状态，或将并发性退化为偶然的顺序追踪。相反，基于模型和系统化测试技术提供了语义控制，但通常需要大量手写代码才能将抽象场景转化为可执行测试。本文解决了形式化场景设计与低成本测试具体化之间的差距。

我们提出了一种用于并发有状态 Rust API 测试生成的 Petri 网指导方法。该方法将 API 资源、生命周期条件和因果依赖表示为着色令牌和变迁；推导出合法的深层状态、近合法状态以及偏序并发场景；并将这些场景作为基于 LLM 的代码合成的约束中间表示。局部保真契约和结构修复循环在具体化过程中保持建模意图，而 Petri 指导的调度整形则优先处理高冲突并发骨架以进行系统化探索。分层语义预言机随后区分合成失败与目标 API 预期行为的违反。

我们为 Rust 并发库实现了一个原型，并定义了一个评估协议，该协议检查可执行性、结构保真度、深层状态可达性、边界故障产出和冲突覆盖率。核心方法学原则是分离职责：Petri 网指定语义意图、资源流、可达性、冲突和与 bug 相关的变异，而 LLM 实现库特定语法、任务脚手架和断言。这种设计为研究形式化资源流模型是否能使 LLM 生成的并发测试更保真、更具状态性和诊断实用性提供了具体基础。

关键词：Petri 网，大型语言模型，Rust，并发测试，有状态 API 测试，测试生成

1. 引言

许多 Rust 库 API 并非孤立的函数接口。它们暴露句柄、许可证、闭包、缓冲状态和任务级交互模式，其行为取决于先前的操作和竞争的调度。在这种情况下，Rust 的类型系统消除了广泛的内存错误类别，但它并不能证明库遵守其高级协议。剩下的 bug 是语义故障：过时的能力仍然被接受，关闭操作使错误的行为无效，缓冲值丢失，或者测试仅在特定交错到达深层状态后才挂起。

这些 API 难以测试有三个耦合原因。首先，有趣的行为具有强烈的状态依赖性：许多故障模式仅在合法前缀建立非平凡资源配置后才会出现。其次，前缀本身必须在语义上受控；否则，后续观察将毫无意义，因为测试从未 exercised 有效的协议状态。第三，并发性在偏序级别而非原始长度级别起作用。如果长序列偶然序列化了本应暴露的竞争，那么它将毫无用处。

现有方法仅覆盖了这一空间的一部分。基于模型和依赖感知的测试可以描述合法状态、资源流和边界条件，但将这些抽象转化为可执行的 Rust 测试仍然需要大量的手写脚手架、任务编排和 API 特定断言。直接的 LLM 提示减少了这种编码负担，但也把语义责任推回给了模型。在实践中，LLM 可能会虚构事件、违反启用条件、混淆保留能力与新能力、弱化断言，或将并发行为扁平化为方便的顺序追踪。

本文的立场故意更狭窄。我们不要求 LLM 从头发现并发语义，也不声称消除建模工作。相反，我们使用 Petri 网模型对资源多重性、因果关系、冲突和近合法边界情况进行编码，然后仅使用 LLM 将模型生成的场景具体化为可执行的 Rust 代码。调度器仍然探索运行时交错，API 特定的不变量仍然需要人工编写。关键在于分离职责，使语义意图保持在 LLM 之外，而代码实现保持低成本。

这种权衡特别适合并发有状态 Rust API。Petri 网可以将发送者、接收者、许可证、容量、缓冲消息和观察义务表示为令牌，并且可以表达使测试具有诊断实用性的精确冲突和因果依赖。一旦该结构明确，LLM 就可以做它相对擅长的事情：编写目标特定的设置、任务创建、断言和清理。关键的设计规则很简单：模型编写含义，LLM 编写代码。

这种设计的代价也很清楚。SyncPetri 需要手动编写的资源模型、适配器和场景不变量，其调度整形改进了诸如 Loom 等工具之上的 harness 选择，而不是替换它们的内部搜索。我们 upfront 声明这些限制，因为它们定义了适当的贡献：不是全自动的并发验证，而是一种测试架构，用一些建模努力换取对生成测试的更强语义控制。

具体来说，SyncPetri 从着色 Petri 网合成合法深层状态追踪、近合法边界探测和偏序并发场景；通过约束提示和结构修复循环具体化它们；并通过分层预言机判断结果执行，该预言机将具体化失败与语义失败分开。结果是一个为并发 Rust API 设计的测试管道，其困难 bug 存在于资源协议中而非孤立函数输出中。

我们做出五项贡献：

• 我们将并发有状态 Rust API 测试形式化为基于承载资源的变迁的 Petri 网指导场景合成。
• 我们定义了一个适配器模式和局部保真契约，将抽象 Petri 网步骤连接到具体 Rust 执行。
• 我们定义了一个场景表示，统一了合法可达性、近合法边界变异和偏序并发性。
• 我们提出了一个约束具体化循环和一个多层预言机，区分生成失败与语义失败。
• 我们提出了一种用于 Loom 兼容 harness 的 Petri 指导调度整形方法，并在 tokio::sync 风格 API 上实例化了完整工作流程。

2. 问题设定与运行示例

我们针对具有三个基本属性的 API：1) 有状态性：操作的结果或有效性在很大程度上取决于系统的内部抽象资源状态。2) 资源敏感性：操作直接操纵能力——消耗、产生、拆分、合并或使句柄、许可证、缓冲数据或访问令牌无效。3) 并发暴露：多个不同的任务或句柄同时交互，意味着不同的执行调度可能产生完全不同的可观察结果。

这涵盖了有用的 Rust 库切片。例如，在 tokio::sync 中，mpsc 通道暴露发送者、接收者、许可证、缓冲和闭包；watch 暴露最新值语义和观察状态；broadcast 暴露滞后接收者和重放边界；Semaphore 暴露获取、释放和闭包行为 (Tokio Contributors, 2026c; Tokio Contributors, 2026e; Tokio Contributors, 2026b; Tokio Contributors, 2026d)。这些 API 足够小，可以在本地测试，但足够丰富，需要真正的语义编排。表 1 展示了运行中的 mpsc 示例的紧凑抽象。

表 1. 有界 mpsc 的示例 Petri 网位置。

因此，研究问题是：我们如何从 Rust API 的 Petri 网模型合成语义上有意义的并发测试场景，使用 LLM 将这些场景具体化为可执行的 Rust 代码，并判断结果执行是否保留或违反了预期的 API 语义？

2.1. Bug 模型

我们针对逃逸 Rust 类型系统和严格内存安全检查的语义故障。我们将这些故障分为四个核心家族：

• B_pre（前置条件强制执行）：即使其抽象前提条件被违反，操作仍错误地成功（例如，向已关闭通道发送）。
• B_state（后状态不一致）：操作执行后，资源记账、所有权转移或清理逻辑偏离规范。
• B_race（竞争敏感性）：依赖于调度的交错暴露出高级协议严格禁止的观察序列或状态变化。
• B_live（活跃性和阻塞）：实现遭受永久阻塞、唤醒丢失或在到达终端协议状态后无法终止。

对于 tokio::sync API，这些类别对应于具体的故障形状，如关闭后发送成功、过时句柄接受、值更新后通知丢失、许可证记账不一致或关闭竞争中的非终止挂起。此 bug 模型作为我们植入变异体评估的基本事实。

2.2. 运行示例与基线陷阱

我们使用容量为一的 Tokio MPSC 通道来激励 SyncPetri 工作流程。设置涉及一个接收者 R0、一个用于保留容量的普通发送者 Sp，以及一个充当边界探测的独立发送者 Sb。

关注的核心语义不变量涉及一个微妙的异步契约：关闭接收者必须立即拒绝新的普通发送操作，但在关闭之前获取的任何预先存在的 Permit 或 OwnedPermit 仍然有效，并且必须允许将其消息提交到缓冲区 (Tokio Contributors, 2026c)。然后接收者有义务在最终终止前排出这个未完成的消息。

这种微妙生命周期契约会产生几种可能的语义故障：实现可能在关闭时错误地丢弃由未完成许可证支持的消息，拒绝有效的许可证提交，或者由于关闭标志和许可证计数器之间的内部去同步而无限期挂起。

传统测试范式难以隔离这种行为。纯粹的随机并发模糊测试极不可能生成击中此深层状态所需的精确交错序列（保留容量、在提交时竞争关闭，然后验证剩余排出）。相反，纯提示驱动的 LLM 经常遭受两种对立的失败：要么将并发执行折叠成简化的顺序追踪，完全错过了竞争；要么虚构严格的顺序规则（例如，假设关闭后所有操作都失败），从而生成与实际 API 契约不匹配的错误测试断言。

步骤 1：资源模型与深层状态。

最初，抽象初始标记 M0 包含两个活动发送者能力、一个活动接收者、一个开放通道令牌和一个容量令牌。第一个建模事件明确针对深层状态，通过保留容量：

e1 = reserveOwned(Sp) → P0.

产生的标记将网络移动到不同的配置，包含 Permit(P0,c) 和 Cap(c,0)。这代表了感兴趣的深层状态：通道拥有一个突出的、隔离的发送能力 (P0)，不同于普通的开放发送者或简单的缓冲项。至关重要的是，模型规定许可证提交变迁消耗 P0 而不需要 Open(c)，而普通发送仍然依赖于 Open(c) 和空闲容量。

步骤 2：场景。

从此标记出发，SyncPetri 在 E={e1,…,e7} 上构建一个偏序图，具有以下标签：

• e1: reserveOwned(Sp) → P0
• e2: spawn(T1, P0)
• e3: permitSend(P0, m1)
• e4: close(R0)
• e5: recv(R0) → m1
• e6: trySend(Sb, m2)
• e7: recvEnd(R0)

与其固定僵化的线性追踪，不如只捕获必要的因果依赖 ≺：

e1 ≺ e2 ≺ e3, e1 ≺ e4, e3 ≺ e5, e4 ≺ e5 ≺ e6 ≺ e7.

事件 e3 和 e4 在因果上是独立的，但竞争重叠的资源字段，因此被标记为显式竞争对：(e3,e4) ∈ #。此偏序安全地封装了两个有效的交错：提交前关闭和关闭前提交。事件 e6 充当近合法边界探测；在 e5 之后，通道的容量空闲但其状态保持关闭，意味着 e6 恰好违反了一个启用条件 (Open(c))。预期观察映射为集合值的允许类：

• Φ_e3 = {SendOk}
• Φ_e5 = {Msg(m1)}
• Φ_e6 = {ClosedLike}
• Φ_e7 = {End}

表 2. SyncPetri 职责划分与动机示例的工件。

步骤 3：约束 LLM 具体化。

结构图被序列化为高度约束的数据提示，而不是松散的文本描述。提示提供明确的资源映射、边依赖和允许的结果信封。

为了弥合抽象事件与可执行任务之间的差距，框架从冲突关系中派生执行脚手架。因为 (e3,e4) ∈ # 是一个活动并发对，提示要求明确的就绪、释放和完成握手，而不是让模型序列化动作。清单 1 说明了生成的代码工件。LLM 仍然可以自由处理目标特定语法和变量作用域，但不能剥离结构仪器标记 (mark)。

清单 1：动机示例的原理图生成 harness。

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)));

步骤 4：Petri 指导的调度探索。

合成的事件图引出两个宏观 harness：

• h_commit = [e1, e2, e3, e4, e5, e6, e7]
• h_close = [e1, e2, e4, e3, e5, e6, e7]

生成的握手保证在竞争窗口打开之前建立深层状态 P0。确定性调度器适配器（或 Loom）然后仅枚举该窗口内的微观交错。这种分工让 Petri 网模型选择宏观并发表面，而运行时调度器探索局部执行选择。

步骤 5：预言机决策与报告。

在合规实现上，任一线性化都可能在运行时发生。无论 e3 还是 e4 首先执行，e3 必须产生 SendOk，e5 必须观察到 m1，关闭后边界检查 e6 必须评估为 ClosedLike。

分层预言机首先调用结构检查器 (O_str) 以验证所有七个运行时标记是否以满足 ≺ 的顺序执行。如果 LLM 错误或编译器优化重新排序或绕过了标记，则运行被标记为 ConcretizationError 并被修剪。如果 O_str 通过但库返回未映射的观察类（例如，如果在关闭优先交错中变异体拒绝未完成许可证），系统注册真正的 SemanticFailure。生成的诊断配置文件记录为：

Report = (S_pc, SemanticFailure, {out}, τ*, h_close).

这种结构化输出确保数百个暴露相同根本bug的相同低级调度交错无缝去重为单个可操作报告。

3. 形式化模型

3.1. API 抽象与着色 Petri 网

我们从轻量级 API 抽象开始

A = (R, O, Σ, Ω),

其中 R 是资源种类集，O 是操作名称集，Σ 将每个操作映射到类型化参数和结果类，Ω 是运行时预言机使用的观察类集。

API 抽象被编译为着色 Petri 网

N_A = (P, T, F, χ, λ, g, u, M0).

其中 P 是有限位置集，T 是有限变迁集，F ⊆ (P×T) ∪ (T×P) 是流关系，χ 将每个位置映射到令牌颜色域，λ: T → O 用 API 或 harness 操作标记变迁，g_t 是每个变迁 t 的守卫谓词，u_t 是每个变迁 t 的令牌更新函数，M0 是初始标记。

令 I_t(p) 和 O_t(p) 表示变迁 t 在位置 p 的输入和输出令牌多重集。变迁在标记 M 下启用 iff

enabled(M,t) ⇔ g_t(M)=true ∧ ∀p∈P, I_t(p) ⊆ M(p).

如果 enabled(M,t) 成立，触发 t 产生新标记 M' 定义为

M' = u_t((M - I_t) + O_t).

我们写 M →^t M' 表示一步触发，M0 →^(t1...tk) Mk 表示有限触发序列。可达集为

Reach(N_A) = {M | ∃π, M0 →^π M}.

网的实际目的不仅是拒绝不可能的调用。它记录资源如何移动、哪些操作竞争资源以及哪些事件在因果上是独立的。

3.2. 适配器模式与局部保真

Petri 网是抽象的，但测试预言机在具体 Rust 执行上运行。因此，我们将每个目标库域 d 与适配器模式关联

A_d = (Ctor, Step, Spawn, Mark, Assert, Cleanup, Γ, ρ_d).

这里 Ctor 构造初始运行时对象，Step 将建模的变迁映射到具体 Rust 操作，Spawn 将可 spawns 的事件组打包成任务，Mark 发出事件标记，Assert 实例化具体检查，Cleanup 有界拆解，Γ 将具体结果映射到 Ω 中的观察类，ρ_d 将具体运行时状态抽象为 Petri 网标记。

我们不要求实现与模型之间的完全双模拟。方法学要求是在建模事件边界处的局部保真契约。对于事件 e 且 η(e)=t，令

Step_d(t, σ, β(e)) ↝ (σ', o)

表示从运行时状态 σ 到 σ' 的一个具体适配器步骤，带有原始观察 o，令 Ω_t^ok, Ω_t^err ⊆ Ω 表示 t 的建模成功和错误观察类。对于合法步骤，我们要求

ρ_d(σ)=M ∧ M →^t M' ⟹ ∃σ',o. Step_d(t, σ, β(e)) ↝ (σ', o) ∧ ρ_d(σ')=M' ∧ Γ(o) ∈ Ω_t^ok.

对于近合法步骤，我们要求单一前提条件违反映射到显式错误类结果：

ρ_d(σ)=M ∧ |Δ_F(M,t)| + |Δ_G(M,t)| = 1 ⟹ ∃σ',o. Step_d(t, σ, β(e)) ↝ (σ', o) ∧ Γ(o) ∈ Ω_t^err.

此契约故意轻量化。它要求适配器保持建模步骤和边界故障的含义，而不要求公开或重建每个内部库状态。

3.3. 可重用变迁模式

为了避免使每个 Petri 网成为一次性工件，我们使用小型可重用变迁模式库对并发 Rust API 建模。模式是一个元组

θ = (P_θ^in, P_θ^out, g_θ, u_θ, Ω_θ),

由类型化输入位置、类型化输出位置、守卫、令牌更新规则和附加到步骤的观察类组成。实例化模式只需要绑定符号位置名称和资源标识符。

四种模式在 tokio::sync API 中尤其常见：

• θ_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(RecvOk)

θ_reserve 和 θ_consume 的守卫另外要求 n>0。近合法变异然后通过违反这些守卫或令牌条件中的一个自然产生，例如在通道关闭或容量耗尽时尝试 θ_reserve。

这些模式跨目标 API 家族转移。在 mpsc 中，θ_reserve 建模许可证获取；在 Semaphore 中，相同模式建模容量令牌上的获取；在 watch 中，θ_consume 变为观察未见更新；在 broadcast 中，它变为滞后敏感接收，具有更丰富的结果类映射。关键是方法论：Petri 模型不是为每个调用序列从头手写，而是从并发 Rust 库中反复出现的资源转换习语组装而成。

3.4. 场景语义

抽象场景是一个元组

S = (E, ≺, #, η, β, Φ),

其中 E 是有限事件集，≺ ⊆ E×E 是严格偏序，# ⊆ E×E 是对称冲突关系，η: E → T 将事件映射到 Petri 网变迁，β 将符号资源和有效负载绑定到事件参数，Φ 包含预期结果谓词和全局不变量。

S 的线性化是尊重 ≺ 的 E 上的任何双射序列。我们写

Lin(S) = {π | π 是 (E,≺) 的线性化}.

网 N_A 下场景的可执行语义为

Exec(S, N_A) = {π ∈ Lin(S) | M0 →^(η(π)) M 对于某个 M},

其中 η(π) 将 η 逐点从事件提升到变迁序列。场景是合法的 iff Exec(S, N_A) ≠ ∅。等价地，至少有一个线性化 e1,...,en 满足 M0 →^(η(e1))...→^(η(en)) Mn。

为了形式化边界变异，令 Δ_F(M,t) = {p∈P | I_t(p) ⊈ M(p)}，并假设 t 的守卫写为 g_t = q1 ∧ ... ∧ qr。令 Δ_G(M,t) = {q_j | q_j(M)=false, 1≤j≤r}，以便缺失令牌和违反原子守卫分别计数。禁用变迁 t 在 M 处是近合法的 if |Δ_F(M,t)| + |Δ_G(M,t)| = 1。此定义捕获了我们想要的特定类型的语义边界情况：几乎启用的追踪，但恰好违反了一个前提条件。

冲突关系 # 记录应该对抗性调度的事件对，因为它们竞争令牌类、触及相同的线性资源或对应于用户声明的竞争对。偏序 ≺ 仅记录必要的因果性，而不是完全提交的线程调度。

对于并发场景，Φ 是集合值而非调度单例。如果不可比事件可以竞争，事件 e 的允许结果类可能是

Φ_e = ⋃_{π∈Exec(S,N_A)} Φ_e^π,

其中 Φ_e^π 是线性化 π 下 e 的建模观察类。这允许预言机接受多个竞争允许的结果，同时仍然拒绝任何合法线性化不允许的类。

4. 场景合成

4.1. 三个场景家族

SyncPetri 从同一个 Petri 网模型合成三类场景。这些类可以独立使用或组合：在第 2.2 节中，偏序合法核心后面跟着近合法边界探测。

这些是完全启用的追踪，被选择以达到语义上不常见的标记，而不仅仅是长追踪。我们分配启发式分数

Depth(π) = α U(Mk) + β C(π) + γ X(π),

其中 π 是结束于标记 Mk 的合法追踪，U(Mk) 是标记新颖性项，C(π) 测量结构覆盖（例如，不同的变迁或位置类），X(π) 测量由追踪引起的冲突暴露。

这些由合法前缀后跟一个近合法事件组成。它们针对边界检查、过时资源处理和错误传播，而不会退化为无意义的无效序列。这些开始为合法事件集，但独立步骤保持无序。因此输出是因果关系的 DAG 加上冲突关系，而不是单个线性调度。

4.2. 生成算法

算法 1 Petri 网场景合成

1. 输入：网 N_A，家族 f，长度界限 L
2. 输出：抽象场景 S
3. M ← M0, E ← [], ≺ ← ∅, # ← ∅
4. for i=1 to L do
5. C_en ← {t ∈ T | enabled(M,t)}
6. C_near ← {t ∈ T | |Δ_F(M,t)| + |Δ_G(M,t)| = 1}
7. if f = NearLegal 且 i 是变异点 then
8. 从 C_near 选择 t*
9. 追加边界事件 e_i 且 η(e_i)=t*
10. break
11. else
12. 从 C_en 选择最大化 Depth 的 t*
13. 追加合法事件 e_i 且 η(e_i)=t*
14. 添加由令牌生产和消费引起的因果边
15. 添加由共享资源引起的冲突边
16. 触发 t* 并更新 M
17. end if
18. end for
19. if f = PartialOrder then
20. 移除不必要的顺序边同时保持因果性
21. end if
22. return S = (E, ≺, #, η, β, Φ)

算法 1 故意以模型为中心。下一个事件的选择由可达性和冲突结构驱动，而不是由代码生成便利性驱动。

在实践中，近合法变异不是均匀插入的。在合法前缀到达标记 M 后，我们通过以下方式对候选边界事件评分：

MutScore(M,t) = w1 * 1[|Δ_F(M,t)|+|Δ_G(M,t)|=1] + w2 * Stale(M,t) + w3 * ConflictCtx(M,t),

其中 Stale 奖励重用最近无效资源的操作，ConflictCtx 奖励放置在高冲突前线附近的变异。这将预算集中在并发库通常处理不当的那类边界错误上。

5. LLM 具体化

5.1. 提示契约

LLM 接收从场景元组和 API 适配器模式组装的类型化提示：

P(S, A_d) = (Hdr, Res, Ev, Ord, Conf, Obs, Out, Ban).

字段编码资源声明、类型化事件、顺序边、并发提示、预期观察类和禁止行为（如虚构的语义事件或弱化的断言）。代表性提示片段见清单 2。

清单 2：具体化的约束提示片段。

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

LLM 输出表示为 Y=(c, μ, a)，其中 c 是 Rust 测试代码，μ 将场景事件映射到发出的运行时标记，a 是一组生成的断言。

我们仅在以下情况下接受生成的工件执行：

WellFormed(Y,S) ⇔ Compiles(c) ∧ ∀e∈E, μ(e)↓ ∧ NoInventedEvents(Y,E).

这是静态准入过滤器；结构预言机稍后检查运行时追踪是否实际上尊重预期的偏序。

对于评估，我们还使用部分结构保真度分数。令 h* 为从场景事件到发出标记的最大基数保序部分匹配。我们定义

Fid(S,τ) = |dom(h*)| / |E|.

这允许工具测量即使在完整结构预言机失败时，预期结构的多少部分在具体化中幸存。关键规则是 LLM 可以选择语法、助手名称和本地脚手架，但它不能虚构新语义事件、放宽顺序约束或重新定义预期结果类。

5.2. 具体化与修复循环

我们要求生成的测试编译并暴露运行时预言机所需的标记结构。算法 2 给出了循环。此循环故意严格，因为成功的编译本身不足以证明场景已正确具体化。

算法 2 带结构修复的具体化

1. 输入：场景 S，适配器模式 A_d，LLM L，重试界限 R
2. 输出：保真测试工件或失败
3. for r=1 to R do
4. 构建提示 P(S, A_d)
5. Y ← L(P)
6. if Y.c 编译失败 then
7. 将编译器诊断反馈给 L
8. continue
9. end if
10. if 标记覆盖不完整 then
11. 将结构诊断反馈给 L
12. continue
13. end if
14. return Y
15. end for
16. return Fail

6. Petri 指导的调度探索

场景元组已经告诉我们哪些事件受到因果约束，哪些对处于语义冲突中。我们使用该信息来塑造调度探索，而不是将所有 harness 变体视为同等重要。

对于前缀 ρ ⊆ E，定义就绪前线为

frontier_S(ρ) = {e ∈ E\ρ | ∀e'≺e, e'∈ρ}.

对于任何就绪事件 e，我们定义冲突优先优先级

prio_ρ(e) = α * Σ_{e'∈frontier_S(ρ)\{e}} 1[(e,e')∈#] + β * Rare(e) - γ * Seen(ρ,e),

其中 Rare(e) 奖励不常见的变迁类，Seen 惩罚已探索的前缀。

偏序场景还引出任务骨架

K_S = (V_task, E_spawn, E_conf),

其中 V_task 按任务所有权划分事件，E_spawn 记录 spawn-parent 关系，E_conf = {(e_i,e_j) | e_i∥e_j ∧ (e_i,e_j)∈#} 收集不可比的冲突对。具体 harness 变体选择任务创建顺序、屏障放置和在 E_conf 中选定对周围的显式屈服点。

我们不需要修改 Loom 内部来使用此信号。相反，我们生成一小套调度整形 harness 变体，优先考虑不同的高冲突前线选择，然后在存在 Loom 兼容 harness 时在 Loom 下运行每个变体。对于无法直接集成 Loom 的 API，可以在确定性调度器包装器下执行相同的调度整形变体。因此改进是在 Loom 之上而不是之内：Petri 网选择哪些并发骨架值得调度预算。

算法 3 Petri 指导的调度整形

1. 输入：偏序场景 S，变体预算 K
2. 输出：harness 变体 H
3. H ← ∅
4. for j=1 to K do
5. ρ ← ∅, h_j ← []
6. while ρ ≠ E do
7. F ← frontier_S(ρ)
8. 选择最大化 prio_ρ(e) 的 e* ∈ F
9. 将 e* 追加到 h_j
10. 在冲突的不可比对周围插入屈服/屏障钩子
11. ρ ← ρ ∪ {e*}
12. end while
13. 将 h_j 添加到 H
14. end for
15. return H

令 YieldPts(h) 表示 harness 变体 h 显式暴露的具有屏障或屈服的冲突对，令 C_{j-1} 为先前变体已覆盖的集合。然后我们可以通过未覆盖冲突增益对候选变体排名：

h_j = arg max_{h∈H(S)} Σ_{(e,e')∈YieldPts(h)\C_{j-1}} w(e,e').

这提供了优于朴素调度枚举的具体方法论改进：Loom 仍然在每个 harness 内探索调度，但 Petri 层首先通过最大化语义上有意义的冲突覆盖来决定哪些 harness 值得调度预算。

7. 多层语义预言机

执行 harness 记录追踪

τ = ((m1,o1), (m2,o2), ..., (mk,ok)),

其中每个 m_i 是发出的标记，每个 o_i 是对应的局部观察或返回类。

我们将预言机定义为四层的合取：

O(S,τ) = O_str ∧ O_out ∧ O_inv ∧ O_live.

结构预言机。 O_str(S,τ)=1 iff 存在单射匹配 h: E → {1,...,k} 使得：(1) 位置 h(e) 的标记对应事件 e；(2) 如果 e_i ≺ e_j，则 h(e_i) < h(e_j)。如果 O_str=0，测试被视为具体化失败而不是 API bug。

结果预言机。 每个事件 e 可能携带允许的观察类集 Φ_e。则 O_out(S,τ)=1 iff 对于每个匹配事件 e，h(e) 处的观察类属于 Φ_e。这允许预言机表达一组允许的并发结果，而不是脆弱的单值期望。

不变量预言机。 令 Ψ 为全局场景不变量集。则 O_inv(S,τ)=1 iff Ψ 中的每个不变量在观察到的执行摘要上都成立。典型示例包括资源守恒、无幽灵消息、有界缓冲计数或单调关闭状态。

活跃性预言机。 O_live(S,τ)=1 iff 运行在有界时间内终止且没有预期完成的任务永久阻塞。这很重要，因为许多并发故障表现为挂起而不是错误的返回值。

令 O_sem = O_out ∧ O_inv ∧ O_live。我们分类结果为：

• ConcretizationError：如果 O_str=0
• SemanticFailure：如果 O_str=1 ∧ O_sem=0
• Pass：否则

此决策规则在操作上很重要：只有第二种情况成为 bug 候选。

表 3 总结了每层的作用。

表 3. 语义预言机层。

这种分离很重要。它防止系统将糟糕的生成测试与糟糕的库行为混淆。

健全性直觉。

假设 (1) 适配器 A_d 是局部保真的，(2) 标记 μ(e) 在 e 的具体步骤之前立即发出，(3) 助手代码不发出生成的建模标记。如果 O_str(S,τ)=1，则 τ 包含与某个 π∈Exec(S,N_A) 相同顺序的匹配子序列。换句话说，运行时追踪细化了预期场景的建模线性化，直到未建模的助手步骤。在此假设下，语义预言机失败指向具体化场景下的 API 行为，而不是缺失事件或重新排序的脚手架。

失败报告。

当运行失败时，系统报告

Report = (S, Class, L_f, τ*, h_j),

其中 L_f ⊆ {out,inv,live} 是失败的预言机层集，τ* 是匹配的事件子序列，h_j 是暴露行为的 harness 变体。此报告结构在实践中很重要，因为它支持分类、去重和提示修复，而不会将所有失败合并到单个不加区分的 bug 桶中。

8. 评估与结果

本节报告了对所审查的 MPSC 运行示例的初步评估。目标不是大型基准测试，而是论文级别的检查，即当前原型可以携带一个手动建模的 CPN 和一个审查过的 ScenarioBlueprint 一直到可执行的 Tokio 代码，并且生成的运行时追踪与模型衍生的预言机一致。

8.1. 对象与设置

评估的对象是有界容量为一的 Tokio MPSC 通道。审查的场景包含七个事件和恰好两个合法线性化：

e3_before_e4: e1 e2 e3 e4 e5 e6 e7
e4_before_e3: e1 e2 e4 e3 e5 e6 e7

修复后的生成源代码编译通过，在一个 Tokio 测试中执行两个合法调度，每次运行发出 14 条 JSONL 记录。我们用通用 artifact 驱动评估器评估同一源代码三次；所有三次运行都通过，评估器没有报告任何问题。

表 4. 当前 MPSC 原型证据。

8.2. RQ1：artifact 约束提示能否产生可执行的 Tokio 代码？

生成的测试在记录的工具链下编译通过，并在通用评估器下运行完成。这是管道的第一个要求：提示和生成契约足够强大，可以产生真正的 Tokio 测试，而不是草图或伪代码片段。

同一源代码还携带了评估器消耗的场景标签、预期观察和运行时证据点。对于这个 MPSC 示例，这些要素足以获得三次成功执行，而无需在评估 crate 中使用任何 MPSC 特定检查器。

8.3. RQ2：生成的运行器是否保留调度敏感结构？

场景通过 e3 和 e4 的相对顺序区分两个合法线性化，运行器在运行时追踪中保留了这种区别。每次执行发出相同的 14 条记录，在两个调度之间平均分配，评估器确认观察到的记录顺序与 artifact 预言机匹配。

这很重要，因为该示例不仅仅是"某些通过的测试"。它是一个小型调度家族，其合法顺序在最终追踪中仍然可见。这是原型旨在保留的具体结构属性。

8.4. RQ3：反馈修复能否在不改变场景的情况下从具体不匹配中恢复？

这里使用的修复源代码是有界运行时反馈修复的结果。修复将发出的操作标签调整为精确的 Scenario 字符串，同时保持相同的调度、相同的可观察行为和相同的记录计数。换句话说，修复修复了契约不匹配，而不是将测试重写为不同的测试。

这是当前原型的相关修复形式：生成的代码可能会更改其表面语法和证据管道，但不应静默更改建模场景或削弱预言机。

8.5. RQ4：artifact 边界是否足够严格以将通用管道与主题特定模型隔离？

通用 LLM 和评估器层消耗便携 artifact，而不是手写的 MPSC 逻辑。主题特定语义存在于家族 crate 中：审查的 CPN、审查的场景和运行时观察契约。然后通用管道编译生成的源代码，执行它，并根据 artifact 衍生的预言机检查发出的 JSONL 记录。

限制是范围。这仍然是对一个运行示例的初步评估，而不是大规模变异研究或调度预算基准测试。结果支持可行性，而不是统计优越性。

8.6. 有效性威胁

主要威胁是规模。当前评估涵盖一个审查的 MPSC 主题和一个修复的生成运行器。它尚未包括变异体语料库、纯提示基线或调度探索比较。即便如此，可用证据足以支持 arXiv 提交，声称工作原型和验证的 artifact 边界，而不是完成的基准测试。

9. 相关工作

使用 Petri 网的基于模型的测试。

Petri 网长期以来一直用于形式化建模、可达性推理和有状态系统中的测试推导 (Murata, 1989; Manral, 2015)。这条工作确立了为什么基于令牌的模型有用：它们比平面状态机更自然地表达多重性、因果性和冲突。我们的设置增加了一个缺失的具体化问题。输出不能停留在抽象追踪；它必须成为具有任务、所有权移动、时间界限和可执行断言的可编译 Rust 测试。因此 SyncPetri 使用 Petri 网作为语义中间表示，而不是整个测试引擎。

有状态 API 测试和深层状态探索。

REST-ler 表明依赖感知生成对于有状态 API 是必要的，因为 naive 请求组合很少达到有意义的深层状态 (Atlidakis et al., 2018)。StateAFL 和后来的有状态灰盒工作同样认为故障通常仅在系统进入语义上不同的状态后才会出现 (Natella, 2021; Ba et al., 2022)。我们分享了这一动机，但目标和抽象不同。那些系统专注于网络面向或协议面向的接口，而 SyncPetri 针对进程内 Rust 库 API，其困难行为取决于资源所有权、句柄失效、保留能力和调度敏感的偏序。我们的近合法场景也旨在针对模型定义的语义边界，而不是任意无效输入。

基于 LLM 的测试生成。

TitanFuzz 和 Fuzz4All 表明 LLMs 可以在手动生成器成本高昂的领域生成多样化的测试和程序 (Deng et al., 2022; Xia et al., 2023)。CoverUp 进一步表明，即使对于强大的模型，外部反馈和结构仍然很重要 (Pizzorno and Berger, 2024)。SyncPetri 采用了这一教训，但改变了指导信号。我们不依赖于开放式提示或单独覆盖，而是提供具有资源绑定、顺序约束、允许结果类和禁止语义编辑的类型化事件图，然后用结构预言机判断结果。因此贡献不仅仅是使用 LLM 进行测试，而是将 LLM 限制在代码实现，同时将语义意图保持在模型之外。

系统化并发探索。

Loom 为 Rust 并发代码提供受控调度探索 (Tokio Contributors, 2026a)。我们的工作互补而非竞争。Loom 在 harness 内探索微观交错；SyncPetri 试图通过从资源模型中提取竞争窗口和冲突对来使 harness 首先在语义上有意义。因此调度整形组件在调度器之上运行：它优先考虑哪些并发骨架值得探索预算，但不修改调度器的内部搜索算法。

定位。

在这些工作线中，缺失的组合是从资源感知并发语义到可执行 Rust 测试的模型驱动路径，而不将语义预言机委托给 LLM。SyncPetri 通过将 Petri 网场景合成、约束具体化、调度感知 harness 构建和分层运行时判断结合在一个测试工作流程中来占据该空间。

10. 结论

本文提出了 SyncPetri，一种用于并发有状态 Rust API 的基于 LLM 测试生成的 Petri 网约束架构。主要论点是模型结构应控制语义、边界变异和并发暴露，而 LLM 应仅控制可执行实现。为了支持这一论点，我们形式化了目标域，定义了场景语言，指定了具体化和修复循环，提出了 Petri 指导的调度整形，并引入了多层语义预言机。这些部分共同形成了一个主线大小的方法论：不仅仅是 Petri 网和 LLMs 可以结合的草图，而是它们应在测试生成系统中如何结合的具体设计。

署名与许可

本文译自 arXiv 论文 From Resource Flow to Executable Tests: Petri-Net-Guided LLM Test Generation for Concurrent Stateful Rust APIs（arXiv:2607.21530），原文以 CC BY 4.0 许可发布。

译者：智测团队