Non-blind debugging of reference count problems.

[Alberth289346]

I am extending data-based synthesis in the ESCET project.
The application gives a "User called break" exception.

The message is completely meaningless to me, but the code suggests it has to do with lack of a reference. That somewhat makes sense because the problem happens while releasing references.

I can see two likely causes currently:

1. Due to lack of documentation, I have guessed the reference count semantics. Maybe I guessed wrong.
2. I made a reference counting error somewhere.

The question is, how do I debug this? Clearly my counting abilities are not sufficient. I looked for a way to get the actual reference count, and failed to find that.

Other ways that are helpful are welcome too.

---

I can likely add a way to get the reference count if the project allows that. That would at least make it possible to write checking code that counts behave as they should across a piece of code.

Somewhat more expensive but much more solid is the option to eliminate the problem entirely by leveraging Java semantics to handle this automagically with a derived WeakReferenceQueue class.

[dhendriks]

I looked for a way to get the actual reference count, and failed to find that.

I think that is an internal implementation detail that is not exposed to the user. The information is not trivial to get. As far as I remember, BDDs given to the user get a reference count increase. Then there is the reference stack of in-progress things of the current operation. Together they determine which BDDs are reachable and their counts. Note that only the root of a BDD given to the user gets a reference count increase, not all its descendants. Hence, during garbage collection, JavaBDD does a mark and sweep to determine which nodes are still referenceable.

Other ways that are helpful are welcome too.

See https://gitlab.eclipse.org/eclipse/escet/escet/-/work_items/267.

@wytseoortwijn Do you have any other ideas?

Somewhat more expensive but much more solid is the option to eliminate the problem entirely by leveraging Java semantics to handle this automagically with a derived WeakReferenceQueue class.

This has serious downsides. If GC doesn't trigger, things don't get removed. Mixing managed an unmanaged memory arbitrarily is typically not a good idea, I think. It is not as easy as at it would seem.

---

Note that JavaBDD is difficult to change. Hence (and for other reasons) we're working on JavaDD to replace JavaBDD, see https://gitlab.eclipse.org/eclipse/escet/escet/-/work_items/1000. I think we're quite close to starting contributing that to ESCET, step by step. Progress has been slower than we had hoped. Currently, we're not putting much effort into JavaBDD anymore.

[wytseoortwijn]

@wytseoortwijn Do you have any other ideas?

The problem seems that a BDD has been used after it has been freed. (When freeing a BDD, its internal reference will be set to INVALID_BDD. And when using a BDD with such a reference, a bdd_error(BDD_BREAK) will be given.)

Getting the actual reference count of a BDD is difficult, since (1) reference counting is an internal mechanism that's not exposed to users, and (2) indeed only user-specified 'root nodes' have their reference count increased.

One possibility is to expose more of reference counting to the users of JavaBDD. For example, in principle it's possible to implement a new method that only performs the 'mark' phase of mark-and-sweep garbage collection, to mark all nodes that are directly or indirectly referenced. From that, you might get information on what nodes still have a positive refcount. (In case you just want to know how many nodes still have a positive refcount, there's already the internal JFactory#bdd_used_nodes_count method. But I don't think it's exposed to users.) Getting the exact current reference count of all nodes in the node table would require some more effort.

[Alberth289346]

Some time after writing this, I realized that counts at the start and the end are not sufficient either, even if you have them. As a side-effect of doing the computations, another node may become the same value, and thus the reference count is different from expected.
It would still be findable though, by checking the count after each bdd operation. Somewhere the count must jump in an unexpected way in such a case.

I fought the problem for 3 days, until I suspected that a.fooWith(b) may not be doing what I believed it was doing (besides destroying b, I got that message). I rewrote the fooWith operations to plain foo operations, and then it all magically worked. Checking the source code then revealed an assignment to a which confirmed I found the culprit.

Nnonetheless, in its current form, writing *DD manipulation code is heroic work. It's complicated already to ensure you got all the bits correctly computed, and then the setup makes it even more complicated by not allowing any form of checking correctness beyond your own ideas.
If you decrease too many you at least get an error (even though clarity could be much better). If you forget to decrease, it's near impossible to ever find that.

[dhendriks]

