Replace dependency on domain_shims with lightweight DLS shim for single-threaded OCaml

[michael-schwarz]

Instead of using the domain_shims library to simulate all aspects of domains, this provides just a shim for DLS as we don't use multiple domains for OCaml 4 anyway.

This fixes goblint/analyzer#1781 without any principled rework.

[sim642]

Besides the clear race condition, I think doing it like this in CIL won't really fix the problem. For the same reason like our Zarith patch: it needs to be fork and pin of the original package, not in a new package, because other things we depend on would probably still use the original domain_shims.

I think we should just remove the global state from Pretty and be done with it. There's no reason it shouldn't be possible and there's every reason to have less global state anyway.

[sim642]

I'm not sure this really works. There's a race condition here (yes, on OCaml 4 without threads!):
If the signal handler fires between these two lines to set something, then this get (!) will overwrite the "new" value with the initial one.

There's a good reason why domain_shims uses atomicity (although via a Dirk-style mutex). I think atomicity is inevitable in a correct solution: it's just that the atomicity probably should be proper, not using a mutex, possibly with a lock-free data structure.

[michael-schwarz]

For the same reason like our Zarith patch: it needs to be fork and pin of the original package, not in a new package, because other things we depend on would probably still use the original domain_shims.

It is not a general fix of the problem in Domain_shims (it doesn't work for multiple domains simulated via threads).

This is a fix to get back pre-DLS behavior from OCaml 4. Yes, the usage in Goblint is problematic, but it has been problematic all along, and this solution is no less problematic then the old solution using ref.
Having random fluctuations with results all the time in our nightly jobs is bad, as people will not notice when actual changes happen.

I think we should just remove the global state from Pretty and be done with it.

If you want to commit resources to this within the next few days, sure. Otherwise, I think this is a good stop-gap until someone invests the time in such a re-write of Pretty (it has more state than just these few things btw).

[sim642]

If you want to commit resources to this within the next few days, sure.

It was 30 min of straightforward work: PR #187.

[michael-schwarz]

Closing in favor of #187. It is the more principled approach.