Barriers in Concurrent Separation Logic

DOI10.1007/978-3-642-19718-5_15MaRDI QIDQ3000585zbMATH OpenOpenAlexFDO

Authors Aquinas Hobor, Cristian Gherghina

Publication date 19 May 2011

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

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

Mathematics Subject Classification ID

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

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.

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

Cites work

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

Cited in

(7)

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

Describes a project that uses

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)