Controller checker: checker is not very performant (mostly the confluence check)
The performance problem
This issue is about the performance of the checker in general. (It was created when we only had confluence and finite response checks. Both are/were MDD-based. We since have bounded response, a BDD-based check, per #621.)
From #686 (closed):
[...] if one runs the confluence check on the bridge model in the CIF examples, it still takes a lot of computation time to perform the confluence check (so much time that I didn't had the patience to wait to let it finish; @koenveldik reported to me in private communication that he is waiting over 2 days for the confluence check to finish on a bridge model (not the CIF example)).
Related issues
- Issue #686 (closed) is about adding more debug output to show progress (what is it doing) and more termination checks (allowing to actually terminate it).
- Issue #693 (closed) is about improving the performance of the update conversion (potentially reversing it for instance).
- Issue #410 discusses the (future) implementation of the non-blocking under control check, and the performance aspects of it, which relates very closely to the discussion in this issue.
- Issue #844 proposes a completely different algorithm for checking confluence. If we go for that, we'd have to see what the performance is.
Addresses #892
This issue
Issue #693 (closed) it also lists some general ideas to improve performance, more or less related to BDDs vs MDDs and their implementations. This issue is split off from #693 (closed) to discuss such more general performance issues for the controller checker. The relevant parts from #693 (closed) are:
[...]
- Switch the whole tool to BDDs rather than MDDs. The JavaBDD implementation of BDDs is much more efficient than MDDs.
MDD works nicer in our multi-value domain, and it avoids to think in terms of bits so it's easier to understand for people without CS education.
That is however just one part of why it exists. The other at least as big part is that the BDD packages are all very much minimalistic. Their authors never considered much how to use it in practice in everyday programming at a large scale.
- Everything is a number. You as programmer has to make sure you keep node numbers and variable numbers separately. Nothing in the package prevents or warns you about mistakes. If you do make a mistake, likely it just crashes. MDD has different classes for nodes and variables. It's not even possible to make a mess here unless you explicitly construct invalid instances.
- You as programmer are responsible for assigning numbers to variables (which is fair). You however also have to write code that produces those numbers again when manipulating the tree since the BDD package has no support for storing such data. So if you wrote some non-trivial code, knowledge of variable numbers spreads itself into all corners of the software. If you ever want to change variable numbers, that in itself becomes already a non-trivial problem. So MDD has a variable storage class instead (forgot its name) where you can just configure the variables. The class handles the number details, and it will give me the right variable numbers again when you ask for "variables of level X". Change the configuration, and the code simply gives you the new numbers.
- You as programmer are responsible for dropping nodes that you don't need any more. There is no indication whatsoever if you make an error there. Instead it likely crashes or keep parts of trees that shouldn't even be kept. So MDD uses the garbage collection mechanism to handle that, so you can't even make a mistake.
While writing MDD code, I did find that adding nodes in the right order is difficult to get right each time. I also found doing it wrong can make a huge difference. I fixed it somewhat by smarter updates in a single node. That does help significantly, but not across different MDD nodes of course.
To handle the order of adding properly I think the computer should handle that problem rather than the programmer. The idea that I have there is that you normally build a new chain of nodes on top of some existing sub-tree. Each new node has a different variable and for each value of the variable it either branches away from the existing sub-tree (eg it decides "yes" or "no" or defers to a different tree for the final decision), or it daisy-chains to the next variable that should be added on top of the sub-tree. This daisy-chaining is where things may go wrong with respect to the order of adding nodes.
To solve this, if we could specify the new nodes all separately, with the daisy-chain values something special so it can be recognized as a "gap that should be changed", you could give all the new nodes to a function that then figures out the order to add the new nodes and replaces the special values to proper child nodes. I believe that would solve much of the "order of adding" problem.
Note that in essence there is nothing in this support code that only works for MDD. As such, all of it could be done for BDD as well.
I do see some benefits indeed with the MDD approach, although I wonder if we could not make a wrapper around JavaBDD that solves most of the same issues. My problem with the MDD stuff is that it is something custom that we made. It has nowhere near the performance of JavaBDD (yet?). This issue is about the performance of the confluence check, which is a big problem in real-world application (see description of #686 (closed)). I see only two real solutions, besides small changes that won't help enough:
- Improve the performance of MDD, to get it to the level of JavaBDD performance.
- Reimplement the controller checker using BDDs, or at least the confluence check.
I've been asked by RWS to give an estimate on how much time it would take to address this, but I think it depends a lot on the direction we go with this. I think we should agree on that first.
I wonder if we will ever get MDD up to the level of BDD, but I also see that reimplementing the confluence check in BDDs will be some work, as it would require splitting the data-based synthesis tool into a synthesis part and a CIF to BDD conversion part, to allow reusing the latter. Although, the splitting may be required anyway, for #410 ('non-blocking under control' check).
I'd love to year how you all think about this.
I've also started the discussion on #410, and I think they are related discussions.