Decomposable relaxation for concurrent data structures

DOI10.1007/978-3-319-51963-0_15MaRDI QIDQ2971134zbMATH OpenOpenAlexFDO

Authors Chao Wang, Yi Lv, Peng Wu

Publication date 4 April 2017

Published in SOFSEM 2017: Theory and Practice of Computer Science (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1007/978-3-319-51963-0_15

Mathematics Subject Classification ID

Data structures (68P05) Formal languages and automata (68Q45) Specification and verification (program logics, model checking, etc.) (68Q60) Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.) (68Q85)

Recommendations

• Quantitative relaxation of concurrent data structures
• The computability of relaxed data structures: queues and stacks as examples
• The computability of relaxed data structures: queues and stacks as examples
• An integrated specification and verification technique for highly concurrent data structures
• Verifying concurrent data structures by simulation

Cites work

• An integrated specification and verification technique for highly concurrent data structures
• Aspect-oriented linearizability proofs
• Decomposable relaxation for concurrent data structures
• Quantitative relaxation of concurrent data structures
• Quasi-linearizability is undecidable
• Verifying concurrent programs against sequential specifications

Cited in

(6)

• Quantitative relaxation of concurrent data structures
• Decomposable relaxation for concurrent data structures
• scientific article; zbMATH DE number 437540 (Why is no real title available?)
• The computability of relaxed data structures: queues and stacks as examples
• The computability of relaxed data structures: queues and stacks as examples
• Monotonically relaxing concurrent data-structure semantics for increasing performance: an efficient 2D design framework

This page was built for publication: Decomposable relaxation for concurrent data structures

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