next up previous index
Next: Debugging Up: Programmer's Manual Previous: The Unique Table

Allowing Asynchronous Reordering

  

Asynchronous reordering is the reordering that is triggered automatically by the increase of the number of nodes. Asynchronous reordering takes place when a new internal node must be created, and the number of nodes has reached a given threshold . (The threshold is adjusted by the package every time reordering takes place.)

Those procedures that do not create new nodes (e.g., procedures that count the number of nodes or minterms ) need not worry about asynchronous reordering: No special precaution is necessary in writing them.

Procedures that only manipulate decision diagrams through the exported functions of the CUDD package also need not concern themselves with asynchronous reordering. (See Section 3.2.1 for the one exception.)

The remaining class of procedures is composed of functions that visit the diagrams and may create new nodes. All such procedures in the CUDD package are written so that they can be interrupted by dynamic reordering. The general approach followed goes under the name of ``abort and retry ." As the name implies, a computation that is interrupted by dynamic reordering is aborted and tried again.

A recursive procedure that can be interrupted by dynamic reordering (an interruptible  procedure from now on) is composed of two functions. One is responsible for the real computation. The other is a simple wrapper , which tests whether reordering occurred and restarts the computation if it did.

Asynchronous reordering of BDDs and ADDs can only be triggered inside cuddUniqueInter , when a new node is about to be created. Likewise, asynchronous reordering of ZDDs can only be triggered inside cuddUniqueInterZdd . When reordering is triggered, three things happen:

  1. cuddUniqueInter  returns a NULL value;
  2. The flag reordered of the manager is set to 1. (0 means no reordering, while 2 indicates an error occurred during reordering.)
  3. The counter reorderings of the manager is incremented. The counter is initialized to 0 when the manager is started and can be accessed by calling Cudd_ReadReorderings . By taking two readings of the counter, an application can determine if variable reordering has taken place between the first and the second reading. The package itself, however, does not make use of the counter: It is mentioned here for completeness.

The recursive procedure that receives a NULL value from cuddUniqueInter  must free all intermediate results that it may have computed before, and return NULL in its turn.

The wrapper  function does not decide whether reordering occurred based on the NULL return value, because the NULL value may be the result of lack of memory. Instead, it checks the reordered flag.

When a recursive procedure calls another recursive procedure that may cause reordering, it should bypass the wrapper and call the recursive procedure directly. Otherwise, the calling procedure will not know whether reordering occurred, and will not be able to restart. This is the main reason why most recursive procedures are internal, rather than static. (The wrappers, on the other hand, are mostly exported.)


next up previous index
Next: Debugging Up: Programmer's Manual Previous: The Unique Table

Fabio Somenzi
Tue May 12 18:47:58 MDT 1998