until I suspected that a.fooWith(b) may not be doing what I believed it was doing (besides destroying b, I got that message).

It eats up both a and b.

Nnonetheless, in its current form, writing *DD manipulation code is heroic work.

I disagree. If you know how it works, it is quite doable after a little bit of practice. Sure, you have to track what you're still 'owning' and make sure you free it.

But, essentially every operation that returns a BDD gives you one that you then own. This applies to ithVar, and, relnext, saturation, all of them. None of these operations free their arguments. You have to free them yourself. Alternatively, you can use *With operations that are the same as the non-With variants, but also automatically free their inputs.

That is all there is too it. Sure, I also make some mistakes sometimes. But then I just look at the code, track what I still own, and fix it. It really isn't rocket science, to be honest. Would I like to not have to take care of all this, sure. But that is not so easy to achieve.

[Alberth289346]

This has serious downsides. If GC doesn't trigger, things don't get removed. Mixing managed an unmanaged memory arbitrarily is typically not a good idea, I think. It is not as easy as at it would seem.

In my view, it's crucial that you don't leak references or use non-valid references. GC is one way out, by automating the problem away from the programmer. I agree that in production use, you definitely want a mode that does not rely on GC.
However, I don't see why it's impossible to configure behavior of the BDD package in that respect.

Pondering about it, I had the following idea, first under the assumption of one global scope: Make the the BDD variables used in the code managed by a hypothetical BDD package p. That is:

1. The user must initialize their BDD variables explicitly BDD x = p.initVar();
2. Perform logic operations much like before, except you must specify a destination, eg p.apply(x.and(x, y), z);. (In C++, you could use the assignment/move operation here.)
3. De-initialize the BDD variables explicitly p.destroy(x).
4. Verify with p that there are no usable variables anymore p.checkNoVars();

This looks airtight at first sight.

For nested scopes, the idea stays the same, except you do the above in every scope. Likely it needs a scope concept inside p or attached to p (that is, make a BddScope s = p.makeScope() and perform the above things with s instead of p).

A new thing with nested scopes is that references may 'leak' into a parent scope, or get 'stolen' from a parent scope. Eg a method computes some value that is about to be used by other methods, or the global value gets used in sub-scope. It's detectable if p maintains a tree of scopes. Then it needs some kind of policy how to decide what is allowed. I am not sure what kind of policies are useful there, but one option is to explicitly state what to do, eg p.apply(p. or(glob.copy(), x), y); or p.apply(p. or(glob.steal(), x), y); (Although arguably, just using glob and then destroying glob is perhaps a better solution here.)

For production use, you may want to disable all checking by toggling a boolean flag when creating p. Besides a little startup overhead, the JIT will soon eliminate the checking code. (At first sight, I am not sure disabling will make a huge difference though; the administrative operations look quite cheap.)
Note that the used policy needs to support disabling however. For example, automatically dropping a previous reference, eg with v in p.apply(p.not(v), v); must be written as a stricter policy p.apply(p.not(v.steal()), v); if the policy may get disabled completely.

[dhendriks]

Pondering about it, I had the following idea, [...]

If we would do this in a serious application of BDDs, I feat the code will become littered will all these extra calls adding complexity to the code.

As an alternative, isn't the following sufficient? If you have a method where you do some BDD calculations, then typically you have some inputs and you produce some outputs. From that, it should be easy to see how many more/less BDDs you should have after the operation. Say, you have 3 inputs and 1 output. Say 2 of the inputs must be 'eaten' according to the method JavaDoc, and one must not. Then you get -2 + 1 is 1 less BDD in use after the method. We could maybe add a method getBddRefCount or so. You could invoke that at the start of the method and save the result. At the end of the method, you could invoke it again, and see if the diff is what you expect. This way, you can check method contracts. You can also do it for smaller parts of a method, obviously. Or over whole heaps of code. It would need to be disabled in production, as the getBddRefCount would do a full marking, so it is not that cheap. A slightly nicer API could maybe be devised around this.

