[Investigation] TLA+ model for restorer

[talex5]

Investigation of how the planned Lwt changes may affect existing code, by making a model of one function and using TLA+ to discover what implicit assumptions it makes about the behaviour of Lwt (for which, until recently at least, the source code was the only real documentation).

I have added some comments to the function where I think there may be problems. See the new spec/Restorer.tla file for more details.

Conclusion: the new semantics would break one or maybe two implicit assumptions in this function and would result in a race condition, allowing user code to receive an object with a ref-count of zero.

There are likely similar assumptions throughout the code - this is just looking at one minor function.

Note: this is my first attempt at using TLA+, and may be wrong and/or stupid.

/cc @yomimono (who mentioned examples of this in mirage/mirage#889) and @aantron.

(It's also possible that this still works under the new semantics, which aren't entirely clear to me. A TLA model of the old and new behaviours of Lwt would be welcome...)

[aantron]

@talex5, @yomimono, I haven't yet looked at this closely, but I want to say that we will probably delay and/or abandon applying the new semantics in 4.0.0, due in considerable part to your feedback. Thinking about this, with other issues in mind as well, it seems that breaking a large amount of code (or rather, making maintainers doubt its reliability) is not worth the minor semantic improvement, especially since the semantics bug is often meaningless in practice. We may have an opportunity to get the semantics right later in a new Lwt front API, anyway.

I was planning on announcing that in the discuss topic tomorrow.

On the other hand, if you think you might have a good way of adapting a large codebase safely to the new semantics, please let me know. However, looking at the diff in this PR, it seems a large amount of work went into this function, and it looks like too much to me.

Another thing we might try is adding some kind of order-randomization mode for testing, so that projects can gradually discover unwarranted assumptions in their code. Maybe after long-term use of this mode, the average project would become more relatively agnostic to implementation details of Lwt.

[talex5]

That's good to hear! Note that the spec is a bit longer than really necessary. From line 270 onwards it is all proofs, but using only the model checker to test it would have been reasonable - I just wanted to learn how to write proofs. But even so, it would be too much work to test the rest of the code like this.