Trace-based derivation of a scalable lock-free stack algorithm
type: Item
instance of: scholarly article
title: Trace-based derivation of a scalable lock-free stack algorithm
zbMATH Open document ID: 1165.68064
author: Lindsay Groves
author: Robert Colvin
published in: Formal Aspects of Computing
publication date: 2009-05-27T00:00:00Z
Mathematics Subject Classification ID: 68W05
zbMATH DE Number: 5558118
zbMATH Keywords: elimination process
zbMATH Keywords: elimination algorithm
zbMATH Keywords: Lipton's reduction method
describes a project that uses: PVS
describes a project that uses: Atomizer
describes a project that uses: Z
MaRDI profile type: Publication
full work available at URL: s00165-008-0092-5
OpenAlex ID: W1996684662
cites work: Distributed cooperation with action systems
cites work: Encoding, decoding and data refinement
cites work: Relational concurrent refinement
cites work: Formal Techniques for Networked and Distributed Systems – FORTE 2004
cites work: A refinement calculus for shared-variable parallel and distributed programming
cites work: Data Refinement
cites work: Atomizer: A dynamic atomicity checker for multithreaded programs
cites work: Randomized wait-free concurrent objects (extended abstract)
cites work: A scalable lock-free stack algorithm
cites work: Reduction
cites work: Forward and backward simulations. I. Untimed Systems
cites work: Q3126969
cites work: Data refinement by calculation
cites work: Practical implementations of non-blocking synchronization primitives
cites work: Q4301161
cites work: Nonblocking algorithms and preemption-safe locking on multiprogrammed shared memory multiprocessors
cites work: Q4278674
cites work: Q3995087
cites work: The Rely-Guarantee method for verifying shared variable concurrent programs
DOI: 10.1007/S00165-008-0092-5
description: scientific article; zbMATH DE number 5558118