{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,7,30]],"date-time":"2025-07-30T15:36:09Z","timestamp":1753889769047,"version":"3.41.2"},"reference-count":23,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2011,9,2]],"date-time":"2011-09-02T00:00:00Z","timestamp":1314921600000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>We are interested in identifying and enforcing the isolation requirements of\na concurrent program, i.e., concurrency control that ensures that the program\nmeets its specification. The thesis of this paper is that this can be done\nsystematically starting from a sequential proof, i.e., a proof of correctness\nof the program in the absence of concurrent interleavings. We illustrate our\nthesis by presenting a solution to the problem of making a sequential library\nthread-safe for concurrent clients. We consider a sequential library annotated\nwith assertions along with a proof that these assertions hold in a sequential\nexecution. We show how we can use the proof to derive concurrency control that\nensures that any execution of the library methods, when invoked by concurrent\nclients, satisfies the same assertions. We also present an extension to\nguarantee that the library methods are linearizable or atomic.<\/jats:p>","DOI":"10.2168\/lmcs-7(3:10)2011","type":"journal-article","created":{"date-parts":[[2014,11,14]],"date-time":"2014-11-14T13:45:24Z","timestamp":1415972724000},"source":"Crossref","is-referenced-by-count":0,"title":["Logical Concurrency Control from Sequential Proofs"],"prefix":"10.46298","volume":"Volume 7, Issue 3","author":[{"given":"Jyotirmoy","family":"Deshmukh","sequence":"first","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"G.","family":"Ramalingam","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"ORCID":"https:\/\/orcid.org\/0000-0001-7684-6086","authenticated-orcid":false,"given":"Venkatesh-Prasad","family":"Ranganath","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]},{"given":"Kapil","family":"Vaswani","sequence":"additional","affiliation":[],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"25203","published-online":{"date-parts":[[2011,9,2]]},"reference":[{"issue":"4","key":"10.2168\/LMCS-7(3:10)2011_Yogi:TSE","doi-asserted-by":"crossref","first-page":"495","DOI":"10.1109\/TSE.2010.49","volume":"36","author":"Nels E. Beckman, Aditya V. Nori, Sriram","year":"2010","journal-title":"IEEE Trans. Software Eng."},{"key":"10.2168\/LMCS-7(3:10)2011_cherem08inferring","doi-asserted-by":"crossref","unstructured":"Sigmund Cherem, Trishul Chilimbi, and Sumit Gulwani. Inferring locks for atomic sections. InProc. of PLDI, 2008.","DOI":"10.1145\/1375581.1375619"},{"key":"10.2168\/LMCS-7(3:10)2011_Z3:TACAS","doi-asserted-by":"crossref","unstructured":"Leonardo Mendonca de Moura and Nikolaj Bj\u00f8rner. Z3: An efficient smt solver. InTACAS, pages 337-340, 2008.","DOI":"10.1007\/978-3-540-78800-3_24"},{"key":"10.2168\/LMCS-7(3:10)2011_deng02invariant","doi-asserted-by":"crossref","unstructured":"Xianghua Deng, Matthew B. Dwyer, John Hatcliff, and Masaaki Mizuno. Invariant-based specification, synthesis, and verification of synchronization in concurrent programs. InProc. of ICSE, pages 442-452, 2002.","DOI":"10.1145\/581339.581394"},{"key":"10.2168\/LMCS-7(3:10)2011_shaz09calculus","doi-asserted-by":"crossref","unstructured":"Tyfun Elmas, Serdar Tasiran, and Shaz Qadeer. A calculus of atomic sections. InProc. of POPL, 2009.","DOI":"10.1145\/1594834.1480885"},{"key":"10.2168\/LMCS-7(3:10)2011_emmi07allocation","doi-asserted-by":"crossref","unstructured":"Michael Emmi, Jeff Fischer, Ranjit Jhala, and Rupak Majumdar. Lock allocation. InProc. of POPL, 2007.","DOI":"10.1145\/1190216.1190260"},{"key":"10.2168\/LMCS-7(3:10)2011_flanagan05automatic","unstructured":"Cormac Flanagan and Stephen N. Freund. Automatic synchronization correction. InProc. of SCOOL, 2005."},{"key":"10.2168\/LMCS-7(3:10)2011_gulvani06synergy","doi-asserted-by":"crossref","unstructured":"Bhargav S. Gulavani, Thomas A. Henzinger, Yamini Kannan, Aditya V. Nori, and Sriram K. Rajamani. Synergy: A new algorithm for property checking. InProc. of FSE, November 2006.","DOI":"10.1145\/1181775.1181790"},{"key":"10.2168\/LMCS-7(3:10)2011_henzinger02lazy","doi-asserted-by":"crossref","unstructured":"T. A. Henzinger, R. Jhala, R. Majumdar, and G. Sutre. Lazy abstraction. InProc. of POPL, pages 58-70, 2002.","DOI":"10.1145\/565816.503279"},{"key":"10.2168\/LMCS-7(3:10)2011_BLAST:POPL04","doi-asserted-by":"crossref","unstructured":"Thomas A. Henzinger, Ranjit Jhala, Rupak Majumdar, and Kenneth L. McMillan. Abstractions from proofs. InProc. of POPL, pages 232-244, 2004.","DOI":"10.1145\/964001.964021"},{"issue":"3","key":"10.2168\/LMCS-7(3:10)2011_HerlihyWing","doi-asserted-by":"crossref","first-page":"463","DOI":"10.1145\/78969.78972","volume":"12","author":"Maurice P. Herlihy and Jeannette M. Wing","year":"1990","journal-title":"Proc. of ACM TOPLAS"},{"key":"10.2168\/LMCS-7(3:10)2011_Hicks06LockInference","unstructured":"Michael Hicks, Jeffrey S. Foster, and Polyvios Pratikakis. Lock inference for atomic sections. InFirst Workshop on Languages, Compilers, and Hardware Support for Transactional Computing, 2006."},{"key":"10.2168\/LMCS-7(3:10)2011_janjua06automaticCorrecting","unstructured":"Muhammad Umar Janjua and Alan Mycroft. Automatic correcting transformations for safety property violations. InProc. of Thread Verification, pages 111-116, 2006."},{"key":"10.2168\/LMCS-7(3:10)2011_mccloskey06autolocker","doi-asserted-by":"crossref","unstructured":"Bill McCloskey, Feng Zhou, David Gay, and Eric A. Brewer. Autolocker: Synchronization inference for atomic sections. InProc. of POPL, 2006.","DOI":"10.1145\/1111037.1111068"},{"issue":"1-3","key":"10.2168\/LMCS-7(3:10)2011_OHearn:TCS07","doi-asserted-by":"crossref","first-page":"271","DOI":"10.1016\/j.tcs.2006.12.035","volume":"375","author":"Peter W. O'Hearn","year":"2007","journal-title":"Theor. Comput. Sci."},{"key":"10.2168\/LMCS-7(3:10)2011_owicki76verifying","doi-asserted-by":"crossref","unstructured":"Susan Owicki and David Gries. Verifying properties of parallel programs : An axiomatic approach. InProc. of CACM, 1976.","DOI":"10.1145\/360051.360224"},{"key":"10.2168\/LMCS-7(3:10)2011_RazaEtAl:ESOP2009","doi-asserted-by":"crossref","unstructured":"Mohammad Raza, Cristiano Calcagno, and Philippa Gardner. Automatic parallelization with separation logic. InESOP, pages 348-362, 2009.","DOI":"10.1007\/978-3-642-00590-9_25"},{"key":"10.2168\/LMCS-7(3:10)2011_solar08sketching","doi-asserted-by":"crossref","unstructured":"Armando Solar-Lezama, Christopher Grant Jones, and Rastislav Bodik. Sketching concurrent data structures. InProc. of PLDI, pages 136-148, 2008.","DOI":"10.1145\/1375581.1375599"},{"key":"10.2168\/LMCS-7(3:10)2011_vaziri06associating","doi-asserted-by":"crossref","unstructured":"Mandana Vaziri, Frank Tip, and Julian Dolby. Associating synchronization constraints with data in an object-oriented language. InProc. of POPL, pages 334-345, 2006.","DOI":"10.1145\/1111320.1111067"},{"key":"10.2168\/LMCS-7(3:10)2011_vechev08derivingLinearizable","doi-asserted-by":"crossref","unstructured":"Martin Vechev and Eran Yahav. Deriving linearizable fine-grained concurrent objects. InIn Proc. of PLDI, pages 125-135, 2008.","DOI":"10.1145\/1375581.1375598"},{"key":"10.2168\/LMCS-7(3:10)2011_vechev08inferring","doi-asserted-by":"crossref","unstructured":"Martin Vechev, Eran Yahav, and Greta Yorsh. Inferring synchronization under limited observability. InProc. of TACAS, 2009.","DOI":"10.1007\/978-3-642-00768-2_13"},{"key":"10.2168\/LMCS-7(3:10)2011_VechevEtAl:POPL2010","doi-asserted-by":"crossref","unstructured":"Martin T. Vechev, Eran Yahav, and Greta Yorsh. Abstraction-guided synthesis of synchronization. InPOPL, pages 327-338, 2010.","DOI":"10.1145\/1707801.1706338"},{"key":"10.2168\/LMCS-7(3:10)2011_BOOK:WV01","doi-asserted-by":"crossref","unstructured":"Gerhard Weikum and Gottfried Vossen.Transactional Information Systems: Theory, Algorithms, and the Practice of Concurrency Control. Morgan Kaufmann, 2001.","DOI":"10.1016\/B978-155860508-4\/50005-3"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/986\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/986\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:00:43Z","timestamp":1681243243000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/986"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2011,9,2]]},"references-count":23,"URL":"https:\/\/doi.org\/10.2168\/lmcs-7(3:10)2011","relation":{"is-same-as":[{"id-type":"arxiv","id":"1107.4422","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1107.4422","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"type":"electronic","value":"1860-5974"}],"subject":[],"published":{"date-parts":[[2011,9,2]]},"article-number":"986"}}