On reducing linearizability to state reachability

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.