--- _id: '1832' abstract: - lang: eng text: 'Linearizability of concurrent data structures is usually proved by monolithic simulation arguments relying on the identification of the so-called linearization points. Regrettably, such proofs, whether manual or automatic, are often complicated and scale poorly to advanced non-blocking concurrency patterns, such as helping and optimistic updates. In response, we propose a more modular way of checking linearizability of concurrent queue algorithms that does not involve identifying linearization points. We reduce the task of proving linearizability with respect to the queue specification to establishing four basic properties, each of which can be proved independently by simpler arguments. As a demonstration of our approach, we verify the Herlihy and Wing queue, an algorithm that is challenging to verify by a simulation proof. ' article_number: '20' article_processing_charge: No article_type: original author: - first_name: Soham full_name: Chakraborty, Soham last_name: Chakraborty - first_name: Thomas A full_name: Henzinger, Thomas A id: 40876CD8-F248-11E8-B48F-1D18A9856A87 last_name: Henzinger orcid: 0000−0002−2985−7724 - first_name: Ali full_name: Sezgin, Ali last_name: Sezgin - first_name: Viktor full_name: Vafeiadis, Viktor last_name: Vafeiadis citation: ama: Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 2015;11(1). doi:10.2168/LMCS-11(1:20)2015 apa: Chakraborty, S., Henzinger, T. A., Sezgin, A., & Vafeiadis, V. (2015). Aspect-oriented linearizability proofs. Logical Methods in Computer Science. International Federation of Computational Logic. https://doi.org/10.2168/LMCS-11(1:20)2015 chicago: Chakraborty, Soham, Thomas A Henzinger, Ali Sezgin, and Viktor Vafeiadis. “Aspect-Oriented Linearizability Proofs.” Logical Methods in Computer Science. International Federation of Computational Logic, 2015. https://doi.org/10.2168/LMCS-11(1:20)2015. ieee: S. Chakraborty, T. A. Henzinger, A. Sezgin, and V. Vafeiadis, “Aspect-oriented linearizability proofs,” Logical Methods in Computer Science, vol. 11, no. 1. International Federation of Computational Logic, 2015. ista: Chakraborty S, Henzinger TA, Sezgin A, Vafeiadis V. 2015. Aspect-oriented linearizability proofs. Logical Methods in Computer Science. 11(1), 20. mla: Chakraborty, Soham, et al. “Aspect-Oriented Linearizability Proofs.” Logical Methods in Computer Science, vol. 11, no. 1, 20, International Federation of Computational Logic, 2015, doi:10.2168/LMCS-11(1:20)2015. short: S. Chakraborty, T.A. Henzinger, A. Sezgin, V. Vafeiadis, Logical Methods in Computer Science 11 (2015). date_created: 2018-12-11T11:54:15Z date_published: 2015-04-01T00:00:00Z date_updated: 2023-02-23T10:38:13Z day: '01' ddc: - '000' department: - _id: ToHe doi: 10.2168/LMCS-11(1:20)2015 ec_funded: 1 file: - access_level: open_access checksum: 7370e164d0a731f442424a92669efc34 content_type: application/pdf creator: system date_created: 2018-12-12T10:11:27Z date_updated: 2020-07-14T12:45:17Z file_id: '4881' file_name: IST-2015-390-v1+1_1502.07639.pdf file_size: 380203 relation: main_file file_date_updated: 2020-07-14T12:45:17Z has_accepted_license: '1' intvolume: ' 11' issue: '1' language: - iso: eng license: https://creativecommons.org/licenses/by-nd/4.0/ month: '04' oa: 1 oa_version: Published Version project: - _id: 25832EC2-B435-11E9-9278-68D0E5697425 call_identifier: FWF grant_number: S 11407_N23 name: Rigorous Systems Engineering - _id: 25EE3708-B435-11E9-9278-68D0E5697425 call_identifier: FP7 grant_number: '267989' name: Quantitative Reactive Modeling publication: Logical Methods in Computer Science publication_status: published publisher: International Federation of Computational Logic publist_id: '5271' pubrep_id: '390' quality_controlled: '1' related_material: record: - id: '2328' relation: earlier_version status: public scopus_import: 1 status: public title: Aspect-oriented linearizability proofs tmp: image: /image/cc_by_nd.png legal_code_url: https://creativecommons.org/licenses/by-nd/4.0/legalcode name: Creative Commons Attribution-NoDerivatives 4.0 International (CC BY-ND 4.0) short: CC BY-ND (4.0) type: journal_article user_id: 2DF688A6-F248-11E8-B48F-1D18A9856A87 volume: 11 year: '2015' ...