Search papers, labs, and topics across Lattice.
This paper introduces Parcas, a concurrent separation logic designed for verifying the parallel time complexity of fork-join programs by utilizing work and span credits as metrics for performance measurement. By innovatively handling span credits through duplication at fork points and logical task identifiers, the authors provide a robust framework for modular specifications of parallel constructs. The effectiveness of Parcas is validated through case studies, including parallel prefix sums and merge sort, all mechanized in the Rocq prover, showcasing its practical applicability in verifying complex parallel algorithms.
Parcas reveals that effective management of span credits can significantly enhance the verification of parallel program performance, challenging traditional approaches to time complexity.
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.
