{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,2,5]],"date-time":"2026-02-05T09:11:26Z","timestamp":1770282686212,"version":"3.49.0"},"reference-count":24,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA1","license":[{"start":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T00:00:00Z","timestamp":1651190400000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/creativecommons.org\/licenses\/by\/4.0\/"}],"funder":[{"name":"NSF","award":["CCF-1918889,CCF-1811865"],"award-info":[{"award-number":["CCF-1918889,CCF-1811865"]}]},{"DOI":"10.13039\/100000015","name":"U.S. Department of Energy","doi-asserted-by":"publisher","award":["SC0021110"],"award-info":[{"award-number":["SC0021110"]}],"id":[{"id":"10.13039\/100000015","id-type":"DOI","asserted-by":"publisher"}]}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2022,4,29]]},"abstract":"<jats:p>A monitor is a widely-used concurrent programming abstraction that encapsulates all shared state between threads. Monitors can be classified as being either implicit or explicit depending on the primitives they provide. Implicit monitors are much easier to program but typically not as efficient. To address this gap, there has been recent research on automatically synthesizing explicit-signal monitors from an implicit specification, but prior work does not exploit all paralellization opportunities due to the use of a single lock for the entire monitor. This paper presents a new technique for synthesizing fine-grained explicit-synchronization protocols from implicit monitors. Our method is based on two key innovations: First, we present a new static analysis for inferring safe interleavings that allow violating mutual exclusion of monitor operations without changing its semantics. Second, we use the results of this static analysis to generate a MaxSAT instance whose models correspond to correct-by-construction synchronization protocols. We have implemented our approach in a tool called Cortado and evaluate it on monitors that contain parallelization opportunities. Our evaluation shows that Cortado can synthesize synchronization policies that are competitive with, or even better than, expert-written ones on these benchmarks.<\/jats:p>","DOI":"10.1145\/3527311","type":"journal-article","created":{"date-parts":[[2022,4,29]],"date-time":"2022-04-29T15:42:03Z","timestamp":1651246923000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":1,"title":["Synthesizing fine-grained synchronization protocols for implicit monitors"],"prefix":"10.1145","volume":"6","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-8370-5465","authenticated-orcid":false,"given":"Kostas","family":"Ferles","sequence":"first","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-4924-3009","authenticated-orcid":false,"given":"Benjamin","family":"Sepanski","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0003-0230-5185","authenticated-orcid":false,"given":"Rahul","family":"Krishnan","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0002-3258-3226","authenticated-orcid":false,"given":"James","family":"Bornholt","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8006-1230","authenticated-orcid":false,"given":"I\u015fil","family":"Dillig","sequence":"additional","affiliation":[{"name":"University of Texas at Austin, USA"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2022,4,29]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1007\/BF02579381"},{"key":"e_1_2_1_2_1","volume-title":"An introduction to programming with threads","author":"Birrell Andrew D","unstructured":"Andrew D Birrell . 1989. An introduction to programming with threads . Digital Systems Research Center , Palo Alto , California. Andrew D Birrell. 1989. An introduction to programming with threads. Digital Systems Research Center, Palo Alto, California."},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/214037.214100"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375619"},{"key":"e_1_2_1_5_1","volume-title":"Tools and Algorithms for the Construction and Analysis of Systems","author":"de Moura Leonardo","unstructured":"Leonardo de Moura and Nikolaj Bj\u00f8rner . 2008. Z3: An Efficient SMT Solver . In Tools and Algorithms for the Construction and Analysis of Systems , C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg , Berlin, Heidelberg . 337\u2013340. isbn:978-3-540-78800-3 Leonardo de Moura and Nikolaj Bj\u00f8rner. 2008. Z3: An Efficient SMT Solver. In Tools and Algorithms for the Construction and Analysis of Systems, C. R. Ramakrishnan and Jakob Rehof (Eds.). Springer Berlin Heidelberg, Berlin, Heidelberg. 337\u2013340. isbn:978-3-540-78800-3"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190260"},{"key":"e_1_2_1_7_1","doi-asserted-by":"crossref","unstructured":"Kostas Ferles Benjamin Sepanski Rahul Krishnan James Bornholt and Isil Dillig. 2022. Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors (Extended Version). arxiv:2203.00783.  Kostas Ferles Benjamin Sepanski Rahul Krishnan James Bornholt and Isil Dillig. 2022. Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors (Extended Version). arxiv:2203.00783.","DOI":"10.1145\/3527311"},{"key":"e_1_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/3192366.3192395"},{"key":"e_1_2_1_9_1","unstructured":"GitHub. 2022. GitHub REST API. https:\/\/docs.github.com\/en\/rest  GitHub. 2022. GitHub REST API. https:\/\/docs.github.com\/en\/rest"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/2076021.2048086"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46681-0_41"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/1299042.1299061"},{"key":"e_1_2_1_13_1","volume-title":"Operating System Principles","author":"Hansen Per Brinch","unstructured":"Per Brinch Hansen . 1973. Operating System Principles . Prentice-Hall , Englewood Cliffs , New Jersey. isbn:0-13-637843-9 Per Brinch Hansen. 1973. Operating System Principles. Prentice-Hall, Englewood Cliffs, New Jersey. isbn:0-13-637843-9"},{"key":"e_1_2_1_14_1","unstructured":"Michael Hicks Jeffrey S Foster and Polyvios Pratikakis. 2006. Lock inference for atomic sections. In On-Line Proceedings of the First ACM SIGPLAN Workshop on Languages Compilers and Hardware Support for Transactional Computing (TRANSACT). http:\/\/www.cs.purdue.edu\/homes\/jv\/events\/TRANSACT\/transact-06.tgz  Michael Hicks Jeffrey S Foster and Polyvios Pratikakis. 2006. Lock inference for atomic sections. In On-Line Proceedings of the First ACM SIGPLAN Workshop on Languages Compilers and Hardware Support for Transactional Computing (TRANSACT). http:\/\/www.cs.purdue.edu\/homes\/jv\/events\/TRANSACT\/transact-06.tgz"},{"key":"e_1_2_1_15_1","volume-title":"Operating Systems Techniques, Proceedings of a Seminar at","author":"Hoare C. A. R.","unstructured":"C. A. R. Hoare . 1971. Towards a theory of parallel programming . In Operating Systems Techniques, Proceedings of a Seminar at Queen\u2019s University, Belfast . Springer-Verlag , Belfast, Northern Ireland. 231\u2013244. isbn:0387954015 C. A. R. Hoare. 1971. Towards a theory of parallel programming. In Operating Systems Techniques, Proceedings of a Seminar at Queen\u2019s University, Belfast. Springer-Verlag, Belfast, Northern Ireland. 231\u2013244. isbn:0387954015"},{"key":"e_1_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.1145\/355620.361161"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462175"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/358818.358824"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/143103.143137"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/361227.361234"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111037.1111068"},{"key":"e_1_2_1_22_1","volume-title":"Discrete Appl. Math., 154, 8","author":"Michael T. S.","year":"2006","unstructured":"T. S. Michael and Thomas Quint . 2006. Sphericity, Cubicity, and Edge Clique Covers of Graphs . Discrete Appl. Math., 154, 8 ( 2006 ), may, 1309\u20131313. issn:0166-218X T. S. Michael and Thomas Quint. 2006. Sphericity, Cubicity, and Edge Clique Covers of Graphs. Discrete Appl. Math., 154, 8 (2006), may, 1309\u20131313. issn:0166-218X"},{"key":"e_1_2_1_23_1","unstructured":"Aleksey Shipilev Sergey Kuksenko Astrand Astrand Staffan Freiberg and Henrik Loef. 2021. OpenJDK: jmh. http:\/\/openjdk.java.net\/projects\/code-tools\/jmh\/  Aleksey Shipilev Sergey Kuksenko Astrand Astrand Staffan Freiberg and Henrik Loef. 2021. OpenJDK: jmh. http:\/\/openjdk.java.net\/projects\/code-tools\/jmh\/"},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/781995.782008"}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527311","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527311","content-type":"application\/pdf","content-version":"vor","intended-application":"syndication"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3527311","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,17]],"date-time":"2025-06-17T20:18:52Z","timestamp":1750191532000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3527311"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2022,4,29]]},"references-count":24,"journal-issue":{"issue":"OOPSLA1","published-print":{"date-parts":[[2022,4,29]]}},"alternative-id":["10.1145\/3527311"],"URL":"https:\/\/doi.org\/10.1145\/3527311","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2022,4,29]]},"assertion":[{"value":"2022-04-29","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}