TY - GEN
T1 - Better Predicates and Heuristics for Improved Commutativity Synthesis
AU - Chen, Adam
AU - Fathololumi, Parisa
AU - Nicola, Mihai
AU - Pincus, Jared
AU - Brennan, Tegan
AU - Koskinen, Eric
N1 - Publisher Copyright:
© 2023, The Author(s), under exclusive license to Springer Nature Switzerland AG.
PY - 2023
Y1 - 2023
N2 - 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.
AB - 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.
UR - http://www.scopus.com/inward/record.url?scp=85175964096&partnerID=8YFLogxK
UR - http://www.scopus.com/inward/citedby.url?scp=85175964096&partnerID=8YFLogxK
U2 - 10.1007/978-3-031-45332-8_5
DO - 10.1007/978-3-031-45332-8_5
M3 - Conference contribution
AN - SCOPUS:85175964096
SN - 9783031453311
T3 - Lecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
SP - 93
EP - 113
BT - Automated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
A2 - André, Étienne
A2 - Sun, Jun
T2 - 21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023
Y2 - 24 October 2023 through 27 October 2023
ER -