{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,9,7]],"date-time":"2024-09-07T00:46:55Z","timestamp":1725670015287},"publisher-location":"Berlin, Heidelberg","reference-count":20,"publisher":"Springer Berlin Heidelberg","isbn-type":[{"type":"print","value":"9783642288685"},{"type":"electronic","value":"9783642288692"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"published-print":{"date-parts":[[2012]]},"DOI":"10.1007\/978-3-642-28869-2_17","type":"book-chapter","created":{"date-parts":[[2012,3,22]],"date-time":"2012-03-22T20:44:36Z","timestamp":1332449076000},"page":"336-356","source":"Crossref","is-referenced-by-count":6,"title":["Reasoning about Lock Placements"],"prefix":"10.1007","author":[{"given":"Peter","family":"Hawkins","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Alex","family":"Aiken","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kathleen","family":"Fisher","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Martin","family":"Rinard","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Mooly","family":"Sagiv","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"297","reference":[{"key":"17_CR1","first-page":"31","volume-title":"POPL","author":"H. Attiya","year":"2010","unstructured":"Attiya, H., Ramalingam, G., Rinetzky, N.: Sequential verification of serializability. In: POPL, pp. 31\u201342. ACM, New York (2010)"},{"key":"17_CR2","first-page":"6","volume-title":"PODC","author":"N.G. Bronson","year":"2010","unstructured":"Bronson, N.G., Casper, J., Chafi, H., Olukotun, K.: Transactional predication: high-performance concurrent sets and maps for STM. In: PODC, pp. 6\u201315. ACM, New York (2010)"},{"key":"17_CR3","doi-asserted-by":"publisher","first-page":"304","DOI":"10.1145\/1375581.1375619","volume-title":"PLDI","author":"S. Cherem","year":"2008","unstructured":"Cherem, S., Chilimbi, T., Gulwani, S.: Inferring locks for atomic sections. In: PLDI, pp. 304\u2013315. ACM, New York (2008)"},{"key":"17_CR4","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"276","DOI":"10.1007\/978-3-540-78791-4_19","volume-title":"Compiler Construction","author":"D. Cunningham","year":"2008","unstructured":"Cunningham, D., Gudka, K., Eisenbach, S.: Keep Off the Grass: Locking the Right Path for Atomicity. In: Hendren, L. (ed.) CC 2008. LNCS, vol.\u00a04959, pp. 276\u2013290. Springer, Heidelberg (2008)"},{"key":"17_CR5","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"226","DOI":"10.1007\/978-3-642-11957-6_13","volume-title":"Programming Languages and Systems","author":"J. Deshmukh","year":"2010","unstructured":"Deshmukh, J., Ramalingam, G., Ranganath, V.-P., Vaswani, K.: Logical Concurrency Control from Sequential Proofs. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 226\u2013245. Springer, Heidelberg (2010)"},{"issue":"2","key":"17_CR6","first-page":"218","volume":"49","author":"P.C. Diniz","year":"1998","unstructured":"Diniz, P.C., Rinard, M.C.: Lock coarsening: Eliminating lock overhead in automatically parallelized object-based programs. JPDC\u00a049(2), 218\u2013244 (1998)","journal-title":"JPDC"},{"key":"17_CR7","doi-asserted-by":"crossref","first-page":"291","DOI":"10.1145\/1190216.1190260","volume-title":"POPL","author":"M. Emmi","year":"2007","unstructured":"Emmi, M., Fischer, J.S., Jhala, R., Majumdar, R.: Lock allocation. In: POPL, pp. 291\u2013296. ACM, New York (2007)"},{"key":"17_CR8","doi-asserted-by":"publisher","first-page":"624","DOI":"10.1145\/360363.360369","volume":"19","author":"K.P. Eswaran","year":"1976","unstructured":"Eswaran, K.P., Gray, J.N., Lorie, R.A., Traiger, I.L.: The notions of consistency and predicate locks in a database system. Commun. ACM\u00a019, 624\u2013633 (1976)","journal-title":"Commun. ACM"},{"key":"17_CR9","doi-asserted-by":"crossref","unstructured":"Golan-Gueta, G., Bronson, N., Aiken, A., Ramalingam, G., Sagiv, M., Yahav, E.: Automatic fine-grained locking using shape properties. In: OOPSLA (2011)","DOI":"10.1145\/2048066.2048086"},{"key":"17_CR10","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"19","DOI":"10.1007\/978-3-540-76637-7_3","volume-title":"Programming Languages and Systems","author":"A. Gotsman","year":"2007","unstructured":"Gotsman, A., Berdine, J., Cook, B., Rinetzky, N., Sagiv, M.: Local Reasoning for Storable Locks and Threads. In: Shao, Z. (ed.) APLAS 2007. LNCS, vol.\u00a04807, pp. 19\u201337. Springer, Heidelberg (2007)"},{"key":"17_CR11","first-page":"353","volume-title":"PACT","author":"R.L. Halpert","year":"2007","unstructured":"Halpert, R.L., Pickett, C.J.F., Verbrugge, C.: Component-based lock allocation. In: PACT, pp. 353\u2013364. IEEE Computer Society, Washington, DC (2007)"},{"key":"17_CR12","doi-asserted-by":"crossref","unstructured":"Hawkins, P., Aiken, A., Fisher, K., Rinard, M., Sagiv, M.: Reasoning about lock placements (extended version). Tech. rep., Stanford University (2011), http:\/\/theory.stanford.edu\/~hawkinsp\/papers\/tr\/lockplacements.pdf","DOI":"10.1007\/978-3-642-28869-2_17"},{"key":"17_CR13","first-page":"38","volume-title":"PLDI","author":"P. Hawkins","year":"2011","unstructured":"Hawkins, P., Aiken, A., Fisher, K., Rinard, M., Sagiv, M.: Data representation synthesis. In: PLDI, pp. 38\u201349. ACM, New York (2011)"},{"key":"17_CR14","unstructured":"Hicks, M., Foster, J.S., Pratikakis, P.: Lock inference for atomic sections. In: TRANSACT (2006)"},{"key":"17_CR15","unstructured":"Jones, C.: Development methods for computer programs including a notion of interference. Ph.D. thesis, Oxford University (1981)"},{"key":"17_CR16","first-page":"346","volume-title":"POPL","author":"B. McCloskey","year":"2006","unstructured":"McCloskey, B., Zhou, F., Gay, D., Brewer, E.: Autolocker: Synchronization inference for atomic sections. In: POPL, pp. 346\u2013358. ACM, New York (2006)"},{"issue":"1-3","key":"17_CR17","doi-asserted-by":"publisher","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"P.W. O\u2019Hearn","year":"2007","unstructured":"O\u2019Hearn, P.W.: Resources, concurrency, and local reasoning. Theoretical Computer Science\u00a0375(1-3), 271\u2013307 (2007)","journal-title":"Theoretical Computer Science"},{"key":"17_CR18","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"256","DOI":"10.1007\/978-3-540-74407-8_18","volume-title":"CONCUR 2007 \u2013 Concurrency Theory","author":"V. Vafeiadis","year":"2007","unstructured":"Vafeiadis, V., Parkinson, M.: A Marriage of Rely\/Guarantee and Separation Logic. In: Caires, L., Vasconcelos, V.T. (eds.) CONCUR 2007. LNCS, vol.\u00a04703, pp. 256\u2013271. Springer, Heidelberg (2007)"},{"key":"17_CR19","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"610","DOI":"10.1007\/978-3-642-11957-6_32","volume-title":"Programming Languages and Systems","author":"J. Wickerson","year":"2010","unstructured":"Wickerson, J., Dodds, M., Parkinson, M.: Explicit Stabilisation for Modular Rely-Guarantee Reasoning. In: Gordon, A.D. (ed.) ESOP 2010. LNCS, vol.\u00a06012, pp. 610\u2013629. Springer, Heidelberg (2010)"},{"key":"17_CR20","series-title":"Lecture Notes in Computer Science","doi-asserted-by":"publisher","first-page":"141","DOI":"10.1007\/978-3-540-89740-8_10","volume-title":"Languages and Compilers for Parallel Computing","author":"Y. Zhang","year":"2008","unstructured":"Zhang, Y., Sreedhar, V., Zhu, W., Sarkar, V., Gao, G.: Minimum Lock Assignment: A Method for Exploiting Concurrency among Critical Sections. In: Amaral, J.N. (ed.) LCPC 2008. LNCS, vol.\u00a05335, pp. 141\u2013155. Springer, Heidelberg (2008)"}],"container-title":["Lecture Notes in Computer Science","Programming Languages and Systems"],"original-title":[],"link":[{"URL":"http:\/\/link.springer.com\/content\/pdf\/10.1007\/978-3-642-28869-2_17.pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,6,21]],"date-time":"2023-06-21T10:09:17Z","timestamp":1687342157000},"score":1,"resource":{"primary":{"URL":"http:\/\/link.springer.com\/10.1007\/978-3-642-28869-2_17"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2012]]},"ISBN":["9783642288685","9783642288692"],"references-count":20,"URL":"https:\/\/doi.org\/10.1007\/978-3-642-28869-2_17","relation":{},"ISSN":["0302-9743","1611-3349"],"issn-type":[{"type":"print","value":"0302-9743"},{"type":"electronic","value":"1611-3349"}],"subject":[],"published":{"date-parts":[[2012]]}}}