I think that if this is added in an application in strategic places, then it doesn't need to be in all detailed code. If it is around a larger computation, we can see that it didn't break anything (too many freeing will crash, too little freeing and the count will be off). If it does, one can debug by drilling down. But then that doesn't need to be permanently in the code. Often, for such larger computations, I think the count will be the same before and after the larger computation. For instance, for supervisory controller synthesis in ESCET, you could put it around a single fixed-point computation, and the entire fixed-point computations outer loop, as well as maybe around the whole synthesis application from start to end.

What do you think?

[Alberth289346]

I think I wrote kind-of the same idea in the first text block of #90 (comment)

I think it makes sense, but not sure. That got however thrown out before getting off the ground. Possibly for good reasons like bdd caches and distributed computing, but I don't know.

Note that the 'vars managed by the BDD packages' description in #90 (comment) is optimized for explaining the idea rather than for usage at large scale. It does address the need for internal ref-count information though, which seemed non-feasible.

The proposed form is not the only form that can exist. Since the BDD variables are essentially managed by the BDD package, you don't quite need to have your own variables at all. It just needs some form of labels such that the BDD package knows what you want to compute, eg "q = a & (b | C)" would work as computation except you need to have a more clear specification of the variables. This could be done as a kind-of meta-model for describing BDD computations.

[dhendriks]

I think I wrote kind-of the same idea in the first text block of #90 (comment)

I think I understood what you were indicating earlier as 'how often is a BDD node used in the whole BDD forest'. That is complex and requires a full marking to find out, but can be computed.

If you just want to know how many root references (BDD objects) are still outstanding that the user hasn't freed yet, you can just do a linear sweep over the node table and sum the reference counts of the nodes in the node/unique table. Whenever a new BDD object is created, the reference count for its corresponding root node is incremented by one. If free is called by the user, it is decremented by one. The *With variants do the decrementing similarly internally. (JavaBDD there reuses for binary operations the first argument to a *With operation, so it only frees the 'other' BDD and kind of 'overwrites' the first BDD. I find that a bit hacky, but that's mostly an implementation detail.)

That got however thrown out before getting off the ground. BDD caches etc don't play into this. [...] internal ref-count information though, which seemed non-feasible.

We're discussing, so thoughts can change. When you're not doing any computation, so your in the user's code (and since JavaBDD is single-threaded), then the stacks are not relevant. Only the reference counts of the nodes. So, an operation to sum the reference counts is not difficult to make. BDD caches etc are also not relevant. I don't see why it would be infeasible.

Since the BDD variables are essentially managed by the BDD package, you don't quite need to have your own variables at all.

JavaBDD knows how many variables there are, but it doesn't know what they represent. If in your domain you have multi-valued variables, you need to map them to binary variables yourself and indicate the number of them to JavaBDD. You can use BDD domains for that, which JavaBDD will then manage. Note that in JavaDD we did away with all this. A BDD factory doesn't know how many variables there are, and it doesn't do domains either. The user of JavaDD will have to manage that. In CIF/BDD, we already have our own administration, so that is not a problem there.

I'm not sure I get your whole last paragraph about the variables and metamodels. Is this the idea you had before, from https://gitlab.eclipse.org/eclipse/escet/escet/-/work_items/1274? To specify the operations you want to perform and have the library perform that, with the that it then somehow figures out what to free along the way, and at least for intermediate operations you won't get leaks?

[Alberth289346]

I'm not sure I get your whole last paragraph about the variables and metamodels.

Not quite. The problem is to find a convenient way to define the variables and the computations. One path is express that in a meta-model, that you can interpret or generated code for. Probably a bit too heavy for the purpose though.

[dhendriks]

The problem is to find a convenient way to define the variables and the computations.

Isn't that a different problem than the debugging problem that is the scope of this issue?

[Alberth289346]

Depends on how you look at it, I think.

The standard programming language isn't much equipped to monitor or manage ref-counting in a useful way for the programmer. An alternative is to build some kind of framework on top of that to solve that in a more generic way. A simple approach is what I sketched above. The ultimate is probably to generate code from the meta-model, and then you can have anything.

Didn't Java provide code customization/generation features with the @ annotation? That could be a perhaps cheaper path.

[dhendriks]

Didn't Java provide code customization/generation features with the @ annotation? That could be a perhaps cheaper path.

Yes, Java supports annotations and annotation processors. Could perhaps inject some reference checking code or analyze the source code to find leaks.