4 ms·

Use of Formal Methods at Amazon Web Services (2013) [pdf]

91 points by yankcrime 12y ago

xxpor 12y ago
404 :(
- hyperliner 12y ago
  It's working for me.
coldcode 12y ago
Odd to see something about Amazon from Microsoft.
- dlgeek 12y ago
  Looks like it's a personal directory for Leslie Lamport (http://en.wikipedia.org/wiki/Leslie_Lamport http://en.wikipedia.org/wiki/Leslie_Lamport), who is cited several times in the paper. Think of it as a professor hosting research papers that cite him in his field on his university site, rather than a business site.
  - mcguire 12y ago
    And that use his research. Lamport created TLA+.
- ryanburk 12y ago
  TLA and much of the initial research in distributed systems (paxos!) came from Lamport who has been at microsoft for years now. if you look at the references in the document, many point to his work.
- hyperliner 12y ago
  Actually, there is a lot of respect for AWS at Microsoft. Huge partners and competitors. Think about it as Microsoft giving you access for free to a good doc for the whole world. Also known as "don't look at the gift horse in the tooth."
jedberg 12y ago
This explains why it takes so long for them to release new features in AWS. Fascinating.
saosebastiao 12y ago
Really cool stuff. I have a couple of questions: 1) How do you model the myriad fault types that could possibly occur in distributed systems? 2) Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs?
- mjb 12y ago
  > 1) How do you model the myriad fault types that could possibly occur in distributed systems? You need to think at the right level of abstraction. Are packet loss and reordering really different faults? Are packet loss to a node and the stop failure of that node different faults? The answers depend on your model. Lamport's Fast Paxos model is a good example of how different faults are handled in different levels of models (http://research.microsoft.com/pubs/64624/tr-2005-112.pdf http://research.microsoft.com/pubs/64624/tr-2005-112.pdf). > Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? Yes, there are several powerful techniques for partially modelling systems. One of the most successful is the idea of abstraction (modelling less) and refinement (modelling more). Abstraction and refinement let you move up and down the levels of detail, and "refinement mappings" provide a rigorous tool for ensuring the validity of these moves. "The existence of refinement mappings" (http://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-existence.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/a...) is the classic paper in this area, and Lamport's earlier "What good is temporal logic?" was one of the first to introduce the idea (http://research.microsoft.com/en-us/um/people/lamport/pubs/what-good.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/w...). This paper from Van Renesse et al (http://arxiv.org/abs/1309.5671 http://arxiv.org/abs/1309.5671) is a good illustration of the kind of formal things that can be done with refinement. In practice, choosing the level of abstraction to apply these techniques is key to their success, but their flexibility makes it easy to work at any level. Choosing the right one is very application specific, and requires engineering and mathematical judgement. > 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs? That depends hugely on the complexity of the model. TLC is a very brute-force solution to the problem of model checking (with a few clever optimizations), and run time rises very quickly with model complexity. Model checking is tractable for some very meaningful models.
gone35 12y ago
We are concerned with two major classes of problems with large distributed systems; 1) bugs and operator errors that cause a departure from the logical intent of the system, and 2) surprising 'sustained emergent performance degradation' of complex systems that inevitably contain feedback loops. We know how to use formal specification to find the first class of problems. However, problems in the second category can cripple a system even though no logic bug is involved. (...) A common example is when a momentary slowdown in a server (perhaps due to Java garbage collection) causes timeouts to be breached on clients, which causes the clients to retry requests, which adds more load to the server, which causes further slowdown. In such scenarios the system will eventually make progress; it is not stuck in a logical deadlock, livelock, or other cycle. But from the customer's perspective it is effectively unavailable due to sustained unacceptable response times. (...) TLA+ could be used to specify an upper bound on response time, as a real-time safety property. However, our systems are built on infrastructure (disks, operating systems, network) that do not support hard real-time scheduling or guarantees, so real-time safety properties would not be realistic. We build soft real-time systems in which very short periods of slow responses are not considered errors. However, prolonged severe slowdowns are considered errors. We don't yet know of a feasible way to model a real system that would enable tools to predict such emergent behavior. Interesting. TLA+ of course allows for hybrid specifications that incorporate physical constraints --real-time itself being the prime example--, so constraints based on more complicated 'loss functions' like, say, weighted average or total variation of response times, in principle ought to be feasible as well. Leslie Lamport himself laments such specifications are still 'of only academic interest' [1, §9.5], so I wonder how impractical such specifications could they really get. [1] http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo...
edwinnathaniel 12y ago
This is VERY interesting and feels like utilizing the very core of Computer Science. I'm definitely done reading blog/article on how TDD/BDD/ATDD or Clojure/Haskell make one more productive without scientific background ;)

91 points by yankcrime 12y ago

xxpor 12y ago

