{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T11:03:48Z","timestamp":1784199828622,"version":"3.55.0"},"reference-count":57,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA2","funder":[{"name":"Independent Research Fund Denmark","award":["Hyben"],"award-info":[{"award-number":["Hyben"]}]},{"name":"University of Malta Research Seed Fund","award":["CPSRP01-25"],"award-info":[{"award-number":["CPSRP01-25"]}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2025,10,9]]},"abstract":"<jats:p>Many software applications rely on concurrent and distributed (micro)services that interact via message passing and various forms of remote procedure calls (RPC). As these systems organically evolve and grow in scale and complexity, the risk of introducing deadlocks increases and their impact may worsen: even if only a few services deadlock, many other services may block while awaiting responses from the deadlocked ones. As a result, the \u201ccore\u201d of the deadlock can be obfuscated by its consequences on the rest of the system, and diagnosing and fixing the problem can be challenging.<\/jats:p>\n                  <jats:p>\n                    In this work we tackle the challenge by proposing\n                    <jats:italic toggle=\"yes\">distributed black-box monitors<\/jats:italic>\n                    that are deployed alongside each service and detect deadlocks by only observing the incoming and outgoing messages, and exchanging\n                    <jats:italic toggle=\"yes\">probes<\/jats:italic>\n                    with other monitors. We present a formal model that captures popular RPC-based application styles (e.g.,\n                    <jats:monospace>gen_servers<\/jats:monospace>\n                    in Erlang\/OTP), and a distributed black-box monitoring algorithm that we prove sound and complete (i.e., identifies deadlocked services with neither false positives nor false negatives). We implement our results in a tool called DDMon for the monitoring of Erlang\/OTP applications, and we evaluate its performance.\n                  <\/jats:p>\n                  <jats:p>This is the first work that formalises, proves the correctness, and implements distributed black-box monitors for deadlock detection. Our results are mechanised in Coq. DDMon is the companion artifact of this paper.<\/jats:p>","DOI":"10.1145\/3763069","type":"journal-article","created":{"date-parts":[[2025,10,9]],"date-time":"2025-10-09T08:49:50Z","timestamp":1759999790000},"page":"527-554","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation"],"prefix":"10.1145","volume":"9","author":[{"ORCID":"https:\/\/orcid.org\/0009-0003-0758-722X","authenticated-orcid":false,"given":"Rados\u0142aw Jan","family":"Rowicki","sequence":"first","affiliation":[{"name":"Technical University of Denmark, Kongens Lyngby, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-3829-7391","authenticated-orcid":false,"given":"Adrian","family":"Francalanza","sequence":"additional","affiliation":[{"name":"University of Malta, Msida, Malta"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-1153-6164","authenticated-orcid":false,"given":"Alceste","family":"Scalas","sequence":"additional","affiliation":[{"name":"Technical University of Denmark, Kongens Lyngby, Denmark"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2025,10,9]]},"reference":[{"key":"e_1_3_1_2_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-031-08679-3_1"},{"key":"e_1_3_1_3_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.CONCUR.2024.4"},{"key":"e_1_3_1_4_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-030-71500-7_1"},{"key":"e_1_3_1_5_2","doi-asserted-by":"publisher","DOI":"10.4230\/LIPIcs.ECOOP.2024.2"},{"key":"e_1_3_1_6_2","doi-asserted-by":"publisher","DOI":"10.1007\/11678779_14"},{"key":"e_1_3_1_7_2","unstructured":"Akka and Pekko developers team. 2025. Apache Pekko gRPC Apache Software Foundation https:\/\/pekko.apache.org\/docs\/pekko-grpc\/current\/index.html Accessed: 2025-03-10."},{"key":"e_1_3_1_8_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2021.111014"},{"key":"e_1_3_1_9_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-33693-0_26"},{"key":"e_1_3_1_10_2","doi-asserted-by":"publisher","unstructured":"Sara Abbaspour Asadollah Daniel Daniel Sigrid Eldh and Hans Hansson. 2018. A Runtime Verification Tool for Detecting Concurrency Bugs in FreeRTOS Embedded Software.In 2018 17th International Symposium on Parallel and Distributed Computing (ISPDC). 172\u2013179.doi:10.1109\/ISPDC2018.2018.00032","DOI":"10.1109\/ISPDC2018.2018.00032"},{"key":"e_1_3_1_11_2","doi-asserted-by":"publisher","DOI":"10.1016\/J.JSS.2023.111788"},{"key":"e_1_3_1_12_2","doi-asserted-by":"publisher","DOI":"10.1145\/3605159.3605857"},{"key":"e_1_3_1_13_2","doi-asserted-by":"publisher","DOI":"10.1145\/6513.6516"},{"key":"e_1_3_1_14_2","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-75632-5_1"},{"key":"e_1_3_1_15_2","doi-asserted-by":"publisher","DOI":"10.1145\/1147403.1147412"},{"key":"e_1_3_1_16_2","doi-asserted-by":"publisher","DOI":"10.1007\/11678779_15"},{"key":"e_1_3_1_17_2","doi-asserted-by":"publisher","DOI":"10.1145\/800222.806756"},{"key":"e_1_3_1_18_2","doi-asserted-by":"publisher","DOI":"10.1145\/357360.357365"},{"key":"e_1_3_1_19_2","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094852"},{"key":"e_1_3_1_20_2","doi-asserted-by":"publisher","DOI":"10.1109\/32.21721"},{"key":"e_1_3_1_21_2","doi-asserted-by":"publisher","DOI":"10.1145\/3229060"},{"key":"e_1_3_1_22_2","doi-asserted-by":"publisher","DOI":"10.1017\/S0960129515000230"},{"key":"e_1_3_1_23_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.jlamp.2021.100717"},{"key":"e_1_3_1_24_2","unstructured":"Ericsson AB. 2025. Erlang\/OTP System Documentation 14.2.5.8. https:\/\/www.erlang.org\/docs\/26\/pdf\/otp-system-documentation.pdf Accessed: 2025-03-10."},{"key":"e_1_3_1_25_2","unstructured":"Erlang\/OTP Team. 2025. Erlang\/OTP documentation: gen_server Behaviour. Ericsson AB. https:\/\/www.erlang.org\/doc\/system\/gen_server_concepts Accessed: 2025-03-10."},{"key":"e_1_3_1_26_2","unstructured":"Erlang\/OTP Team. 2025. Erlang\/OTP documentation: gen_statem Behaviour. Ericsson AB. https:\/\/www.erlang.org\/doc\/system\/statem.html Accessed: 2025-03-10."},{"key":"e_1_3_1_27_2","unstructured":"Erlang\/OTP Team. 2025. Erlang\/OTP documentation: the trace interface. Ericsson AB. https:\/\/www.erlang.org\/doc\/apps\/kernel\/trace.html Accessed: 2025-03-10."},{"key":"e_1_3_1_28_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10703-019-00334-z"},{"key":"e_1_3_1_29_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2021.104704"},{"key":"e_1_3_1_30_2","doi-asserted-by":"publisher","DOI":"10.1145\/3329125"},{"key":"e_1_3_1_31_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1980.230491"},{"key":"e_1_3_1_32_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2010.05.002"},{"key":"e_1_3_1_33_2","first-page":"115","volume-title":"18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021,","author":"Hance Travis","year":"2021","unstructured":"Travis Hance, Marijn Heule, Ruben Martins, and Bryan Parno. 2021. Finding Invariants of Distributed Systems: It\u2019s a Small (Enough) World After All. In 18th USENIX Symposium on Networked Systems Design and Implementation, NSDI 2021, April 12-14, 2021,, James Mickens and Renata Teixeira (Eds.). USENIX Association, 115\u2013131. https:\/\/www.usenix.org\/conference\/nsdi21\/presentation\/hance"},{"key":"e_1_3_1_34_2","doi-asserted-by":"publisher","DOI":"10.1007\/10722468_15"},{"key":"e_1_3_1_35_2","doi-asserted-by":"publisher","DOI":"10.1145\/2503210.2503237"},{"key":"e_1_3_1_36_2","doi-asserted-by":"publisher","DOI":"10.1109\/CMPSAC.1978.810401"},{"key":"e_1_3_1_37_2","doi-asserted-by":"publisher","DOI":"10.1109\/PRDC.2010.49"},{"key":"e_1_3_1_38_2","doi-asserted-by":"publisher","DOI":"10.1145\/360248.360251"},{"key":"e_1_3_1_39_2","doi-asserted-by":"publisher","DOI":"10.1109\/ICPADS.1997.652603"},{"key":"e_1_3_1_40_2","doi-asserted-by":"publisher","DOI":"10.1145\/276393.278524"},{"key":"e_1_3_1_41_2","doi-asserted-by":"publisher","DOI":"10.1007\/11817949_16"},{"key":"e_1_3_1_42_2","doi-asserted-by":"publisher","DOI":"10.1016\/j.ic.2016.03.004"},{"key":"e_1_3_1_43_2","doi-asserted-by":"publisher","DOI":"10.1109\/TC.2006.151"},{"key":"e_1_3_1_44_2","volume-title":"Communication and concurrency","author":"Milner Robin","year":"1989","unstructured":"Robin Milner. 1989. Communication and concurrency. Prentice Hall."},{"key":"e_1_3_1_45_2","doi-asserted-by":"publisher","DOI":"10.1145\/800222.806755"},{"key":"e_1_3_1_46_2","doi-asserted-by":"publisher","DOI":"10.5555\/3529"},{"key":"e_1_3_1_47_2","doi-asserted-by":"publisher","DOI":"10.1007\/s00450-019-00407-8"},{"key":"e_1_3_1_48_2","doi-asserted-by":"publisher","DOI":"10.1145\/2892208.2892232"},{"key":"e_1_3_1_49_2","doi-asserted-by":"publisher","DOI":"10.1145\/2603088.2603116"},{"key":"e_1_3_1_50_2","doi-asserted-by":"publisher","DOI":"10.4204\/EPTCS.190.4"},{"key":"e_1_3_1_51_2","doi-asserted-by":"publisher","unstructured":"Radoslaw Jan Rowicki. 2025. Coq Mechanisation of a Theory of Black-Box Monitors for Correct Distributed Deadlock Detection (version 0.9.0). doi:10.5281\/zenodo.l6909482","DOI":"10.5281\/zenodo.l6909482"},{"key":"e_1_3_1_52_2","doi-asserted-by":"publisher","unstructured":"Radoslaw Jan Rowicki. 2025. DDMon: a Monitoring Tool for Distributed Deadlock Detection (version 0.1.0). doi:10.5281\/zenodo.16909304","DOI":"10.5281\/zenodo.16909304"},{"key":"e_1_3_1_53_2","doi-asserted-by":"publisher","unstructured":"Radoslaw Jan Rowicki Adrian Francalanza and Alceste Scalas. 2025. Correct Black-Box Monitors for Distributed Deadlock Detection: Formalisation and Implementation (Technical Report). doi:10.48550\/arXiv.2508.14851","DOI":"10.48550\/arXiv.2508.14851"},{"key":"e_1_3_1_54_2","doi-asserted-by":"publisher","DOI":"10.5555\/559050"},{"key":"e_1_3_1_55_2","doi-asserted-by":"publisher","DOI":"10.1109\/TSE.1985.231844"},{"key":"e_1_3_1_56_2","doi-asserted-by":"publisher","DOI":"10.1007\/s10619-011-7078-7"},{"key":"e_1_3_1_57_2","doi-asserted-by":"publisher","DOI":"10.1145\/2737924.2737958"},{"key":"e_1_3_1_58_2","doi-asserted-by":"publisher","DOI":"10.1145\/187436.187447"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3763069","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2026,7,16]],"date-time":"2026-07-16T10:04:02Z","timestamp":1784196242000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3763069"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,10,9]]},"references-count":57,"journal-issue":{"issue":"OOPSLA2","published-print":{"date-parts":[[2025,10,9]]}},"alternative-id":["10.1145\/3763069"],"URL":"https:\/\/doi.org\/10.1145\/3763069","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2025,10,9]]},"assertion":[{"value":"2025-03-26","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-08-12","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-10-09","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}