一种带有工作和跨度信用的并行时间复杂度分离逻辑
A Separation Logic for Parallel Time Complexity with Work and Span Credits
浏览论文内容
中文总结 AI 辅助
该研究提出Parcas并发分离逻辑验证fork-join程序并行时间复杂度，用工作和跨度信用衡量，工作信用可累加分割，跨度信用有独特处理规则，能给出并行原语规范，通过案例研究验证，结果在Rocq证明器中机械化验证。
中文摘要 AI 辅助
我们提出了Parcas，一种用于验证fork-join程序并行时间复杂度的并发分离逻辑。为了抽象出机器的具体细节，并行程序的时间复杂度由两个指标给出：工作，衡量操作总数；跨度，衡量最长的顺序依赖链。这两个指标共同决定了在任意数量处理器上的运行时间。为了证明工作和跨度的界限，Parcas配备了工作信用和跨度信用，它们是表示产生成本权限的逻辑设备。工作信用是时间信用的直接改编，可在并行任务之间累加分割。然而，跨度信用需要根本不同的处理。两个任务并行组合的跨度是两个任务跨度的最大值。为此，我们提出了一个在分叉点复制跨度信用的规则，每个副本都带有一个逻辑任务标识符，限制哪个任务可以使用它们。一个转移规则允许未使用的跨度信用跨顺序组合转发给后续任务。该逻辑足以给出常见并行原语（如并行for循环和制表函数）的模块化、高阶规范。我们在几个案例研究中展示了Parcas，包括并行前缀和、并行归并排序以及混合并发与并行的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.
