Barriers in Concurrent Separation Logic: Now With Tool Support!

TL;DR

This paper introduces a sound concurrent separation logic tailored for Pthreads-style barriers, addressing their unique stateful resource redistribution, and provides a machine-checked proof and automated tool support for verification.

Contribution

It develops the first sound separation logic for Pthreads barriers, including a Coq proof and an automated verification toolset.

Findings

Logic is sound and applicable to real programs

Toolset automates proof obligations

Machine-checked proofs ensure correctness

Abstract

We develop and prove sound a concurrent separation logic for Pthreads-style barriers. Although Pthreads barriers are widely used in systems, and separation logic is widely used for verification, there has not been any effort to combine the two. Unlike locks and critical sections, Pthreads barriers enable simultaneous resource redistribution between multiple threads and are inherently stateful, leading to significant complications in the design of the logic and its soundness proof. We show how our logic can be applied to a specific example program in a modular way. Our proofs are machine-checked in Coq. We showcase a program verification toolset that automatically applies the logic rules and discharges the associated proof obligations.