buddy-developers — Participating in BuDDy development

[Buddy-developers] [ buddy-Bugs-1111195 ] bug in mark_roots causes BDD corruption

[SourceForge.net <no...@so...>]

Bugs item #1111195, was opened at 2005-01-27 19:05
Message generated for change (Comment added) made by joewhaley
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1111195&group_id=112658

Category: code
Group: None
>Status: Closed
Resolution: None
Priority: 8
Submitted By: John Whaley (joewhaley)
Assigned to: John Whaley (joewhaley)
Summary: bug in mark_roots causes BDD corruption

Initial Comment:

I have tracked down a tricky bug involving garbage
collection and variable reordering.  When calling
setvarorder(), some BDDs are not getting reordered,
leading to invalid BDDs because the levels are no
longer monotonically increasing.  This bug affects all
BDD reordering (swapvar, dynamic reordering, etc.)

The problem seems to be in the construction of the
dependency imatrix.  mark_roots() is supposed to mark
the externally-accessible BDD references and mark which
variables depend on each other in the imatrix.

mark_roots() calls addref_rec(), which is supposed to
recurse down the BDD, adding variable dependencies. 
mark_roots() uses "REF(r) == 0" to test whether or not
it has already visited and therefore computed the
dependencies for a BDD node.

Herein lies the problem.  If an internal BDD node has
an external reference, its refcount will not be zero,
and mark_roots() will assume it has computed the
imatrix dependencies when it has not.

The whole mark_roots() process seems to assume that it
can use the refcount field as a marker for BDD nodes. 
This is wrong and we should think about the right way
to do this.  We may need to use an external table instead.

Coming up with a test case that exhibits the bug is
nontrivial because the BDDs must be allocated in a
non-sequential order.  For this to happen, there must
have been a garbage collection in the past where nodes
were reclaimed and new nodes were given numbers before
old nodes.


----------------------------------------------------------------------

>Comment By: John Whaley (joewhaley)
Date: 2005-01-28 13:24

Message:
Logged In: YES 
user_id=93687

Fixed in CVS.
I will be doing a new release shortly.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1111195&group_id=112658

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv21226/src

Modified Files:
	reorder.c 
Log Message:
Oops, reversed the test condition.

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv13558/src

Modified Files:
	reorder.c 
Log Message:
Probable fix for Bug#1111195:
bug in mark_roots causes BDD corruption

[Buddy-developers] bug in buddy library: reordering

[John W. <jw...@st...>]

I have tracked down a tricky bug involving garbage collection and variable
reordering.  When calling setvarorder(), some BDDs are not getting
reordered, leading to invalid BDDs because the levels are no longer
monotonically increasing.  This bug affects all BDD reordering (swapvar,
dynamic reordering, etc.)

This is a serious bug because it will cause the library to silently give
incorrect results to BDD operations.

The problem seems to be in the construction of the dependency imatrix.
mark_roots() is supposed to mark the externally-accessible BDD references
and mark which variables depend on each other in the imatrix.

mark_roots() calls addref_rec(), which is supposed to recurse down the BDD,
adding variable dependencies.  mark_roots() uses "REF(r) == 0" to test
whether or not it has already visited and therefore computed the
dependencies for a BDD node.

Herein lies the problem. If an internal BDD node has an external reference,
its refcount will not be zero, and mark_roots() will assume it has computed
the imatrix dependencies when it has not.

The whole mark_roots() process seems to assume that it can use the refcount
field as a marker for BDD nodes.  This is wrong and we should think about
the right way to do this. We may need to use an external table instead.

Coming up with a test case that exhibits the bug is nontrivial because the
BDDs must be allocated in a non-sequential order.  For this to happen, there
must have been a garbage collection in the past where nodes were reclaimed
and new nodes were given numbers before old nodes.  Thus, all of the test
cases that exhibit the bug are rather large.

-John

[Buddy-developers] [ buddy-Bugs-1111195 ] bug in mark_roots causes BDD corruption

[SourceForge.net <no...@so...>]

Bugs item #1111195, was opened at 2005-01-27 19:05
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1111195&group_id=112658

Category: code
Group: None
Status: Open
Resolution: None
Priority: 8
Submitted By: John Whaley (joewhaley)
Assigned to: John Whaley (joewhaley)
Summary: bug in mark_roots causes BDD corruption

Initial Comment:

I have tracked down a tricky bug involving garbage
collection and variable reordering.  When calling
setvarorder(), some BDDs are not getting reordered,
leading to invalid BDDs because the levels are no
longer monotonically increasing.  This bug affects all
BDD reordering (swapvar, dynamic reordering, etc.)

The problem seems to be in the construction of the
dependency imatrix.  mark_roots() is supposed to mark
the externally-accessible BDD references and mark which
variables depend on each other in the imatrix.

