"Tackling Concurrency Bugs with TLA+" by Hillel Wayne
Strange Loop Conference3 HN recommenders · recommended in 3 months, 2018–2025
talk · intro · evergreen · 2018–2025 on HN
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.
Recommended as a concise, high-level intro to what TLA+ is and when it helps.
Up next
10 mo on HNBrian Beckman: Don't fear the Monad
jasonofthel33t
9 HN recommender · 2012–2024
9 mo on HN28c3: The Science of Insecurity
28c3
9 HN recommender · 2012–2024
8 mo on HN"Propositions as Types" by Philip Wadler
Strange Loop Conference
9 HN recommender · 2015–2026
7 mo on HNMath's Fundamental Flaw
Veritasium
7 HN recommender · 2021–2024
7 mo on HNThe Banach–Tarski Paradox
Vsauce
6 HN recommender · 2015–2024
7 mo on HNThe Future of Mathematics?
Microsoft Research
9 HN recommender · 2019–2025
5 mo on HNLeslie Lamport: Thinking Above the Code
Microsoft Research
5 HN recommender · 2015–2026
5 mo on HNHow To Count Past Infinity
Vsauce
6 HN recommender · 2016–2022
4 mo on HN"Finding bugs without running or even looking at code" by Jay Parlar
Strange Loop Conference
4 HN recommender · 2019–2023
4 mo on HNEdwin Brady - Idris 2 - Type-driven Development of Idris
Curry On!
4 HN recommender · 2019–2023
4 mo on HNInfinity is bigger than you think - Numberphile
Numberphile
3 HN recommender · 2014–2022
4 mo on HN2017 ACM PPoPP Keynote: It's Time for a New Old Language
Guy Steele
3 HN recommender · 2018–2023
5 comments from Hacker News
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.
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.
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.
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)
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!