A Separation Logic for Parallel Time Complexity with Work and Span Credits

Jul 16, 2026

Parcas presents a concurrent separation logic for proving parallel time complexity bounds for fork-join programs, abstracting away machine specifics through two metrics: work (total operations) and span (longest chain of dependent steps). Work is tracked with split and recombined work credits, adapting time-credits techniques for sequential programs. Span requires a different approach: span credits are duplicated at fork points with task identifiers, and unused credits can be transferred across sequential compositions. The logic supports modular specifications for parallel primitives and is mechanized in Coq using Iris, with demonstrations on prefix sums, merge sort, and a lock-free stack variant.

LanguageEnglish

CategoryResearch & Report

FormatPDF

Pages30

Reading Time1 h 16 min

Introduction

Work and span metrics for fork-join programs

Credits-based reasoning in Parcas

arXiv :2607 . 1 1582v 1 [ cs .PL] 13 Jul 2026 A Separation Logic for Parallel Time Complexity with Work and Span Credits ALEXANDRE MOINE, New York University, USA SAM WESTRICK, New York University, USA JOSEPH TASSAROTTI∗ , New York University, USA 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 ofTreiber’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. CCS Concepts: • Software and its engineering → Parallel programming languages; • Theory of computation → Separation logic; Program verification. Additional Key Words and Phrases: parallelism, separation logic, time complexity ACM Reference Format: Alexandre Moine, Sam Westrick, and Joseph Tassarotti. 2026. A Separation Logic for Parallel Time Complexity with Work and Span Credits. Proc. ACM Program. Lang. 10, ICFP, Article 281 (August 2026), 30 pages. [https:](https:)//[doi.org/10.1145/3828679](doi.org/10.1145/3828679) 1 Introduction A variety of techniques exist for formally establishing bounds on the resource consumption of programs. One approach is to introduce substructural credits or potentials into a type system [36] or program logic [3], which must be spent at each point in which a program consumes a corresponding resource. The credits thereby represent a “budget” that upper bounds the resource consumption of a program. This approach has been used to reason about a range of different kinds of resources, ∗ Also affiliated with Amazon Web Services. This paper does not reflect the views of Amazon Web Services. Authors’ Contact Information: Alexandre Moine, New York University, New York, USA, [alexandre.moine@nyu.edu](alexandre.moine@nyu.edu); Sam Westrick, New York University, New York, USA, [shw8119@nyu.edu](shw8119@nyu.edu); Joseph Tassarotti, New York University, New York, USA, [jt4767@nyu.edu](jt4767@nyu.edu). This work is licensed under a Creative Commons Attribution 4 .0 International License. © 2026 Copyright held by the owner/author(s) . ACM 2475-1421/2026/8-ART281 [https://doi.org/10.1145/3828679](https://doi.org/10.1145/3828679) Proc. ACM Program. Lang., Vol. 10, No. ICFP, Article 281 . Publication date: August 2026 . 281:2 Alexandre Moine, Sam Westrick, and Joseph Tassarotti including running time [32, 18, 50], heap memory under both manual management [36] and garbage collection [53, 43, 46], and stack space [14, 15] . This paper introduces Parcas, a concurrent separati

FAQs

What are the two metrics used to define parallel time complexity in Parcas?

Parcas uses work and span. Work counts the total operations, while span measures the longest chain of sequential dependencies.

How does Parcas handle work credits for parallel tasks?

Work credits can be split additively between parallel threads, and any unused portion can be recombined at the join point.

Why is span credits treatment different from work credits in fork-join programs?

Because the span of the fork-join composition is the maximum span among children, additively splitting and naively combining span credits would be unsound. Parcas duplicates span credits at fork points with task identifiers and restricts which task may spend them, with transfer rules for unused credits.

Jul 16, 2026

Upload by Valentina