mark_roots() calls addref_rec(), which is supposed to
recurse down the BDD, adding variable dependencies. 
mark_roots() uses "REF(r) == 0" to test whether or not
it has already visited and therefore computed the
dependencies for a BDD node.

Herein lies the problem.  If an internal BDD node has
an external reference, its refcount will not be zero,
and mark_roots() will assume it has computed the
imatrix dependencies when it has not.

The whole mark_roots() process seems to assume that it
can use the refcount field as a marker for BDD nodes. 
This is wrong and we should think about the right way
to do this.  We may need to use an external table instead.

Coming up with a test case that exhibits the bug is
nontrivial because the BDDs must be allocated in a
non-sequential order.  For this to happen, there must
have been a garbage collection in the past where nodes
were reclaimed and new nodes were given numbers before
old nodes.


----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1111195&group_id=112658

[Buddy-developers] [ buddy-Bugs-1040620 ] Bug in bdd_appuni and in bdd_unique

[SourceForge.net <no...@so...>]

Bugs item #1040620, was opened at 2004-10-05 14:52
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658

Category: None
Group: None
Status: Open
Resolution: None
Priority: 5
Submitted By: Christophe Mauras (mauras)
Assigned to: Nobody/Anonymous (nobody)
Summary: Bug in bdd_appuni and in bdd_unique

Initial Comment:
It seems to me there is a bug in bdd_appuni and same in
bdd_unique. These operations may not depend on variable
order :

   Exists unique x0 such that (x0 or x1)
= (x0 or x1)[x0\0] xor (x0 or x1)[x0\1]
= x1 xor true
= not x1

   Exists unique x1 such that x0 or x1
= (x0 or x1)[x1\0] xor (x0 or x1)[x1\1]
= x0 xor true
= not x0
Here is the bug : Buddy reply 1

More simply :
  Exists unique x0 such that true
= (true)[x0\0] xor (true)[x0\1]
= true xor true
= false
Buddy reply 1

Please look at following code :

----------------------------------
#include "bdd.h"
#include "stdio.h"

main(void)
{
  bdd x0,x1,y0,y1,z0,z1,t;
  bdd_init (100,10);
  bdd_setvarnum(5);
  x0 = bdd_ithvar(0);
  x1 = bdd_ithvar(1);

  y0 = bdd_appuni(x0,x1,bddop_or,x0);
  printf("Result should be  1: 1 0 \n");
  bdd_printtable(y0);
  printf("Good!\n\n");

  y1 = bdd_appuni(x0,x1,bddop_or,x1);
  printf("Result should be  0: 1 0 \n");
  bdd_printtable(y1);
  printf("Bad !\n");

  z0 = bdd_unique(bdd_or(x0,x1),x0);
  printf("Result should be  1: 1 0 \n");
  bdd_printtable(z0);
  printf("Good!\n\n");

  z1 = bdd_unique(bdd_or(x0,x1),x1);
  printf("Result should be  0: 1 0 \n");
  bdd_printtable(z1);
  printf("Bad !\n");

  t = bdd_unique(bdd_true(), x0);
  printf("Result should be  0 \n");
  bdd_printtable(z1);
  printf("Bad !\n");


  bdd_done();
}

   


----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1040620&group_id=112658

[Buddy-developers] performance improvements to check in

[John W. <jw...@st...>]

I have a few possible performance updates to buddy that I can check in.

- Optimized cache entry structure.  The current version of buddy wastes 1 to
2 words of space on every cache entry.  I have a simple patch that fixes
this problem, improving performance by ~5% on programs that make use of the
cache, while also reducing memory usage.  It will also allocate the caches
on demand, so operation caches will not be allocated until they are actually
used.

- Hardware prefetch directives.  BDDs are very memory-bound: Profiling the
BDD library with VTune shows that over 80% of the time is spent on L2 cache
misses.  Although there are many true dependencies in the code, some amount
of prefetching is possible and beneficial (~5% performance improvement).
The prefetch calls do not change the semantics of the code and are ignored
on architectures that do not support them.

- Specialized code for apply operators.  Right now, there is one function
(apply_rec) for all apply operators.  This means at every node, it must do a
switch on the operator.  By splitting operations into separate functions,
performance is improved due to tighter code and more optimization
opportunities.  Also, using separate caches for different operations reduces
the cache entry size by a word, speeds up hash computations, improves cache
hit rates and reduces collisions.

I have been using these modifications for a while with no problems.  What do
people think about them?  The first two are fairly minor.  The third is more
involved because it increases the amount of code, but is still
straightforward.

Also, was there any consensus on the other patches I described earlier
(support for automatic generation of BDD traces and preallocation of node
table)?  I've been sitting on those in my local version for the last few
months and they seem rock solid.

One option is I could check in the changes on an experimental branch until
they are proven to be stable and worthwhile, at which point we could merge
it back into the trunk.

