Synthesizing Precise and Useful Commutativity Conditions
- PDF / 1,434,631 Bytes
- 27 Pages / 439.37 x 666.142 pts Page_size
- 100 Downloads / 174 Views
Synthesizing Precise and Useful Commutativity Conditions Kshitij Bansal1 · Eric Koskinen2 · Omer Tripp3 Received: 20 June 2020 / Accepted: 27 June 2020 © Springer Nature B.V. 2020
Abstract Reasoning about commutativity between data-structure operations is an important problem with many applications. In the sequential setting, commutativity can be used to reason about the correctness of refactoring, compiler transformations, and identify instances of nondeterminism. In parallel contexts, commutativity dates back to the database (Weihl in IEEE Trans Comput 37(12):1488–1505, 1988) and compilers (Rinard and Diniz in ACM Trans Program Lang Syst 19(6):942–991, 1997) communities and, more recently, appears in optimistic parallelization (Herlihy and Koskinen in Proceedings of the 13th ACM SIGPLAN symposium on principles and practice of parallel programming, 2008), dynamic concurrency (Tripp et al. in Proceedings of the 33rd ACM SIGPLAN conference on programming language design and implementation, PLDI ’12, New York, NY, USA, ACM, pp 145–156, 2012; Dimitrov et al. in Proceedings of the 35th ACM SIGPLAN conference on programming language design and implementation, 2014), scalable systems (Clements et al. in ACM Trans Comput Syst 32(4):10, 2015) and even smart contracts (Dickerson et al. in Proceedings of the ACM symposium on principles of distributed computing, PODC ’17, New York, NY, USA, ACM, pp 303–312, 2017). There have been research results on automatic generation of commutativity conditions, yet we are unaware of any fully automated technique to generate conditions that are both sound and effective. We have designed such a technique, driven by an algorithm that iteratively refines a conservative approximation of the commutativity (and non-commutativity) condition for a pair of methods into an increasingly precise version. The algorithm terminates if/when the entire state space has been considered, and can be aborted at any time to obtain a partial yet sound commutativity condition. We have generalized our work to left-/right-movers (Lipton in Commun ACM 8(12):717–721, 1975) and proved relative completeness. We describe aspects of our technique that lead to useful commutativity conditions, including how predicates are selected during refinement and heuristics that impact the output shape of the condition. We have implemented our technique in a prototype open-
This article extends our prior work [3], with the addition of proofs (Theorems 1 and 2), support for left- and right-movers (Sect. 6), and a new set of applications (Sect. 9), including memories and lock-based synchronization, transactional memory, distributed systems, refactoring, verification, and code synthesis. K. Bansal was partially supported by NSF award #1228768. E. Koskinen was partially supported by NSF CCF Award #1421126, CCF Award #1618542, and CCF Award #1813745, and some of the work was done while he was at New York University and at IBM Research. K. Bansal was at New York University when part of the work was completed. The work by O. Tripp was done
Data Loading...
