Better Predicates and Heuristics for Improved Commutativity Synthesis

Adam Chen, Parisa Fathololumi, Mihai Nicola, Jared Pincus, Tegan Brennan, Eric Koskinen

Research output: Chapter in Book/Report/Conference proceedingConference contributionpeer-review

Abstract

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.

Original languageEnglish
Title of host publicationAutomated Technology for Verification and Analysis - 21st International Symposium, ATVA 2023, Proceedings
EditorsÉtienne André, Jun Sun
Pages93-113
Number of pages21
DOIs
StatePublished - 2023
Event21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023 - Singapore, Singapore
Duration: 24 Oct 202327 Oct 2023

Publication series

NameLecture Notes in Computer Science (including subseries Lecture Notes in Artificial Intelligence and Lecture Notes in Bioinformatics)
Volume14216 LNCS
ISSN (Print)0302-9743
ISSN (Electronic)1611-3349

Conference

Conference21st International Symposium on Automated Technology for Verification and Analysis, ATVA 2023
Country/TerritorySingapore
CitySingapore
Period24/10/2327/10/23

Fingerprint

Dive into the research topics of 'Better Predicates and Heuristics for Improved Commutativity Synthesis'. Together they form a unique fingerprint.

Cite this