Synthesizing Precise and Useful Commutativity Conditions

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 non-determinism. 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-source tool Servois. Our algorithm produces quantifier-free queries that are dispatched to a back-end SMT solver. We evaluate Servois first by synthesizing commutativity conditions for a range of data structures including Set, HashTable, Accumulator, Counter, and Stack. We then show several applications of our work including reasoning about memories and locks, finding vulnerabilities in Ethereum smart contracts, improving transactional memory performance, distributed applications, code refactoring, verification, and synthesis.