{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,19]],"date-time":"2025-06-19T04:19:26Z","timestamp":1750306766378,"version":"3.41.0"},"reference-count":45,"publisher":"Association for Computing Machinery (ACM)","issue":"2","license":[{"start":{"date-parts":[[2013,7,1]],"date-time":"2013-07-01T00:00:00Z","timestamp":1372636800000},"content-version":"vor","delay-in-days":0,"URL":"https:\/\/www.acm.org\/publications\/policies\/copyright_policy#Background"}],"funder":[{"DOI":"10.13039\/501100005370","name":"Gates Cambridge Trust","doi-asserted-by":"publisher","id":[{"id":"10.13039\/501100005370","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/501100000266","name":"Engineering and Physical Sciences Research Council","doi-asserted-by":"publisher","award":["EP\/H010815\/1, EP\/H005633\/1, EP\/F036345"],"award-info":[{"award-number":["EP\/H010815\/1, EP\/H005633\/1, EP\/F036345"]}],"id":[{"id":"10.13039\/501100000266","id-type":"DOI","asserted-by":"publisher"}]},{"DOI":"10.13039\/100000143","name":"Division of Computing and Communication Foundations","doi-asserted-by":"publisher","award":["CCF-0811631"],"award-info":[{"award-number":["CCF-0811631"]}],"id":[{"id":"10.13039\/100000143","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":[[2013,7]]},"abstract":"<jats:p>We present an analysis which takes as its input a sequential program, augmented with annotations indicating potential parallelization opportunities, and a sequential proof, written in separation logic, and produces a correctly synchronized parallelized program and proof of that program. Unlike previous work, ours is not a simple independence analysis that admits parallelization only when threads do not interfere; rather, we insert synchronization to preserve dependencies in the sequential program that might be violated by a na\u00efve translation. Separation logic allows us to parallelize fine-grained patterns of resource usage, moving beyond straightforward points-to analysis. The sequential proof need only represent shape properties, meaning we can handle complex algorithms without verifying every aspect of their behavior.<\/jats:p>\n          <jats:p>Our analysis works by using the sequential proof to discover dependencies between different parts of the program. It leverages these discovered dependencies to guide the insertion of synchronization primitives into the parallelized program, and to ensure that the resulting parallelized program satisfies the same specification as the original sequential program, and exhibits the same sequential behavior. Our analysis is built using frame inference and abduction, two techniques supported by an increasing number of separation logic tools.<\/jats:p>","DOI":"10.1145\/2491522.2491525","type":"journal-article","created":{"date-parts":[[2013,7,30]],"date-time":"2013-07-30T13:35:22Z","timestamp":1375191322000},"page":"1-60","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":10,"title":["Proof-Directed Parallelization Synthesis by Separation Logic"],"prefix":"10.1145","volume":"35","author":[{"given":"Matko","family":"Botin\u010dan","sequence":"first","affiliation":[{"name":"University of Cambridge"}]},{"given":"Mike","family":"Dodds","sequence":"additional","affiliation":[{"name":"University of Cambridge"}]},{"given":"Suresh","family":"Jagannathan","sequence":"additional","affiliation":[{"name":"Purdue University"}]}],"member":"320","published-online":{"date-parts":[[2013,7]]},"reference":[{"key":"e_1_2_2_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/1504176.1504209"},{"key":"e_1_2_2_2_1","doi-asserted-by":"publisher","DOI":"10.5555\/1882094.1882104"},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11804192_6"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1007\/11575467_5"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1735970.1736029"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640096"},{"key":"e_1_2_2_7_1","doi-asserted-by":"publisher","DOI":"10.1145\/1640089.1640097"},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"volume-title":"Proceedings of the Workshop on Formal Techniques for Java-like Programs. 65--77","author":"Botin\u010dan M.","key":"e_1_2_2_9_1","unstructured":"Botin\u010dan, M., Distefano, D., Dodds, M., Griore, R., Naud\u017ei\u016bnien\u0117, and Parkinson, M. 2011. coreStar: The core of jStar. In Proceedings of the Workshop on Formal Techniques for Java-like Programs. 65--77."},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1145\/1743546.1743572"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2049697.2049700"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-10672-9_19"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/2040235.2040256"},{"key":"e_1_2_2_14_1","unstructured":"Cook B. Magill S. Raza M. Simsa J. and Singh S. 2010. Making fast hardware with separation logic. http:\/\/cs.cmu.edu\/~smagill\/papers\/fast-hardware.pdf."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1137\/S0097539704446311"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_13"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12029-9_20"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1145\/1449764.1449782"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/1926385.1926416"},{"key":"e_1_2_2_20_1","doi-asserted-by":"publisher","DOI":"10.1145\/200836.200838"},{"key":"e_1_2_2_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/647474.727598"},{"key":"e_1_2_2_22_1","doi-asserted-by":"publisher","DOI":"10.1145\/2048066.2048086"},{"key":"e_1_2_2_23_1","doi-asserted-by":"publisher","DOI":"10.5555\/1784774.1784779"},{"key":"e_1_2_2_24_1","doi-asserted-by":"publisher","DOI":"10.1016\/S0167-8191(99)00086-1"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-89330-1_13"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.1109\/71.80123"},{"key":"e_1_2_2_27_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.entcs.2008.04.050"},{"key":"e_1_2_2_28_1","doi-asserted-by":"publisher","DOI":"10.5555\/1792878.1792914"},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.1145\/73141.74821"},{"key":"e_1_2_2_30_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-03237-0_6"},{"key":"e_1_2_2_31_1","unstructured":"Jacobs B. and Piessens F. 2009. Modular full functional specification and verification of lock-free data structures. Tech. rep. CW 551 Department of Computer Science Katholieke Universiteit Leuven."},{"key":"e_1_2_2_32_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-11957-6_22"},{"key":"e_1_2_2_33_1","doi-asserted-by":"publisher","DOI":"10.1145\/2043556.2043587"},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","DOI":"10.1145\/1345206.1345212"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1109\/MICRO.2005.13"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1993498.1993501"},{"volume-title":"Proceedings of the International Static Analysis Symposium. Springer.","author":"Raychev V.","key":"e_1_2_2_38_1","unstructured":"Raychev, V., Vechev, M., and Yahav, E. 2013. Automatic synthesis of deterministic concurrency. In Proceedings of the International Static Analysis Symposium. Springer."},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-00590-9_25"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.5555\/645683.664578"},{"key":"e_1_2_2_41_1","unstructured":"SV-Comp. 2013. http:\/\/sv-comp.sosy-lab.org\/2013\/."},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/181181.181261"},{"key":"e_1_2_2_43_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-12002-2_23"},{"key":"e_1_2_2_44_1","doi-asserted-by":"publisher","DOI":"10.1145\/1094811.1094845"},{"key":"e_1_2_2_45_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_36"}],"container-title":["ACM Transactions on Programming Languages and Systems"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491522.2491525","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/2491522.2491525","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T07:28:50Z","timestamp":1750231730000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/2491522.2491525"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2013,7]]},"references-count":45,"journal-issue":{"issue":"2","published-print":{"date-parts":[[2013,7]]}},"alternative-id":["10.1145\/2491522.2491525"],"URL":"https:\/\/doi.org\/10.1145\/2491522.2491525","relation":{},"ISSN":["0164-0925","1558-4593"],"issn-type":[{"type":"print","value":"0164-0925"},{"type":"electronic","value":"1558-4593"}],"subject":[],"published":{"date-parts":[[2013,7]]},"assertion":[{"value":"2012-02-01","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-03-01","order":1,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2013-07-01","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}