3 ms·

Does anyone have personal/anecdotal experience with TLA+ being used in a professional setting? I'm interested in hearing stories/use-cases of practical applicat

by keyanp 7y ago

Does anyone have personal/anecdotal experience with TLA+ being used in a professional setting? I'm interested in hearing stories/use-cases of practical application. I've always been intrigued by formal methods but when I try to think of an application of TLA+ my problems are either too trivial to need formal analysis or too complicated for formal analysis to appear feasible.

senthil_rajasek 7y ago
Check the video I posted in the comments. Leslie Lamport goes into how Amazon Cloud services team uses TLA+.
Twirrim 7y ago
Yes indeed. Seen it in use in AWS across a number of critical components. The team I was on in AWS used it for the implementation of a particular component that needed to operate at large scale and had absolutely zero tolerance of failure. Two engineers learned TLA+, started writing up the logic and discovered various ways in which the logic would work on small scale but wouldn't scale up to parallel operation across multiple servers. It's fair to say TLA+ saved our bacon there before we'd written a single line of service code. In the end we actually got the component out to production faster than predicted. The TLA+ code gave solid shape for the actual production code, and we were quickly able to prove that the code was valid and that things were working correctly. In my current role in Oracle Cloud Infrastructure, there is actually a small dedicated team of engineers that help services use TLA+ for components, headed by Chris Newcombe, one of the authors of the TLA+ whitepaper that came out of Amazon (https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....) My current team has just started exploring it for use for a component that similarly has little tolerance for error. It's not in the same territory of "if it fails it's catastrophic", thankfully, but if it fails it's a major inconvenience for customers.
ausimian 7y ago
I used it for the first time in firmware design at MSFT a few years ago, and I've used it since in the areas of protocol design. I don't use it frequently but it's a tool I'm glad I took the time to learn, and have to hand when I need it. My experience is that, using TLA+, or other tools like it, encourages you to think precisely about the problem and at the same time exclude unnecessary details. That alone I find useful in terms of the insights it gives e.g. surfacing interesting invariants, or alternatively, invalidating them. In any case, you use the model-checker (TLC) to test these assumptions quite easily, and then bring these invariants into your code, either in the form of assertions, contracts or perhaps in property-based testing. In any case, I would say the process of writing such a specification yields benefits. Perhaps this can best be summed up by something I think Leslie Lamport once said: "If you're not writing when you're thinking, you only think you're thinking." I should add that despite claims about TLA+ being particularly well-suited to concurrency problems, my implementation targets have never been 'concurrent' in the 'multi-threaded' sense. Rather, they have been single-threaded event-driven state machines, and I personally find that it excels in this space. However, as you will find, in TLA+, concurrency is just a matter of abstraction... I have found that, because TLA+ doesn't 'generate code', many colleagues struggle to see the tangible benefit. I personally think that there is a gap between the whiteboard and the editor which tools like TLA+ fill very nicely. It's not a panacea or a magic bullet, and like any tool you must still exercise judgement about when to use it, and how to use it effectively, which includes understanding the limitations of the tooling (TLC cannot check arbitrary specifications). But if I find myself faced with a potentially tricky algorithm, or indeed want to understand an existing algorithm, I reach for TLA+.
hedora 7y ago
I highly recommend learning TLA+ before writing any papers with math involving set logic (foreach, exists, etc), if only to teach you standard mathematical syntax for those things (like “{ s \in S : \A t \in s : func(t) }“, which is valid TLA, and will also emit a human readable formula if pasted into Latex). This would have saved me tons of work in hindsight.
mcpherrinm 7y ago
One of my coworkers used TLA+ to prove a change to a service my teams runs was correct. The service was essentially a key/value store. If one region didn't know about a key, it would recursively ask the other regions in parallel for the data. Eventually we needed to add support for deleting data. We deleted data that hadn't been read in a few months. We used TLA+ to prove our region-sync code and deletion code interacted properly along with regular get/put operations.
geoka9 7y ago
This conference paper has an anecdote: https://www.researchgate.net/publication/220757452_Specifying_and_verifying_systems_with_TLA https://www.researchgate.net/publication/220757452_Specifyin...
qcoh 7y ago
There's a paper describing the use for railway applications [0]. A few years back I had an interesting discussion with one of its authors and was shown the real model and code. Interestingly, they generated C from the TLA+ spec and this code generator was "unproven". However, the software itself had high coverage requirements and needed to be tested extensively (100% code/branch/MCD coverage, I don't quite remember). One of the points he made was that the upfront cost pays for itself by avoiding bugs that are hard to debug. [0]: https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1lpx9C/view https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...
superice 7y ago
Not really a professional setting, but I teach TLA+ to the above average kids in my class (I teach 2 hours a week) in high school (15 / 16 yo). I started this a few weeks ago as an experiment, but the results are great. The students are enthousiastic, and while they need a bit of help, it's not too hard to get into for simpeler projects. So far a student has used it to model his rubiks cube solving bot can do every move a human can. Furthermore, we are currently using it for proving their anti collision system for multiple robots navigating a grid is sound.
dmytroi 7y ago
Started using it at work, mostly to verify lock-free code. After verifying a new code for multi producer multi consumer (MPMC) lock free queue, tests were still not passing on iOS in debug... So trust in the model allowed us to start asking if compiler was broken, and ... it was, apparently in Apple's fork of llvm, as they don't really use upstream llvm as-is, 128-bit atomic compare exchange (DCAS) is broken in debug in Xcode 8. In general it is quite useful exercise to even just model existing code line-by-line and see what possible states it can have. I'm still learning though, next step would be to try TLAPS.
jandrewrogers 7y ago
We've used it at various times to verify the design of some database kernel internals e.g. I/O scheduling. This is partly to give you confidence that the design is not broken, but on rare occasion it also surfaces design defects, like non-obvious race conditions. Defects surfaced in the model may not imply defects in the software e.g. obscure race conditions in the model that cannot actually occur in implementation due to details not captured in the model. But it forces you to explicitly acknowledge and investigate that.
hwayne 7y ago
I wrote a few case studies here: https://www.hillelwayne.com/post/business-case-formal-methods/#why-use-formal-methods https://www.hillelwayne.com/post/business-case-formal-method.... They're case studies that are targeted towards bosses, so focus on how it saves time and money. A couple more I know of: * https://andy.hammerhartes.de/finding-bugs-in-systems-through-formalization.html https://andy.hammerhartes.de/finding-bugs-in-systems-through... * http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/ http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-u... * https://www.youtube.com/watch?v=oMSmkRGzQ64 https://www.youtube.com/watch?v=oMSmkRGzQ64

