Aquinas Hobor ; Cristian Gherghina - Barriers in Concurrent Separation Logic: Now With Tool Support!

lmcs:800 - Logical Methods in Computer Science, April 20, 2012, Volume 8, Issue 2 -
Barriers in Concurrent Separation Logic: Now With Tool Support!Article

Authors: Aquinas Hobor ; Cristian Gherghina

    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.

    Volume: Volume 8, Issue 2
    Published on: April 20, 2012
    Imported on: September 24, 2011
    Keywords: Computer Science - Logic in Computer Science,D.1.3 , D.2.1 D.2.4, D.4.4, F.3.1, F.3.3, F.4.1, F.4.3


    Is referenced by
    Logical Reasoning for Disjoint Permissions
    • 1 ScholeXplorer


    Consultation statistics

    This page has been seen 1010 times.
    This article's PDF has been downloaded 482 times.