trolando / sylvan Goto Github PK

Hi, I find this issue again...

When I monitored the "Bdd::ExistAbstract" Function, I found that, as the number of workers increases, so does the computational overhead of the "sylvan_exist(cube)" function, as well as sylvan_and_exist(sylvan_true, cube).

Logically, I think it should be that the more workers there are, the faster the function runs.

Hello,

My program consists of 3 phases in which Sylvan is used in first two phases:

1. Construct MTBDDs using external API operations like sum/product/abstract etc
2. Traverse the constructed MTBDDs to create a custom copy of the mtbdd DAGs represented using my own sylvan-independent datastructure. I use mtbdd_gethigh/low, as well as sylvan internals like MTBDD_GETNODE and mtbdd_getvar. I store mtbddnode_t values returned by MTBDD_GETNODE in an stl unordered_map to ensure I'm not re-processing already visited nodes
3. Perform operations on my datastructure created in phase 2, without using sylvan in anyway

My program is running without errors to completion in both cases when n_workers is set to 0 (auto detect) as well as 1 (single threaded). However, I noticed that when n_workers is set to 0 (running 8 threads since there are 8 cores on my pc), the CPU usage remains at close to 800% even in phase 3 (i.e. after all sylvan operations should have ceased). This is unexpected because I am not doing any multithreading in my program (or interacting with LACE) in phase 3. The running time of phase 3 is actually taking a hit as compared to running with n_workers set to 1. Ideally, I would like to use multiple threads only in phase 1, while both phase 2 and 3 should run with just 1 thread. How would you recommend going about resolving this?

Note: I am using a version of Sylvan from before the recent API breaking changes for compatibility reasons. (commit 5e9da7)

Thanks!
Aditya

(filing new case here, just realised I created the issue on the mirror repo)

Just tried building latest on macOS:

jocke@solid sylvan-master % clang --version
Apple clang version 12.0.0 (clang-1200.0.32.28)
Target: x86_64-apple-darwin20.2.0
Thread model: posix
InstalledDir: /Library/Developer/CommandLineTools/usr/bin
jocke@solid sylvan-master % 
jocke@solid sylvan-master % make && make test && make install
Scanning dependencies of target sylvan
[  5%] Building C object src/CMakeFiles/sylvan.dir/lace.c.o
[ 10%] Building C object src/CMakeFiles/sylvan.dir/sha2.c.o
[ 15%] Building C object src/CMakeFiles/sylvan.dir/sylvan_bdd.c.o
[ 20%] Building C object src/CMakeFiles/sylvan.dir/sylvan_cache.c.o
[ 25%] Building C object src/CMakeFiles/sylvan.dir/sylvan_common.c.o
/Users/jocke/source/sylvan-master/src/sylvan_common.c:309:26: error: overlapping comparisons always evaluate to false [-Werror,-Wtautological-overlap-compare]
    if (table_ratio > 10 && table_ratio < 10) {
        ~~~~~~~~~~~~~~~~~^~~~~~~~~~~~~~~~~~~
1 error generated.
make[2]: *** [src/CMakeFiles/sylvan.dir/sylvan_common.c.o] Error 1
make[1]: *** [src/CMakeFiles/sylvan.dir/all] Error 2
make: *** [all] Error 2
jocke@solid sylvan-master % 

While trying to build sylvan on macOS 11.3 using Apple Clang 12.0.5 and the latest version of the xcode command line tools I run into the following issue:

/Users/bork/sylvan/src/lace.c:496:9: error: 'sem_init' is deprecated [-Werror,-Wdeprecated-declarations]
        sem_init(&et.sem, 0, 0);
        ^
/Users/bork/sylvan/src/lace.c:503:9: error: 'sem_destroy' is deprecated [-Werror,-Wdeprecated-declarations]
        sem_destroy(&et.sem);
        ^
/Users/bork/sylvan/src/lace.c:694:5: error: 'sem_init' is deprecated [-Werror,-Wdeprecated-declarations]
    sem_init(&suspend_semaphore, 0, 0);
    ^
/Users/bork/sylvan/src/lace.c:911:5: error: 'sem_destroy' is deprecated [-Werror,-Wdeprecated-declarations]
    sem_destroy(&suspend_semaphore);
    ^

I just had a first good look at the ZDD branch that needs to be merged eventually with master.

Most of is it good state.

Unfortunately the examples are not all working well, the satdd program has a weird crash that I need to figure out first. And I'm also not completely happy with all the code duplication related to reference management.

I also noticed that I was working on an inventory of desirable ZDD functions, based on what is supported by CUDD and the EXTRA extension to ZDD. What I actually implemented in the ZDD branch is everything I needed to play with "representing SAT clauses using a ZDD" which is still somewhat limited, although usable. So I need to convert this into a better overview or maybe a roadmap of some sorts.

Another observation is that a lot of the functionality that is in MTBDD would be useful for ZDD. For example, why should we duplicate all the leaf management? First of all most use cases probably don't have mixed decision diagrams. So the only expected leaves would be either the int/double/fraction/custom leaf that is expected, or False if some input is not in the domain of the set.

Then another thing I noticed is that I was experimenting with a kind-of complement edge to have a little bit of compression on the tree. It's not a true complement edge, they don't work well with ZDDs. But I don't completely recall the semantics and how it was supposed to work. I'd have to reverse engineer that.

Hello,

I was trying to incorporate the latest version on Sylvan into my program, as my progam was still using a much older commit from 2021, before the API breaking changes to Lace. While attempting this, I noticed some inconsistencies in the docs at https://trolando.github.io/sylvan/# and the current codebase. I might be missing something obvious, but was unable to pinpoint the issue.

Firstly the lace functions for init and exit seem to have changed as compared to the docs. I was able to fix those errors by looking at the examples and changing them (lace_start / lace_startup , lace_exit/lace_stop)

Secondly, the macro LACE_ME no longer seems to be available -- is this by design or is there some error on my side? Is it still needed?

More importantly, I am getting a weird compilation error when I try to compile with the functions gmp_plus, gmp_max etc:

‘mtbdd_apply_RUN’ was not declared in this scope; did you mean ‘sylvan::mtbdd_apply_RUN’

(see the attached file for full compiler output).

Any help is appreciated.

Thanks,
Aditya
compilation_errors.txt

I notice that there are no functions to update the reference in sylvan_obj.cpp, just like "example/simple.cpp" (which is a simple task written with sylvan_obj). So I wonder when do I need to update the reference manually, like using Sylvan.sylvan_ref().

Hello,

I am running into an issue with memory when using Sylvan with multi-precision (GMP) enabled. I notice that the memory usage spikes very quickly and I sometimes encounter the following error:

GNU MP: Cannot reallocate memory (old_size=8 new_size=3088)

Since the memory usage is reasonable when not using GMP, I assume the reason is because of the overhead of having to store large precision numbers. I wanted to check if you think this is the likely case or if there is an alternative explanation. Either way, is there any workaround to this problem? For example, I am currently initializing Sylvan with Table ratio 1 and Init ratio 10 -- will it help to use some other values?

Thanks,
Aditya

When trying to build LTSmin with the newest version of Sylvan (as on this repository) then one gets the error messages below. Somehow LACE was not build or installed together with Sylvan.

Maybe one needs to install LACE independently? Maybe from its own repo? If so, then one needs to fix trolando/lace#6 .

sylvan.Tpo -c vset_sylvan.c -o libvset_la-vset_sylvan.o
vset_sylvan.c: In function ‘set_create’:
vset_sylvan.c:99:5: error: ‘LACE_ME’ undeclared (first use in this function)
   99 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c:99:5: note: each undeclared identifier is reported only once for each function it appears in
vset_sylvan.c: In function ‘rel_create_rw’:
vset_sylvan.c:257:5: error: ‘LACE_ME’ undeclared (first use in this function)
  257 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_add’:
vset_sylvan.c:426:9: error: ‘LACE_ME’ undeclared (first use in this function)
  426 |         LACE_ME;
      |         ^~~~~~~
vset_sylvan.c: In function ‘set_member’:
vset_sylvan.c:459:9: error: ‘LACE_ME’ undeclared (first use in this function)
  459 |         LACE_ME;
      |         ^~~~~~~
vset_sylvan.c: In function ‘set_update’:
vset_sylvan.c:584:5: error: ‘LACE_ME’ undeclared (first use in this function)
  584 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_enum_match’:
vset_sylvan.c:616:5: error: ‘LACE_ME’ undeclared (first use in this function)
  616 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_copy_match’:
vset_sylvan.c:670:5: error: ‘LACE_ME’ undeclared (first use in this function)
  670 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_count’:
vset_sylvan.c:708:5: error: ‘LACE_ME’ undeclared (first use in this function)
  708 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘rel_count’:
vset_sylvan.c:716:5: error: ‘LACE_ME’ undeclared (first use in this function)
  716 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_union’:
vset_sylvan.c:728:5: error: ‘LACE_ME’ undeclared (first use in this function)
  728 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_intersect’:
vset_sylvan.c:751:5: error: ‘LACE_ME’ undeclared (first use in this function)
  751 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_minus’:
vset_sylvan.c:764:5: error: ‘LACE_ME’ undeclared (first use in this function)
  764 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_next’:
vset_sylvan.c:779:5: error: ‘LACE_ME’ undeclared (first use in this function)
  779 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_prev’:
vset_sylvan.c:793:5: error: ‘LACE_ME’ undeclared (first use in this function)
  793 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_project’:
vset_sylvan.c:816:9: error: ‘LACE_ME’ undeclared (first use in this function)
  816 |         LACE_ME;
      |         ^~~~~~~
vset_sylvan.c: In function ‘set_zip’:
vset_sylvan.c:831:5: error: ‘LACE_ME’ undeclared (first use in this function)
  831 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘rel_add_act’:
vset_sylvan.c:852:5: error: ‘LACE_ME’ undeclared (first use in this function)
  852 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘rel_add_cpy’:
vset_sylvan.c:943:5: error: ‘LACE_ME’ undeclared (first use in this function)
  943 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘rel_update’:
vset_sylvan.c:1064:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1064 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_least_fixpoint’:
vset_sylvan.c:1258:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1258 |     LACE_ME;
      |     ^~~~~~~
In file included from /usr/local/include/sylvan.h:45,
                 from vset_sylvan.c:13:
vset_sylvan.c:1259:16: error: ‘__lace_worker’ undeclared (first use in this function); did you mean ‘lace_workers’?
 1259 |     dst->bdd = CALL(go_sat, src->bdd, rels, rel_count, id);
      |                ^~~~
vset_sylvan.c:1259:16: error: ‘__lace_dq_head’ undeclared (first use in this function)
 1259 |     dst->bdd = CALL(go_sat, src->bdd, rels, rel_count, id);
      |                ^~~~
vset_sylvan.c: In function ‘set_least_fixpoint_par’:
vset_sylvan.c:1271:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1271 |     LACE_ME;
      |     ^~~~~~~
In file included from /usr/local/include/sylvan.h:45,
                 from vset_sylvan.c:13:
vset_sylvan.c:1272:16: error: ‘__lace_worker’ undeclared (first use in this function); did you mean ‘lace_workers’?
 1272 |     dst->bdd = CALL(go_sat_par, src->bdd, rels, rel_count, id);
      |                ^~~~
vset_sylvan.c:1272:16: error: ‘__lace_dq_head’ undeclared (first use in this function)
 1272 |     dst->bdd = CALL(go_sat_par, src->bdd, rels, rel_count, id);
      |                ^~~~
vset_sylvan.c: In function ‘set_save’:
vset_sylvan.c:1299:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1299 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘rel_save’:
vset_sylvan.c:1315:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1315 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘set_load’:
vset_sylvan.c:1336:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1336 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘rel_load’:
vset_sylvan.c:1357:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1357 |     LACE_ME;
      |     ^~~~~~~
vset_sylvan.c: In function ‘dom_create’:
vset_sylvan.c:1529:5: error: ‘LACE_ME’ undeclared (first use in this function)
 1529 |     LACE_ME;
      |     ^~~~~~~

CMakeLists gets version 1.4.1 while pkg-config asks for version >=1.4.2

Hi there,
GitHub pages have moved; the documentation is now at https://trolando.github.io/sylvan/. This documentation seems to be dated, by the way.
Cheers,
M.

Hi,

I am running Sylvan on machines with at least 32GB RAM. I set the memory cap in the function sylvan_set_limits to 28GB (table ratio 3 and init ratio 5). However, Sylvan exits with the "BDD Unique table full" error. I checked the max resident set size (as reported by time command) and it was always at most ~15GB . In other words, I suspect Sylvan is not using the full available RAM. Is there a workaround?

Thanks,
Aditya

The lines at

ISO C++17 does not allow ‘register’ storage class specifier

Sylvan does not yet support the new M1 chip.

I'm working on creating a repository that contains benchmarks implemented with different OBDD packages. Before I try to write my own code using Sylvan, I would like to be sure I can build and run the current N-Queens example.

Expected way to include Sylvan within CMake:

The project structure is as follows

|- CMakeLists.txt
|- external/
|  |- sylvan/
|- src/
|  |- CMakeLists.txt
|  |- sylvan_queens.cpp

Where based on my understanding of how to use CMake I would expect ./CMakeLists.txt should be as follows

add_subdirectory (external/sylvan sylvan)
add_subdirectory (src)

and ./src/CMakeLists.txt as follows

add_executable(sylvan_queens sylvan_queens.cpp)
target_link_libraries(sylvan_queens sylvan)

At this point I would expect to have linked everything to be able to build the Sylvan queens example as follows

mkdir -p build/ && cd build/
cmake ..
make sylvan_queens

Actual result:

With only the above, then during compilation, the linker is not capable of finding the Sylvan files as shown below

/obdd-benchmark/src/sylvan/queens.cpp:14:10: fatal error: sylvan.h: No such file or directory
 #include <sylvan.h>
          ^~~~~~~~~~

Instead one has to install Sylvan separately as described in the documentation, which at the time of writing this issue is as follows

mkdir external/sylvan/build && cd external/sylvan/build
cmake ..
sudo make
sudo make install

Final comments:

From experience with other libraries, such as TPIE it is possible to do merely as shown above. I suspect one would have to compare the following two files to find out how to do so

• TPIE: tpie/CMakeLists.txt

• Sylvan: src/CMakeLists.txt

I definitely notice, that the header files for Sylvan are not included as part of the add_library, but they are instead only placed in the installation directory. That seems to be in line with the observed behaviour.

This can prevent auto inference of operator== and operator!= in classes that have a Bdd field. Not entirely sure after some testing, but in any case, is there a reason why they aren't bool?

Due to the API redesign of Lace, it is no longer standard that the main() thread of a program is initialized as a Lace worker. However Sylvan assumes that makenode functions are called from Lace workers, because otherwise garbage collection is not properly synchronized. The reason makenode is itself not a Lace task is simply because of performance reasons.

Probably it's sufficient to add some check like are we in Lace? which is relatively easy to do, that is only active when DEBUG is enabled.

The Adiar BDD package will inherently always struggle to deal with small decision diagrams in comparison to the classical depth-first implementations. Hence, combining a depth-first implementation with Adiar would create something that is the best of both worlds.

How I imagine this could be achieved is as follows:

• If Sylvan runs out of memory: Run Adiar's algorithms on the BDDs from Sylvan (wrapping the node table into something that works with Adiar's algorithms)
• If the output from Adiar is very small: During the Reduction Phase, create the nodes in Sylvan's unique node table instead in one of Adiar's files.

