  Reasoning about commutativity between data-structure operations is an
important problem with applications including parallelizing compilers,
optimistic parallelization and, more recently, Ethereum smart contracts. 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 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 through two case studies: (i) We
synthesize commutativity conditions for a range of data structures including
Set, HashTable, Accumulator, Counter, and Stack. (ii) We consider an Ethereum
smart contract called BlockKing, and show that Servois can detect serious
concurrency-related vulnerabilities and guide developers to construct robust
and efficient implementations.
