arXiv subjects

Tangliu Wen

Publications and source records attributed to Tangliu Wen.

3 recordsLinked to original sources

arXiv2021

Verify Linearizability of Concurrent Stacks

Proving linearizability of concurrent data structures is crucial for ensuring their correctness, but is challenging especially for implementations that employ sophisticated synchronization techniques. In this paper, we propose a new proof technique for verifying linearizability of concurrent stacks. We first prove the soundness of the elimination mechanism, a common optimization used in concurrent stacks, which enables simplifying the linearizability proofs. We then present a stack theorem that reduces the problem of proving linearizability to establishing a set of conditions based on the happened-before order of operations. The key idea is to use an extended partial order to capture when a pop operation can observe the effect of a push operation. We apply our proof technique to verify two concurrent stack algorithms: the Treiber stack and the Time-Stamped stack, demonstrating its practicality. Our approach provides a systematic and compositional way to prove linearizability of concurrent stacks.

cs.SE↗

arXiv2018

Proving Linearizability Using Reduction

Lipton's reduction theory provides an intuitive and simple way for deducing the non-interference properties of concurrent programs, but it is difficult to directly apply the technique to verify linearizability of sophisticated fine-grained concurrent data structures. In this paper, we propose three reduction-based proof methods that can handle such data structures. The key idea behind our reduction methods is that an irreducible operation can be viewed as an atomic operation at a higher level of abstraction. This allows us to focus on the reduction properties of an operation related to its abstract semantics. We have successfully applied the methods to verify 11 concurrent data structures including the most challenging ones: the Herlihy and Wing queue, the HSY elimination-based stack, and the time-stamped queue, and the lazy list. Our methods inherit intuition and simplicity of Lipton's reduction, and concurrent data structures designers can easily and quickly learn to use the methods.

cs.PL↗

arXiv2018

Strict Linearizability and Abstract Atomicity

Linearizability is a commonly accepted consistency condition for concurrent objects. Filipović et al. show that linearizability is equivalent to observational refinement. However, linearizability does not permit concurrent objects to share memory spaces with their client programs. We show that linearizability (or observational refinement) can be broken even though a client program of an object accesses the shared memory spaces without interference from the methods of the object. In this paper, we present strict linearizability which lifts this limitation and can ensure client-side traces and final-states equivalence even in a relaxed program model allowing clients to directly access the states of concurrent objects. We also investigate several important properties of strict linearizability. At a high level of abstraction, a concurrent object can be viewed as a concurrent implementation of an abstract data type (ADT). We also present a correctness criterion for relating an ADT and its concurrent implementation, which is the combination of linearizability and data abstraction and can ensure observational equivalence. We also investigate its relationship with strict linearizability.

cs.SE↗