by keyanp 7y ago

senthil_rajasek 7y ago

Check the video I posted in the comments. Leslie Lamport goes into how Amazon Cloud services team uses TLA+.

Twirrim 7y ago

Yes indeed. Seen it in use in AWS across a number of critical components. The team I was on in AWS used it for the implementation of a particular component that needed to operate at large scale and had absolutely zero tolerance of failure. Two engineers learned TLA+, started writing up the logic and discovered various ways in which the logic would work on small scale but wouldn't scale up to parallel operation across multiple servers. It's fair to say TLA+ saved our bacon there before we'd written a single line of service code. In the end we actually got the component out to production faster than predicted. The TLA+ code gave solid shape for the actual production code, and we were quickly able to prove that the code was valid and that things were working correctly. In my current role in Oracle Cloud Infrastructure, there is actually a small dedicated team of engineers that help services use TLA+ for components, headed by Chris Newcombe, one of the authors of the TLA+ whitepaper that came out of Amazon (https://lamport.azurewebsites.net/tla/formal-methods-amazon.pdf https://lamport.azurewebsites.net/tla/formal-methods-amazon....) My current team has just started exploring it for use for a component that similarly has little tolerance for error. It's not in the same territory of "if it fails it's catastrophic", thankfully, but if it fails it's a major inconvenience for customers.

ausimian 7y ago

I used it for the first time in firmware design at MSFT a few years ago, and I've used it since in the areas of protocol design. I don't use it frequently but it's a tool I'm glad I took the time to learn, and have to hand when I need it. My experience is that, using TLA+, or other tools like it, encourages you to think precisely about the problem and at the same time exclude unnecessary details. That alone I find useful in terms of the insights it gives e.g. surfacing interesting invariants, or alternatively, invalidating them. In any case, you use the model-checker (TLC) to test these assumptions quite easily, and then bring these invariants into your code, either in the form of assertions, contracts or perhaps in property-based testing. In any case, I would say the process of writing such a specification yields benefits. Perhaps this can best be summed up by something I think Leslie Lamport once said: "If you're not writing when you're thinking, you only think you're thinking." I should add that despite claims about TLA+ being particularly well-suited to concurrency problems, my implementation targets have never been 'concurrent' in the 'multi-threaded' sense. Rather, they have been single-threaded event-driven state machines, and I personally find that it excels in this space. However, as you will find, in TLA+, concurrency is just a matter of abstraction... I have found that, because TLA+ doesn't 'generate code', many colleagues struggle to see the tangible benefit. I personally think that there is a gap between the whiteboard and the editor which tools like TLA+ fill very nicely. It's not a panacea or a magic bullet, and like any tool you must still exercise judgement about when to use it, and how to use it effectively, which includes understanding the limitations of the tooling (TLC cannot check arbitrary specifications). But if I find myself faced with a potentially tricky algorithm, or indeed want to understand an existing algorithm, I reach for TLA+.

