一句话：提出 Parcas，用 work credit 与 span credit 在并发分离逻辑中模块化验证 fork-join 程序的并行时间上界，并在 Rocq/Iris 中机器化。
本文关注 fork-join 并行程序的时间复杂度验证。并行时间通常由 work（总操作数）与 span（最长顺序依赖链）两个指标刻画，二者共同决定任意处理器数量下的运行时间。作者提出 Parcas，一个并发分离逻辑，用于证明这两个指标的上界。其核心是两类逻辑资源：work credit 直接沿用顺序程序时间信用（time credit）的思路，可在并行任务间可加地拆分；而 span credit 由于并行组合的 span 取二者最大值，需根本不同的处理——在 fork 点复制 span credit，并为每份副本附加逻辑任务标识，限制其只能由对应任务消费，同时通过转移规则把未使用的 span credit 沿顺序组合传递给后续任务。该逻辑足以为并行 for 循环、tabulate 等常见并行原语给出模块化、高阶的规约。作者在并行前缀和、并行归并排序以及混合并发与并行的一种 Treiber 无锁栈变体等案例上验证了方法，所有结果均在 Rocq 证明助手中基于 Iris 分离逻辑框架机器化。
We present Parcas, a concurrent separation logic for verifying the parallel time complexity of fork-join programs. In order to abstract from the specifics of the machine, time complexity for parallel programs is given in terms of two metrics: the work, measuring the total number of operations, and the span, measuring the longest chain of sequential dependencies. Together, these two metrics determine the running time on any number of processors. For proving bounds on the work and span, Parcas is equipped with work credits and span credits, logical devices that represent permissions to incur costs. Work credits are a straightforward adaptation of time credits, a standard tool for bounding time complexity of sequential programs, and can be split additively between parallel tasks. Span credits, however, require a fundamentally different treatment. Indeed, the span of the parallel composition of two tasks is the maximum of the span of the two tasks. To account for this, we propose a rule for duplicating span credits at fork points, with each copy tagged by a logical task identifier that restricts which task may spend them. A transfer rule allows unused span credits to be forwarded across sequential compositions to subsequent tasks. The logic is expressive enough to give modular, higher-order specifications for common parallel primitives such as a parallel for loop and a tabulate function. We demonstrate Parcas on several case studies, including parallel prefix sums, parallel merge sort, and a variant of Treiber's lock-free stack that mixes concurrency with parallelism. All the presented results are mechanized in the Rocq prover using the Iris separation logic framework.
DOI 原文 · arXiv · PDF（开放获取） · DBLP
@article{abs-2607-11582,
title = {A Separation Logic for Parallel Time Complexity with Work and Span Credits},
author = {Alexandre Moine and Sam Westrick and Joseph Tassarotti},
journal = {Proceedings of the ACM on Programming Languages},
volume = {10},
number = {ICFP},
year = {2026},
doi = {10.1145/3828679}
}