{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,9,28]],"date-time":"2025-09-28T04:08:35Z","timestamp":1759032515489,"version":"3.41.2"},"reference-count":32,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2012,4,20]],"date-time":"2012-04-20T00:00:00Z","timestamp":1334880000000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We develop and prove sound a concurrent separation logic for Pthreads-style\nbarriers. Although Pthreads barriers are widely used in systems, and separation\nlogic is widely used for verification, there has not been any effort to combine\nthe two. Unlike locks and critical sections, Pthreads barriers enable\nsimultaneous resource redistribution between multiple threads and are\ninherently stateful, leading to significant complications in the design of the\nlogic and its soundness proof. We show how our logic can be applied to a\nspecific example program in a modular way. Our proofs are machine-checked in\nCoq. We showcase a program verification toolset that automatically applies the\nlogic rules and discharges the associated proof obligations.<\/jats:p>","DOI":"10.2168\/lmcs-8(2:2)2012","type":"journal-article","created":{"date-parts":[[2013,9,23]],"date-time":"2013-09-23T14:50:43Z","timestamp":1379947843000},"source":"Crossref","is-referenced-by-count":10,"title":["Barriers in Concurrent Separation Logic: Now With Tool Support!"],"prefix":"10.46298","volume":"Volume 8, Issue 2","author":[{"given":"Aquinas","family":"Hobor","sequence":"first","affiliation":[]},{"given":"Cristian","family":"Gherghina","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2012,4,20]]},"reference":[{"key":"10.2168\/LMCS-8(2:2)2012_MSL","unstructured":"Andrew Appel, Robert Dockins, and Aquinas Hobor. Mechanized Semantic Library. Available at http:\/\/msl.cs.princeton.edu, 2009-2010."},{"key":"10.2168\/LMCS-8(2:2)2012_appel:cpp11","unstructured":"Andrew W. Appel. VeriSmall: Verified smallfoot shape analysis. InCPP 2011: First International Conference on Certified Programs and Proofs, pages 231-246, 2011."},{"key":"10.2168\/LMCS-8(2:2)2012_appel07:tphols","doi-asserted-by":"crossref","unstructured":"Andrew W. Appel and Sandrine Blazy. Separation logic for small-step C minor. InTPHOLs, pages 5-21, 2007.","DOI":"10.1007\/978-3-540-74591-4_3"},{"key":"10.2168\/LMCS-8(2:2)2012_BellAW10","doi-asserted-by":"crossref","unstructured":"Christian J. Bell, Andrew W. Appel, and David Walker. Concurrent separation logic for pipelined parallelization. InSAS, pages 151-166, 2010.","DOI":"10.1007\/978-3-642-15769-1_10"},{"key":"10.2168\/LMCS-8(2:2)2012_bienia10:phd","unstructured":"Christian Bienia.Benchmarking Modern Multiprocessors. PhD thesis, Princeton University, Department of Computer Science, Princeton, NJ, December 2010."},{"key":"10.2168\/LMCS-8(2:2)2012_bornat05:popl","doi-asserted-by":"crossref","unstructured":"Richard Bornat, Cristiano Calcagno, Peter O'Hearn, and Matthew Parkinson. Permission accounting in separation logic. InPOPL, pages 259-270, 2005.","DOI":"10.1145\/1047659.1040327"},{"key":"10.2168\/LMCS-8(2:2)2012_bp:cpp11:aac","doi-asserted-by":"crossref","unstructured":"Thomas Braibant and Damien Pous. Tactics for reasoning modulo AC in Coq. InCPP, pages 167-182, 2011.","DOI":"10.1007\/978-3-642-25379-9_14"},{"key":"10.2168\/LMCS-8(2:2)2012_Brookes04","doi-asserted-by":"crossref","unstructured":"Stephen D. Brookes. A semantics for concurrent separation logic. InCONCUR, pages 16-34, 2004.","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"10.2168\/LMCS-8(2:2)2012_PThreadsBook","unstructured":"David R. Butenhof.Programming with POSIX Threads. Addison-Wesley, 1997."},{"key":"10.2168\/LMCS-8(2:2)2012_Calcagno:APLAS09","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno, Dino Distefano, and Vikor Vafeiadis. Bi-abductive resource invariant synthesis. InAPLAS, pages 259-274, 2009.","DOI":"10.1007\/978-3-642-10672-9_19"},{"key":"10.2168\/LMCS-8(2:2)2012_calcagno2007","doi-asserted-by":"crossref","unstructured":"Cristiano Calcagno, Peter W. O'Hearn, and Hongseok Yang. Local action and abstract separation logic. InLICS, pages 366-378, 2007.","DOI":"10.1109\/LICS.2007.30"},{"key":"10.2168\/LMCS-8(2:2)2012_Chin2010","unstructured":"Wei-Ngan Chin, Cristina David, Huu Hai Nguyen, and Shengchao Qin. Automated verification of shape, size and bag properties via user-defined predicates in separation logic.Science of Computer Programming, 2010."},{"key":"10.2168\/LMCS-8(2:2)2012_DBLP:conf\/cav\/ChinGVLCQ11","doi-asserted-by":"crossref","unstructured":"Wei-Ngan Chin, Cristian Gherghina, Razvan Voicu, Quang Loc Le, Florin Craciun, and Shengchao Qin. A specialization calculus for pruning disjunctive predicates to support verification. InCAV, pages 293-309, 2011.","DOI":"10.1007\/978-3-642-22110-1_23"},{"key":"10.2168\/LMCS-8(2:2)2012_dinsdale-young:ecoop10","doi-asserted-by":"crossref","unstructured":"Thomas Dinsdale-Young, Mike Dodds, Philippa Gardner, Matthew J. Parkinson, and Viktor Vafeiadis. Concurrent abstract predicates. InECOOP, pages 504-528, 2010.","DOI":"10.1007\/978-3-642-14107-2_24"},{"key":"10.2168\/LMCS-8(2:2)2012_dockins09:sa","doi-asserted-by":"crossref","unstructured":"Robert Dockins, Aquinas Hobor, and Andrew W. Appel. A fresh look at separation algebras and share accounting. InAPLAS, pages 161-177, 2009.","DOI":"10.1007\/978-3-642-10672-9_13"},{"key":"10.2168\/LMCS-8(2:2)2012_dodds:esop09","doi-asserted-by":"crossref","unstructured":"Mike Dodds, Xinyu Feng, Matthew J. Parkinson, and Viktor Vafeiadis. Deny-guarantee reasoning. InESOP, pages 363-377, 2009.","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"10.2168\/LMCS-8(2:2)2012_FM11:Gherghina","doi-asserted-by":"crossref","unstructured":"Cristian Gherghina, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Structured specifications for better verification of heap-manipulating programs. InFM, pages 386-401, 2011.","DOI":"10.1007\/978-3-642-21437-0_29"},{"key":"10.2168\/LMCS-8(2:2)2012_gonthier:icfp11","doi-asserted-by":"crossref","unstructured":"Georges Gonthier, Beta Ziliani, Aleksandar Nanevski, and Derek Dreyer. How to make ad hoc proof automation less ad hoc. InICFP, pages 163-175, 2011.","DOI":"10.1145\/2034574.2034798"},{"key":"10.2168\/LMCS-8(2:2)2012_Gotsman:SAS06","doi-asserted-by":"crossref","unstructured":"Alexey Gotsman, Josh Berdine, and Byron Cook. Interprocedural Shape Analysis with Separated Heap Abstractions. InSAS, pages 240-260, 2006.","DOI":"10.1007\/11823230_16"},{"key":"10.2168\/LMCS-8(2:2)2012_GotsmanBCRS07","doi-asserted-by":"crossref","unstructured":"Alexey Gotsman, Josh Berdine, Byron Cook, Noam Rinetzky, and Mooly Sagiv. Local reasoning for storable locks and threads. InAPLAS, pages 19-37, 2007.","DOI":"10.1007\/978-3-540-76637-7_3"},{"key":"10.2168\/LMCS-8(2:2)2012_Hobor:Thesis","unstructured":"Aquinas Hobor. Oracle semantics. Technical Report TR-836-08, Princeton, 2008."},{"key":"10.2168\/LMCS-8(2:2)2012_HoborAN08","doi-asserted-by":"crossref","unstructured":"Aquinas Hobor, Andrew W. Appel, and Francesco Zappa Nardelli. Oracle semantics for concurrent separation logic. InESOP, pages 353-367, 2008.","DOI":"10.1007\/978-3-540-78739-6_27"},{"key":"10.2168\/LMCS-8(2:2)2012_hobor10:popl","doi-asserted-by":"crossref","unstructured":"Aquinas Hobor, Robert Dockins, and Andrew W. Appel. A theory of indirection via approximation. InPOPL, pages 171-185, 2010.","DOI":"10.1145\/1707801.1706322"},{"key":"10.2168\/LMCS-8(2:2)2012_hobor11:esop","doi-asserted-by":"crossref","unstructured":"Aquinas Hobor and Cristian Gherghina. Barriers in concurrent separation logic. InESOP, pages 276-296, 2011.","DOI":"10.1007\/978-3-642-19718-5_15"},{"key":"10.2168\/LMCS-8(2:2)2012_jacobs:popl11","doi-asserted-by":"crossref","unstructured":"Bart Jacobs and Frank Piessens. Expressive modular fine-grained concurrency specification. InPOPL, pages 271-282, 2011.","DOI":"10.1145\/1925844.1926417"},{"key":"10.2168\/LMCS-8(2:2)2012_nanevski:popl10","doi-asserted-by":"crossref","unstructured":"Aleksandar Nanevski, Viktor Vafeiadis, and Josh Berdine. Structuring the verification of heap-manipulating programs. InPOPL, pages 261-274, 2010.","DOI":"10.1145\/1707801.1706331"},{"key":"10.2168\/LMCS-8(2:2)2012_ChinCav08","doi-asserted-by":"crossref","unstructured":"Huu Hai Nguyen and Wei-Ngan Chin. Enhancing program verification with lemmas. InCAV, pages 355-369, 2008.","DOI":"10.1007\/978-3-540-70545-1_34"},{"key":"10.2168\/LMCS-8(2:2)2012_nguyenVMCAI","doi-asserted-by":"crossref","unstructured":"Huu Hai Nguyen, Cristina David, Shengchao Qin, and Wei-Ngan Chin. Automated verification of shape and size properties via separation logic. InVMCAI, pages 251-266, 2007.","DOI":"10.1007\/978-3-540-69738-1_18"},{"key":"10.2168\/LMCS-8(2:2)2012_OHearn05resconc","doi-asserted-by":"crossref","unstructured":"Peter W. O'Hearn. Resources, concurrency and local reasoning.Theoretical Computer Science, 375(1):271-307, May 2007.","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"10.2168\/LMCS-8(2:2)2012_vafeiadis:concur07","doi-asserted-by":"crossref","unstructured":"Viktor Vafeiadis and Matthew J. Parkinson. A marriage of rely\/guarantee and separation logic. InCONCUR, pages 256-271, 2007.","DOI":"10.1007\/978-3-540-74407-8_18"},{"key":"10.2168\/LMCS-8(2:2)2012_villard:aplas09","doi-asserted-by":"crossref","unstructured":"Jules Villard, \u00c9tienne Lozes, and Cristiano Calcagno. Proving copyless message passing. InAPLAS, pages 194-209, 2009.","DOI":"10.1007\/978-3-642-10672-9_15"},{"key":"10.2168\/LMCS-8(2:2)2012_villard:tacas10","doi-asserted-by":"crossref","unstructured":"Jules Villard, \u00c9tienne Lozes, and Cristiano Calcagno. Tracking heaps that hop with heap-hop. InTACAS, pages 275-279, 2010.","DOI":"10.1007\/978-3-642-12002-2_23"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/800\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/800\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T19:56:21Z","timestamp":1681242981000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/800"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012,4,20]]},"references-count":32,"URL":"https:\/\/doi.org\/10.2168\/lmcs-8(2:2)2012","relation":{"is-same-as":[{"id-type":"arxiv","id":"1203.6412","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1203.6412","asserted-by":"subject"}],"is-referenced-by":[{"id-type":"doi","id":"10.1007\/978-3-319-89884-1_14","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2012,4,20]]},"article-number":"800"}}