24K views · Oct 2, 2017 · 30:06 · 3 HN recommenders · 5 mentions · discussed 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.
Why Hacker News points people here: Recommended as a concise, high-level intro to what TLA+ is and when it helps.
“If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk.”HN comment, 2018
“If you are new to TLA+ and just want to get the basic idea and use cases, I recommend the talk.”
Basic idea and use cases of TLA+
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.
“there is a nice talk by Hillel Wayne on youtube”
High-level overview of what TLA+ is
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.
“is fairly concise and gives some recommendations for literature and techniques”
Concise talk showing how subtle simple concurrent algorithms can be
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've used it for caching, batch processing, and concurrent web apps, and it's been a huge help.”
Author's own talk on using TLA+ for concurrency bugs
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!
“as shown in Wayne's Strange Loop presentation”
Shows refining a PlusCal spec by adding labels
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)
