Please use this identifier to cite or link to this item: https://doi.org/10.1007/978-3-642-19718-5_15
Title: Barriers in concurrent separation logic
Authors: Hobor, A. 
Gherghina, C.
Issue Date: 2011
Source: Hobor, A.,Gherghina, C. (2011). Barriers in concurrent separation logic. Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics) 6602 LNCS : 276-296. ScholarBank@NUS Repository. https://doi.org/10.1007/978-3-642-19718-5_15
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. © 2011 Springer-Verlag.
Source Title: Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
URI: http://scholarbank.nus.edu.sg/handle/10635/40436
ISBN: 9783642197178
ISSN: 03029743
DOI: 10.1007/978-3-642-19718-5_15
Appears in Collections:Staff Publications

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

SCOPUSTM   
Citations

17
checked on Dec 13, 2017

Page view(s)

49
checked on Dec 9, 2017

Google ScholarTM

Check

Altmetric


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