"Tackling Concurrency Bugs with TLA+" by Hillel Wayne
"Tackling Concurrency Bugs with TLA+" by Hillel Wayne on HackerTube: recommended by 3 Hacker News commenters across 3 separate months, 2018–2025.
Hillel Wayne's Strange Loop talk introducing TLA+ as a specification language for finding concurrency bugs in designs. It covers stalling, race conditions and dropped messages, with PlusCal examples.
What HN commenters said
5 Hacker News comments link this video. Each one links back to its thread.
cess11May 2025Recommends
The literature on distributed systems is huge. It depends a lot on your use case what you ought to do. If you're lucky you can avoid shared state, as in no race conditions in either end of your executions. ▶ this video is fairly concise and gives some recommendations for literature and techniques, obviously making an effort in promoting PlusCal/TLA+ along the way but showcases how even apparently simple algorithms can be problematic as well as how deep analysis has to go to get you a guarantee that the execution will be bug free.
in “The first year of free-threaded Python” · View on HN
bandwitchJul 2018Recommends
I feel TLA+ would be too much to ask in a system interview which is what this site is about. In case anybody is interested, there is a nice talk by Hillel Wayne on youtube ( ▶ this video ) that provides a high-level overview on what TLA+ is about.
in “Learn how to design large-scale systems” · View on HN
ajmurmannMar 2018Recommends
Hillel gave a pretty interesting talk on TLA+ at last year's StrangeLoop: ▶ this video If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk. Edit: I think he also brought home made granola or something. So attending his talks in person has benefits.
in “Modeling Redux with TLA+” · View on HN
strangecastsApr 2019Cites it
PlusCal uses labels (e.g. "Give:") to designate atomic actions - when you translate it, each labelled section is turned into an atomic action [1]. You can start off with a very simple spec with totally atomic transactions, and gradually make it more granular by introducing more labels, as shown in Wayne's Strange Loop presentation [2] [1] [link] [2] ▶ this video (15:55)
in “Learn TLA+ (2018)” · View on HN
hwayneMar 2018Cites it
I've used it for caching, batch processing, and concurrent web apps, and it's been a huge help. I've gone into how I used it in a couple of places: - "Tackling Concurrency Bugs with TLA+" ( ▶ this video ) - "Formal Methods in Practice" ( [link] ) I love helping people with this stuff, so ping me if you have any questions!
in “Ask HN: Anyone ever use TLA+ on a Webapp” · View on HN