Verifying atomicity via data independence
Verifying atomicity via data independence
复制标题
通过数据独立性验证原子性
DOI：
--
复制
发表时间：
2014
期刊：
影响因子：
--
通讯作者：
Martin T. Vechev
中科院分区：
文献类型：
--
作者：
Ohad Shacham;Eran Yahav;Guy Golan;A. Aiken;N. Bronson;Shmuel Sagiv;Martin T. Vechev
提出了一种自动验证组合并发操作原子性的技术。我们的方法背后的主要观察是，在实践中发生的许多组合并发操作是数据独立的。也就是说，组合操作的控制流不依赖于特定的输入值。虽然验证数据独立性在一般情况下是不可确定的，但我们提供了简洁的充分条件，可用于将组合操作建立为数据独立的。我们表明，对于并发映射的常见情况，数据独立性将验证线性性的难题降低为可以用有限数量的键和值有效解决的验证问题。我们在一个名为VINE的工具中实现了我们的方法，并对来自57个实际应用程序（112个组合操作）的所有组合操作进行了评估。我们表明，许多组合操作（112个操作中的49个）是数据独立的，并且自动验证其中30个是可线性化的，其余19个违反线性化，可以修复，然后随后自动验证。此外，我们展示了其余63个操作是不可线性化的，从而表明数据独立性并不限制编写现实的可线性化组合操作的表达性。
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 occur 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 reduces 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 evaluated it on all composed operations from 57 real-world applications (112 composed operations). We show that many composed operations (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 automatically verified. Moreover, we show that the remaining 63 operations are not linearizable, thus indicating that data independence does not limit the expressiveness of writing realistic linearizable composed operations.