Barriers in Concurrent Separation Logic

DOI10.1007/978-3-642-19718-5_15zbMATH Open1326.68096arXiv1203.6412OpenAlexW2153880165MaRDI QIDQ3000585FDOQ3000585

Authors: Aquinas Hobor, Cristian Gherghina 

Publication date: 19 May 2011

Published in: Programming Languages and Systems (Search for Journal in Brave)

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.

Full work available at URL: https://arxiv.org/abs/1203.6412

Recommendations

• Barriers in concurrent separation logic: now with tool support!
• Revisiting concurrent separation logic
• Separation logic and concurrency
• A semantics for concurrent separation logic
• CONCUR 2004 - Concurrency Theory
• Concurrent separation logic and operational semantics
• A separation logic for refining concurrent objects
• The essence of higher-order concurrent separation logic
• Fine-grained concurrency with separation logic
• Independence and concurrent separation logic

Mathematics Subject Classification ID

Mathematical aspects of software engineering (specification, verification, metrics, requirements, etc.) (68N30) Logic in computer science (03B70)

Cites Work

• Separation Logic for Small-Step cminor
• Local Reasoning for Storable Locks and Threads
• Permission accounting in separation logic
• CONCUR 2004 - Concurrency Theory
• Resources, concurrency, and local reasoning
• Interprocedural Shape Analysis with Separated Heap Abstractions
• Expressive modular fine-grained concurrency specification
• Oracle Semantics for Concurrent Separation Logic
• A theory of indirection via approximation
• Concurrent separation logic for pipelined parallelization

Cited In (7)

• Barriers in concurrent separation logic: now with tool support!
• Ghost signals: verifying termination of busy waiting
• Inhibited Effects in CP-Logic
• On automation in the verification of software barriers: experience report
• Inter-process buffers in separation logic with rely-guarantee
• Expressing the behavior of three very different concurrent systems by using natural extensions of separation logic
• Verification of concurrent systems with VerCors

Uses Software

• Coq
• pthreads
• Mechanized Semantic Library

This page was built for publication: Barriers in Concurrent Separation Logic

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q3000585)