Performance issue with :prove

[ramsdell]

I have an odd performance issue with :prove in Cryptol 2.10.0. If I specify a property by negating a boolean and combining it using short cut or with another boolean expression, I get a proof much faster than when I rewrite the property by removing the negation and using short cut implication instead. Logically, these two should be exactly the same. I did the obvious test that in fact short cut implication is in fact short cut in the interpreter, and of course it passes that test. I have enclosed a ZIP file that demonstrates the bug. The README explains the contents.

lup.zip

[robdockins]

Looking at the SMTLib output from these two prove commands, I don't see any obvious reason these problems would be significantly different. The exact ordering and numbering of subterms differs slightly, but that seems to be about it, from a quick glance. I'm guessing this is down to some details of the solver's search strategy that happens to do better with one formulation over the other.

For what it's worth, using :set prover=w4-z3 yields a good improvement on both formulations for me, and seems to make the difference disappear. Yices and cvc4 did not do better on this problem.

[robdockins]

I took a look at the LUP algorithm. I don't see any obvious slam-dunk improvements to this algorithm that immediately jump out. In one of the comments you speculate that using update would improve performance; that's possible, but I doubt it will make much difference, and might even be worse. I've been wrong before, though.

However, I will say that I expect the pivoting steps will be very expensive in the symbolic simulators (for :prove, :sat, etc). They will create a lot of internal branching in the terms, which I expect is giving the solvers some difficulty. I don't know offhand of a complete LU-style algorithm that doesn't rely on pivoting, but if there is one, it might perform better.

[ramsdell]

Thank you for you quick replies. I verified that using w4-z3 is much faster. Amazing.

The prove command was extremely useful while debugging the code. It quickly returned useful counterexamples that help me find and fix mistakes. And when it didn't return quickly, I got a good feeling.

Since Friday, I had a machine trying to prove 3 X 3 matrix inverse is correct. I killed Z3 and restarted using w4-z3. I noticed that time reported my cryptol process used little CPU time, but a lot of elapse time. Are you sure cryptol is waiting properly when Z3 is killed? Shouldn't cryptol still be changed Z3's CPU time?

[weaversa]

I believe that Cryptol spins up z3 as an external process (think C’s system call). So, Cryptol essentially pauses and waits while z3 is running.

[ramsdell]

I had this problem with a program I wrote that used Z3 as an external process. I had to patch a module to fix the problem. The end of the source file shows what I did.

SExprProcess.hs.txt

[robdockins]

Process handling is a complicated topic... but I think this is expected behavior. If I remember correctly, solver processes are started in a separate process group, which is necessary for reliable signal handling, and this causes their CPU time to be accounted separately. That might also be OS-specific, I'm not sure.

[ramsdell]

I see, so the code I showed probably didn't create the Z3 process in a separate process group, and that allowed me to collect the missing CPU time using waitForProcess. I tested my code on Linux, and on that platform, I think I remember the CPU time was collected by my Haskell program even when Z3 was killed, but I cannot be sure. I never checked the behavior on any other OS. As you say, handling all OSs is why process handling gets complicated.

[robdockins]

Because I was curious, I implemented this LUP module on GF(2) (aka booleans) just to see how the matrix operations could scale on the simplest field. I got reasonable results for proving LUPCorrect up to n=5 (about 5 seconds) after which the evaluator fell off an exponential cliff and was still computing the problem to send to the prover after several minutes. Interestingly, the What4 backend did much worse here than the SBV backend, taking about 10 times as long, with most of that time spent in Cryptol itself, before invoking the solver. It would be interesting to see if we can discover why.

At any rate, we seem to be climbing a very steep exponential curve. As I mentioned above, I suspect that pivoting is the main culprit here.

[ramsdell]

This is a very interesting result. Thank you for sharing it.

[robdockins]

I don't think there are any other obvious improvements to be had here.