{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2024,6,24]],"date-time":"2024-06-24T23:15:09Z","timestamp":1719270909921},"reference-count":61,"publisher":"Association for Computing Machinery (ACM)","issue":"OOPSLA","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Proc. ACM Program. Lang."],"published-print":{"date-parts":[[2020,11,13]]},"abstract":"Modern highly-concurrent search data structures, such as search trees, obtain multi-core scalability and performance by having operations traverse the data structure without any synchronization. As a result, however, these algorithms are notoriously difficult to prove linearizable, which requires identifying a point in time in which the traversal's result is correct. The problem is that traversing the data structure as it undergoes modifications leads to complex behaviors, necessitating intricate reasoning about all interleavings of reads by traversals and writes mutating the data structure.<\/jats:p>\n In this paper, we present a general proof technique for proving unsynchronized traversals correct in a significantly simpler manner, compared to typical concurrent reasoning and prior proof techniques. Our framework relies only on sequential properties of traversals and on a conceptually simple and widely-applicable condition about the ways an algorithm's writes mutate the data structure. Establishing that a target data structure satisfies our condition requires only simple concurrent reasoning, without considering interactions of writes and reads. This reasoning can be further simplified by using our framework.<\/jats:p>\n To demonstrate our technique, we apply it to prove several interesting and challenging concurrent binary search trees: the logical-ordering AVL tree, the Citrus tree, and the full contention-friendly tree. Both the logical-ordering tree and the full contention-friendly tree are beyond the reach of previous approaches targeted at simplifying linearizability proofs.<\/jats:p>","DOI":"10.1145\/3428196","type":"journal-article","created":{"date-parts":[[2020,11,24]],"date-time":"2020-11-24T23:36:06Z","timestamp":1606260966000},"page":"1-29","update-policy":"http:\/\/dx.doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":6,"title":["Proving highly-concurrent traversals correct"],"prefix":"10.1145","volume":"4","author":[{"given":"Yotam M. Y.","family":"Feldman","sequence":"first","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Artem","family":"Khyzha","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Constantin","family":"Enea","sequence":"additional","affiliation":[{"name":"University of Paris Diderot, France"}]},{"given":"Adam","family":"Morrison","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"ORCID":"http:\/\/orcid.org\/0000-0002-4851-1075","authenticated-orcid":false,"given":"Aleksandar","family":"Nanevski","sequence":"additional","affiliation":[{"name":"IMDEA Software Institute, Spain"}]},{"given":"Noam","family":"Rinetzky","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]},{"given":"Sharon","family":"Shoham","sequence":"additional","affiliation":[{"name":"Tel Aviv University, Israel"}]}],"member":"320","published-online":{"date-parts":[[2020,11,13]]},"reference":[{"key":"e_1_2_2_1_1","first-page":"324","article-title":"An Integrated Specification and Verification Technique for Highly Concurrent Data Structures","author":"Abdulla Parosh Aziz","year":"2013","unstructured":"Parosh Aziz Abdulla, Fr\u00e9d\u00e9ric Haziza, Luk\u00e1s Hol\u00edk, Bengt Jonsson, and Ahmed Rezine. 2013. An Integrated Specification and Verification Technique for Highly Concurrent Data Structures. In TACAS. 324-338.","journal-title":"TACAS."},{"key":"e_1_2_2_2_1","first-page":"477","volume-title":"Comparison Under Abstraction for Verifying Linearizability. In CAV '07 (LNCS)","volume":"4590","author":"Amit Daphna","year":"2007","unstructured":"Daphna Amit, Noam Rinetzky, Thomas W. Reps, Mooly Sagiv, and Eran Yahav. 2007. Comparison Under Abstraction for Verifying Linearizability. In CAV '07 (LNCS), Vol. 4590. 477-490."},{"key":"e_1_2_2_3_1","doi-asserted-by":"publisher","DOI":"10.1145\/2611462.2611471"},{"key":"e_1_2_2_4_1","doi-asserted-by":"publisher","DOI":"10.1145\/1706299.1706305"},{"key":"e_1_2_2_5_1","doi-asserted-by":"publisher","DOI":"10.1145\/1040305.1040327"},{"key":"e_1_2_2_6_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-37036-6_17"},{"key":"e_1_2_2_7_1","volume-title":"ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II. 95-107","author":"Bouajjani Ahmed","year":"2015","unstructured":"Ahmed Bouajjani, Michael Emmi, Constantin Enea, and Jad Hamza. 2015. On Reducing Linearizability to State Reachability. In Automata, Languages, and Programming-42nd International Colloquium, ICALP 2015, Kyoto, Japan, July 6-10, 2015, Proceedings, Part II. 95-107."},{"key":"e_1_2_2_8_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-319-63390-9_28"},{"key":"e_1_2_2_9_1","doi-asserted-by":"publisher","DOI":"10.1145\/1693453.1693488"},{"key":"e_1_2_2_10_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_2"},{"key":"e_1_2_2_11_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555267"},{"key":"e_1_2_2_12_1","doi-asserted-by":"publisher","DOI":"10.1145\/2150976.2150998"},{"key":"e_1_2_2_13_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-40047-6_25"},{"key":"e_1_2_2_14_1","volume-title":"No Hot Spot Non-blocking Skip List. In ICDCS","author":"Crain Tyler","year":"2013","unstructured":"Tyler Crain, Vincent Gramoli, and Michel Raynal. 2013b. No Hot Spot Non-blocking Skip List. In ICDCS 2013."},{"key":"e_1_2_2_15_1","doi-asserted-by":"publisher","DOI":"10.1142\/S0129626416500158"},{"key":"e_1_2_2_16_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-44202-9_9"},{"key":"e_1_2_2_17_1","doi-asserted-by":"publisher","DOI":"10.1145\/2694344.2694359"},{"key":"e_1_2_2_18_1","doi-asserted-by":"publisher","DOI":"10.1109\/TPDS.2011.159"},{"key":"e_1_2_2_19_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555269"},{"key":"e_1_2_2_20_1","volume-title":"Henzinger","author":"Dragoi Cezara","year":"2013","unstructured":"Cezara Dragoi, Ashutosh Gupta, and Thomas A. Henzinger. 2013. Automatic Linearizability Proofs of Concurrent Objects with Cooperating Updates. In CAV '13 (LNCS), Vol. 8044. Springer, 174-190."},{"key":"e_1_2_2_21_1","volume-title":"Non-blocking Binary Search Trees. In PODC","author":"Ellen Faith","year":"2010","unstructured":"Faith Ellen, Panagiota Fatourou, Eric Ruppert, and Franck van Breugel. 2010. Non-blocking Binary Search Trees. In PODC 2010."},{"key":"e_1_2_2_22_1","volume-title":"DISC","author":"Feldman Yotam M. Y.","year":"2018","unstructured":"Yotam M. Y. Feldman, Constantin Enea, Adam Morrison, Noam Rinetzky, and Sharon Shoham. 2018. Order out of Chaos: Proving Linearizability Using Local Views. In DISC 2018."},{"key":"e_1_2_2_23_1","volume-title":"Proving Highly-Concurrent Traversals Correct. CoRR ( 2020 ). https:\/\/arxiv.org\/abs\/","author":"Feldman Yotam M. Y.","year":"2010","unstructured":"Yotam M. Y. Feldman, Artem Khyzha, Constantin Enea, Adam Morrison, Aleksandar Nanevski, Noam Rinetzky, and Sharon Shoham. 2020. Proving Highly-Concurrent Traversals Correct. CoRR ( 2020 ). https:\/\/arxiv.org\/abs\/ 2010.00911"},{"key":"e_1_2_2_25_1","doi-asserted-by":"publisher","DOI":"10.1145\/2688500.2688501"},{"key":"e_1_2_2_26_1","doi-asserted-by":"publisher","DOI":"10.5555\/645958.676105"},{"key":"e_1_2_2_27_1","volume-title":"OPODIS","author":"Heller Steve","year":"2005","unstructured":"Steve Heller, Maurice Herlihy, Victor Luchangco, Mark Moir, Bill Scherer, and Nir Shavit. 2005. A Lazy Concurrent List-based Set Algorithm. In OPODIS 2005."},{"key":"e_1_2_2_28_1","first-page":"242","article-title":"Aspect-Oriented Linearizability Proofs","author":"Henzinger Thomas A.","year":"2013","unstructured":"Thomas A. Henzinger, Ali Sezgin, and Viktor Vafeiadis. 2013. Aspect-Oriented Linearizability Proofs. In CONCUR. 242-256.","journal-title":"CONCUR."},{"key":"e_1_2_2_29_1","doi-asserted-by":"publisher","DOI":"10.5555\/1760631.1760646"},{"key":"e_1_2_2_30_1","volume-title":"The Art of Multiprocessor Programming","author":"Herlihy Maurice","unstructured":"Maurice Herlihy and Nir Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers Inc., San Francisco, CA, USA."},{"key":"e_1_2_2_31_1","doi-asserted-by":"crossref","unstructured":"M. P. Herlihy and J. M. Wing. 1990. Linearizability: a correctness condition for concurrent objects. 12 3 ( 1990 ).","DOI":"10.1145\/78969.78972"},{"key":"e_1_2_2_32_1","volume-title":"SPAA","author":"Shane","year":"2012","unstructured":"Shane V. Howley and Jeremy Jones. 2012. A Non-blocking Internal Binary Search Tree. In SPAA 2012."},{"key":"e_1_2_2_33_1","volume-title":"Specification and Design of (Parallel) Programs. In IFIP Congress. 321-332","author":"Jones Clif B.","year":"1983","unstructured":"Clif B. Jones. 1983. Specification and Design of (Parallel) Programs. In IFIP Congress. 321-332."},{"key":"e_1_2_2_34_1","doi-asserted-by":"publisher","unstructured":"Ralf Jung Robbert Krebbers Jacques-Henri Jourdan Ales Bizjak Lars Birkedal and Derek Dreyer. 2018. Iris from the ground up: A modular foundation for higher-order concurrent separation logic. J. Funct. Program. 28 ( 2018 ) e20. https:\/\/doi.org\/10.1017\/S0956796818000151 10.1017\/S0956796818000151","DOI":"10.1017\/S0956796818000151"},{"key":"e_1_2_2_35_1","doi-asserted-by":"publisher","DOI":"10.1145\/3371113"},{"key":"e_1_2_2_36_1","doi-asserted-by":"publisher","DOI":"10.1145\/3385412.3386029"},{"key":"e_1_2_2_37_1","doi-asserted-by":"publisher","unstructured":"Siddharth Krishna Dennis E. Shasha and Thomas Wies. 2018. Go with the flow: compositional abstractions for concurrent data structures. PACMPL 2 POPL ( 2018 ) 37 : 1-37 : 31. https:\/\/doi.org\/10.1145\/3158125 10.1145\/3158125","DOI":"10.1145\/3158125"},{"key":"e_1_2_2_38_1","doi-asserted-by":"crossref","unstructured":"Kfir Lev-Ari Gregory V. Chockler and Idit Keidar. 2015a. A Constructive Approach for Proving Data Structures' Linearizability. In DISC 205.","DOI":"10.1007\/978-3-662-48653-5_24"},{"key":"e_1_2_2_39_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-48653-5_24"},{"key":"e_1_2_2_40_1","doi-asserted-by":"publisher","DOI":"10.1145\/2429069.2429134"},{"key":"e_1_2_2_41_1","doi-asserted-by":"publisher","DOI":"10.1145\/2491956.2462189"},{"key":"e_1_2_2_42_1","doi-asserted-by":"publisher","DOI":"10.1145\/2168836.2168855"},{"key":"e_1_2_2_44_1","volume-title":"Slingwine","author":"McKenney Paul E.","year":"1998","unstructured":"Paul E. McKenney and John D. Slingwine. 1998. Read-copy update: using execution history to solve concurrency problems. In PDCS."},{"key":"e_1_2_2_45_1","volume-title":"High Performance Dynamic Lock-free Hash Tables and List-based Sets. In SPAA","author":"Michael Maged M.","year":"2002","unstructured":"Maged M. Michael. 2002. High Performance Dynamic Lock-free Hash Tables and List-based Sets. In SPAA 2002."},{"key":"e_1_2_2_46_1","doi-asserted-by":"publisher","DOI":"10.1145\/3360587"},{"key":"e_1_2_2_47_1","doi-asserted-by":"publisher","DOI":"10.1145\/2555243.2555256"},{"key":"e_1_2_2_48_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-540-28644-8_4"},{"key":"e_1_2_2_49_1","volume-title":"Verifying Linearizability with Hindsight. In PODC","author":"O'Hearn P. W.","year":"2010","unstructured":"P. W. O'Hearn, N. Rinetzky, M. T. Vechev, E. Yahav, and G. Yorsh. 2010. Verifying Linearizability with Hindsight. In PODC 2010."},{"key":"e_1_2_2_50_1","doi-asserted-by":"publisher","DOI":"10.1145\/360051.360224"},{"key":"e_1_2_2_51_1","doi-asserted-by":"publisher","DOI":"10.1145\/1190216.1190261"},{"key":"e_1_2_2_52_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_29"},{"key":"e_1_2_2_53_1","doi-asserted-by":"publisher","DOI":"10.1145\/2684464.2684472"},{"key":"e_1_2_2_54_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-662-46669-8_14"},{"key":"e_1_2_2_55_1","doi-asserted-by":"publisher","DOI":"10.1145\/2983990.2983999"},{"key":"e_1_2_2_56_1","doi-asserted-by":"publisher","DOI":"10.1145\/42201.42204"},{"key":"e_1_2_2_57_1","volume-title":"USENIX ATC","author":"Triplett Josh","year":"2011","unstructured":"Josh Triplett, Paul E. McKenney, and Jonathan Walpole. 2011. Resizable, Scalable, Concurrent Hash Tables via Relativistic Programming. In USENIX ATC 2011."},{"key":"e_1_2_2_58_1","volume-title":"Speedy Transactions in Multicore In-memory Databases. In SOSP","author":"Tu Stephen","year":"2013","unstructured":"Stephen Tu, Wenting Zheng, Eddie Kohler, Barbara Liskov, and Samuel Madden. 2013. Speedy Transactions in Multicore In-memory Databases. In SOSP 2013."},{"key":"e_1_2_2_59_1","doi-asserted-by":"publisher","DOI":"10.1145\/2500365.2500600"},{"key":"e_1_2_2_61_1","doi-asserted-by":"crossref","first-page":"335","DOI":"10.1007\/978-3-540-93900-9_27","volume-title":"Shape-Value Abstraction for Verifying Linearizability. In VMCAI '09: Proc. 10th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (LNCS)","volume":"5403","author":"Vafeiadis Viktor","year":"2009","unstructured":"Viktor Vafeiadis. 2009. Shape-Value Abstraction for Verifying Linearizability. In VMCAI '09: Proc. 10th Intl. Conf. on Verification, Model Checking, and Abstract Interpretation (LNCS), Vol. 5403. Springer, 335-348."},{"key":"e_1_2_2_62_1","doi-asserted-by":"publisher","DOI":"10.1007\/978-3-642-14295-6_40"},{"key":"e_1_2_2_64_1","first-page":"129","volume-title":"PPOPP '06","author":"Vafeiadis Viktor","year":"2016","unstructured":"Viktor Vafeiadis, Maurice Herlihy, Tony Hoare, and Marc Shapiro. 2016. Proving correctness of highly-concurrent linearisable objects. In PPOPP '06. ACM, 129-136."},{"key":"e_1_2_2_65_1","volume-title":"Poling: SMT Aided Linearizability Proofs. In Computer Aided Verification-27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. 3-19","author":"Zhu He","year":"2015","unstructured":"He Zhu, Gustavo Petri, and Suresh Jagannathan. 2015. Poling: SMT Aided Linearizability Proofs. In Computer Aided Verification-27th International Conference, CAV 2015, San Francisco, CA, USA, July 18-24, 2015, Proceedings, Part II. 3-19."}],"container-title":["Proceedings of the ACM on Programming Languages"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3428196","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2024,4,25]],"date-time":"2024-04-25T14:33:20Z","timestamp":1714055600000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3428196"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2020,11,13]]},"references-count":61,"journal-issue":{"issue":"OOPSLA","published-print":{"date-parts":[[2020,11,13]]}},"alternative-id":["10.1145\/3428196"],"URL":"https:\/\/doi.org\/10.1145\/3428196","relation":{},"ISSN":["2475-1421"],"issn-type":[{"value":"2475-1421","type":"electronic"}],"subject":[],"published":{"date-parts":[[2020,11,13]]},"assertion":[{"value":"2020-11-13","order":2,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}
