Hacker News Board Hacker News, browsed like a classic message board
Live data from Hacker News

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

cslab.pepperdine.edu

Post reply on HN
Print view View original

11–20 of 30 posts

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

#11

Post by Twirrim »

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 formal methods from scratch. (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).

It took a little bit for them to get up to speed, but they were soon implementing and catching bugs in the proposed designs, and they had all the bugs ironed out within a few weeks.

They then found that going from TLA+ to actual Java code was almost a "fill in the blanks" exercise. The formal model provided almost the exact structure they needed for their final code. Going from model to code took them very little time at all. It was in production, running in shadow mode after not even 2 months, and was fully live not long afterwards.

TLA+ got subsequently used for a number of other features added to the platform.

There had been general push back among developers that learning TLA+ and doing formal verification was only going to slow them down, but we found it was quite to the opposite. TLA+ actually sped up development, with the big bonus of higher confidence of correctness.

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

#12

Post by lwb »

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 engineers, from entry level to principal.

I thought it was especially interesting that several engineers at AWS were effectively writing their own model checkers by writing programs that tried to brute force rare combinations of conditions that would lead to system failure. Obviously TLA+ does this better and faster so they switched to that.

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

#13

Post by exdsq »

mjb wrote: post #9
ignoramous wrote: post #5

Bryon Cook, a principal scientist at Automated Reasoning Group gives an overview of various solvers in-use today at AWS: https://www.youtube.com/watch?v=UKqVY0SSbus Here's a presentation by Eric, a distinguished engineer, and Neha, a principal engineer, on analysing IAM policies (Zelkova?) and Network reachability (Tiros?): https://www.youtube.com/watch?v=x6wsTFnU3eY This webpage has many more links to blog articles…

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…

Is TLA+ only ever used as a tool by developers or do you have "formal methods" engineers who are only involved with that step of the process?

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

#14

Post by mjb »

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+ :)

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

#16

Post by bordercases »

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…

How do you believe using TLA+ compares to the "rich static typing" systems that pump up the valuations of Scala and Haskell?

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

#18

Post by amortize_ »

mjb wrote: post #9
ignoramous wrote: post #5

Bryon Cook, a principal scientist at Automated Reasoning Group gives an overview of various solvers in-use today at AWS: https://www.youtube.com/watch?v=UKqVY0SSbus Here's a presentation by Eric, a distinguished engineer, and Neha, a principal engineer, on analysing IAM policies (Zelkova?) and Network reachability (Tiros?): https://www.youtube.com/watch?v=x6wsTFnU3eY This webpage has many more links to blog articles…

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?

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

#19

Post by zozbot234 »

bordercases wrote: post #16
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…

How do you believe using TLA+ compares to the "rich static typing" systems that pump up the valuations of Scala and Haskell?

Not very comparable. TLA+ involves writing statements in a custom "logic" which adds modalities (i.e. monads) to support 'time' (or rather, state transitions in discrete steps, ala temporal logic) and non-determinism (which is reused to support refinement) to standard propositional logic.

Nothing like this can be done in a standard programming language (even Scala or Haskell), and even in a dependently-typed language you would need to write some support code in order to embed this logic and work with it within the system. (It wouldn't be hard for sure, since even FOL gives you far more power than any (multi-)modal logic, but it's a different, perhaps more elegant take on things than just working directly within TLA).

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

#20

Post by bordercases »

zozbot234 wrote: post #19
bordercases wrote: post #16

Earlier quoted context omitted.

How do you believe using TLA+ compares to the "rich static typing" systems that pump up the valuations of Scala and Haskell?

Not very comparable. TLA+ involves writing statements in a custom "logic" which adds modalities (i.e. monads) to support 'time' (or rather, state transitions in discrete steps, ala temporal logic) and non-determinism (which is reused to support refinement) to standard propositional logic. Nothing like this can be done in a standard programming language (even Scala or Haskell), and even in a dependently-typed language…

Thanks for your response.
Post reply on HN