Strict linearizability and abstract atomicity

DOI10.1142/S0129054121500015MaRDI QIDQ5859670zbMATH OpenFDO

Authors Tangliu Wen, Jie Peng, Jinyun Xue, Zhen You, Lan Song

Publication date 19 April 2021

Published in International Journal of Foundations of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1142/S0129054121500015

zbMATH Keywords

observational equivalenceatomicitydata abstractionlinearizabilityconcurrent objects

Mathematics Subject Classification ID

Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Abstraction for Concurrent Objects
• Abstraction for concurrent objects
• On abstraction and compositionality for weak-memory linearisability
• Relating trace refinement and linearizability
• Proving Linearizability Via Non-atomic Refinement

Cites work

• scientific article; zbMATH DE number 2013836 (Why is no real title available?)
• A semantics for concurrent separation logic
• Abstraction for concurrent objects
• Aspect-oriented linearizability proofs
• Atomizer: a dynamic atomicity checker for multithreaded programs
• How to Make a Multiprocessor Computer That Correctly Executes Multiprocess Programs
• How to write a 21\(^{\text{st}}\) century proof
• Monitoring Atomicity in Concurrent Programs
• Parameterised linearisability
• Proof of correctness of data representations
• Quantitative relaxation of concurrent data structures
• Reduction
• The serializability of concurrent database updates
• Transactions for software model checking
• Using refinement calculus techniques to prove linearizability

Cited in

(9)

• The limits of helping in non-volatile memory data structures
• Nearly \(k\)-universal words -- investigating a part of Simon's congruence
• Abstraction for Concurrent Objects
• Liveness-Preserving Atomicity Abstraction
• On abstraction and compositionality for weak-memory linearisability
• Abstraction for concurrent objects
• Putting strong linearizability in context: preserving hyperproperties in programs that use concurrent objects
• Proving Linearizability Via Non-atomic Refinement
• Relating trace refinement and linearizability

Describes a project that uses

Uses Software

• Atomizer

This page was built for publication: Strict linearizability and abstract atomicity

Report a bug (only for logged in users!)Click here to report a bug for this page (MaRDI item Q5859670)