Universal Construction for Linearizable but Not Strongly Linearizable Concurrent Objects

Universal Construction for Linearizable but Not Strongly Linearizable Concurrent Objects

연구 분야: Verification

학회: International Symposium on Dependable Software Engineering: Theories, Tools, and Applications

Strong linearizability is a variant of linearizability and is more suitable for verification. In this paper we investigate the following two problems: (1) for which deterministic sequential specifications there exist linearizable but not strongly linearizable objects; (2) can we capture any violation scheme of strong linearizability for practical objects that are linearizable but not strongly linearizable. To deal with the first problem, we propose two classes of deterministic sequential specifications called inclusively-permutative sequential specifications and exclusively-permutative sequential specifications. The first class of sequential specifications contains sequential specifications of counter, register, max-register, snapshot, set, queue, stack and priority queue. The second class of sequential specifications contains sequential specifications of blocking queue, blocking stack and blocking priority queue. To establish these results, we propose a uniform methodology to construct a wait-free, linearizable but not strongly linearizable object for these two classes of sequential specifications. Our universal construction is based on the classical universal construction, and it additionally permits each operation to change the “take-effect-order” of previous operations. To deal with the second problem, we use bi-branch distinguishable executions to represent violations of strong linearizability. We investigate eight objects that are linearizable but not strongly linearizable, and we show that for each object, it has a pair of bi-branch distinguishable executions such that our universal construction can generate another pair of bi-branch distinguishable executions with the same set of histories.