New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

[Investigation] TLA+ model for restorer #149

Open
wants to merge 1 commit into
base: master
from

Conversation

Projects
None yet
2 participants
@talex5
Copy link
Contributor

talex5 commented Mar 11, 2018

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...)

TLA+ model for restorer
Investigation of how the planned Lwt changes will affect existing code,
by making a model of one function.

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.
@aantron

This comment has been minimized.

Copy link

aantron commented Mar 11, 2018

@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.

@aantron aantron referenced this pull request Mar 11, 2018

Open

preparing for lwt 4.0.0 #889

@talex5

This comment has been minimized.

Copy link
Contributor

talex5 commented Mar 12, 2018

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.

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment