Bug #511
closedSMTlib interface spends too much time generating predicates
0%
Description
The mechanism to decrease the number of interpolation calls relies on getting only significant blocks from an error trace. It is done by adding block predicates one-by-one into a big conjunction, and testing it for satisfiability.
SMTlib interface in BLAST is implemented in such a way that at each satisfiability test the whole conjunction is converted to the SMTlib format. This way each minterm undergoes the same conversion over and over.
According to profiling results, this is a bottleneck in error trace analysis. So this should be fixed.
Files
Updated by Pavel Shved about 14 years ago
I thought, well, SMT solvers are used in BLAST like incremental Simplify solvers. Why then couldn't I convert each predicate as soon as they're pushed to predicate stack? If SMTlib interface component of BLAST is used like Simplify, why couldn't we take advantage of it? :-)
I implemented a fix to the SMTlib implementation of Simplify interface, and it works like a charm. It's currently being tested on my machine.
A small drawback is that it adds a lot of extrafuns declarations even to very small queries. I hope that it won't be a problem for solvers.
Updated by Pavel Shved about 14 years ago
- File drivers-kbdrivers-0032-2.6.31.6-test-0032-2.6.31.6-verdict-safe-drivers--media--dvb--dvb-usb--cxusb.c-cxusb.c.common.i drivers-kbdrivers-0032-2.6.31.6-test-0032-2.6.31.6-verdict-safe-drivers--media--dvb--dvb-usb--cxusb.c-cxusb.c.common.i added
Well, if it's a charm, it's not the best one. It's still a bottleneck. I launched one of the safe drivers from generic test set, without lattices, and I had to set limit on iterations. Here are the timings:
TOTAL 17.293 s
...
check_error 15.293 s (1)
...
get useful blocks 12.505 s (1)
convert to SMTlib 12.325 s (162)
contradiction check 0.112 s (90)
Converting predicates to SMT format takes 70% of the total time.
Command:
pblast.opt cxusb.c.common.i -predH 7 -craig 2 -ignoredupfn -nosserr -main ldv_main0_plain_sorted_withcheck -L LDV_ERROR -cldepth 0 -reroute -reroute-map mutex_lock_interruptible -reroute-map mutex_lock_killable -reroute-map mutex_lock -reroute-map mutex_trylock -reroute-map mutex_unlock -reroute-foreach check_final_state -reroute-foreach ldv_initialize -reroute-placeholder TEMPLATE -systime -devdebug -skipnorm -iter-bound 2000
Updated by Pavel Shved about 14 years ago
After some experiments, I learned that such an enormous time is spent on generating only on the predicate of the initialization block! With -noinitialize option, it takes an insignificantly small amount of time to convert predicates on the driver given.
- Suppress initialization with
-noinitialize - Implement a more tricky caching mechanism (such that can share conversion of the block between error trace analyses)
- Any suggestions are welcome!
Updated by Pavel Shved about 14 years ago
Wow. With Yices solver and with latest BLAST fixes, the tool can process the cxusb driver attached! It traverses about 41 thousand nodes!
I specifically compared, how much time converting the first block (initial assignment of static variables) takes. Here's the result of SMTlib mediator profiling:
get useful blocks 303.427 s (10)
convert to SMTlib 0.076 s (16114)
contradiction check 69.440 s (1860)
convert 1st 231.610 s (10)
So each time an error trace was analyzed, conversion of the first initialization block predicate to SMTlib format took 23 seconds, all other blocks having been converted in no time. Out of total BLAST's CPU time, conversion of init blocks took 53%. Also, processing these blocks takes a lot of memory (though, I wouldn't say it's spent on conversion only).
Apparently, something should be done with these huge bastards.
Updated by Pavel Shved about 14 years ago
It's quite strange actually. The initialization block conversion seems to take 23 seconds for only 6 thousand of assignments. This seems too high to me. I think that the conversion procedure could be improved.
A couple of ways to improve it:
- Rewrite it as tail-recursive
- Implement it in C
- ??? (Suggestions are welcome)
Updated by Pavel Shved about 14 years ago
We're going to address this issue soon. If we won't manage to fix it by means of OCaml code improvements, we'll resort to implementing conversion in C.
Updated by Pavel Shved about 14 years ago
- Due date set to 12/02/2010
- Priority changed from High to Urgent
Forgot to set the priority up...
Updated by Pavel Shved about 14 years ago
The bug was fixed in BLAST, and was merged to BLAST's master (not that of LDV tools). Will be merged to LDV as soon as general tests finish and are fixed.
Updated by Pavel Shved about 14 years ago
- Status changed from Open to Resolved
- Published in build set to f252fe5
Interesting... General tests don't show any discrepancies with previous behavior. They definitely should be updated soon!
The commit commit:f252fe5 is in master now, and will soon appear in public repo.
The profile for the 41k-iterations cxausb driver looks now like this:
get useful blocks 18.573 s (10)
convert to SMTlib 0.048 s (16114)
contradiction check 14.885 s (1860)
convert 8.189 s (1860)
printf conj 0.316 s (1860)
fct 0.000 s (1860)
symbol 7.508 s (1860)
Pipe the query 6.620 s (1860)
convert 1st 0.296 s (10)
The convert to SMTlib and convert 1st now takes just a few milliseconds, which is a dramatic improvement.
Just for your amusement: the function was rewritten using OCaml Buffers.
Updated by Pavel Shved almost 14 years ago
- Status changed from Resolved to Closed
Blast was run many times (for work on bug #330) and the fix doesn't seem to introduce any regressions.
Updated by Pavel Shved over 13 years ago
- Project changed from Linux Driver Verification to BLAST
- Category deleted (
BLAST)