404 :(

hyperliner 12y ago
It's working for me.

coldcode 12y ago

Odd to see something about Amazon from Microsoft.

dlgeek 12y ago
Looks like it's a personal directory for Leslie Lamport (http://en.wikipedia.org/wiki/Leslie_Lamport http://en.wikipedia.org/wiki/Leslie_Lamport), who is cited several times in the paper. Think of it as a professor hosting research papers that cite him in his field on his university site, rather than a business site.
- mcguire 12y ago
  And that use his research. Lamport created TLA+.
ryanburk 12y ago
TLA and much of the initial research in distributed systems (paxos!) came from Lamport who has been at microsoft for years now. if you look at the references in the document, many point to his work.
hyperliner 12y ago
Actually, there is a lot of respect for AWS at Microsoft. Huge partners and competitors. Think about it as Microsoft giving you access for free to a good doc for the whole world. Also known as "don't look at the gift horse in the tooth."

jedberg 12y ago

This explains why it takes so long for them to release new features in AWS. Fascinating.

saosebastiao 12y ago

Really cool stuff. I have a couple of questions: 1) How do you model the myriad fault types that could possibly occur in distributed systems? 2) Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs?

mjb 12y ago
> 1) How do you model the myriad fault types that could possibly occur in distributed systems? You need to think at the right level of abstraction. Are packet loss and reordering really different faults? Are packet loss to a node and the stop failure of that node different faults? The answers depend on your model. Lamport's Fast Paxos model is a good example of how different faults are handled in different levels of models (http://research.microsoft.com/pubs/64624/tr-2005-112.pdf http://research.microsoft.com/pubs/64624/tr-2005-112.pdf). > Is it possible to partially model a system? For example, in SOA, the behavior of a service can depend on and be greatly affected by the behavior of other services. Can each service be modeled in isolation with meaningful results? Yes, there are several powerful techniques for partially modelling systems. One of the most successful is the idea of abstraction (modelling less) and refinement (modelling more). Abstraction and refinement let you move up and down the levels of detail, and "refinement mappings" provide a rigorous tool for ensuring the validity of these moves. "The existence of refinement mappings" (http://research.microsoft.com/en-us/um/people/lamport/pubs/abadi-existence.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/a...) is the classic paper in this area, and Lamport's earlier "What good is temporal logic?" was one of the first to introduce the idea (http://research.microsoft.com/en-us/um/people/lamport/pubs/what-good.pdf http://research.microsoft.com/en-us/um/people/lamport/pubs/w...). This paper from Van Renesse et al (http://arxiv.org/abs/1309.5671 http://arxiv.org/abs/1309.5671) is a good illustration of the kind of formal things that can be done with refinement. In practice, choosing the level of abstraction to apply these techniques is key to their success, but their flexibility makes it easy to work at any level. Choosing the right one is very application specific, and requires engineering and mathematical judgement. > 3) Is the run time of model checking managable? The paper mentioned a few seconds to find bugs, but how long to exhaustively check a model without bugs? That depends hugely on the complexity of the model. TLC is a very brute-force solution to the problem of model checking (with a few clever optimizations), and run time rises very quickly with model complexity. Model checking is tractable for some very meaningful models.

gone35 12y ago

We are concerned with two major classes of problems with large distributed systems; 1) bugs and operator errors that cause a departure from the logical intent of the system, and 2) surprising 'sustained emergent performance degradation' of complex systems that inevitably contain feedback loops. We know how to use formal specification to find the first class of problems. However, problems in the second category can cripple a system even though no logic bug is involved. (...) A common example is when a momentary slowdown in a server (perhaps due to Java garbage collection) causes timeouts to be breached on clients, which causes the clients to retry requests, which adds more load to the server, which causes further slowdown. In such scenarios the system will eventually make progress; it is not stuck in a logical deadlock, livelock, or other cycle. But from the customer's perspective it is effectively unavailable due to sustained unacceptable response times. (...) TLA+ could be used to specify an upper bound on response time, as a real-time safety property. However, our systems are built on infrastructure (disks, operating systems, network) that do not support hard real-time scheduling or guarantees, so real-time safety properties would not be realistic. We build soft real-time systems in which very short periods of slow responses are not considered errors. However, prolonged severe slowdowns are considered errors. We don't yet know of a feasible way to model a real system that would enable tools to predict such emergent behavior. Interesting. TLA+ of course allows for hybrid specifications that incorporate physical constraints --real-time itself being the prime example--, so constraints based on more complicated 'loss functions' like, say, weighted average or total variation of response times, in principle ought to be feasible as well. Leslie Lamport himself laments such specifications are still 'of only academic interest' [1, §9.5], so I wonder how impractical such specifications could they really get. [1] http://research.microsoft.com/en-us/um/people/lamport/tla/book-02-08-08.pdf http://research.microsoft.com/en-us/um/people/lamport/tla/bo...

edwinnathaniel 12y ago

This is VERY interesting and feels like utilizing the very core of Computer Science. I'm definitely done reading blog/article on how TDD/BDD/ATDD or Clojure/Haskell make one more productive without scientific background ;)