For this to work, I'd need Sylvan to not exit the entire program, if it runs out of memory. Instead, it needs to fail gracefully and merely returns a null pointer. Would that be a lot of work?

Hi, I find this issue again...

When I monitored the "Bdd::ExistAbstract" Function, I found that, as the number of workers increases, so does the computational overhead of the "sylvan_exist(cube)" function, as well as sylvan_and_exist(sylvan_true, cube).

Logically, I think it should be that the more workers there are, the faster the function runs.

Shouldn‘t it be memory_order_acquire here:

I‘m not an expert about the C/C++ memory model, but as far as I understand it, the compiler or CPU is free to reorder the instructions roughly like this (i.e. move the load instructions of the bucket values before the load of the status):

    uint64_t bucket_a = bucket->a, bucket_b = bucket->b, bucket_c = bucket->c;
    const uint32_t s = atomic_load_explicit(s_bucket, memory_order_relaxed);
    // abort if locked or if part of a 2-part cache entry
    if (s & 0xc0000000) return 0;
    // abort if different hash
    if ((s ^ (hash>>32)) & 0x3fff0000) return 0;
    // abort if key different
    if (bucket_a != a || bucket_b != b || bucket_c != c) return 0;
    *res = bucket->res;
    // abort if status field changed after compiler_barrier()
    return atomic_load_explicit(s_bucket, memory_order_acquire) == s ? 1 : 0;

