search

SSoelvsten / bdd-benchmark

Benchmarking Suite for BDD packages
MIT License
11 stars 2 forks source link

Sylvan : Crash in Lib-BDD reconstruction #138

Open SSoelvsten opened 1 month ago

SSoelvsten commented 1 month ago

Sylvan seems to crash due to a LACE Stack overflow during the reconstruction of the input for the RelProd benchmark. This would presumably also happen in the Apply benchmark.

jacopol commented 1 month ago

Could increase the stacksize through ulimit -s <size> (in KiB?)

SSoelvsten commented 1 month ago

The only operation that is used during reconstruction of the input (serialized BDDs) is the ITE . Simultaneously, the BDD is built bottom-up, meaning the ITE should take O(1) . Hence, the issue is something much more subtle and weird.

SSoelvsten commented 3 weeks ago

The issue lies in the fact, that Sylvan's garbage collection has the following undocumented assumption:

The number of BDD roots (i.e. references from the user's program) is smaller than the size of the Lace queue.

Hence, Sylvan breaks when the vector<sylvan:Bdd> out in common/libbdd_parser.h::reconstruct<Adapter>(...), which contains all BDD nodes for reconstruction, is larger than the Lace stack.

SSoelvsten commented 3 weeks ago

Merging that PR does not fully resolve the issue - just push the boundary of what Sylvan can deserialize. Closing this was not the intention.