Bug #514
closedBLAST's useful blocks generation algorithm is suboptimal for SMT solvers
0%
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
Updated by Pavel Shved almost 14 years ago
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.
Updated by Pavel Shved almost 14 years ago
- File before_ub_profile_short before_ub_profile_short added
- File after_ub_profile_short after_ub_profile_short added
- Status changed from New to Resolved
- Published in build set to 9c0646f
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.
Updated by Pavel Shved almost 14 years ago
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.
Updated by Pavel Shved over 13 years ago
- 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.
Updated by Pavel Shved about 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)