Great talk! Didn't know TLA. Looks like such a useful tool in so many cases. I do feel like it'd be easy to make a wrong model, though. For example, if you're doing concurrency in python you may be confused as to when the interpreter can switch between threads (because it's not that simple), so if you're trying to model things like lock-free shared write access to mutable objects in python, it might be really hard to model correctly (may need to have each bytecode op as a separate state for proper modelling). Even if you get a working model, sometimes the hard part is knowing whether your code actually follows your mental model. Still really useful to be able to check that your mental model is correct in the first place.
An in-depth TLA+ walkthrough tutorial of the producer/consumer example - including safety proofs, refinement, trace validation, ... - can be found at github.com/lemmy/BlockingQueue/
Great talk! Didn't know TLA.
Looks like such a useful tool in so many cases.
I do feel like it'd be easy to make a wrong model, though. For example, if you're doing concurrency in python you may be confused as to when the interpreter can switch between threads (because it's not that simple), so if you're trying to model things like lock-free shared write access to mutable objects in python, it might be really hard to model correctly (may need to have each bytecode op as a separate state for proper modelling).
Even if you get a working model, sometimes the hard part is knowing whether your code actually follows your mental model.
Still really useful to be able to check that your mental model is correct in the first place.
An in-depth TLA+ walkthrough tutorial of the producer/consumer example - including safety proofs, refinement, trace validation, ... - can be found at github.com/lemmy/BlockingQueue/
Excellent explanation!
TLA's syntax is weirdly intuitive. The symbols are very abstract but I remember their meaning from the very first explanation.