Project

General

Profile

Actions

Bug #511

closed

SMTlib interface spends too much time generating predicates

Added by Pavel Shved almost 14 years ago. Updated about 13 years ago.

Status:
Closed
Priority:
Urgent
Assignee:
Category:
-
Target version:
Start date:
10/29/2010
Due date:
12/02/2010
% Done:

0%

Estimated time:
Detected in build:
all of them
Platform:
Published in build:
f252fe5

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

Actions #1

Updated by Pavel Shved almost 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.

Actions #2

Updated by Pavel Shved almost 14 years ago

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

Actions #3

Updated by Pavel Shved almost 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.

How could we mitigate this issue?
  1. Suppress initialization with -noinitialize
  2. Implement a more tricky caching mechanism (such that can share conversion of the block between error trace analyses)
  3. Any suggestions are welcome!
Actions #4

Updated by Pavel Shved almost 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.

Actions #5

Updated by Pavel Shved almost 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:

  1. Rewrite it as tail-recursive
  2. Implement it in C
  3. ??? (Suggestions are welcome)
Actions #6

Updated by Pavel Shved almost 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.

Actions #7

Updated by Pavel Shved almost 14 years ago

  • Due date set to 12/02/2010
  • Priority changed from High to Urgent

Forgot to set the priority up...

Actions #8

Updated by Pavel Shved almost 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.

Actions #9

Updated by Pavel Shved almost 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.

Actions #10

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.

Actions #11

Updated by Pavel Shved about 13 years ago

  • Project changed from Linux Driver Verification to BLAST
  • Category deleted (BLAST)
Actions #12

Updated by Pavel Shved about 13 years ago

  • Target version set to 2.6
Actions

Also available in: Atom PDF