severe performance problem in buddy/JavaBDD function for loading BDD from disk

[GoogleCodeExporter]

Both BuDDyFactory (which calls the bdd_fnload function in file bddio.c in the 
BuDDy distribution) and JFactory (which is essentially the same C code from the 
BuDDy distribution re-written in Java) have a severe performance problem when 
they load a BDD stored in a file on disk.  The problem lies in method ite_rec 
in file JFactory.java.

Replace the code which invokes the if-then-else BDD operation for each entry in 
the file, which in turn typically creates exponentially many BDD nodes, to a 
single constant-time call to create a new BDD node.

It appears that this code tries to reuse the implementation of the if-then-else 
BDD operation from file bddop.c in the BuDDy distribution, but while it is the 
valid implementation of the if-then-else BDD operation, it is unnecessary when 
loading a BDD from a file.

Notice the exponential allocation of BDD nodes in the resizing messages ("0 
free" BDD nodes after each resizing), only to be freed at the end (almost all 
BDD nodes freed at the end):

     [java] Loading initial relations: Loading BDD from file: thrOblAbbrCICM.bdd
     [java] Garbage collection #1: 499979 nodes / 0 free / 0.0s / 0.0090s total
     [java] Garbage collection #2: 499979 nodes / 0 free / 0.068s / 0.077s total
     [java] Resizing node table from 499979 to 1499933
     [java] Garbage collection #2: 1499933 nodes / 0 free / 0.0s / 0.077s total
     [java] Garbage collection #3: 1499933 nodes / 0 free / 0.173s / 0.25s total
     [java] Resizing node table from 1499933 to 4499783
     [java] Garbage collection #3: 4499783 nodes / 0 free / 0.0s / 0.25s total
     [java] Garbage collection #4: 4499783 nodes / 0 free / 0.546s / 0.796s total
     [java] Resizing node table from 4499783 to 13499327
     [java] Garbage collection #4: 13499327 nodes / 0 free / 0.0s / 0.796s total
     [java] Garbage collection #5: 13499327 nodes / 0 free / 1.869s / 2.665s total
     [java] Resizing node table from 13499327 to 23499323
     [java] Garbage collection #5: 23499323 nodes / 0 free / 0.0s / 2.665s total
     [java] Garbage collection #6: 23499323 nodes / 22599406 free / 0.623s / 3.288s total
     [java] Resizing node table from 23499323 to 33499267
     [java] 361318 nodes, 4.0256746E7 elements. 

Note: I have not fixed this bug for BuDDyFactory (i.e. I have left bddio.c 
untouched) but I have fixed it for JFactory.  The reason is that ProgramRel 
analyses in Chord use JFactory (you cannot create multiple BuDDyFactory 
instances simultaneously), and although Datalog analyses in Chord use 
BuDDyFactory, the code in BDDRelation.java actually loads a BDD from file using 
JFactory's load method that is written in Java, instead of using BuDDyFactory's 
load method which calls the bdd_fnload function in file bddio.c from the BuDDy 
distribution.

Original issue reported on code.google.com by mayur.naik on 11 Jul 2010 at 5:11

[GoogleCodeExporter]

"... and although Datalog analyses in Chord use BuDDyFactory, the code in 
BDDRelation.java actually loads a BDD from file using JFactory's load method 
that is written in Java, instead of using BuDDyFactory's load method ..."

This is incorrect: the code in BDDRelation.java loads a BDD from file using 
BDDFactory's load method (that is, neither JFactory's nor BuDDyFactory's):

    public BDD load(BufferedReader ifile, int[] translate) throws IOException {
        ...
        root = b.ite(high, low);
        ...
    }

The culprit is the "ite" call.  It needs to be replaced in a manner similar to 
my fix in JFactory's load method.  For now, I've switched the BDD factory to be 
used for solving Datalog analyses in chord to JFactory (by passing the 
"-Dbdd=j" option in chord/bddbddb/Solver.java); I've also added this option to 
the solve and debug targets in build.xml 

Original comment by mayur.naik on 11 Jul 2010 at 5:32

[GoogleCodeExporter]

Fixed in r935.  Changed the call solver.bdd.load(in) in BDDRelation.java in 
bddbddb to solver.bdd.load(in,map) where map is the map from variables used in 
the BDD file to be loaded to the corresponding variables already in the 
factory.  Works with both BuDDyFactory and JFactory.  

Original comment by mayur.naik on 12 Jul 2010 at 9:03

[GoogleCodeExporter]

Original comment by mayur.naik on 12 Jul 2010 at 9:04

• Changed state: Fixed