A scalable, correct time-stamped stack

DOI10.1145/2676726.2676963MaRDI QIDQ2819810zbMATH OpenOpenAlexFDO

Authors Mike Dodds, Andreas Haas, Christoph M. Kirsch

Publication date 29 September 2016

Published in Proceedings of the 42nd Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (Search for Journal in Brave)

Full work available at URL https://doi.org/10.1145/2676726.2676963

zbMATH Keywords

concurrent stacklinearizabilitytimestampsverification

Mathematics Subject Classification ID

Data structures (68P05)

Recommendations

• A scalable lock-free stack algorithm
• Bounded Concurrent Time-Stamping
• Aspect-oriented linearizability proofs
• Simple and efficient bounded concurrent timestamping and the traceable use abstraction
• Proving linearizability using forward simulations

Cited in

(5)

• A mechanized refinement proof of the Chase-Lev deque using a proof system
• Proving linearizability using partial orders
• Checking linearizability of concurrent priority queues
• Visibility and separability for a declarative linearizability proof of the timestamped stack
• Optimal concolic dynamic partial order reduction

Describes a project that uses

Uses Software

• Isabelle
• Scal

This page was built for publication: A scalable, correct time-stamped stack

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