{"status":"ok","message-type":"work","message-version":"1.0.0","message":{"indexed":{"date-parts":[[2026,4,16]],"date-time":"2026-04-16T02:04:21Z","timestamp":1776305061646,"version":"3.50.1"},"reference-count":1,"publisher":"Centre pour la Communication Scientifique Directe (CCSD)","license":[{"start":{"date-parts":[[2015,4,1]],"date-time":"2015-04-01T00:00:00Z","timestamp":1427846400000},"content-version":"unspecified","delay-in-days":0,"URL":"https:\/\/arxiv.org\/licenses\/nonexclusive-distrib\/1.0"}],"funder":[{"DOI":"10.13039\/100014013","name":"UK Research and Innovation","doi-asserted-by":"crossref","award":["EP\/H005633\/1"],"award-info":[{"award-number":["EP\/H005633\/1"]}],"id":[{"id":"10.13039\/100014013","id-type":"DOI","asserted-by":"crossref"}]},{"DOI":"10.13039\/501100000780","name":"European Commission","doi-asserted-by":"crossref","award":["267989"],"award-info":[{"award-number":["267989"]}],"id":[{"id":"10.13039\/501100000780","id-type":"DOI","asserted-by":"crossref"}]}],"content-domain":{"domain":[],"crossmark-restriction":false},"short-container-title":[],"abstract":"<jats:p>Linearizability of concurrent data structures is usually proved by monolithic\nsimulation arguments relying on the identification of the so-called\nlinearization points. Regrettably, such proofs, whether manual or automatic,\nare often complicated and scale poorly to advanced non-blocking concurrency\npatterns, such as helping and optimistic updates. In response, we propose a\nmore modular way of checking linearizability of concurrent queue algorithms\nthat does not involve identifying linearization points. We reduce the task of\nproving linearizability with respect to the queue specification to establishing\nfour basic properties, each of which can be proved independently by simpler\narguments. As a demonstration of our approach, we verify the Herlihy and Wing\nqueue, an algorithm that is challenging to verify by a simulation proof.<\/jats:p>","DOI":"10.2168\/lmcs-11(1:20)2015","type":"journal-article","created":{"date-parts":[[2015,5,18]],"date-time":"2015-05-18T07:33:27Z","timestamp":1431934407000},"source":"Crossref","is-referenced-by-count":16,"title":["Aspect-oriented linearizability proofs"],"prefix":"10.46298","volume":"Volume 11, Issue 1","author":[{"given":"Soham","family":"Chakraborty","sequence":"first","affiliation":[]},{"given":"Thomas A.","family":"Henzinger","sequence":"additional","affiliation":[]},{"given":"Ali","family":"Sezgin","sequence":"additional","affiliation":[]},{"ORCID":"https:\/\/orcid.org\/0000-0001-8436-0334","authenticated-orcid":false,"given":"Viktor","family":"Vafeiadis","sequence":"additional","affiliation":[]}],"member":"25203","published-online":{"date-parts":[[2015,4,1]]},"reference":[{"key":"983:not-found"}],"container-title":["Logical Methods in Computer Science"],"original-title":[],"language":"en","link":[{"URL":"https:\/\/lmcs.episciences.org\/1051\/pdf","content-type":"application\/pdf","content-version":"vor","intended-application":"text-mining"},{"URL":"https:\/\/lmcs.episciences.org\/1051\/pdf","content-type":"unspecified","content-version":"vor","intended-application":"similarity-checking"}],"deposited":{"date-parts":[[2023,4,11]],"date-time":"2023-04-11T20:02:10Z","timestamp":1681243330000},"score":1,"resource":{"primary":{"URL":"https:\/\/lmcs.episciences.org\/1051"}},"subtitle":[],"short-title":[],"issued":{"date-parts":[[2015,4,1]]},"references-count":1,"URL":"https:\/\/doi.org\/10.2168\/lmcs-11(1:20)2015","relation":{"is-same-as":[{"id-type":"arxiv","id":"1502.07639","asserted-by":"subject"},{"id-type":"doi","id":"10.48550\/arXiv.1502.07639","asserted-by":"subject"}]},"ISSN":["1860-5974"],"issn-type":[{"value":"1860-5974","type":"electronic"}],"subject":[],"published":{"date-parts":[[2015,4,1]]},"article-number":"1051"}}