Sylvan is a parallel (multi-core) BDD library in C. Sylvan allows both sequential and parallel BDD-based algorithms to benefit from parallelism. Sylvan uses the work-stealing framework Lace and a scalable lockless hashtable to implement scalable multi-core BDD operations.
Dijk, T. van (2012) [The parallelization of binary decision diagram operations for model checking](http://essay.utwente.nl/61650/). Master’s Thesis, University of Twente, 27 April 2012.
T. van Dijk and J. van de Pol (2015) [Sylvan: Multi-core Decision Diagrams](http://dx.doi.org/10.1007/978-3-662-46681-0_60). In: TACAS 2015, LNCS 9035. Springer.
Dijk, T. van and Laarman, A.W. and Pol, J.C. van de (2012) [Multi-Core BDD Operations for Symbolic Reachability](http://eprints.eemcs.utwente.nl/22166/). In: 11th International Workshop on Parallel and Distributed Methods in verifiCation, PDMC 2012, 17 Sept. 2012, London, UK. Electronic Notes in Theoretical Computer Science. Elsevier.
T. van Dijk and A.W. Laarman and J. van de Pol (2012) [Multi-Core BDD Operations for Symbolic Reachability](http://eprints.eemcs.utwente.nl/22166/). In: PDMC 2012, ENTCS. Elsevier.
Usage
-----
For a quick demo, you can find an example of a simple BDD-based reachability algorithm in `test/mc.c`. This demo features both a sequential (bfs) and a parallel (par) symbolic reachability algorithm, demonstrating how both sequential programs and parallel programs can benefit from parallized BDD operations.
Simple examples can be found in the `examples` subdirectory. The file `simple.cpp` contains a toy program that
uses the C++ objects to perform basic BDD manipulation.
The `mc.c` and `lddmc.c` programs are more advanced examples of symbolic model checking (with example models in the `models` subdirectory).
To use Sylvan, include header file `sylvan.h`.
Sylvan depends on the [work-stealing framework Lace](http://fmt.ewi.utwente.nl/tools/lace) for its implementation. Currently, Lace is embedded in the Sylvan distribution, but this may change in the future. To use the BDD operations of Sylvan, you must first start Lace and run all workers.
Sylvan must be initialized after `lace_init` with a call to `sylvan_init`. This function takes three parameters: the log2 size of the BDD nodes table, the log2 size of the operation cache and the caching granularity. For example, `sylvan_init(16, 15, 4)` will initialize Sylvan with a BDD nodes table of size 65536, an operation cache of size 32768 and granularity 4. See below for detailed information about caching granularity.
Example C code for initialization:
```
#include<sylvan.h>
// initialize with queue size of 1000000
// autodetect number of workers
lace_init(0, 1000000);
// startup with defaults (create N-1 workers)
lace_startup(0, NULL, NULL);
// initialize with unique table size = 2^25
// cache table size = 2^24
// cache granularity = 4
sylvan_init(25, 24, 4);
```
Sylvan may require a larger than normal program stack. You may need to increase the program stack size on your system using `ulimit -s`. Segmentation faults on large computations typically indicate a program stack overflow.
Sylvan depends on the [work-stealing framework Lace](http://fmt.ewi.utwente.nl/tools/lace) for its implementation. Lace is embedded in the Sylvan distribution.
To use Sylvan, Lace must be initialized first.
For more details, see the comments in `src/sylvan.h`.
### Basic functionality
To create new BDDs, you can use:
- `sylvan_true`: representation of constant `true`.
- `sylvan_false`: representation of constant `false`.
- `sylvan_ithvar(var)`: representation of literal <var>.
- `sylvan_nithvar(var)`: representation of literal <var> negated.
- `sylvan_cube(variables, count, vector)`: create conjunction of variables in <variables> according to the corresponding value in <vector>.
- `sylvan_ithvar(var)`: representation of literal <var> (negated: `sylvan_nithvar(var)`)
To walk the BDD edges and obtain the variable at the root of a BDD, you can use:
To follow the BDD edges and obtain the variable at the root of a BDD, you can use:
- `sylvan_var(bdd)`: obtain variable of the root node of <bdd> - requires that <bdd> is not constant `true` or `false`.
- `sylvan_high(bdd)`: follow high edge of <bdd>.
- `sylvan_low(bdd)`: follow low edge of <bdd>.
@ -60,68 +41,57 @@ To walk the BDD edges and obtain the variable at the root of a BDD, you can use:
You need to manually reference BDDs that you want to keep during garbage collection:
- `sylvan_ref(bdd)`: add reference to <bdd>.
- `sylvan_deref(bdd)`: remove reference to <bdd>.
- `sylvan_protect(bddptr)`: add a pointer reference to the BDD variable <bddptr>
- `sylvan_unprotect(bddptr)`: remove a pointer reference to the BDD variable <bddptr>
See below for more detailed information about garbage collection. Note that garbage collection does not proceed outside BDD operations, e.g., you can safely call `sylvan_ref` on the result of a BDD operation.
It is recommended to use `sylvan_protect` and `sylvan_unprotect`.
The C++ objects handle this automatically.
The following 'primitives' are implemented:
- `sylvan_not(bdd)`: negation of <bdd>.
- `sylvan_ite(a,b,c)`: calculate 'if <a> then <b> else <c>'.
- `sylvan_exists(bdd, vars)`: existential quantification of <bdd> with respect to variables <vars>. Here, <vars> is a disjunction of literals.
Sylvan uses complement edges to implement negation, therefore negation is performed in constant time.
These primitives are used to implement the following operations:
- `sylvan_and(a, b)`
- `sylvan_or(a, b)`
- `sylvan_nand(a, b)`
- `sylvan_nor(a, b)`
- `sylvan_imp(a, b)` (a implies b)
- `sylvan_invimp(a, b)` (b implies a)
- `sylvan_xor(a, b)`
- `sylvan_equiv(a, b)` (alias: `sylvan_biimp`)
- `sylvan_diff(a, b)` (a and not b)
- `sylvan_less(a, b)` (b and not a)
- `sylvan_forall(bdd, vars)`
- `sylvan_and(a, b)`: calculate a and b
- `sylvan_or(a, b)`: calculate a or b
- `sylvan_nand(a, b)`: calculate not (a and b)
- `sylvan_nor(a, b)`: calculate not (a or b)
- `sylvan_imp(a, b)`: calculate a implies b
- `sylvan_invimp(a, b)`: calculate implies a
- `sylvan_xor(a, b)`: calculate a xor b
- `sylvan_equiv(a, b)`: calculate a = b
- `sylvan_diff(a, b)`: calculate a and not b
- `sylvan_less(a, b)`: calculate b and not a
- `sylvan_exists(bdd, vars)`: existential quantification of <bdd> with respect to variables <vars>. Here, <vars> is a conjunction of literals.
- `sylvan_forall(bdd, vars)`: universal quantification of <bdd> with respect to variables <vars>. Here, <vars> is a conjunction of literals.
### Other BDD operations
We also implemented the following BDD operations:
- `sylvan_restrict(f, c)`: calculate the restrict algorithm on f,c.
- `sylvan_constrain(f, c)`: calculate the constrain f@c, also called generalized co-factor (gcf).
- `sylvan_relprod_paired(a, t, vars)`: calculate the relational product by applying transition relation <t> on <a>. Assumes variables in <a> are even and primed variables (only in <t>) are odd and paired (i.e., x' = x+1). Assumes <t> is defined on variables in <vars>, which is a disjunction of literals, including non-primed and primed variables.
- `sylvan_relprod_paired_prev(a, t, vars)`: calculate the relational product backwards, i.e., calculate previous states instead of next states.
- `sylvan_support(bdd)`: calculate the support of <bdd>, i.e., all variables that occur in the BDD; returns a disjunction of literals.
- `sylvan_satcount(bdd, vars)`: calculate the number of assignments that satisfy <bdd> with respect to the variables in <vars>, which is a disjunction of literals.
- `sylvan_pathcount(bdd)`: calculate the number of distinct paths from the root node of <bdd> to constant 'true'.
- `sylvan_nodecount(bdd)`: calculate the number of nodes in <bdd> (not thread-safe).
- `sylvan_sat_one_bdd(bdd)`: calculate a cube that satisfies <bdd>.
- `sylvan_sat_one(bdd, vars, count, vector)`: reverse of `sylvan_cube` on the result of `sylvan_sat_one_bdd`. Alias: `sylvan_pick_cube`.
See `src/sylvan_bdd.h`, `src/sylvan_mtbdd.h` and `src/sylvan_ldd.h` for other implemented operations.
See `src/sylvan_obj.hpp` for the C++ interface.
### Garbage collection
Garbage collection is triggered when trying to insert a new node and no new bucket can be found within a reasonable upper bound. This upper bound is typically 8*(4+tablesize) buckets, where tablesize is the log2 size of the table. In practice, garbage collection occurs when the table is about 90% full. Garbage collection occurs by rehashing all BDD nodes that must stay in the table. It is designed such that all workers must cooperate on garbage collection. This condition is checked in `sylvan_gc_test()` which is called from every BDD operation and from a callback in the Lace framework that is called when there is no work.
Garbage collection is triggered when trying to insert a new node and no new bucket can be found within a reasonable upper bound.
Garbage collection is stop-the-world and all workers must cooperate on garbage collection. (Beware of deadlocks if you use Sylvan operations in critical sections!)
Caching granularity works as follows: with granularity G, each variable x is in a variable group x/G, e.g. the first G variables are in variable group 0, the next G variables are in variable group 1, etc.
BDD operations only consult the operation cache when they change variable groups.
### Table resizing
Higher granularity values result in less cache use. In practice, values between 4 and 8 tend to work well, but this depends on many factors, such as the structure and size of the BDDs and the characteristics of the computer architecture.
During garbage collection, it is possible to resize the nodes table and the cache.
Sylvan provides two default implementations: an agressive version that resizes every time garbage collection is performed,
and a less agressive version that only resizes when at least half the table is full.
This can be configured in `src/sylvan_config.h`
It is not possible to decrease the size of the nodes table and the cache.
### Dynamic reordering
Dynamic reordening is currently not supported.
We are interested in examples where this is necessary for good performance and would like to perform research into parallel dynamic reordering in future work.
For now, we suggest users find a good static variable ordering.
### Resizing tables
Resizing of nodes table and operation cache is currently not supported. In theory stop-the-world resizing can be implemented to grow the nodes table, but not to shrink the nodes table, since shrinking requires recreating all BDDs. Operation cache resizing is trivial to implement.
Please let us know if you need this functionality.
Troubleshooting
---------------
Sylvan may require a larger than normal program stack. You may need to increase the program stack size on your system using `ulimit -s`. Segmentation faults on large computations typically indicate a program stack overflow.
### I am getting the error "unable to allocate memory: ...!"
Sylvan allocates virtual memory using mmap. If you specify a combined size for the cache and node table larger than your actual available memory you may need to set `vm.overcommit_memory` to `1`. E.g. `echo 1 > /proc/sys/vm/overcommit_memory`. You can make this setting permanent with `echo "vm.overcommit_memory = 1" > /etc/sysctl.d/99-sylvan.conf`. You can verify the setting with `cat /proc/sys/vm/overcommit_memory`. It should report `1`.
Mavo
9 years ago