-John

PS. The recent lrand48() change broke the Windows build so I'll check in a
small fix that makes it compile cleanly again on Windows.

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv16714

Modified Files:
	bddop.c kernel.c 
Log Message:
Allow buddy to be reinitialized after calling "done()" without
core-dumping.  Some fields were not reset to NULL, so the second
time you called bdd_done() it would lead to a core dump.

[Buddy-developers] Files have been committed to CVS

[Haim C. <hai...@us...>]

Update of /cvsroot/buddy/buddy
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv30893

Modified Files:
	ChangeLog 
Log Message:
Updating after committing files

[Buddy-developers] Files have been committed to CVS

[Haim C. <hai...@us...>]

Update of /cvsroot/buddy/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv25286/src

Modified Files:
	kernel.c kernel.h prime.c reorder.c 
Log Message:

rand() was replaced by lrand48() because:
1. rand() seems to have different implementations on different platforms.
2. rand man pages explain it might have not-so-random LSBs, so it is not
goot to use it with % to randomize numbers to to limit. 
Since lrand48() does not have default seed, ( like rand() has ) the 
pseudo random generator of lrand48 is seeded with arbitrary seed in bdd_init().

[Buddy-developers] [ buddy-Bugs-1002675 ] bddtest test fails on solaris

[SourceForge.net <no...@so...>]

Bugs item #1002675, was opened at 2004-08-03 18:16
Message generated for change (Settings changed) made by haimcohen
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1002675&group_id=112658

Category: other
Group: None
>Status: Closed
>Resolution: Fixed
Priority: 1
Submitted By: Haim Cohen (haimcohen)
>Assigned to: Haim Cohen (haimcohen)
Summary: bddtest test fails on solaris

Initial Comment:
The test fails when running on Solaris.
The reason is because this test use rand(), which gives
different sequence on Linux and Solaris.

The solution is to use lrand48() ( together with
srand48() ), which has a  well defined linear
congruential formula, so it gives the same sequence on
both systems.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1002675&group_id=112658

[Buddy-developers] Files have been committed to CVS

[Haim C. <hai...@us...>]

Update of /cvsroot/buddy/buddy/examples/bddtest
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv23741/examples/bddtest

Modified Files:
	bddtest.cxx expected 
Log Message:

Fixing 'bug' [ 1002675 ] bddtest test fails on solaris.
Since the test uses rand() which seems to have different
implemetnations, it was replaced by lrand48() which man pages say it
has a well defined formula.

[Buddy-developers] [ buddy-Bugs-1002675 ] bddtest test fails on solaris

[SourceForge.net <no...@so...>]

Bugs item #1002675, was opened at 2004-08-03 18:16
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1002675&group_id=112658

Category: other
Group: None
Status: Open
Resolution: None
Priority: 1
Submitted By: Haim Cohen (haimcohen)
Assigned to: Nobody/Anonymous (nobody)
Summary: bddtest test fails on solaris

Initial Comment:
The test fails when running on Solaris.
The reason is because this test use rand(), which gives
different sequence on Linux and Solaris.

The solution is to use lrand48() ( together with
srand48() ), which has a  well defined linear
congruential formula, so it gives the same sequence on
both systems.

----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1002675&group_id=112658

[Buddy-developers] Files have been committed to CVS

[Haim C. <hai...@us...>]

Update of /cvsroot/buddy/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv24914

Modified Files:
	kernel.c 
Log Message:

Improvement by Alexandre Duret-Lutz:
This changes the default handler to abort().
This is much more useful because since that will preserve the
context in a coredump, and from their you can narrow the bug in
your application.

[Buddy-developers] Files have been committed to CVS

[Haim C. <hai...@us...>]

Update of /cvsroot/buddy/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv26561

Modified Files:
	bddop.c 
Log Message:
Fixing documentation typos. Patch was submitted by Alexandre

Re: [Buddy-developers] Checked in satcount() bug fix

[Haim C. <hai...@us...>]

John,

Please see my comments below.

>
>1. Automatic generation of BDD trace files.  This is controlled by a
>compile-time switch, so if you don't define the switch, nothing is changed.
>Basically it involves adding a line at the start of every BDD API function,
>and changing "return" instructions to a "RETURN" macro.  It touches almost
>every function in BuDDy, but I think it is pretty minor because it will be
>disabled by default.
>  
>
That's a nice feature, but one can easily use gprof to analyze the trace 
of a program.
It gives you a nice dynamic call graph. However, it does not trace 
parameters and return values to/from functions.
You can add such mechanism to every program, but - isn't that what 
debuggers are for ?
My opinion is that it is a "nice to have" debugging feature.
We can wait for other developers' comments.

