Better Predicates and Heuristics for Improved Commutativity Synthesis.

Code commutativity has increasingly many applications including proof methodologies for concurrency, reductions, automated parallelization, distributed systems and blockchain smart contracts. While there has been some work on automatically generating commutativity conditions through abstraction refinement, the performance of such refinement algorithms critically depends on (i) the universe of predicates and (ii) the choice of the next predicate during search, and thus far this has not been examined in detail. In this paper, we improve commutativity synthesis by addressing these under-explored requirements. We prune the universe of predicates through a combination of better predicate generation, new a priori syntactic filtering, and through dynamic reduction of the search space. We also present new predicate selection heuristics: one based on look-ahead, and one that utilizes model counting to greedily cover the search space. Our work is embodied in the new commutativity synthesis tool Servois2, a generational improvement over the state-of-the-art tool Servois. Servois2 is implemented in a faster language and has support for CVC5 and Z3. We contribute new, non-trivial commutativity benchmarks. All of the new features in Servois2 are shown to either increase performance (geomean 3.58 × speedup) or simplify the conditions generated, when compared against Servois. We also show that our look-ahead heuristic leads to better scaling with respect to the number of predicates.