How to analyze issues of performance regression when upgrading Boogie

[rahxephon89]

Hi, we are recently trying to upgrade Boogie from 2.15.9 to 2.16.9 but there is a regression on verification time. I am wondering whether there is a way to find out the reason and then probably solve this issue. Thanks!

The backend SMT solver is z3 4.11.8 and this is the option being used by default:

boogie -doModSetAnalysis -printVerifiedProceduresCount:0 -printModel:1 -enhancedErrorMessages:1 -proverOpt:O:model_validate=true -proverOpt:PROVER_PATH=z3 -proverOpt:O:smt.QI.EAGER_THRESHOLD=100 -proverOpt:O:smt.QI.LAZY_THRESHOLD=100 -proverLog:@[email protected] boogie.bpl

[atomb]

You might experiment with differences between -typeEncoding:a, -typeEncoding:m, and -typeEncoding:p, since the default changed recently.

When using -typeEncoding:p, we recently fixed a soundness issue that unfortunately also incurs a performance penalty.

[rahxephon89]

Thanks Aaron and Shaz! Could we replace /useArrayTheory with /useArrayAxioms in general? What is the difference between these two options?

[shazqadeer]

In the latest version, Boogie has two ways to handle arrays: (1) use SMT arrays, (2) use axioms. Both options are available with /typeEncoding:m. Only the latter is available with /typeEncoding:p and /typeEncoding:a. You are using /typeEncoding:m and I believe you would like to use axioms because that is what the Move Prover has traditionally used. To use axioms with the latest Boogie, you have to supply /useArrayAxioms.

/useArrayTheory does not exist any more. When it existed, the default in Boogie was to use axioms regardless of the type encoding and /useArrayTheory was needed for using SMT arrays.

[rahxephon89]

Thanks, Shaz! Another question is that in the previous version, the Move prover does not allow /useArrayTheory to be used together with -proverOpt:O:smt.QI.EAGER_THRESHOLD=xxx and -proverOpt:O:smt.QI.LAZY_THRESHOLD=xxx when invoking boogie. I am wondering why it is the case and is it safe to use /useArrayAxioms with these two QI threshold options?

[shazqadeer]

In the previous version, axioms were the default and you got that since you did not use /useArrayTheory. You were using axioms because it gave you better performance. In the new version, the default is SMT arrays but I think you still want axioms so you should use /useArrayAxioms.

[rahxephon89]

Just confirmed that when /useArrayAxioms is set, verification time is reduced. However, it is still somehow slower than the previous version, especially when there are non-linear arithmetic operations. I am wonder whether there are other options or techniques that I can further explore? Thanks

[shazqadeer]

I don't recall anything changing for non-linear arithmetic operations.

You could try playing with the two thresholds you are specifying on the command-line.

Also see the documentation for /randomizeVcIterations. Check if you have large variation in the running time as the VC for your problem is randomized. Perhaps the butterfly effect is kicking in for you.

[rahxephon89]

Thanks Shaz!

[rahxephon89]

@shazqadeer Sorry to bother you again but are there any other changes (algorithms, boogie or z3 options) between 2.15.8 and 2.16.9 that may have potential influence on efficiency of verification? Thanks