sp
/
tempest
1
0
Fork 0
Code Issues Pull Requests Projects Releases Wiki Activity
You can not select more than 25 topics Topics must start with a letter or number, can include dashes ('-') and can be up to 35 characters long.
2666 Commits
1 Branch
0 Tags
187 MiB
Tree: 5b6dcd0eed
Branches Tags
${ item.name }
Create tag ${ searchTerm }
Create branch ${ searchTerm }
from '5b6dcd0eed'
${ noResults }
tempest/resources/3rdparty/sylvan/README.md

127 lines
8.4 KiB
Raw Normal View History

added sylvan and started making it compile using cmake Former-commit-id: b6b6171d0fa0b2f9b5f59112cf1f774ef2ebb595
9 years ago
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
​
  1. Sylvan
  2. ======
  3. 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.
  5. Sylvan is developed (© 2011-2014) by the [Formal Methods and Tools](http://fmt.ewi.utwente.nl/) group at the University of Twente as part of the MaDriD project, which is funded by NWO. Sylvan is licensed with the Apache 2.0 license.
  7. You can contact the main author of Sylvan at <t.vandijk@utwente.nl>. Please let us know if you use Sylvan in your projects.
  9. Sylvan is available at: https://github.com/utwente-fmt/sylvan
  10. Java/JNI bindings: https://github.com/trolando/jsylvan
  11. Haskell bindings: https://github.com/adamwalker/sylvan-haskell
  13. Publications
  14. ------------
  15. 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.
  17. 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.
  19. Usage
  20. -----
  21. 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.
  23. To use Sylvan, include header file `sylvan.h`.
  25. 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.
  27. 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.
  29. Example C code for initialization:
  30. ```
  31. #include <sylvan.h>
  33. // initialize with queue size of 1000000
  34. // autodetect number of workers
  35. lace_init(0, 1000000);
  36. // startup with defaults (create N-1 workers)
  37. lace_startup(0, NULL, NULL);
  38. // initialize with unique table size = 2^25
  39. // cache table size = 2^24
  40. // cache granularity = 4
  41. sylvan_init(25, 24, 4);
  42. ```
  44. 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.
  46. ### Basic functionality
  48. To create new BDDs, you can use:
  49. - `sylvan_true`: representation of constant `true`.
  50. - `sylvan_false`: representation of constant `false`.
  51. - `sylvan_ithvar(var)`: representation of literal &lt;var&gt;.
  52. - `sylvan_nithvar(var)`: representation of literal &lt;var&gt; negated.
  53. - `sylvan_cube(variables, count, vector)`: create conjunction of variables in &lt;variables&gt; according to the corresponding value in &lt;vector&gt;.
  55. To walk the BDD edges and obtain the variable at the root of a BDD, you can use:
  56. - `sylvan_var(bdd)`: obtain variable of the root node of &lt;bdd&gt; - requires that &lt;bdd&gt; is not constant `true` or `false`.
  57. - `sylvan_high(bdd)`: follow high edge of &lt;bdd&gt;.
  58. - `sylvan_low(bdd)`: follow low edge of &lt;bdd&gt;.
  60. You need to manually reference BDDs that you want to keep during garbage collection:
  61. - `sylvan_ref(bdd)`: add reference to &lt;bdd&gt;.
  62. - `sylvan_deref(bdd)`: remove reference to &lt;bdd&gt;.
  64. 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.
  66. The following 'primitives' are implemented:
  67. - `sylvan_not(bdd)`: negation of &lt;bdd&gt;.
  68. - `sylvan_ite(a,b,c)`: calculate 'if &lt;a&gt; then &lt;b&gt; else &lt;c&gt;'.
  69. - `sylvan_exists(bdd, vars)`: existential quantification of &lt;bdd&gt; with respect to variables &lt;vars&gt;. Here, &lt;vars&gt; is a disjunction of literals.
  71. Sylvan uses complement edges to implement negation, therefore negation is performed in constant time.
  73. These primitives are used to implement the following operations:
  74. - `sylvan_and(a, b)`
  75. - `sylvan_or(a, b)`
  76. - `sylvan_nand(a, b)`
  77. - `sylvan_nor(a, b)`
  78. - `sylvan_imp(a, b)` (a implies b)
  79. - `sylvan_invimp(a, b)` (b implies a)
  80. - `sylvan_xor(a, b)`
  81. - `sylvan_equiv(a, b)` (alias: `sylvan_biimp`)
  82. - `sylvan_diff(a, b)` (a and not b)
  83. - `sylvan_less(a, b)` (b and not a)
  84. - `sylvan_forall(bdd, vars)`
  86. ### Other BDD operations
  88. We also implemented the following BDD operations:
  89. - `sylvan_restrict(f, c)`: calculate the restrict algorithm on f,c.
  90. - `sylvan_constrain(f, c)`: calculate the constrain f@c, also called generalized co-factor (gcf).
  91. - `sylvan_relprod_paired(a, t, vars)`: calculate the relational product by applying transition relation &lt;t&gt; on &lt;a&gt;. Assumes variables in &lt;a&gt; are even and primed variables (only in &lt;t&gt;) are odd and paired (i.e., x' = x+1). Assumes &lt;t&gt; is defined on variables in &lt;vars&gt;, which is a disjunction of literals, including non-primed and primed variables.
  92. - `sylvan_relprod_paired_prev(a, t, vars)`: calculate the relational product backwards, i.e., calculate previous states instead of next states.
  93. - `sylvan_support(bdd)`: calculate the support of &lt;bdd&gt;, i.e., all variables that occur in the BDD; returns a disjunction of literals.
  94. - `sylvan_satcount(bdd, vars)`: calculate the number of assignments that satisfy &lt;bdd&gt; with respect to the variables in &lt;vars&gt;, which is a disjunction of literals.
  95. - `sylvan_pathcount(bdd)`: calculate the number of distinct paths from the root node of &lt;bdd&gt; to constant 'true'.
  96. - `sylvan_nodecount(bdd)`: calculate the number of nodes in &lt;bdd&gt; (not thread-safe).
  97. - `sylvan_sat_one_bdd(bdd)`: calculate a cube that satisfies &lt;bdd&gt;.
  98. - `sylvan_sat_one(bdd, vars, count, vector)`: reverse of `sylvan_cube` on the result of `sylvan_sat_one_bdd`. Alias: `sylvan_pick_cube`.
  100. ### Garbage collection
  102. 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.
  104. - `sylvan_gc()`: manually trigger garbage collection.
  105. - `sylvan_gc_enable()`: enable garbage collection.
  106. - `sylvan_gc_disable()`: disable garbage collection.
  108. ### Caching granularity
  110. 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.
  111. BDD operations only consult the operation cache when they change variable groups.
  113. 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.
  115. ### Dynamic reordering
  117. Dynamic reordening is currently not supported.
  118. 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.
  120. For now, we suggest users find a good static variable ordering.
  122. ### Resizing tables
  124. 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.
  126. Please let us know if you need this functionality.