Verifying Atomicity via Data Independence

We present a technique for automatically verifying atomicity of composed concurrent operations. The main observation behind our approach is that many composed concurrent operations which oc-cur in practice are data-independent. That is, the control-flow of the composed operation does not depend on specific input values. While verifying data-independence is undecidable in the general case, we provide succint sufficient conditions that can be used to establish a composed operation as data-independent. We show that for the common case of concurrent maps, data-independence re-duces the hard problem of verifying linearizability to a verification problem that can be solved efficiently with a bounded number of keys and values. We implemented our approach in a tool called VINE and evalu-ated it on all composed operations from 57 real-world applications (112 composed operations). We show that many composed opera-tions (49 out of 112) are data-independent, and automatically verify 30 of them as linearizable and the rest 19 as having violations of linearizability that could be repaired and then subsequently auto-matically verified. Moreover, we show that the remaining 63 oper-ations are not linearizable, thus indicating that data independence does not limit the expressiveness of writing realistic linearizable composed operations. Categories and Subject Descriptors