How Amazon Web Services Uses Formal Methods (2015) [pdf] • Hacker News Board

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#21

Post by hwayne » Mon, Jan 20, 2020, 6:25 PM UTC

Twirrim wrote: post #11

One of the teams I worked for in AWS used TLA+ on a new back-end feature that was added. It was one that, if things went wrong, would be extremely bad for customers. The needs for operating on scale only added to the necessary complexity. Paranoia was key. They'd estimated something like an optimistic 4 months for the work. Two of the more senior developers were assigned the task, and they had to learn TLA+ and forma…

> (one dev's main complaint was that he was forced to use Eclipse, I don't know if integration has now happened with other IDEs since then)

There are a few projects to make this more accessible. We have

vscode: https://github.com/alygin/vscode-tlaplus

Jupyter notebooks: https://github.com/kelvich/tlaplus_jupyter

emacs: https://github.com/mrc/tla-tools

I sort of wrote a vim plugin, but it's nowhere near as sophisticated as the above three. I also recently made public a personal CLI tool (https://github.com/hwayne/tlacli) for running TLC on the command line. It's experimental but I find it really useful.

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#22

Post by hwayne » Mon, Jan 20, 2020, 6:28 PM UTC

_cairn wrote: post #15

Does anyone have resources that talk about writing a TLA+ model for an existing software system as opposed to designing a new system using TLA+ as the design reference?

Check out Marianne Bellotti's work. She recently gave a talk at Strange Loop on writing specifications of existing systems: https://www.youtube.com/watch?v=oMSmkRGzQ64

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#23

Post by martythemaniak » Mon, Jan 20, 2020, 6:52 PM UTC

One thing I'm wondering is whether (or rather, what kind of) bugs arise when you try to translate a model (described as "exhaustively tested pseudocode" elsewhere in this thread) into a real system. For example, if there is if-branch somewhere that gets missed etc?

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#24

Post by lemmster » Mon, Jan 20, 2020, 7:07 PM UTC

_cairn wrote: post #15

Does anyone have resources that talk about writing a TLA+ model for an existing software system as opposed to designing a new system using TLA+ as the design reference?

Below are a few specs related to refactoring/rewriting the TLA+ model checker to scale to more cores:

* https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...

* https://github.com/lemmy/PageQueue

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#25

Post by exdsq » Mon, Jan 20, 2020, 7:35 PM UTC

amortize_ wrote: post #18

mjb wrote: post #9

Earlier quoted context omitted.

Yes, since we published this (I'm one of the authors), the Automated Reasoning Group have done amazing work applying formal methods to a broad range of problems at AWS. We're also still using TLA+ in many places for the reasons the paper describes. One aspect of TLA+ (and formal specifications in general) that I under appreciated when we wrote this was how useful they are as a communication tool. I've found well-comm…

Does your team hire PhDs with formal verification backgrounds? If so, what is the interview process like? Do you make them go through the standard leetcode type interviews?

Side note - did you do a PhD in formal verification? I'd love to hear more about it? I am seriously considering it myself.

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#26

Post by zozbot234 » Mon, Jan 20, 2020, 7:38 PM UTC

martythemaniak wrote: post #23

One thing I'm wondering is whether (or rather, what kind of) bugs arise when you try to translate a model (described as "exhaustively tested pseudocode" elsewhere in this thread) into a real system. For example, if there is if-branch somewhere that gets missed etc?

A TLA+ specification is generally a simplified model of a real system design. So issues can definitely arise when building the real thing, but model testing on a TLA+ spec can definitely help with quickly surfacing bugs that would exist even in a simplified design. Just don't expect it to do more than that.

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#27

Post by lemmster » Mon, Jan 20, 2020, 7:40 PM UTC

martythemaniak wrote: post #23

One thing I'm wondering is whether (or rather, what kind of) bugs arise when you try to translate a model (described as "exhaustively tested pseudocode" elsewhere in this thread) into a real system. For example, if there is if-branch somewhere that gets missed etc?

I am the engineer who translated https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/... into Java (https://github.com/tlaplus/tlaplus/blob/master/tlatools/src/...). The translation took me about half a day. Later, while running scalability experiments, a correctness bug intermittently showed up, on which I spent approximately two weeks to find the root cause. The two weeks included fixing around a dozen bugs in code that was not specified in TLA+. However, none of these bugs were correctness bugs and unrelated to the correctness bug. Eventually, I translated the TLA+ spec into input for Java Pathfinder, which found the cause of the correctness bug immediately: The Java translation contained an off-by-one bug in a for loops (TLA+ is one-indexed while Java is zero-indexed). I am still convinced that a code review would have found the bug and that JPF was a very heavyweight substitute for a fresh pair of eyes. In other words, the bugs that get introduced during the translation phase are shallow and easily corrected.

Note that no other bugs have been reported for the code since.

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#28

Post by amortize_ » Mon, Jan 20, 2020, 7:57 PM UTC

exdsq wrote: post #25

amortize_ wrote: post #18

Earlier quoted context omitted.

Does your team hire PhDs with formal verification backgrounds? If so, what is the interview process like? Do you make them go through the standard leetcode type interviews?

Side note - did you do a PhD in formal verification? I'd love to hear more about it? I am seriously considering it myself.

I have not, but like you am considering getting a PhD in this area.

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#29

Post by _cairn » Tue, Jan 21, 2020, 4:10 PM UTC

hwayne wrote: post #22

_cairn wrote: post #15

Does anyone have resources that talk about writing a TLA+ model for an existing software system as opposed to designing a new system using TLA+ as the design reference?

Check out Marianne Bellotti's work. She recently gave a talk at Strange Loop on writing specifications of existing systems: https://www.youtube.com/watch?v=oMSmkRGzQ64

Thank you! I will check this out.

Re: How Amazon Web Services Uses Formal Methods (2015) [pdf]

#30

Post by lwb » Tue, Jan 21, 2020, 11:10 PM UTC

mjb wrote: post #14

lwb wrote: post #12

Questions I wondered about that weren't answered until the end of the paper: Q: Do engineers actually implement AWS systems in TLA+? A: No, TLA+ is called "exhaustively testable pseudo-code" internally, and is only used for designs. Q: Which AWS systems use it? A: The first was DynamoDB, followed by S3, and now there are 8 additional complex systems that use it for designs. Q: Who uses TLA+ at Amazon? A: All engineer…

Thanks for the useful summary. > All engineers, from entry level to principal. I'd phrase that as "some engineers of all levels". It's certainly not true that all engineers at AWS use TLA+ :)

Yes, thanks for the correction!