Bug #514
closed
BLAST's useful blocks generation algorithm is suboptimal for SMT solvers
Added by Pavel Shved over 13 years ago.
Updated over 12 years ago.
Published in build:
9c0646f
Description
One of the core tasks in the useful-blocks algorithm is to find the first i such that conjunction of predicates from 1 to i is UNSAT.
For incremental solvers it was OK to push predicates one-by-one, anbd check for satisfiability. But for SMTlib solvers it's suboptimal. An algorithm that employs some kind of binary search and works in a logarithmic number of calls to solvers could—oh, no, should—be much faster.
We need to carefully design and implement it.
Files
Logarithmic algorithm was implemented, and it resides on our development server in branch useful-blocks-fix. It demonstrated performance improvement, although most time seems to be taken by processing of initialization block (see #511).
As soon as tests on my machine finish, I'll merge the fix to the ldv-tools main branch.
As a result of this optimization, for example, on cxusb driver, the number of calls to SMT solver reduced from 32630 to 831, and the overall time is 7 times less than it was before (10 times less if you count BLAST exclusively).
Attached to the post are a couple of [shortened] profiles of analysis of a cxusb driver with iteration limit. Other than in runtime, the launches differ in nothing else.
The fixes are now merged into master, and reside in commit:9c0646f.
I wouldn't actually close it before we resolve bug #566 and/or make another full-kernel run with analysis of all the errors appeared. Let it hang for a while.
- Status changed from Resolved to Closed
Since there was no dramatic increase of these issues (moreover, I feel that amount of satisfiable blocksets decreased), closing this bug.
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)
- Target version set to 2.6
Also available in: Atom
PDF