{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,10,4]],"date-time":"2026-10-04T18:04:09Z","timestamp":1791137049476,"version":"4.1.0"},"publisher-location":"New York, NY, USA","reference-count":37,"publisher":"ACM","license":[{"start":{"date-parts":[[2009,1,21]],"date-time":"2009-01-21T00:00:00Z","timestamp":1232496000000},"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":[],"published-print":{"date-parts":[[2009,1,21]]},"DOI":"10.1145\/1480881.1480886","type":"proceedings-article","created":{"date-parts":[[2009,1,20]],"date-time":"2009-01-20T09:41:38Z","timestamp":1232444498000},"page":"16-28","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":25,"title":["Proving that non-blocking algorithms don't block"],"prefix":"10.1145","author":[{"given":"Alexey","family":"Gotsman","sequence":"first","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Byron","family":"Cook","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Matthew","family":"Parkinson","sequence":"additional","affiliation":[{"name":"University of Cambridge, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]},{"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[{"name":"Microsoft Research, Cambridge, United Kingdom"}],"role":[{"vocabulary":"crossref","role":"author"}]}],"member":"320","published-online":{"date-parts":[[2009,1,21]]},"reference":[{"key":"e_1_3_2_1_1_1","doi-asserted-by":"publisher","DOI":"10.1145\/203095.201069"},{"key":"e_1_3_2_1_2_1","doi-asserted-by":"publisher","DOI":"10.1016\/0020-0190(85)90056-0"},{"key":"e_1_3_2_1_3_1","doi-asserted-by":"publisher","DOI":"10.1007\/11817963_35"},{"key":"e_1_3_2_1_4_1","doi-asserted-by":"publisher","DOI":"10.1006\/inco.1996.0056"},{"key":"e_1_3_2_1_5_1","doi-asserted-by":"publisher","DOI":"10.1109\/LICS.2007.30"},{"key":"e_1_3_2_1_6_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391468"},{"key":"e_1_3_2_1_7_1","series-title":"LNCS","first-page":"124","volume-title":"ICTAC'07: International Colloquium on Theoretical Aspects of Computing","author":"Colvin R.","year":"2007","unstructured":"R. Colvin and B. Dongol . Verifying lock-freedom using well-founded orders . In ICTAC'07: International Colloquium on Theoretical Aspects of Computing , volume 4711 of LNCS , pages 124 -- 138 . Springer , 2007 . R. Colvin and B. Dongol. Verifying lock-freedom using well-founded orders. In ICTAC'07: International Colloquium on Theoretical Aspects of Computing, volume 4711 of LNCS, pages 124--138. Springer, 2007."},{"key":"e_1_3_2_1_8_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190257"},{"key":"e_1_3_2_1_9_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-30232-2_7"},{"key":"e_1_3_2_1_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/11901433_16"},{"key":"e_1_3_2_1_11_1","doi-asserted-by":"publisher","DOI":"10.5555\/1762174.1762193"},{"key":"e_1_3_2_1_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/1250734.1250765"},{"key":"e_1_3_2_1_13_1","doi-asserted-by":"publisher","DOI":"10.5555\/645959.676137"},{"key":"e_1_3_2_1_14_1","doi-asserted-by":"publisher","DOI":"10.1145\/1007912.1007944"},{"key":"e_1_3_2_1_15_1","doi-asserted-by":"publisher","DOI":"10.1145\/114005.102808"},{"key":"e_1_3_2_1_16_1","doi-asserted-by":"publisher","DOI":"10.5555\/850929.851942"},{"key":"e_1_3_2_1_17_1","volume-title":"Morgan Kaufmann","author":"Herlihy M.","year":"2008","unstructured":"M. Herlihy and N. Shavit . The Art of Multiprocessor Programming . Morgan Kaufmann , 2008 . M. Herlihy and N. Shavit. The Art of Multiprocessor Programming. Morgan Kaufmann, 2008."},{"key":"e_1_3_2_1_18_1","first-page":"321","volume-title":"IFIP Congress","author":"Jones C. B.","year":"1983","unstructured":"C. B. Jones . Specification and design of (parallel) programs . In IFIP Congress , pages 321 -- 332 . North-Holland , 1983 . C. B. Jones. Specification and design of (parallel) programs. In IFIP Congress, pages 321--332. North-Holland, 1983."},{"key":"e_1_3_2_1_19_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-70545-1_10"},{"key":"e_1_3_2_1_20_1","doi-asserted-by":"publisher","DOI":"10.5555\/648065.747612"},{"key":"e_1_3_2_1_21_1","doi-asserted-by":"publisher","DOI":"10.5555\/2391451.2391479"},{"key":"e_1_3_2_1_22_1","doi-asserted-by":"publisher","DOI":"10.5555\/128869"},{"key":"e_1_3_2_1_23_1","doi-asserted-by":"publisher","DOI":"10.1145\/142111.964561"},{"key":"e_1_3_2_1_24_1","doi-asserted-by":"publisher","DOI":"10.5555\/646704.701881"},{"key":"e_1_3_2_1_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/564870.564881"},{"key":"e_1_3_2_1_26_1","doi-asserted-by":"publisher","DOI":"10.1145\/248052.248106"},{"key":"e_1_3_2_1_27_1","doi-asserted-by":"publisher","DOI":"10.1023\/A:1008624904634"},{"key":"e_1_3_2_1_28_1","doi-asserted-by":"publisher","DOI":"10.1016\/j.tcs.2006.12.035"},{"key":"e_1_3_2_1_29_1","first-page":"123","volume-title":"transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems","author":"Pnueli A.","year":"1985","unstructured":"A. Pnueli . In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems , pages 123 -- 144 . Springer , 1985 . A. Pnueli. In transition from global to modular temporal reasoning about programs. In Logics and Models of Concurrent Systems, pages 123--144. Springer, 1985."},{"key":"e_1_3_2_1_30_1","first-page":"55","volume-title":"LICS'02: Symposium on Logic in Computer Science","author":"Reynolds J.","year":"2002","unstructured":"J. Reynolds . Separation logic : A logic for shared mutable data structures . In LICS'02: Symposium on Logic in Computer Science , pages 55 -- 74 . IEEE, 2002 . J. Reynolds. Separation logic: A logic for shared mutable data structures. In LICS'02: Symposium on Logic in Computer Science, pages 55--74. IEEE, 2002."},{"key":"e_1_3_2_1_31_1","unstructured":"S. Sarkar P. Sewell F. Zappa Nardelli S. Owens T. Ridge T. Braibant M. Myreen and J. Alglave. The semantics of x86 multiprocessor machine code. This volume.  S. Sarkar P. Sewell F. Zappa Nardelli S. Owens T. Ridge T. Braibant M. Myreen and J. Alglave. The semantics of x86 multiprocessor machine code. This volume."},{"issue":"1","key":"e_1_3_2_1_32_1","first-page":"17","article-title":"Four-slot fully asynchronous communication mechanism","volume":"137","author":"Simpson H.","year":"1990","unstructured":"H. Simpson . Four-slot fully asynchronous communication mechanism . IEE Proceedings , 137 ( 1 ): 17 -- 30 , 1990 . H. Simpson. Four-slot fully asynchronous communication mechanism. IEE Proceedings, 137(1):17--30, 1990.","journal-title":"IEE Proceedings"},{"key":"e_1_3_2_1_34_1","volume-title":"University of Cambridge Computer Laboratory","author":"Vafeiadis V.","year":"2008","unstructured":"V. Vafeiadis . Modular fine-grained concurrency verification. PhD Thesis , University of Cambridge Computer Laboratory , 2008 . V. Vafeiadis. Modular fine-grained concurrency verification. PhD Thesis, University of Cambridge Computer Laboratory, 2008."},{"key":"e_1_3_2_1_35_1","doi-asserted-by":"publisher","DOI":"10.5555\/2392200.2392220"},{"key":"e_1_3_2_1_36_1","doi-asserted-by":"publisher","DOI":"10.1016\/0168-0072(91)90066-U"},{"key":"e_1_3_2_1_37_1","doi-asserted-by":"publisher","DOI":"10.1145\/1375581.1375598"},{"key":"e_1_3_2_1_38_1","doi-asserted-by":"publisher","DOI":"10.1145\/1122971.1122994"}],"event":{"name":"POPL09: The 36th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages","location":"Savannah GA USA","acronym":"POPL09","sponsor":["SIGPLAN ACM Special Interest Group on Programming Languages","ACM Association for Computing Machinery","SIGACT ACM Special Interest Group on Algorithms and Computation Theory"]},"container-title":["Proceedings of the 36th annual ACM SIGPLAN-SIGACT symposium on Principles of programming languages"],"original-title":[],"link":[{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480886","content-type":"unspecified","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/1480881.1480886","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,18]],"date-time":"2025-06-18T09:29:59Z","timestamp":1750238999000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/1480881.1480886"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2009,1,21]]},"references-count":37,"alternative-id":["10.1145\/1480881.1480886","10.1145\/1480881"],"URL":"https:\/\/doi.org\/10.1145\/1480881.1480886","relation":{"is-identical-to":[{"id-type":"doi","id":"10.1145\/1594834.1480886","asserted-by":"object"}]},"subject":[],"published":{"date-parts":[[2009,1,21]]},"assertion":[{"value":"2009-01-21","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}