{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,6,9]],"date-time":"2026-06-09T08:42:57Z","timestamp":1780994577012,"version":"3.54.1"},"reference-count":33,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2016,1,4]],"date-time":"2016-01-04T00:00:00Z","timestamp":1451865600000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"name":"NSF"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2016,1,4]]},"abstract":"<jats:p>Synchronization constructs lie at the heart of any reliable concurrent program. Many such constructs are standard (e.g., locks, queues, stacks, and hash-tables). However, many concurrent applications require custom synchronization constructs with special-purpose behavior. These constructs present a significant challenge for verification. Like standard constructs, they rely on subtle racy behavior, but unlike standard constructs, they may not have well-understood abstract interfaces. As they are custom built, such constructs are also far more likely to be unreliable.<\/jats:p>\n          <jats:p>This article examines the formal specification and verification of custom synchronization constructs. Our target is a library of channels used in automated parallelization to enforce sequential behavior between program statements. Our high-level specification captures the conditions necessary for correct execution; these conditions reflect program dependencies necessary to ensure sequential behavior. We connect the high-level specification with the low-level library implementation to prove that a client\u2019s requirements are satisfied. Significantly, we can reason about program and library correctness without breaking abstraction boundaries.<\/jats:p>\n          <jats:p>To achieve this, we use a program logic called iCAP (impredicative Concurrent Abstract Predicates) based on separation logic. iCAP supports both high-level abstraction and low-level reasoning about races. We use this to show that our high-level channel specification abstracts three different, increasingly complex low-level implementations of the library. iCAP\u2019s support for higher-order reasoning lets us prove that sequential dependencies are respected, while iCAP\u2019s next-generation semantic model lets us avoid ugly problems with cyclic dependencies.<\/jats:p>","DOI":"10.1145\/2818638","type":"journal-article","created":{"date-parts":[[2016,4,11]],"date-time":"2016-04-11T13:34:08Z","timestamp":1460381648000},"page":"1-72","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":12,"title":["Verifying Custom Synchronization Constructs Using Higher-Order Separation Logic"],"prefix":"10.1145","volume":"38","author":[{"given":"Mike","family":"Dodds","sequence":"first","affiliation":[{"name":"University of York, York, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University, Indiana, USA"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew J.","family":"Parkinson","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, UK"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Kasper","family":"Svendsen","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Lars","family":"Birkedal","sequence":"additional","affiliation":[{"name":"Aarhus University, Aarhus, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2016,1,4]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","unstructured":"C. J. Bell A. Appel and D. Walker. 2009. Concurrent separation logic for pipelined parallelization. In SAS.","DOI":"10.5555\/1882094.1882104"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640096"},{"key":"e_1_2_1_3_1","doi-asserted-by":"crossref","unstructured":"L. Birkedal R. E. M\u00f8gelberg J. Schwinghammer and K. St\u00f8vring. 2012. First steps in synthetic guarded domain theory: Step-indexing in the topos of trees. Logical Methods in Computer Science 8 4 (2012).","DOI":"10.2168\/LMCS-8(4:1)2012"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","unstructured":"R. L. Bocchino Jr. V. S. Adve D. Dig S. V. Adve S. Heumann R. Komuravelli J. Overbey P. Simmons H. Sung and M. Vakilian. 2009. A type and effect system for deterministic parallel Java. In OOPSLA. 10.1145\/1640089.1640097","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","unstructured":"R. Bornat C. Calcagno P. O\u2019Hearn and M. Parkinson. 2005. Permission accounting in separation logic. In POPL. 10.1145\/1040305.1040327","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_1_6_1","unstructured":"M. Botin\u010dan M. Dodds and S. Jagannathan. 2013. Resource-sensitive synchronization inference by abduction. TOPLAS 32 2 (2013)."},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","unstructured":"P. da Rocha Pinto T. Dinsdale-Young M. Dodds P. Gardner and M. Wheelhouse. 2011. A simple abstraction for complex concurrent indexes. In OOPSLA. 10.1145\/2048066.2048131","DOI":"10.1145\/2048066.2048131"},{"key":"e_1_2_1_8_1","doi-asserted-by":"crossref","unstructured":"P. da Rocha Pinto T. Dinsdale-Young and P. Gardner. 2014. TaDA: A logic for time and data abstraction. In ECOOP.","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","unstructured":"T. Dinsdale-Young M. Dodds P. Gardner M. J. Parkinson and V. Vafeiadis. 2010. Concurrent abstract predicates. In ECOOP.","DOI":"10.5555\/1883978.1884012"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"M. Dodds X. Feng M. J. Parkinson and V. Vafeiadis. 2009. Deny-guarantee reasoning. In ESOP. 10.1007\/978-3-642-00590-9_26","DOI":"10.1007\/978-3-642-00590-9_26"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","unstructured":"M. Dodds S. Jagannathan and M. J. Parkinson. 2011. Modular reasoning for deterministic parallelism. In POPL. 10.1145\/1926385.1926416","DOI":"10.1145\/1926385.1926416"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","unstructured":"X. Feng R. Ferreira and Z. Shao. 2007. On the relationship between concurrent separation logic and assume-guarantee reasoning. In ESOP.","DOI":"10.5555\/1762174.1762193"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"A. Gotsman J. Berdine B. Cook N. Rinetzky and M. Sagiv. 2007. Local reasoning for storable locks and threads. In APLAS.","DOI":"10.5555\/1784774.1784779"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","unstructured":"C. Haack M. Huisman and C. Hurlin. 2008. Reasoning about Java\u2019s reentrant locks. In APLAS. 10.1007\/978-3-540-89330-1_13","DOI":"10.1007\/978-3-540-89330-1_13"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.050"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","unstructured":"A. Hobor A. W. Appel and F. Z. Nardelli. 2008. Oracle semantics for concurrent separation logic. In ESOP.","DOI":"10.5555\/1792878.1792914"},{"key":"e_1_2_1_17_1","unstructured":"B. Jacobs and F. Piessens. 2009. Modular Full Functional Specification and Verification of Lock-Free Data Structures. Technical Report CW 551. Katholieke Universiteit Leuven Dept. of Computer Science."},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/69575.69577"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","unstructured":"N. R. Krishnaswami L. Birkedal and J. Aldrich. 2010. Verifying event-driven programs using ramified frame properties. In TLDI. 10.1145\/1708016.1708025","DOI":"10.1145\/1708016.1708025"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","unstructured":"K. R. M. Leino P. M\u00fcller and J. Smans. 2010. Deadlock-free channels and locks. In ESOP. 10.1007\/978-3-642-11957-6_22","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"e_1_2_1_21_1","doi-asserted-by":"crossref","unstructured":"A. Nanevski R. Ley-Wild I. Sergey and G. A. Delbianco. 2014. Communicating state transition systems for fine-grained concurrent resources. In ESOP.","DOI":"10.1007\/978-3-642-54833-8_16"},{"key":"e_1_2_1_22_1","doi-asserted-by":"publisher","unstructured":"A. Navabi X. Zhang and S. Jagannathan. 2008. Quasi-static scheduling for safe futures. In PPoPP. 10.1145\/1345206.1345212","DOI":"10.1145\/1345206.1345212"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","unstructured":"M. J. Parkinson and G. M. Bierman. 2005. Separation logic and abstraction. In POPL. 10.1145\/1040305.1040326","DOI":"10.1145\/1040305.1040326"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","unstructured":"M. C. Rinard and M. S. Lam. 1992. Semantic foundations of Jade. In POPL. 10.1145\/143165.143189","DOI":"10.1145\/143165.143189"},{"key":"e_1_2_1_26_1","doi-asserted-by":"crossref","unstructured":"K. Svendsen and L. Birkedal. 2014a. Impredicative concurrent abstract predicates. In ESOP.","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_27_1","doi-asserted-by":"crossref","unstructured":"K. Svendsen and L. Birkedal. 2014b. Impredicative Concurrent Abstract Predicates. Technical Report. Aarhus University. Retrieved from https:\/\/bitbucket.org\/logsem\/public\/src\/master\/icap\/esop2014-tr.pdf.","DOI":"10.1007\/978-3-642-54833-8_9"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-39038-8_14"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","unstructured":"A. Turon D. Dreyer and L. Birkedal. 2013. Unifying refinement and hoare-style reasoning in a logic for higher-order concurrency. In ICFP. 10.1145\/2500365.2500600","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","unstructured":"V. Vafeiadis and M. J. Parkinson. 2007. A marriage of rely\/guarantee and separation logic. In CONCUR.","DOI":"10.5555\/2392200.2392220"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","unstructured":"J. Villard \u00c9. Lozes and C. Calcagno. 2010. Tracking heaps that hop with heap-hop. In TACAS. 10.1007\/978-3-642-12002-2_23","DOI":"10.1007\/978-3-642-12002-2_23"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","unstructured":"A. Welc S. Jagannathan and A. Hosking. 2005. Safe futures for Java. In OOPSLA. 10.1145\/1094811.1094845","DOI":"10.1145\/1094811.1094845"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","unstructured":"J. Wickerson M. Dodds and M. Parkinson. 2010. Explicit stabilisation for modular rely-guarantee reasoning. In ESOP. 10.1007\/978-3-642-11957-6_32","DOI":"10.1007\/978-3-642-11957-6_32"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2818638","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2818638","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T05:42:49Z","timestamp":1750225369000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2818638"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2016,1,4]]},"references-count":33,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2016,1,4]]}},"alternative-id":["10.1145\/2818638"],"URL":"https:\/\/doi.org\/10.1145\/2818638","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"value":"0164-0925","type":"print"},{"value":"1558-4593","type":"electronic"}],"subject":[],"published":{"date-parts":[[2016,1,4]]},"assertion":[{"value":"2014-08-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2015-08-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2016-01-04","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}