ensureDef performance problem

[tgiannak]

Alloy version: 5.1.0 Java version:

$ java -version
openjdk version "11.0.8" 2020-07-14
OpenJDK Runtime Environment AdoptOpenJDK (build 11.0.8+10)
OpenJDK 64-Bit Server VM AdoptOpenJDK (build 11.0.8+10, mixed mode)

OS version: macOS 10.14.6

I've run into a performance bug in ensureDef. Unfortunately, I can't share the actual model that led me to discover the problem, but I was able to create the following synthetic model that is much smaller and has the same issue.

The model below takes approximately 200 seconds to translate to CNF with "Prevent overflows" on and Skolem depth 0. With "Prevent overflows" turned off and Skolem depth 0, it takes less than 5 seconds. When running with "Prevent overflows" turned on, more than 90% of the time is spent in calls to toString within calls to ensureDef. When there are larger expressions in the quantifier bindings, the discrepancy is even more dramatic and an even larger percent of the time is spent in toString. (I had one run that took nearly 10 minutes with "Prevent overflows" on but less than one second with it off.)

From reading the code, I could identify three causes of the poor performance:

1. The isInt method is calling toString on non-trivial data structures. This is both slow and causes a lot of garbage to be produced.

   This might be improved by changing the !(expression instanceof Expression) condition to !(expression instanceof ConstantExpression).

2. ensureDef repeats the expensive isInt call for every element of env for every element of dcs, rather than filtering env once, up-front.
3. ensureDef is called redundantly between eq and subset.

Changing the conditional is probably the easiest way to get a big performance win for ensureDef in situations where there are nested quantifiers over non-trivial expressions, since it would limit the calls to toString to a cheap case (with no String concatenation) without affecting the result of the isInt call. All three issues probably have to be addressed for a true fix.

(Sorry for the oddness of the model. It took some work to get the rest of Alloy and Kodkod not to optimize everything away before reaching the problematic code.)

sig A {
  foo: A
}
sig B {}

pred p[x: A, y: A] { y = x.foo }

pred isUnivQuantPerformanceBug1 {
    all a0 : A+B+A+B |
    some a1 : A+B+A+B+A+B+A+B |
    some a2 : A+B+A+B+A+B+A+B |
    some a3 : A+B+A+B+A+B+A+B |
    some a4 : A+B+A+B+A+B+A+B |
    some a5 : A+B+A+B+A+B+A+B |
    some a6 : A+B+A+B+A+B+A+B |
    some a7 : A+B+A+B+A+B+A+B |
    some a8 : A+B+A+B+A+B+A+B |
    some a9 : A+B+A+B+A+B+A+B |
    some a10 : A+B+A+B+A+B+A+B |
    some a11 : A+B+A+B+A+B+A+B |
        p[a1, a2]
        and p[a2, a3]
        and p[a3, a4]
        and p[a4, a5]
        and p[a5, a6]
        and p[a6, a7]
        and p[a7, a8]
        and p[a8, a9]
        and p[a9, a10]
        and p[a10, a11]
}
// Prevent overflows: Yes
// a7:   Translate: 54 vars. 6 primary vars. 65 clauses. 142ms. Solve: 5ms.
// a8:   Translate: 114 vars. 6 primary vars. 140 clauses. 795ms. Solve: 8ms.
// a9:   Translate: 174 vars. 6 primary vars. 210 clauses. 2246ms. Solve: 8ms.
// a10:   Translate: 270 vars. 6 primary vars. 305 clauses. 43487ms. Solve: 3ms.
// a11:   Translate: 812 vars. 6 primary vars. 909 clauses. 196147ms. Solve: 6ms.

// Prevent overflows: No
// a7:   Translate: 54 vars. 6 primary vars. 65 clauses. 25ms. Solve: 8ms.
// a8:   Translate: 114 vars. 6 primary vars. 140 clauses. 62ms. Solve: 6ms.
// a9:   Translate: 229 vars. 6 primary vars. 263 clauses. 268ms. Solve: 5ms.
// a10:   Translate: 270 vars. 6 primary vars. 305 clauses. 1055ms. Solve: 5ms.
// a11:   Translate: 812 vars. 6 primary vars. 909 clauses. 4199ms. Solve: 5ms.

run isUnivQuantPerformanceBug1 for exactly 2 A, 2 B

[pkriens]

@nmacedo did we take care of this issue in the change to 6.0?

[grayswandyr]

Seems instantaneous on 6.0.

openjdk version "11.0.18" 2023-01-17
OpenJDK Runtime Environment (build 11.0.18+10-post-Ubuntu-0ubuntu122.04)
OpenJDK 64-Bit Server VM (build 11.0.18+10-post-Ubuntu-0ubuntu122.04, mixed mode, sharing)

[pkriens]

@tgiannak please reopen if this issue still exists in 6.x