{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T12:40:01Z","timestamp":1749732001983,"version":"3.41.0"},"reference-count":16,"publisher":"Association for Computing Machinery (ACM)","issue":"3","content-domain":{"domain":["dl.acm.org"],"crossmark-restriction":true},"short-container-title":["Form. Asp. Comput."],"published-print":{"date-parts":[[2025,9,30]]},"abstract":"<jats:p>Waitfree linearization of data objects was introduced by Herlihy in 1991. The present article proposes an algorithm for waitfree linearization of a possibly nondeterministic data object in bounded memory, together with a complete proof of correctness supported by the proof assistant PVS. The project is exceptional in that the proofs of 70 invariants are recorded systematically, and that waitfree progress is quantified in waitfree complexity and is formally proved.<\/jats:p>","DOI":"10.1145\/3725535","type":"journal-article","created":{"date-parts":[[2025,4,3]],"date-time":"2025-04-03T10:55:26Z","timestamp":1743677726000},"page":"1-26","update-policy":"https:\/\/doi.org\/10.1145\/crossmark-policy","source":"Crossref","is-referenced-by-count":0,"title":["Waitfree Linearization of an Arbitrary Data Object"],"prefix":"10.1145","volume":"37","author":[{"ORCID":"https:\/\/orcid.org\/0000-0002-1413-4320","authenticated-orcid":false,"given":"Wim Hendrik","family":"Hesselink","sequence":"first","affiliation":[{"name":"Computer Science, University of Groningen, Groningen, Netherlands"}],"role":[{"role":"author","vocabulary":"crossref"}]}],"member":"320","published-online":{"date-parts":[[2025,6,12]]},"reference":[{"key":"e_1_3_2_2_2","doi-asserted-by":"crossref","unstructured":"K. R. Apt F. S. de Boer and E.-R. Olderog. 2009. Verification of Sequential and Concurrent Programs. Springer New York.","DOI":"10.1007\/978-1-84882-745-5"},{"key":"e_1_3_2_3_2","doi-asserted-by":"crossref","unstructured":"M. Abadi and L. Lamport. 1991. The existence of refinement mappings. Theor. Comput. Sci. 82 2 (1991) 253\u2013284.","DOI":"10.1016\/0304-3975(91)90224-P"},{"key":"e_1_3_2_4_2","doi-asserted-by":"crossref","unstructured":"K. M. Chandy and J. Misra. 1988. Parallel Program Design A Foundation. Addison\u2013Wesley.","DOI":"10.1007\/978-1-4613-9668-0_6"},{"key":"e_1_3_2_5_2","doi-asserted-by":"crossref","unstructured":"E. W. Dijkstra. 1965. Solution of a problem in concurrent programming control. Commun. ACM 8 9 (1965) 569.","DOI":"10.1145\/365559.365617"},{"key":"e_1_3_2_6_2","doi-asserted-by":"crossref","unstructured":"W. H. Hesselink and P. A. Buhr. 2023. MCSH a lock with the standard interface. ACM Transactions on Parallel Computing 10 2 (2023) 1\u201323. Article number 11.","DOI":"10.1145\/3584696"},{"key":"e_1_3_2_7_2","doi-asserted-by":"crossref","unstructured":"M. Herlihy. 1991. Wait\u2013free synchronization. ACM Trans. Program. Lang. Syst. 13 1 (1991) 124\u2013149.","DOI":"10.1145\/114005.102808"},{"key":"e_1_3_2_8_2","doi-asserted-by":"crossref","unstructured":"M. Herlihy. 1993. A methodology for implementing highly concurrent data objects. ACM Trans. Program. Lang. Syst. 15 5 (1993) 745\u2013770.","DOI":"10.1145\/161468.161469"},{"key":"e_1_3_2_9_2","doi-asserted-by":"crossref","unstructured":"W. H. Hesselink. 1994. Wait\u2013free linearization with an assertional proof. Distr. Comput. 8 2 (1994) 65\u201380.","DOI":"10.1007\/BF02280829"},{"key":"e_1_3_2_10_2","doi-asserted-by":"crossref","unstructured":"W. H. Hesselink. 1995. Wait\u2013free linearization with a mechanical proof. Distr. Comput. 9 1 (1995) 21\u201336.","DOI":"10.1007\/BF01784240"},{"key":"e_1_3_2_11_2","doi-asserted-by":"publisher","unstructured":"W. H. Hesselink. 2017. Tournaments for mutual exclusion: Verification and concurrent complexity. Formal Aspects of Comput. 29 5 (2017) 833\u2013852. DOI:10.1007\/s00165-016-0407-x","DOI":"10.1007\/s00165-016-0407-x"},{"key":"e_1_3_2_12_2","doi-asserted-by":"crossref","unstructured":"W. H. Hesselink. 2022. Trylock a case for temporal logic and eternity variables. Science of Computer Programming 216 C (102767) 1\u201312.","DOI":"10.1016\/j.scico.2021.102767"},{"key":"e_1_3_2_13_2","unstructured":"W. H. Hesselink. 2024. PVS proof script for waitfree linearization. Retrieved from http:\/\/wimhesselink.nl\/mechver\/waitfreelinear"},{"key":"e_1_3_2_14_2","unstructured":"M. Herlihy and N. Shavit. 2008. The Art of Multiprocessor Programming. Morgan Kaufmann Publishers."},{"key":"e_1_3_2_15_2","doi-asserted-by":"crossref","unstructured":"L. Lamport. 1986. On interprocess communication. Parts I and II. Distr. Comput. 1 1 (1986) 77\u2013101.","DOI":"10.1007\/BF01786228"},{"key":"e_1_3_2_16_2","doi-asserted-by":"crossref","unstructured":"S. Owicki and D. Gries. 1976. An axiomatic proof technique for parallel programs. Acta Inf. 6 (1976) 319\u2013340.","DOI":"10.1007\/BF00268134"},{"key":"e_1_3_2_17_2","unstructured":"S. Owre N. Shankar J. M. Rushby and D. W. J. Stringer-Calvert. 2020. PVS Version 7.1 System Guide Prover Guide PVS Language Reference. Retrieved from http:\/\/pvs.csl.sri.com accessed 1 Dec. 2021."}],"container-title":["Formal Aspects of Computing"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/dl.acm.org\/doi\/pdf\/10.1145\/3725535","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2025,6,12]],"date-time":"2025-06-12T12:22:35Z","timestamp":1749730955000},"score":1,"resource":{"primary":{"URL":"https:\/\/dl.acm.org\/doi\/10.1145\/3725535"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2025,6,12]]},"references-count":16,"journal-issue":{"issue":"3","published-print":{"date-parts":[[2025,9,30]]}},"alternative-id":["10.1145\/3725535"],"URL":"https:\/\/doi.org\/10.1145\/3725535","relation":{},"ISSN":["0934-5043","1433-299X"],"issn-type":[{"type":"print","value":"0934-5043"},{"type":"electronic","value":"1433-299X"}],"subject":[],"published":{"date-parts":[[2025,6,12]]},"assertion":[{"value":"2024-04-25","order":0,"name":"received","label":"Received","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-03-18","order":2,"name":"accepted","label":"Accepted","group":{"name":"publication_history","label":"Publication History"}},{"value":"2025-06-12","order":3,"name":"published","label":"Published","group":{"name":"publication_history","label":"Publication History"}}]}}