{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T20:46:42Z","timestamp":1760042802807,"version":"3.41.0"},"reference-count":72,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2018,12,11]],"date-time":"2018-12-11T00:00:00Z","timestamp":1544486400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"DOI":"10.13039\/100000001","name":"National Science Foundation","doi-asserted-by":"publisher","award":["1302570"],"award-info":[{"award-number":["1302570"]}],"id":[{"id":"10.13039\/100000001","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/K034413\/1, EP\/K011715\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1"],"award-info":[{"award-number":["EP\/K034413\/1, EP\/K011715\/1, EP\/L00058X\/1, EP\/N027833\/1, EP\/N028201\/1"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100001871","name":"Funda\u00e7\u00e3o para a Ci\u00eancia e a Tecnologia","doi-asserted-by":"publisher","award":["UID\/CEC\/00408\/2013"],"award-info":[{"award-number":["UID\/CEC\/00408\/2013"]}],"id":[{"id":"10.13039\/501100001871","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100011199","name":"Seventh Framework Programme","doi-asserted-by":"publisher","award":["612985"],"award-info":[{"award-number":["612985"]}],"id":[{"id":"10.13039\/100011199","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["ACM Trans. Program. Lang. Syst."],"published-print":{"date-parts":[[2019,3,31]]},"abstract":"<jats:p>We present Armus, a verification tool for dynamically detecting or avoiding barrier deadlocks. The core design of Armus is based on phasers, a generalisation of barriers that supports split-phase synchronisation, dynamic membership, and optional-waits. This allows Armus to handle the key barrier synchronisation patterns found in modern languages and libraries. We implement Armus for X10 and Java, giving the first sound and complete barrier deadlock verification tools in these settings.<\/jats:p>\n          <jats:p>Armus introduces a novel event-based graph model of barrier concurrency constraints that distinguishes task-event and event-task dependencies. Decoupling these two kinds of dependencies facilitates the verification of distributed barriers with dynamic membership, a challenging feature of X10. Further, our base graph representation can be dynamically switched between a task-to-task model, Wait-for Graph (WFG), and an event-to-event model, State Graph (SG), to improve the scalability of the analysis.<\/jats:p>\n          <jats:p>Formally, we show that the verification is sound and complete with respect to the occurrence of deadlock in our core phaser language, and that switching graph representations preserves the soundness and completeness properties. These results are machine checked with the Coq proof assistant. Practically, we evaluate the runtime overhead of our implementations using three benchmark suites in local and distributed scenarios. Regarding deadlock detection, distributed scenarios show negligible overheads and local scenarios show overheads below\u00a01.15\u00d7. Deadlock avoidance is more demanding, and highlights the potential gains from dynamic graph selection. In one benchmark scenario, the runtime overheads vary from 1.8\u00d7 for dynamic selection, 2.6\u00d7 for SG-static selection, and 5.9\u00d7 for WFG-static selection.<\/jats:p>","DOI":"10.1145\/3229060","type":"journal-article","created":{"date-parts":[[2018,12,11]],"date-time":"2018-12-11T13:17:46Z","timestamp":1544534266000},"page":"1-38","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Dynamic Deadlock Verification for General Barrier Synchronisation"],"prefix":"10.1145","volume":"41","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-3209-9258","authenticated-orcid":false,"given":"Tiago","family":"Cogumbreiro","sequence":"first","affiliation":[{"name":"Rice University, USA"}]},{"given":"Raymond","family":"Hu","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]},{"given":"Francisco","family":"Martins","sequence":"additional","affiliation":[{"name":"LASIGE, Faculdade de Ci\u00eancias, Universidade de Lisboa, Portugal and University of the Azores, Portugal"}]},{"given":"Nobuko","family":"Yoshida","sequence":"additional","affiliation":[{"name":"Imperial College London, UK"}]}],"member":"320","published-online":{"date-parts":[[2018,12,11]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1229428.1229471"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/2525401.2525411"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11602569_48"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.5555\/1523254"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/12.55690"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03466-4_9"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.2014.2301725"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","unstructured":"Vincent Cav\u00e9 Jisheng Zhao Jun Shirako and Vivek Sarkar. 2011. Habanero-Java: The new adventures of old X10. In PPPJ. ACM 51--61. 10.1145\/2093157.2093165","DOI":"10.1145\/2093157.2093165"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/249069.231391"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","unstructured":"Philippe Charles Christian Grothoff Vijay Saraswat Christopher Donawa Allan Kielstra Kemal Ebcioglu Christoph von Praun and Vivek Sarkar. 2005. X10: An object-oriented approach to non-uniform cluster computing. In OOPSLA. ACM 519--538. 10.1145\/1094811.1094852","DOI":"10.1145\/1094811.1094852"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/645533.656491"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/356586.356588"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","unstructured":"Tiago Cogumbreiro Raymond Hu Francisco Martins and Nobuko Yoshida. 2015. Dynamic deadlock verification for general barrier synchronisation. In PPoPP. ACM 150--160. 10.1145\/2688500.2688519","DOI":"10.1145\/2688500.2688519"},{"key":"e_1_2_1_14_1","series-title":"Lecture Notes in Computer Science","volume-title":"COORDINATION","author":"Cogumbreiro Tiago","unstructured":"Tiago Cogumbreiro, Francisco Martins, and Vasco Thudichum Vasconcelos. 2013. Coordinating phased activities while maintaining progress. In COORDINATION, Lecture Notes in Computer Science, Vol. 7890. Springer, 31--44."},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2017.02.006"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/3143359"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0747-7171(08)80013-2"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_27"},{"key":"e_1_2_1_19_1","volume-title":"Parallel Programming in Chapel. Retrieved","author":"Deitz Steve","year":"2018","unstructured":"Steve Deitz. 2006. Parallel Programming in Chapel. Retrieved January 2018 from https:\/\/www.cct.lsu.edu\/&sim;estrabd\/LACSI2006\/Programming%20Models\/deitz.pdf. Presented at LACSI."},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/1059513.1059514"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1007\/s10515-011-0085-0"},{"key":"e_1_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/2635868.2635918"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/838237.838618"},{"key":"e_1_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.5555\/3168451.3168471"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","unstructured":"Andy Georges Dries Buytaert and Lieven Eeckhout. 2007. Statistically rigorous Java performance evaluation. In OOPSLA. ACM 57--76. 10.1145\/1297027.1297033","DOI":"10.1145\/1297027.1297033"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","unstructured":"Prodromos Gerakios Nikolaos Papaspyrou Konstantinos Sagonas and Panagiotis Vekris. 2011. Dynamic deadlock avoidance in systems code using statically inferred effects. In PLOS. ACM 1--5. 10.1145\/2039239.2039247","DOI":"10.1145\/2039239.2039247"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1109\/ICST.2012.81"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/68182.68187"},{"key":"e_1_2_1_30_1","doi-asserted-by":"publisher","DOI":"10.1145\/2488551.2488570"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1145\/2503210.2503237"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/1542275.1542319"},{"key":"e_1_2_1_33_1","doi-asserted-by":"publisher","DOI":"10.5555\/2042476.2042481"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/2388996.2389037"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/356603.356607"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1007\/b75033"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1007\/11523468_69"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1013153020460"},{"key":"e_1_2_1_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-13374-9_25"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/45075.46163"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/359545.359563"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1007\/3-540-45482-9"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1693453.1693459"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","unstructured":"Daan Leijen Wolfram Schulte and Sebastian Burckhardt. 2009. The design of a task parallel library. In OOPSLA. ACM 227--242. 10.1145\/1640089.1640106","DOI":"10.1145\/1640089.1640106"},{"key":"e_1_2_1_45_1","doi-asserted-by":"publisher","DOI":"10.1145\/1810479.1810526"},{"key":"e_1_2_1_46_1","doi-asserted-by":"publisher","unstructured":"Piotr R. Luszczek David H. Bailey Jack J. Dongarra Jeremy Kepner Robert F. Lucas Rolf Rabenseifner and Daisuke Takahashi. 2006. The HPC challenge (HPCC) benchmark suite. In SC. ACM. 10.1145\/1188455.1188677","DOI":"10.1145\/1188455.1188677"},{"key":"e_1_2_1_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/322344.322351"},{"key":"e_1_2_1_48_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(71)90006-8"},{"key":"e_1_2_1_49_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-43659-3_30"},{"key":"e_1_2_1_50_1","doi-asserted-by":"publisher","unstructured":"Armand Navabi Xiangyu Zhang and Suresh Jagannathan. 2008. Quasi-static scheduling for safe futures. In PPoPP. ACM 23--32. 10.1145\/1345206.1345212","DOI":"10.1145\/1345206.1345212"},{"key":"e_1_2_1_51_1","series-title":"Lecture Notes in Computer Science","volume-title":"Deadlocks: From exhibiting to healing","author":"Nir-Buchbinder Yarden","year":"2008","unstructured":"Yarden Nir-Buchbinder, Rachel Tzoref, and Shmuel Ur. 2008. Deadlocks: From exhibiting to healing. Lecture Notes in Computer Science, Vol. 5289. Springer, 104--118."},{"key":"e_1_2_1_52_1","doi-asserted-by":"publisher","DOI":"10.5555\/872020.872393"},{"key":"e_1_2_1_53_1","volume-title":"Dietz","author":"O\u2019Keefe Matthew T.","year":"1990","unstructured":"Matthew T. O\u2019Keefe and Henry G. Dietz. 1990. Hardware barrier synchronization: Dynamic barrier MIMD (DBM). In ICPP. Pennsylvania State University, 43--46."},{"key":"e_1_2_1_54_1","doi-asserted-by":"publisher","DOI":"10.1145\/2400682.2400712"},{"key":"e_1_2_1_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/1854273.1854288"},{"key":"e_1_2_1_56_1","doi-asserted-by":"publisher","DOI":"10.1109\/9.633824"},{"key":"e_1_2_1_57_1","volume-title":"A scalable deadlock detection algorithm for UPC collective operations","author":"Roy Indranil","year":"2013","unstructured":"Indranil Roy, Glenn R. Luecke, James Coyle, and Marina Kraeva. 2013. A scalable deadlock detection algorithm for UPC collective operations. In PGAS. University of Edinburgh, 2--15. http:\/\/www.pgas2013.org.uk\/sites\/default\/files\/pgas2013proceedings.pdf."},{"key":"e_1_2_1_58_1","doi-asserted-by":"publisher","unstructured":"Malavika Samak and Murali Krishna Ramanathan. 2014. Trace driven dynamic deadlock detection and reproduction. In PPoPP. ACM 29--42. 10.1145\/2555243.2555262","DOI":"10.1145\/2555243.2555262"},{"key":"e_1_2_1_59_1","doi-asserted-by":"publisher","DOI":"10.1007\/11539452_28"},{"key":"e_1_2_1_60_1","doi-asserted-by":"publisher","unstructured":"Rahul Sharma Michael Bauer and Alex Aiken. 2015. Verification of producer-consumer synchronization in GPU programs. In PLDI. ACM 88--98. 10.1145\/2737924.2737962","DOI":"10.1145\/2737924.2737962"},{"key":"e_1_2_1_61_1","doi-asserted-by":"publisher","DOI":"10.5555\/896944"},{"key":"e_1_2_1_62_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375527.1375568"},{"key":"e_1_2_1_63_1","doi-asserted-by":"publisher","DOI":"10.1109\/IPDPS.2009.5161071"},{"key":"e_1_2_1_64_1","volume-title":"X10 Workshop.","author":"Shirako Jun","year":"2011","unstructured":"Jun Shirako, David M. Peixotto, Drago\u015f-Dumitru Sb\u00eerlea, and Vivek Sarkar. 2011. Phaser beams: Integrating stream parallelism with task parallelism. Presented at the X10 Workshop."},{"key":"e_1_2_1_65_1","doi-asserted-by":"publisher","DOI":"10.1145\/582034.582042"},{"key":"e_1_2_1_66_1","doi-asserted-by":"publisher","DOI":"10.1137\/0201010"},{"key":"e_1_2_1_67_1","doi-asserted-by":"publisher","unstructured":"Franklyn Turbak. 1996. First-class synchronization barriers. In ICFP. ACM 157--168. 10.1145\/232627.232645","DOI":"10.1145\/232627.232645"},{"key":"e_1_2_1_68_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00722-4_5"},{"key":"e_1_2_1_70_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855761"},{"key":"e_1_2_1_71_1","doi-asserted-by":"publisher","unstructured":"Haitao Wei Hong Tan Xiaoxian Liu and Junqing Yu. 2012. StreamX10: A stream programming framework on X10. In X10. ACM 1--6. 10.1145\/2246056.2246057","DOI":"10.1145\/2246056.2246057"},{"key":"e_1_2_1_72_1","doi-asserted-by":"publisher","unstructured":"Adam Welc Suresh Jagannathan and Antony Hosking. 2005. Safe futures for Java. In OOPSLA. ACM 439--453. 10.1145\/1094811.1094845","DOI":"10.1145\/1094811.1094845"},{"key":"e_1_2_1_73_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-85261-2_7"},{"key":"e_1_2_1_74_1","doi-asserted-by":"publisher","DOI":"10.1145\/277650.277723"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3229060","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3229060","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3229060","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T02:07:35Z","timestamp":1750212455000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3229060"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2018,12,11]]},"references-count":72,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2019,3,31]]}},"alternative-id":["10.1145\/3229060"],"URL":"https:\/\/doi.org\/10.1145\/3229060","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2018,12,11]]},"assertion":[{"value":"2017-03-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-05-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2018-12-11","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}