Sciweavers

ESOP
2011
Springer

Barriers in Concurrent Separation Logic

13 years 2 months ago
Barriers in Concurrent Separation Logic
We develop and prove sound a concurrent separation logic for a language with 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 the traditional synchronization primitives used in concurrent separation logic (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 and also how it covers the common barrier use cases. Our proofs are machine-checked in Coq.
Aquinas Hobor, Cristian Gherghina
Added 27 Aug 2011
Updated 27 Aug 2011
Type Journal
Year 2011
Where ESOP
Authors Aquinas Hobor, Cristian Gherghina
Comments (0)