Please use this identifier to cite or link to this item:
Title: Barriers in concurrent separation logic: Now with tool support!
Authors: Hobor, A. 
Gherghina, C.
Keywords: Concurrency
Concurrent Separation Logic
Verification Tools
Issue Date: 2012
Citation: Hobor, A., Gherghina, C. (2012). Barriers in concurrent separation logic: Now with tool support!. Logical Methods in Computer Science 8 (2) : 2-. ScholarBank@NUS Repository.
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. © Aquinas Hobor and Cristian Gherghina.
Source Title: Logical Methods in Computer Science
ISSN: 18605974
DOI: 10.2168/LMCS-8(2:02)2012
Appears in Collections:Staff Publications

Show full item record
Files in This Item:
There are no files associated with this item.


checked on Sep 29, 2022


checked on Sep 29, 2022

Page view(s)

checked on Sep 22, 2022

Google ScholarTM



Items in DSpace are protected by copyright, with all rights reserved, unless otherwise indicated.