hedora 7y ago

I highly recommend learning TLA+ before writing any papers with math involving set logic (foreach, exists, etc), if only to teach you standard mathematical syntax for those things (like “{ s \in S : \A t \in s : func(t) }“, which is valid TLA, and will also emit a human readable formula if pasted into Latex). This would have saved me tons of work in hindsight.

mcpherrinm 7y ago

One of my coworkers used TLA+ to prove a change to a service my teams runs was correct. The service was essentially a key/value store. If one region didn't know about a key, it would recursively ask the other regions in parallel for the data. Eventually we needed to add support for deleting data. We deleted data that hadn't been read in a few months. We used TLA+ to prove our region-sync code and deletion code interacted properly along with regular get/put operations.

geoka9 7y ago

This conference paper has an anecdote: https://www.researchgate.net/publication/220757452_Specifying_and_verifying_systems_with_TLA https://www.researchgate.net/publication/220757452_Specifyin...

qcoh 7y ago

There's a paper describing the use for railway applications [0]. A few years back I had an interesting discussion with one of its authors and was shown the real model and code. Interestingly, they generated C from the TLA+ spec and this code generator was "unproven". However, the software itself had high coverage requirements and needed to be tested extensively (100% code/branch/MCD coverage, I don't quite remember). One of the points he made was that the upfront cost pays for itself by avoiding bugs that are hard to debug. [0]: https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1lpx9C/view https://drive.google.com/file/d/1rAn3N5hViv3xNe2E55lMzpFFym1...

superice 7y ago

Not really a professional setting, but I teach TLA+ to the above average kids in my class (I teach 2 hours a week) in high school (15 / 16 yo). I started this a few weeks ago as an experiment, but the results are great. The students are enthousiastic, and while they need a bit of help, it's not too hard to get into for simpeler projects. So far a student has used it to model his rubiks cube solving bot can do every move a human can. Furthermore, we are currently using it for proving their anti collision system for multiple robots navigating a grid is sound.

dmytroi 7y ago

Started using it at work, mostly to verify lock-free code. After verifying a new code for multi producer multi consumer (MPMC) lock free queue, tests were still not passing on iOS in debug... So trust in the model allowed us to start asking if compiler was broken, and ... it was, apparently in Apple's fork of llvm, as they don't really use upstream llvm as-is, 128-bit atomic compare exchange (DCAS) is broken in debug in Xcode 8. In general it is quite useful exercise to even just model existing code line-by-line and see what possible states it can have. I'm still learning though, next step would be to try TLAPS.

jandrewrogers 7y ago

We've used it at various times to verify the design of some database kernel internals e.g. I/O scheduling. This is partly to give you confidence that the design is not broken, but on rare occasion it also surfaces design defects, like non-obvious race conditions. Defects surfaced in the model may not imply defects in the software e.g. obscure race conditions in the model that cannot actually occur in implementation due to details not captured in the model. But it forces you to explicitly acknowledge and investigate that.

hwayne 7y ago

I wrote a few case studies here: https://www.hillelwayne.com/post/business-case-formal-methods/#why-use-formal-methods https://www.hillelwayne.com/post/business-case-formal-method.... They're case studies that are targeted towards bosses, so focus on how it saves time and money. A couple more I know of: * https://andy.hammerhartes.de/finding-bugs-in-systems-through-formalization.html https://andy.hammerhartes.de/finding-bugs-in-systems-through... * http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-understand-xen-vchan/ http://roscidus.com/blog/blog/2019/01/01/using-tla-plus-to-u... * https://www.youtube.com/watch?v=oMSmkRGzQ64 https://www.youtube.com/watch?v=oMSmkRGzQ64