Re:Applying TLA+ in cloud systems [video]
by Jtsummers on Tuesday December 15, 2020 @10:58AM
(#25431410)
I've used it for small-scale concurrent systems and it's been useful. I've never used it for large distributed systems as I don't build or work on those.
Most of the time I choose built-ins that largely handle the normal concurrency problems (once you have a concurrent queue, if you never share data otherwise, a lot of problems are just gone). But in embedded systems that's not always an option (either you have to build it yourself or the structure of the hardware doesn't really lend itself to it). Sharing data across co-processors can lead to subtle and hard to detect issues. Reasoning about how they communicate via TLA+ (and other systems) can help make these issues tractable and repairable (or prevent them if applied in advance).
And learning to reason using TLA+ doesn't necessarily mean having to use the full toolkit and run models. Just describing the system at this higher level can make issues in the design apparent (this has been my experience, at least).
Most of the time I choose built-ins that largely handle the normal concurrency problems (once you have a concurrent queue, if you never share data otherwise, a lot of problems are just gone). But in embedded systems that's not always an option (either you have to build it yourself or the structure of the hardware doesn't really lend itself to it). Sharing data across co-processors can lead to subtle and hard to detect issues. Reasoning about how they communicate via TLA+ (and other systems) can help make these issues tractable and repairable (or prevent them if applied in advance).
And learning to reason using TLA+ doesn't necessarily mean having to use the full toolkit and run models. Just describing the system at this higher level can make issues in the design apparent (this has been my experience, at least).