Commutativity of data structure methods and program code applies to a wide variety of contexts, ranging from proof methodologies for concurrency (e.g. Siever [1], CIVL [2], Anchor [3]) to exploiting multicore (e.g. parallelizing compilers [4], transactional memory [5] declarative programming [6,7], scalable systems [8]) to distributed systems (e.g. CRDTs [9] and blockchain [10,11]).
Accordingly, there have been a variety of techniques and tools for reasoning about commutativity, including program analysis [4], sampling [12], random Contributions. Our work improves the state-of-the-art in the following ways:
1. Predicate semantics. (Sec. 3) In the state of the art, predicates must be built by manually writing terms, and are then mildly filtered and used without any information as to how one predicate relates to another. Refinement is exponential in the number of predicates so it is important to focus on important predicates. To that end, we improve the treatment of predicates by both syntactically and then semantically filtering redundant predicates. We next show how the information from filtering can be used to construct a lattice of predicates, ordered by implication, and use this lattice to better filter predicates and prune the state space during search. We also automatically extract terms from the input problem's pre/post relations.
2. Search heuristics. (Sec. 4) A key step in the algorithm is choosing the next predicate to divide the search space. We implement two new heuristics:
-poke2: A new predicate selection heuristic which avoids redundant SMT work, while also using the information obtained more directly. Consequently, it performs at most half as many SMT queries, if not fewer, than Servois's original implementation. -mcMax: A heuristic that employs model counting to more quickly cover the search space. Model counting is the problem of computing the number of models (i.e. distinct assignments to variables) that satisfy a given predicate [16]. As many predicates have infinitely many solutions, model-counting constraint solvers return the number of solutions for a given predicate within a given bound [17,18]. The mcMax heuristic takes a quantitative approach to predicate selection by leveraging model-counting to greedily pick predicates based on the largest covering of the state space, making choices based on approximate finite-domain information, yet maintaining soundness of the overall infinite-domain algorithm.
3. New implementation and pragmatic concerns. (Sec. 5) We implemented Servois2 in OCaml, exploiting the expected performance benefits of OCaml over Python. Our implementation is parametric on SMT solver, now supporting CVC4, CVC5 and Z3. We therefore inherit the expanded theory support, expanding the domains in which commute conditions can be synthesized. Ser-vois2 can now, for example, synthesize commute conditions for Strings operations like hasChar and concat. We also support interruption, emitting a sound but incomplete condition, allowing Servois2 to be used in a larger variety of new settings. Finally, Servois2 has a more well-defined API (as an OCaml type), allowing one to use it as a library. Servois2 is publicly available at: github.com/veracity-lang/servois2. The artifact, which contains a copy of the code, is available at: https://www.doi.org/10.5281/zenodo.7935263.
4. Evaluation. (Sec. 6) In order to show that our approaches improve performance in practice, we introduced new, non-trivial benchmarks that Bansal et al. [14]'s tool Servois struggles to solve. We evaluated all of Servois2's new approaches, including the poke2 and mcMax heuristics, in comparison to a faithful re-implementation of the poke heuristic in our new OCaml implementation on both the original benchmarks and our new ones. We also compared the performance improvements between heuristics with additional options for tuning the synthesis (see Sec. 6). Our experiments demonstrate that our approaches do give a substantial speedup-3.58⇥ (geometric mean) faster. In cases that involve theories where model counting can be done e ciently (strings, linear integer arithmetic, integer arrays), mcMax is often able to o↵er better performance. Furthermore, poke2 scales approximately linearly with the number of state variables, while the other heuristics (including all those in the prior work) diverge after only a few variables. Finally, given this wide variety of options, we used a portfolio approach, running each case with all options (solvers, heuristics, approaches to terms, etc.) and reporting back the first one to finish.
We begin with a brief review of abstraction-refinement commutativity condition synthesis, emphasizing key steps.
Suppose we have an abstract data type (ADT) method call m(ā)/r m , with method name m, taking argument vector ā and returning value r m . Similarly, consider a second method call n( b)/r n . We say these method calls commute from an initial ADT state , provided that when methods are applied in either order, they lead to the same final ADT state, and will have observed the same return values along the way. We notate this m ./ ,ā, b,rm,rn n, with subscripts omitted when the context is clear. A commutativity condition is a logical formula ' n m ( , ā, b) describing the conditions on the initial ADT state (and parameters ā and b) under which m and n always commute. (A non-commutativity condition ' describes conditions when they always do not commute.) As an example, a Set ADT with methods insert(x) and remove(y), a su cient commutativity condition would be ' remove insert ⌘ x 6 = y. We synthesize a commutativity condition ' via the Refine algorithm [14], which takes as input, an ADT specification, with methods' pre/post conditions written in SMTLIB. The algorithm uses the binary operator ./, which is defined as ./ on a lifted (total) version of the ADT; we omit the full details as they are not relevant to our improvements on the work. When run on a given pair of methods m and n, the output of the algorithm is a pair (' n m , 'n m ) of commutativity/noncommutativity conditions. Consider as an example input, an ADT for a hashtable that has three variables representing the state: a size integer, a Set over sort E of keys, and a finite array H mapping elements of sort E to sort F . Then, for each method, e.g., put(k, v), the input ADT specification includes a pre-condition (in this case true) and a post-condition relating the pre-state with input vector (size, keys, H, k, v) to a tuple of new values with return value (in this case, true or false representing success) (size new, keys new, H new, r). The Refine algorithm as output synthesizes commutativity conditions for the input method pair. In the case of the hashtable example, the solution for the commutativity synthesis of two calls of the same method put(k 1 , v 1 ) and put(k 2 , v 2 ) generated by the algorithm is '
The Refine algorithm is presented in Fig. 1. The algorithm recursively partitions the logical space along conjunctions of predicates, which are selected from a set of predicates P. When the algorithm finds a region of the state space H that is a su cient condition for commutativity (or mutatis mutandis non-commutativity), it adds it to an accumulated DNF logical commutativity condition. Otherwise, the recursive calls use counterexamples to select a predicate p that di↵erentiates the two counterexamples c and nc . This predicate is conjunctively added to H and used in the children recursive calls, and similarly for its negation. Fig. 2 illustrates this process of partitioning the logical space through the use of di↵erentiating counterexamples. This process continues until a necessary and su cient commutativity condition is found, or all combinations of predicates are exhausted. Typically, exhaustion of predicates is unlikely as there are exponentially many combinations of them. Furthermore, the algorithm can theoretically be interrupted (e.g. after a timeout) to yield a sound commutativity condition.
While the Refine algorithm is a somewhat straightforward form of abstraction-refinement, the e↵ectiveness of the technique and implementation thereof critically depends on how predicates are handled, selected, pruned, etc. We now discuss these details and how Servois2 improves on each of them.
Refine has worst-case exponential runtime in the number of predicates. While a Choose function that picks good predicates helps, it is still important to generate a small set P of relevant predicates and be selective during each recursive call. At the very least, reducing the number of predicates gives linear improvements on runtime, as SMT solvers, as well as Choose, must handle every predicate in P. In this section, we describe better methods of reducing the size of this set P.
(a) Improved predicate filtering. In Servois, after the initial list of predicates was built from manually provided terms, the SMT solver was queried twice for each predicate, and any predicate that was tautologically true or false was discarded. We retain this functionality, but first perform an additional syntactic layer of filtering by dropping any predicate that is:
1. A reflexive operation on two identical terms, 2. An operation between two constants, or 3. A symmetric case of another predicate already included. Since all of these filters are done purely syntactically, we save SMT work.
(b) Pruning by exploiting implication. We next determine which predicates imply other predicates. This can be done via syntactic implication rules such as x > y ) x + n > y + n. As a benefit, we are able to compute the closure of the logical implication relation, and are able to sort predicates into equivalence classes. Thus by removing redundant predicates, the size of the set of predicates can be reduced. Given logical implication relations, we can build a lattice out of the partially ordered set of predicates, ordered by the ) relation. This lattice information can be used to dynamically prune predicates that become redundant during runtime due to selection of other, related predicates. For example, consider the following LIA benchmark multiVarA ./ multiVarB. (Technically Servois/Servois2 inputs are given as ADT pre/post specifications, but we write this example as code illustration purposes.) Here, the lattice identifies implication chains such as 0 > (2x + y)
During search, we are able to use these chains to e ciently pruning the predicate lattice, e↵ectively reducing the height of the lattice and thus width of the search tree.
Fig. 3 illustrates our modifications to the original algorithm in Fig. 1. Starting from main, we perform automated predicate generation PredGen, which we will discuss below. From this set P, we construct the lattice L with MkLat. Within Refine, we parameterize Choose by L, allowing the Choose heuristics discussed in Sec. 4 to make choices based on L. Finally, we prune the search space by using RmUpper to remove all predicates that are weaker, i.e. higher in the lattice, than the selected predicate pair (p, ¬p). We may do similarly with the predicates stronger than the negation (RmLower). As a result, recursive calls will not have to consider any predicates that are already entailed by H.
Constructing the lattice can be costly as the size of the relation is quadratic in the number of predicates. Furthermore, syntactic rules cannot discover all implications, so an SMT solver must be invoked if more precision is desired. As we will see, it is not always worth this overhead. We have thus kept our lattice treatment as an optional feature. When disabled, the lattice simply behaves as a set of predicates (i.e. any predicate is only related to itself), à la Fig. 1, and assume that the set of predicates is closed under negation § .
(c) Automatic predicate generation via term extraction. Servois requires the programmer to manually provide terms with each method in the ADT specification, which can be error-prone and tedious. These terms are then used to build predicates by using boolean relations such as =, >, etc. We are able to automatically generate the terms for synthesizing the predicates by traversing the method specification (state variables, method arguments, pre/post-condition), and extracting basic expressions (categorized by type). The expressions are then combined with predefined operations for each type (e.g. in-/equality for Integers, membership/subset/etc. for Sets, contains/prefix/etc. for Strings, . . . ) to generate the predicates. With this approach, we generate enough predicates to establish a su ciently granular search space across all of our benchmarks and § To satisfy closure, we include negations of all predicates. This comes at no performance loss, as such additions can be skipped over by Choose. This is valid because Refine recurses upon the negation of the chosen predicate. we are not limited in how exhaustively terms are provided. Manual-vs-automatic term extraction leads to di↵erent sets and quantities of predicates, which may a↵ect how conditions are expressed. In Sec. 6 we discuss the performance impact.
(d) Syntax-based generation of predicates. Once predicates are automatically generated, it is natural to consider whether more complex predicates can be generated. While the original tool only considered predicates on two given terms, we found that often, compound terms that may not be provided or directly in the specification's syntax would be present in commutativity conditions. We added the expansion of terms with known and provided functions to allow for the automated generation of compound terms and predicates. Thus more complex commutativity conditions could be expressed, and the user does not have to already have specific predicates in mind when listing terms. Due to the exponential nature of syntax expansion, we get a greatly increased number of predicates. We found that this increase was too detrimental to performance to be practical-two or more iterations often times out. However there were still some test cases that benefited from performing one or two iterations, and the approach would likely be beneficial with improved pruning.
At each step, the Refine algorithm must Choose a predicate that di↵erentiates the commutative and non-commutative examples. While any implementation of Choose maintains the soundness of Refine, due to the exponential nature of the number of subsets of predicates, choosing a "good" predicate is important both to e ciency and quality of the form of the emitted condition. We refer to a Choose strategy as a "heuristic". Bansal et al. [14] describe a heuristic-referred to as poke-which performs a greedy one-step look-ahead.
(1) Choosepoke2(H, P, c, nc){ (2) let P 0 = Di ngPreds(P, c, nc)in
return 0; (7) else if valid(H^!p 0 ) m \ ./ n) then (8) return 0;
return Length(
Di ngPreds(P 0 , 0 c , 0 nc )) (14) in list min(weight, P 0 ) (15) } (16) Di ngPreds(P, c, nc){ (17) return filter((fun p !
Fig. 4: Pseudocode for our poke2 heuristic for choosing which predicate to recurse upon. Here, P may be obtained from L by taking the underlying set of predicates. list min(f, P) returns the element of P that minimizes f . In this section we introduce two new predicate selection heuristics called Choose poke2 and Choose mcMax (or simply, poke2 and mcMax) that, as we show in Sec. 6, perform better than the Choose poke of Bansal et al. [14], with trade-o↵s to consider between the two of them.
We begin by formalizing the poke2 heuristic, and compare it to the previous poke heuristic. When the SMT solver is invoked with the "valid()" queries in Refine, we obtain two satisfying counterexamples: c for commutativity and nc for non-commutativity. poke and poke2 share the common behavior to then proceed with two steps: (1) Test each predicate to see which hold in which counterexample (if either); this can be done in the same SMT query that was used for valid. This testing lets one find predicates that di↵er between the commutative counterexample and the non-commutative counterexample. This is summarized in Di ngPreds; the pseudocode for this subroutine is given at the bottom of Fig. 4. (2) Next, perform a partial look-ahead on each of these predicates-however, the way this is done di↵ers between the heuristics.
-The poke2 heuristic. The full pseudocode for poke2 is given in Fig. 4.
The partial look-ahead is encapsulated in the weight function. If a predicate was true in the commutative case then we can tentatively conjoin it with the commutativity condition and its inverse with the non-commutativity condition (mutatis mutandis for false-keeping track of which case is done on Line 4), then query the solver (Lines 5 and 7) to see how many predicates still
cover(¬p) = 1 cover(p) in (5) let P 00 = list max(cover, P 0 ) in (6) return first(P 00 )
cover(¬p) = 1 cover(p) in (5) let P 00 = list max(cover, P 0 ) in (6) return list min(weight, P 00 ) (7) } (b) mcMax-poke2 Fig. 5: Pseudocode for mcMax heuristics. As before, P is obtained by taking the underlying set of L.
di↵erentiate the two cases. We define the number of remaining di↵erentiating predicates to be the weight of the predicate (Lines 9-11). Finally we pick the di↵erentiating predicate that results in the fewest remaining di↵erentiating predicates in the look-ahead (Line 12). In the case that two predicates have the same number of new di↵erentiating predicates, we prefer the simpler (measured in number of atoms) one (not shown).
-The poke heuristic. By contrast, in poke the predicate and its inverse were tested with both the commutative case and the non-commutative case, irrespective of whether it was true or false in the commutative case. This resulted in many degenerate return values, which not only increased SMT time, but also could pick less beneficial predicates.
There is no need to prove correctness of poke2, as the Refine algorithm is correct for any implementation of Choose that picks a di↵erentiating predicate. Our evaluation of poke2 is thus based on runtime (more detail in Section 6.1).
For theories where model counting is e ciently supported by existing tools, we introduce an additional heuristic called mcMax. mcMax uses model counting to determine the number of satisfying solutions for each constraint on the state space. It then uses this count to quantify how well each predicate covers the state space and picks the predicate with the best coverage. Model counting requires a finite domain, so we treat state variables as finite on a bounded domain, e.g., treating integers as fixed-length bit vectors. Recall that any implementation of Choose is sound, so bounding the domain (temporarily as a heuristic hint) does not threaten soundness. For such fixed-length bit representations, we ideally require a bit width bound that is large enough to properly di↵erentiate between coverage ratios. Experimentally, we found that a bound as low as 4-bit representation of integers was su cient for LIA constraints with relatively small coe cients and a length of 4 was su cient for string constraints.
We now describe how mcMax proceeds using the pseudocode given in Fig. 5. The mcMax heuristic starts o↵ on Line 2 in a similar manner as poke heuristic by constructing the subset of di↵erentiating predicates P 0 from the two satisfying counterexamples. In the next step (Lines 3-4), we calculate the coverage ratio for both p and its complement ¬p as the fraction of their corresponding models' count. Finally, the predicate found to represent the largest state region is chosen (Line 5). Recall that Refine traverses both the given predicate and its negation (shown in the recursive calls in Fig. 1). In the case that execution is interrupted, we observe the first recursive call may be explored, while the second is not. In these cases mcMax often leads to a better (higher coverage ratio) predicate compared to a non-model-counting heuristic, since we greedily pick the larger conjuncts.
To overcome the arbitrary first choice among equally covering predicates at line 6 in Fig. 5a, the variant mcMax-poke2 equips mcMax with the weight-based ranking of predicates from poke2. Whenever the list of maximal coverage predicates returned by mcMax has at least two candidates, the predicate selection is turned over to poke2 applied to the candidate list.
Servois2 is implemented in OCaml and is publicly released under the MIT License ¶ . The tool has an underlying representation for SMT expressions, and parses input YAML files and the SMTLIB2 expressions within them. Examples of the Servois/Servois2 input format are available in the repository. The output commutativity condition is also an SMTLIB2 expression, but may be further constrained: since it is always in disjunctive normal form, and we add one conjunct at a time, we may model disjunctive normal form as a list of conjuncts, which are in turn lists of atoms. The lattice is implemented as a module parameterized by any module exposing an ordering relation, and is encoded as a graph with vertices stored in a map and two edge sets: that of covering elements and that of elements covered by it.
Model counting. For counting the solutions satisfied by each predicate, we use the state-of-the-art model-counting constraint solver ABC [18] that, among other strengths, allows for passing the specific domain bound along with the model-counting query. ABC supports precise solving of model-counting queries over strings, booleans, and linear integer arithmetic. We memorize the counting results in an association list to reuse them in subsequent calls of Choose mcMax .
Model counting for integer arrays. We expand the applicability of mcMax heuristics to predicates over array terms by adopting a method similar to the state-of-the-art model counter for bounded array constraints MCBAT [19]. This approach involves applying a sequence of model-count preserving reductions from the theory of arrays to the theory of uninterpreted functions and linear integer arithmetic before dispatching the query to ABC. While MCBAT focuses on formulas that are universally quantified over index variables, our procedure below addresses quantifier-free array constraints with terms a[i] representing the value stored in the array a at index i. Consider for example, the problem of counting the solutions hx, i, ji satisfying ¶ https://github.com/veracity-lang/servois2 the predicate (x[i] x[j] 1), where i, j are integer variables and x represents arrays of size 4. We accomplish the task in three stages. First, we translate the predicate into a list of linear integer arithmetic constraints that are conjoined into a formula. Then we count the number of satisfying solutions hx i , x j , i, ji by running ABC on this query:
Finally, we obtain the total model count by multiplying the translated query result with the value domain size twice, once for each of the unaccounted and implicitly unconstrained array values.
The reductions below summarize the steps of our model counting procedure for formulas with integer array constraints:
1. Replace all compound array index expressions e with fresh variables i and add corresponding constraints of the form e = i. Perform the replacement from the outermost expression inwardly. Consider, for example, the term
x[k + j 2] > 3 occuring in the query. We first replace the access term k + j 2 by a fresh variable i, and then introduce an additional constraint i = k + j 2 which captures this replacement. 2. Add array bounds constraints for each array index variable i.
-Replace all occurrences of array index terms a[i] with fresh variables a i , keeping track of the replaced mappings for each array variable a. -Add functional consistency constraints for each array variable and each pair of array index terms occurring in the query, i.e. (i = j) ) (a i = a j ). 4. Dispatch the set of constraints to ABC and obtain the model-count #mc tr .
Thus far, there are only minimal di↵erences to the approach in [19]. 5. Identify the unaccounted mappings for each array variable and compute the partial model-count by considering their summation and the unconstrained value domain: #mc unacc = |Z| unacc . 6. Obtain final model count as #mc = (#mc tr ⇤ #mc unacc ).
Additional solvers & theories. Servois was hardcoded to work with CVC4 [20]. We have parameterized Servois2 by SMT solver via OCaml modules and extended support for CVC5 [21] and for Z3 [22]. While mostly an implementation detail, this does allow us to leverage the additional strength of the other solvers. For example, CVC4 (as of version 1.8) did not have good support for modulus and division. Both CVC5 and Z3 are able to support such operations, and Servois2 is able to generate commutativity/non-commutativity conditions for modular arithmetic examples.
With expanded solver support, Servois2 can tackle more theories, including ones for which specialized solvers are useful. Neither bit-vectors nor strings were supported in the original release of Servois, but Servois2 can synthesize commutativity conditions for both theories. As an example, we showed that Servois2 is capable of inferring that bit-vector negation always commutes with itself. We also benchmarked a few string examples, such as substr ./ hasChar, as they also demonstrate the usefulness of model counting.
Early termination. The following theorem is presented in Bansal et al. [14]:
For each Refine m n iteration: ' ) m ./ n, and ' ) m \ ./ n.
Thus, if updates to ' and ' are atomic, then terminating the algorithm at any point will yield valid conditions. We take advantage of this in Servois2 by allowing timeouts: the algorithm gracefully terminates after a designated time by outputting the incomplete (yet valid) conditions ', '. This proves useful in practice, as not all commutativity conditions may be expressible in terms of the predicates available; a necessary and su cient condition for synthesis of a complete commutativity condition via the Refine algorithm is given in Bansal et al. [14]. In such cases, the algorithm must finish its exponential run-time, only to determine that no complete commutativity condition is expressible. Even if the algorithm does terminate, after a certain point, the commutativity condition may be more complex than is useful. Thus it is usually more useful to cut the execution short and report only the most important few disjuncts of the commutativity conditions. In Sec. 6.2 we describe an instance of both a case where the algorithm does not terminate and a case where the algorithm terminates, but we still may obtain a reasonable condition by limiting the execution time.
We evaluated whether Servois2 improved over the state-of-the-art Servois in terms of performance (speed) and expressivity. All experiments below were run on a machine with an AMD EPYC 7452 32-Core CPU, 128GB RAM, Ubuntu 20.04, and OCaml 4.14.0.
Benchmarks. Our suite of 68 benchmarks begins with those used to evaluate Servois in the prior work [14]. Since the core goal of our work is to improve performance, we have pruned down this set, removing those benchmarks for which all tested heuristics can synthesize a condition after zero or one iteration(s). For example, we omitted the counter and accumulator examples because the conditions generated were either true/false or a single atom. We also removed all similar method pairs with simple commutativity conditions from the remaining data structures: sets, hashtables (HT), and stacks (Sta).
In addition to these benchmarks, we contribute new benchmarks for strings (Str) and linear integer arithmetic calculations (LIA), and a benchmark based on rigid motions on hexagons (DiH, for "dihedral"). These serve to show the application of model counting, which works best on these domains. The model counter is not applicable to the other data sets due to presence of custom data declarations. It could also be run on the counter and accumulator benchmarks, but we do not expect that to be illustrative due to triviality. Moreover, we used Veracity project [6] benchmarks as additional nontrivial benchmarks. There are 26 reported benchmarks in Veracity that use commutativity synthesis. We have also implemented some new benchmarks, e.g. Solidity examples translated to Veracity, to demonstrate various aspects of our improvements in addition to more speedup. We elaborate on the usage of Veracity benchmarks in Sec. 6.2.
We would ideally compare the performance of Servois2 versus Servois, but since Servois2 is written in OCaml, and Servois is written in Python, there is an obvious speedup from compilation, and indeed we found Servois2 to be at least twice as fast even using the same heuristics and on the same inputs. (As an example: the Hashtable put/put example was the slowest running benchmarkit took 5.31s with Servois using poke, and 2.61s with Servois2 using the same heuristic.) However, our work is not aimed at comparing Python vs OCaml, so we instead benchmark across our new heuristics (poke2 and mcMax) and features in comparison to a faithful re-implementation of Servois's poke in OCaml. The re-implementation was created by manually translating the source code of Servois.
Comparison to poke baseline. To test the variety of features we have added, we ran each benchmark with all combinations of features:
-The heuristics poke, poke2, and mcMax/mcMax-poke2 (when applicable).
-With each of the CVC4, CVC5, and Z3 solvers.
-With and without automatic term extraction (Sec. 3).
We report the configuration with the best performance in Table 1 * * , using poke with CVC4 and no lattice, no term extraction as a reference point for comparison. The heuristic and solver is given, then whether term extraction was performed (notated TG). The geometric mean of the speedup ratio of the best configuration over poke was 3.58⇥. Note that this speedup is conservative, as the several benchmarks that timed out with poke (and did not with Servois2) are excluded. We also report the change in the complexity of the synthesized commutativity condition in A, indicating the change in the number of atoms in the synthesized condition. The full generated conditions are omitted; note that if synthesis terminates with a complete condition, the generated conditions will be logically equivalent, but sometimes the order of the terms changed. ( † ) indicates the cases where the tool terminated with an incomplete condition. We terminated the benchmarks at 120s, and indicate the ones that still did not finish within this time with T. A few benchmarks could not be run under CVC4, and those are marked with j. All benchmarks whose poke baseline took less than 1 second to execute were omitted from the table due to triviality. T indicates time out (set at 120s). j indicates cannot be run.
The mcMax heuristic only applies to ADTs with theories supported by the model counter ABC [23] extended with our procedure in Sec. 5, hence our results using that heuristic are limited to the String, LIA, and Dihedral ADTs, as well as the Veracity benchmarks. Our extension for integer arrays allowed for the use of mcMax on the majority of the Veracity benchmarks. In some cases, mcMax provides a significant speedup over poke and even poke2. For example, in the hasChar ./ concat benchmark, mcMax is 2.89⇥ as fast as poke2 (not shown) and over 5.41⇥ as fast as poke, with the same configuration aside from heuristic. In other cases, such as in the sum ./ multiVarSum analysis, mcMax underperforms compared to poke2 and poke. The performance of mcMax seems to depend on the methods considered, but there are cases where it can significantly improve run time. In future work, we hope to explore additional model-counting heuristics such as bisecting the search space rather than greedily covering it.
The original Servois tool required users to provide terms, sacrificing some degree of automation which is inconvenient and errorprone. As described in Sec. 3, Servois2 now can automatically extract terms from the method specifications. As shown in Table 1, denoted by TG, the automated term extraction can even outperform manually provided terms.
In addition, by automatically extracting terms, our approach is another step closer to a fully automated commutativity synthesizer-the user does not have to do the manual work of providing terms. We believe that in conjunction with comparable performance, this makes automated term extraction preferable.
We also evaluated the performance using the predicate lattice approach outlined in Sec. 3. In practice, we found that the overhead of lattice construction using SMT queries was typically too high, and it did not substantially improve synthesis time in most cases. When using syntactic rules (using a preliminary set of inference rules and axioms), we did not discover Fig. 6: Experimental results on the scalability of general-purpose heuristics enough implications to be useful in any cases, with still substantial, albeit greatly reduced overhead. However, we did find that some LIA examples were improved by using the SMT implication lattice. sum ./ multiVarSum in particular saw a 2.27⇥ speedup from 8.36s to 3.69s, which is a substantial speedup even accounting for the lattice construction time of 1.87s. In multiVarA ./ multiVarB, the discovery of logically equivalent predicates filtered more than half of the initial list of predicates-from 280 (including negations of predicates) to 106. For the complete results, see Table 2. While it remains unclear whether the predicate lattice can be used for performance gains in most cases, the preliminary results suggest that further work may yield larger gains in di cult cases.
Consider the toy example below, where we have a possibly ordered set described by x variables and we want to compute another element a that can potentially be added to the set after applying a marginal decrement. In this (somewhat artificial) example, the number of predicates increases (Fig. 6b) with the number of variables, while the commutativity problem has a straightforward solution:
(1) int a, b, x 1 , x 2 , ..., x n ;
(2) bool sum(){
a := (a -b); return true; } (4) bool multiVarSum(){ (5) if (a>0 && x 1 <x 2 && x 2 <x 3 && ... && x n 1 <x n ){ (6) a := (x n + a); return true; (7) } else { (8) a := (x n -a); return true; }} Although mcMax shows promising results, due to reduced applicability to cases where e cient model counting is supported, we did not consider it for this particular experiment. Our focus here is on general-purpose heuristics. Fig. 6a reports the results of our experiments running the heuristics simple (presented in [14]), poke, and poke2 on the above example, with increasingly many variables (up to 30) and, consequently, increasingly many predicates. For the precise ADT specification, refer to the "lia scale var template" file in the artifact or Github provided in Sec. 1. We observe an impressive performance benefit from the poke2 heuristic. Firstly, observe that starting from only a small number of predicates, poke2 proved to be one order of magnitude faster than poke which timed out early in our experiment. Secondly, the increase in the number of state variables
x is roughly linear with the increase of poke2 synthesis time. And lastly, the poke2 heuristic led to synthesizing the utmost simple condition, namely the one humanly inferred.
To show Servois2's applicability, we present the case study of its use in the Veracity † † project [6], recalled below. The original Servois lacked features (e.g. solvers, theories, early termination) and performance to be used in such a setting. Despite the use of Servois2 in Veracity, the improvements described in the current paper are orthogonal.
Veracity is a parallelizing compiler for a language in which programmers directly express conditions under which sequential blocks of code commute [6]. Expanding programs with such commutativity annotations enables parallelization of sequential code that has dataflow dependencies, which previously could not be parallelized. We omit the finer details as it is outside the scope of commutativity synthesis. Consider for example, the following Veracity benchmark even-odd includes a commute statement, with a blank commutativity condition to be synthesized (or provided by the user):
Veracity needs Servois2 in order to synthesize the following commutativity condition for these program fragments labeled (1) and ( 2): y = 0 _ (y 6 = 0 ^x%2 =
x + y). In more detail, Servois2 is used by first having the Veracity compiler translate the program code into methods, say block 1 () and block 2 () on an ADT whose state are the program variables x and y. Then, the synthesized commutativity conditions are translated back and inserted in place of the " " in the Veracity commute block. Unfortunately the original Servois's limited support for solvers/theories (as well as limited performance) prevents it from synthesizing a commutativity condition for this benchmark. The divergent behavior of Servois on some benchmarks was a further impediment to its use in Veracity.
A few selected benchmarks are shown in Table 3. These benchmarks are illustrative of the di↵erent kinds of typical output from Servois2. Most cases were similar to the dict example, terminating in a few seconds with a sensible result. The ht-simple case takes more time. The condition is complete, but due to the longer time, it may be worth terminating the algorithm early and only receiving one or two of the disjuncts, especially if they cover the most common cases. Finally, loop-amt is a case that is not amenable to commutativity inference and it would be better to terminate sooner and allow the user to attempt a di↵erent approach. Unlike direct ADT benchmarks, those derived from Veracity programs involve the composition of numerous e↵ects and thus involve complex commutativity conditions. Consequently, most of the Veracity benchmarks make substantially more complex queries to Servois2 than the handwritten ADT specifications. We thus used all of the Veracity benchmarks to test the di↵erent configurations, as mentioned before and shown in Table 1.
New non-trivial benchmarks were manually translated into the Veracity programming language. These were various combinations of functions from the SmartContract/Auction, Solidity/StandardToken, and Solidity/PullPayment source codes. Most of these new benchmarks perform better on the new heuristic poke2 compared to the previously presented approach poke. Also, for several of them, poke did not terminate, so we had to use the early termination feature to synthesize the commutativity condition within a specific time frame. For StandardToken, for example, after executing TransferForm ./ Approve with using poke and 120s timeout, we get an incomplete condition; however, with poke2, we can get a complete condition in about 10 seconds with a reasonable number of atoms.
We have shown a more mature and performant method of automatically synthesizing commutativity conditions in the Servois2 synthesizer. Our results confirm what one might expect: that more advanced heuristics and better treatment of predicates leads to overall performance improvement. Furthermore, we have released a far more usable tool that has already been used in recent work [6] and is ready to be integrated into other commutativity settings such as proof methodologies [1,3,2] or distributed systems [9,11]. There are several directions for future work in this space, discussed below. Algorithmic improvements. We saw great improvements in the performance of the heuristic in keeping track of which predicates aligned with the commutative (resp. non-commutative) case. The algorithm is currently agnostic to which condition is being pursued, and it may be possible to tag such information in the recursive calls, leading to similar improvements in performance. Furthermore, the disjunctive nature of the algorithm may be amenable to parallelization. However, it is unclear whether the actual reasoning is amenable to parallelization or if it is not worth the overhead.
Extended use of model counting. mcMax uses the model-counting solver ABC [23], which targets string, LIA, and boolean constraints, but we could also use other model counters with support for other theories. Approximate model counters [24] are a promising avenue for handling model-counting queries across additional theories, and the integration of such a model counter might lead to further applicability of mcMax.
The mcMax heuristic provides one model counting heuristic to inform predicate selection, but we hypothesize that additional heuristics might provide advantages on di↵erent benchmarks, for example, by maximizing partitioning rather than covering. Given the promising results of mcMax, we plan to pursue a more extensive evaluation of model-counting heuristics.
Model counting might find an additional use in cases where our commutativity analysis terminates early. Using model counting, we can determine what portion of the input domain is covered by the resulting commutativity and noncommutativity conditions, augmenting our analysis with additional reliability information in cases of early termination. It also may be possible to use this information to determine when to terminate.
Improving the use of the predicate lattice. Our experiments indicate that the overhead of lattice construction is significant. Thus for the lattice to be practical, one would need to both increase its performance benefit and decrease the overhead from construction. Although Refine prunes predicates based on the lattice, none of the current heuristics use information about implication chains, and there may be even more gains to be had by using lattices. There are also more sophisticated approaches to building the lattice data structure of logical implications, such as by using the framework GreenTrie [25]. The number of queries can be greatly reduced through semantic reasoning and caching of subformulas. This could greatly reduce the overhead of lattice construction, thus making their use more appealing.
† † http://www.veracity-lang.org