| Article ID | Journal | Published Year | Pages | File Type |
|---|---|---|---|---|
| 6873794 | Information and Computation | 2018 | 18 Pages |
Abstract
In this work we demonstrate that verifying linearizability for certain fixed ADT specifications is reducible to control-state reachability, despite being harder for arbitrary ADTs. We effectuate this reduction for several of the most popular atomic objects. This reduction yields the first decidability results for verification without bounding the number of concurrent threads. Furthermore, it enables the application of existing safety-verification tools to linearizability verification.
Related Topics
Physical Sciences and Engineering
Computer Science
Computational Theory and Mathematics
Authors
Ahmed Bouajjani, Michael Emmi, Constantin Enea, Jad Hamza,