memory_order_acquire guarantees that “no reads or writes in the current thread can be reordered before this load,” which would fix the problem. In return one could probably change the memory_order_acquire of the second atomic load into memory_order_relaxed, at least I don’t see any need for memory_order_acquire here.

Also, atomic_compare_exchange_weak in the put functions could probably be replaced by atomic_compare_exchange_weak_explicit with memory_order_acq_rel for the success case and memory_order_relaxed for the fail case. This may have no effect on the generated assembly for strongly-ordered architectures such as x86-64 but may have a performance impact on others. Furthermore, it would be great if the compiler_barrier() macro and comments could be removed, they are somewhat confusing when reading the code for the first time.

Opening this issue for if anyone has some comment on this.

Currently Sylvan writes and reads BDDs in a somewhat awkward binary file format. While this is nice for parsing, it's unreadable and tricky to figure out what exactly is going on. Essentially, what Sylvan does is it simply collects all BDDs to write, then renumbers them to consecutive IDs.

Maybe we should just abandon binary formats? A BDD is not THAT complicated anyhow, typically we could just represent an internal node as <id> <variable> <then-id> <then-complemented> <else-id> <else-complemented> and a leaf as <id> <type> <value> where the predefined types are 0 (integer), 1 (double), 2 (fraction) or something along those lines.

