{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:46:59Z","timestamp":1750308419544,"version":"3.41.0"},"reference-count":44,"publisher":"Association for Computing Machinery (ACM)","issue":"1","license":[{"start":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T00:00:00Z","timestamp":1598832000000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["SIGOPS Oper. Syst. Rev."],"published-print":{"date-parts":[[2020,8,31]]},"abstract":"<jats:p>Explicit signaling between threads is a perennial cause of bugs in concurrent programs. While there are several runtime techniques to automatically notify threads upon the availability of some shared resource, such techniques are not widely-adopted due to their run-time overhead. This paper proposes a new solution based on static analysis for automatically generating a performant explicit-signal program from its corresponding implicit-signal implementation. The key idea is to generate verification conditions that allow us to minimize the number of required signals and unnecessary context switches, while guaranteeing semantic equivalence between the source and target programs. We have implemented our method in a tool called Expresso and evaluate it on challenging benchmarks from prior papers and open-source software. Expresso-generated code significantly outperforms past automatic signaling mechanisms (avg. 1.56x speedup) and closely matches the performance of hand-optimized explicit-signal code.<\/jats:p>","DOI":"10.1145\/3421473.3421482","type":"journal-article","created":{"date-parts":[[2020,8,31]],"date-time":"2020-08-31T13:31:19Z","timestamp":1598880679000},"page":"64-76","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Symbolic Reasoning for Automatic Signal Placement"],"prefix":"10.1145","volume":"54","author":[{"given":"Kostas","family":"Ferles","sequence":"first","affiliation":[{"name":"The University of Texas at Austin, Austin, TX, USA"}]},{"given":"Jacob","family":"Van Geffen","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin, Austin, TX, USA"}]},{"given":"Isil","family":"Dillig","sequence":"additional","affiliation":[{"name":"The University of Texas at Austin, Austin, TX, USA"}]},{"given":"Yannis","family":"Smaragdakis","sequence":"additional","affiliation":[{"name":"University of Athens, Athens, Greece"}]}],"member":"320","published-online":{"date-parts":[[2020,8,31]]},"reference":[{"key":"e_1_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1147403.1147413"},{"key":"e_1_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/110561"},{"key":"e_1_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/512950.512975"},{"key":"e_1_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/583854.582440"},{"key":"e_1_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640108"},{"key":"e_1_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/214037.214100"},{"key":"e_1_2_1_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1108970.1108975"},{"volume-title":"International Conference on Computer Aided Verification. Springer, 951--967","year":"2013","author":"Pavol","key":"e_1_2_1_8_1"},{"key":"e_1_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1379022.1375619"},{"key":"e_1_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792734.1792766"},{"key":"e_1_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2544173.2509539"},{"key":"e_1_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.5555\/762971.762977"},{"key":"e_1_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/762971.762974"},{"key":"e_1_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.5555\/2050917.2050962"},{"key":"e_1_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190260"},{"volume-title":"Isil Dillig, and Yannis Smaragdakis.","year":"2018","author":"Ferles Kostas","key":"e_1_2_1_16_1"},{"key":"e_1_2_1_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/3296979.3192395"},{"key":"e_1_2_1_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/2786805.2786815"},{"key":"e_1_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.5555\/540365"},{"key":"e_1_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/949343.949340"},{"key":"e_1_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.1145\/173682.165164"},{"volume-title":"Proceedings of the First ACM SIGPLAN Workshop on Languages, Compilers, and Hardware Support for Transactional Computing.","year":"2006","author":"Hicks Michael","key":"e_1_2_1_22_1"},{"key":"e_1_2_1_23_1","unstructured":"C. A. R. Hoare. 1971. Towards a theory of parallel programming. In International Seminar on Operating System Techniques.  C. A. R. Hoare. 1971. Towards a theory of parallel programming. In International Seminar on Operating System Techniques."},{"key":"e_1_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/762971.762982"},{"key":"e_1_2_1_25_1","volume-title":"Proc. of PODC","volume":"4","author":"Hovemeyer David","year":"2004"},{"key":"e_1_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/2499370.2462175"},{"key":"e_1_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.5555\/2387880.2387902"},{"key":"e_1_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-02658-4_54"},{"key":"e_1_2_1_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/1882291.1882339"},{"volume-title":"Formal Methods in Computer-Aided Design (FMCAD)","year":"2012","author":"Kahlon Vineet","key":"e_1_2_1_30_1"},{"key":"e_1_2_1_31_1","doi-asserted-by":"publisher","DOI":"10.1109\/MC.2009.391"},{"key":"e_1_2_1_32_1","doi-asserted-by":"publisher","DOI":"10.1145\/2771783.2771798"},{"volume-title":"Larus and Ravi Rajwar","year":"2007","author":"James","key":"e_1_2_1_33_1"},{"key":"e_1_2_1_34_1","doi-asserted-by":"publisher","DOI":"10.5555\/555067"},{"key":"e_1_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/1669112.1669181"},{"key":"e_1_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/1111320.1111068"},{"key":"e_1_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.5555\/1855741.1855760"},{"key":"e_1_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1133981.1134018"},{"key":"e_1_2_1_39_1","unstructured":"Aleksey Shipilev Sergey Kuksenko Anders Astrand Staffan Freiberg and Henrik Loef. [n. d.]. OpenJDK: JMH. ([n. d.]). http:\/\/openjdk.java. net\/projects\/code-tools\/jmh\/  Aleksey Shipilev Sergey Kuksenko Anders Astrand Staffan Freiberg and Henrik Loef. [n. d.]. OpenJDK: JMH. ([n. d.]). http:\/\/openjdk.java. net\/projects\/code-tools\/jmh\/"},{"key":"e_1_2_1_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2103656.2103702"},{"key":"e_1_2_1_41_1","doi-asserted-by":"publisher","DOI":"10.5555\/781995.782008"},{"key":"e_1_2_1_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/1707801.1706338"},{"key":"e_1_2_1_43_1","doi-asserted-by":"publisher","DOI":"10.1145\/1594834.1480913"},{"key":"e_1_2_1_44_1","doi-asserted-by":"publisher","DOI":"10.5555\/1924943.1924955"}],"container-title":["ACM SIGOPS Operating Systems Review"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421482","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3421473.3421482","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T17:49:21Z","timestamp":1750268961000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3421473.3421482"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,8,31]]},"references-count":44,"journal-issue":{"issue":"1","published-print":{"date-parts":[[2020,8,31]]}},"alternative-id":["10.1145\/3421473.3421482"],"URL":"https:\/\/doi.org\/10.1145\/3421473.3421482","relation":{},"ISSN":["0163-5980"],"issn-type":[{"type":"print","value":"0163-5980"}],"subject":[],"published":{"date-parts":[[2020,8,31]]},"assertion":[{"value":"2020-08-31","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}