>2. Preallocation of memory for node table.  Without this patch, BuDDy runs
>out of memory very quickly, especially on Windows machines (at as low as 12M
>nodes).  This patch reduces the fragmentation by preallocating a large
>memory area and performing initialization on demand.  This is about a 10
>line patch.
>
Sounds like a good performance improvement to me.
I think it must be tested with various node table's initial size and 
size increasing parameters.
My opinion is to go ahead with this and commit to CVS.

>that I can check them in under a new CVS branch until people are convinced
>of the stability.
>  
>
I think that we should minimize branching to minimum. Having one 
code-stream will give all of us the option to check all the features 
combined together.

However, you should be confident in the code you commit.

As I said earlier - the person who commit to CVS should be careful and 
commit near-to-stable code, and the person who update from CVS should 
regard CVS with suspicion about its stability. I think that this 
approach will be the most helpful to keep buddy bug rate to minimum, 
while still keeping innovation.

I would appreciate your comments, John.

Haim

[Buddy-developers] Files have been committed to CVS

[Haim C. <hai...@us...>]

Update of /cvsroot/buddy/buddy
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv12795

Modified Files:
	AUTHORS 
Log Message:
Update authors list

[Buddy-developers] Checked in satcount() bug fix

[John W. <jw...@st...>]

I've checked in a fix to the satcount() bug, and added a regression test to
check for it.

I was wondering what I should check in next.  I have two more items in the
patch I sent around:

1. Automatic generation of BDD trace files.  This is controlled by a
compile-time switch, so if you don't define the switch, nothing is changed.
Basically it involves adding a line at the start of every BDD API function,
and changing "return" instructions to a "RETURN" macro.  It touches almost
every function in BuDDy, but I think it is pretty minor because it will be
disabled by default.

2. Preallocation of memory for node table.  Without this patch, BuDDy runs
out of memory very quickly, especially on Windows machines (at as low as 12M
nodes).  This patch reduces the fragmentation by preallocating a large
memory area and performing initialization on demand.  This is about a 10
line patch.

I sent the proposed patches to the mailing list earlier.  Does anyone have
any thoughts/ideas/concerns about these changes?  Another alternative is
that I can check them in under a new CVS branch until people are convinced
of the stability.

-John

[Buddy-developers] [ buddy-Bugs-1000596 ] satcount gives incorrect answers after setvarnum

[SourceForge.net <no...@so...>]

Bugs item #1000596, was opened at 2004-07-30 02:23
Message generated for change (Settings changed) made by joewhaley
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1000596&group_id=112658

Category: code
Group: v1.0 (example)
>Status: Closed
>Resolution: Fixed
Priority: 5
Submitted By: John Whaley (joewhaley)
Assigned to: John Whaley (joewhaley)
Summary: satcount gives incorrect answers after setvarnum

Initial Comment:
satcount gives incorrect answers after calling 
setvarnum.  This is because it uses the values in the 
cache when computing satcount, and the cache is not 
cleared when setvarnum is called.



----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1000596&group_id=112658

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy/examples
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8187/examples

Modified Files:
	Makefile.am 
Log Message:
Added a regression test case for the satcount() bug.

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8187

Modified Files:
	configure.ac 
Log Message:
Added a regression test case for the satcount() bug.

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy/examples/bddsatcountbug
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv8077/bddsatcountbug

Added Files:
	.cvsignore Makefile.am bddsatcountbug.c expected runtest 
Log Message:
Added a regression test case for the satcount() bug.

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy/examples/bddsatcountbug
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7912/bddsatcountbug

Log Message:
Directory /cvsroot/buddy/buddy/examples/bddsatcountbug added to the repository

[Buddy-developers] Files have been committed to CVS

[John W. <joe...@us...>]

Update of /cvsroot/buddy/buddy/src
In directory sc8-pr-cvs1.sourceforge.net:/tmp/cvs-serv7684

Modified Files:
	bddop.c 
Log Message:
Fixed the bug with satcount().
The misccache should be cleared after changing the number of variables,
because satcount() results in the misccache depend on the number of
BDD variables.

[Buddy-developers] [ buddy-Bugs-1000596 ] satcount gives incorrect answers after setvarnum

[SourceForge.net <no...@so...>]

Bugs item #1000596, was opened at 2004-07-30 02:23
Message generated for change (Tracker Item Submitted) made by Item Submitter
You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1000596&group_id=112658

Category: code
Group: v1.0 (example)
Status: Open
Resolution: None
Priority: 5
Submitted By: John Whaley (joewhaley)
Assigned to: John Whaley (joewhaley)
Summary: satcount gives incorrect answers after setvarnum

Initial Comment:
satcount gives incorrect answers after calling 
setvarnum.  This is because it uses the values in the 
cache when computing satcount, and the cache is not 
cleared when setvarnum is called.



----------------------------------------------------------------------

You can respond by visiting: 
https://sourceforge.net/tracker/?func=detail&atid=662728&aid=1000596&group_id=112658