How to get max var
thanks

I'm having trouble getting cmake to create the make file of Sylvan v1.8.1.
It giving me "Failed to get the hash for HEAD:". The error comes from CMakeLists.txt:19 (when fetching lace.). I've included a screenshot of the terminal:

Ekstra info: I have no trouble with v.1.8.0.

Seems like after the change that uses hwloc backend, sylvan no longer runs correctly.

Lace warning: hwloc_set_cpubind returned -1!
Lace warning: hwloc_set_cpubind returned -1!
Lace warning: hwloc_set_cpubind returned -1!
Lace warning: hwloc_set_cpubind returned -1!
Lace error: Unable to bind worker memory to node!
Lace warning: hwloc_set_cpubind returned -1!
Lace error: Unable to bind worker memory to node!
Lace warning: hwloc_set_cpubind returned -1!
Lace warning: hwloc_set_cpubind returned -1!
Lace error: Unable to bind worker memory to node!
Lace error: Unable to bind worker memory to node!
Lace warning: hwloc_get_area_membind_nodeset returned -1!
Lace error: Unable to bind worker memory to node!
Lace warning: hwloc_get_area_membind_nodeset returned -1!
Lace error: Unable to bind worker memory to node!
Lace error: Unable to bind worker memory to node!
Lace warning: hwloc_get_area_membind_nodeset returned -1!
Lace warning: hwloc_get_area_membind_nodeset returned -1!
Lace warning: Lace worker memory not bound with BIND policy!
Lace warning: hwloc_get_area_membind_nodeset returned -1!
Lace warning: Lace worker memory not bound with BIND policy!
Lace warning: hwloc_get_area_membind_nodeset returned -1!
Lace warning: hwloc_get_area_membind_nodeset returned -1!
Lace warning: Lace worker memory not bound with BIND policy!
Lace warning: Lace worker memory not bound with BIND policy!
Lace warning: Lace worker memory not bound with BIND policy!
Lace warning: Lace worker memory not bound with BIND policy!
Lace warning: Lace worker memory not bound with BIND policy!

I am assuming that my hwloc is not setup correctly, but not sure where to look. Any pointers would be appreciated! I am on an macOS 10.12.4, 2.5 GHz Intel Core i7

hwloc was installed from here: https://www.open-mpi.org/software/hwloc/v1.11/

Hello,

I was getting the following error

Lace fatal error: Task stack overflow! Aborting.

My code is recursive and the recursion is fairly deep for these cases. As per the documentation recommendation, I tried again after ulimit -s unlimited first, but the error still pops up. I checked the max resident memory size (as reported by the time command) and it is fairly low.

I am not sure how to fix this. Any pointers are appreciated!

Thanks,
Aditya

Hi, I implement a simple boolean formula: f= x_0 \and x_1, and want to print the final BDD with sylvan_print(bdd1). The printed info is: 2,[(1,1,0,0,1),(2,0,0,3,0),]

I am confused about the result printed. what does "s->assigned" (1&2 in (1,...)& (2,...)) mean here? and Why there is "3" in the printed info (2,0,0,3,0)? Does this 3 mean x_1?

Also, when I tried f=x_10 and x_11 and x_12, the printed info is:

what do 4 & 6 mean here? I know that they present the high_edge nodes, but why is 4 (6)?

I am trying to install Sylvan in a non-standard location.

I change CMAKE_INSTALL_PREFIX=/home/user using ccmake
However, the change is not reflected in the dependency lace.
So make install still tries to install liblace.a in /usr/local (but I don't have the rights).

Current workaround: manually change _deps/lace-build/cmake_install.cmake,
adding set(CMAKE_INSTALL_PREFIX "/home/user")