I've actually posted on this topic in the past, but I spend so much of my own time thinking about it that I'm going to revisit the question from my "revised and improved" perspective, a year or so down the road.
Context: with the move towards a disaggregated data center model in which we use RDMA or other forms of next-generation direct access to talk to remote memory (perhaps persistent, perhaps not), we find ourselves in a world where the underlying costs and barriers have shifted dramatically relative to the programming style familiar in the past.
Specific example: Consider 2-phase commit, or your favorite consensus protocol, or Paxos. In the recent past, we would program these protocols by having some leader who initiates the protocol and sends out a request to the other participants: "can you commit transaction 71?" or "I vote 1", or "I propose that we place value v into Paxos log slot 22, and this is my 3rd ballot for that slot." Responses eventually come back, and after a round or two of these back-and-forth interactions, the protocol terminates.
In that classic way of thinking, there was a kind of implicit balance in mind between the cost of moving the data (value v in the example above) and the cost of the back-and-forth round-trips. I'm not quite sure how to best express this sense of balance, but what one finds is that the cost of the round-trip actions (the RTT, as we say in the business...) is sort of "reasonable" relative to the bandwidth available for moving the value field, often over TCP connections or UDP.
Today, with new forms of direct remote memory access, talking to remote memory over a technology like RDMA is actually faster than talking to local memory, but only in the sense that RDMA can sustain a far higher bandwidth than local actions like using memcpy (the fastest available copying primitive on a Linux/C computing platform) to move data from one place in memory to another, assuming that the data in question isn't in the L2 cache. As RDMA speeds up, this gap will only get larger. So it is very cheap to move data from machine A to machine B.
In contrast, the RTT for a modern optical Ethernet is surprisingly high, when you consider quite how fast copying can be. We see RTTs in the 1.5us to 2.5us range: quite fast compared to the 1-10ms numbers that were common for protocols running over TCP/UDP/IP, but relatively sluggish if you consider the number of bytes that could have been sent in that time, particularly if you add in the delays for scheduling a thread to notice the request coming in (when A's message arrives on B), or to send the reply (when B's response reaches A).
If A blocks sending while waiting for this RTT to complete, quite a few bytes won't be sent. And as RDMA gets faster (today, 100Gbps, but tomorrow 200, then 400, and 1Tbps is within range now), the amount of missed transmission opportunity gets pretty substantial.
Concurrency feels like the obvious answer, but this instinctive reaction proves to be naive. The theory would be that if A has lots of side by side transactions with B, then while one waits, another can transmit. But that overlooks overheads: concurrency also brings many kinds of costs, and this model is anything but a clear win! Those costs could quickly add up: locking to ensure that the transfers won't interfere with one-another, memory contention on the DRAM chunks where the data lives, various forms of state that might be sitting around while the round-trip interactions are running (threads consume stack space, for example). So concurrency doesn't come for free.
Batching is a second possibility: A could collect a bunch of requests, then send them as a batch (while collecting the next batch), B could respond on the whole series of requests (one by one, but as a batch of responses), and so forth. This amortizes costs in a nice way.
Batching makes sense on a receiver, too. Rather than sending batches and forcing the receiver to use those batch sizes, a sender could send continuously, and the receiver could bite off a chunk of incoming records based on when it happens to be ready to run. So if we have A sending continuously, rather than having A batch 10 items at a time, it could stream steadily to B. B might be ready for its next chunk of input at a moment when there are 11 items available; it treats these as a batch of 11. Then at the next loop, B is perhaps ready for input when 4 new items have turned up: a batch of 4. We still see a benefit of amortized costs, but the batch sizes are variable and determined by when B happens to be ready, rather than fixed and decided by A (the sender).
Derecho works this way.
Now why are we discussing these obvious points? Well, the optimality of Derecho is directly tied to its use of this style of receiver-side batching. The key "thing" about Derecho is that it runs a version of Paxos modified to make decisions as soon as possible, based on the Paxos notion of safety, using receiver-side batches. This allows us to stream an exceptionally high rate of Paxos requests, process them with no unnecessary delays, and amortize all costs over batches of events.
In fact, the value of this method centers on the steady stream of updates. With one update, by itself, classic Paxos is a reasonable choice of protocol. But with a stream of updates, we need to amortize costs for efficiency. The classic protocols run in a greedy way, and cease to be efficient because they miss this opportunity!
So now the question arises: is this a story purely about Derecho, or does the same opportunity transition to other kinds of systems that aren't doing atomic multicast (vertical Paxos) and atomic log updates (classic durable Paxos)? For example, could a distributed file system somehow gain performance by being implemented to use the same sort of pattern? Could a database system be optimized by leveraging this sort of transformation?
And we can pose the problem even more broadly. As a programming question (almost a compilation question), is there a systematic programming methodology here, one that would lead the developer to an optimized solution matched to the underlying cost model mentioned earlier (the cost model in which steady flow works extremely well at high rates and with large data volumes, but RTT looks somewhat costly)? How could one start with a specification of a file system, or a specification of Paxos, and systematically arrive at a solution like Derecho?
I find it fascinating that despite all the work that has been done on stream processing in database systems, there seems to be very little prior work on the kind of protocol optimization I've outlined. The underlying "memory model" is really just an exaggerated NUMA one, with a cache-line memory coherence model, remote memory access, but with unusually high latencies relative to the extremely high bandwidth. By and large, my colleagues in the PL community view the resulting questions as being variations on what they are already used to: they have extensive experience with NUMA programming. Yet here we can see that we actually are after solutions that can be quite different from the classic ones: Derecho doesn't look a lot like Paxos at first glance, and the optimality we achieved emerges from the Paxos protocol transformations that let us optimize for the RDMA environment. So there was something non-trivial happening here, even though it happens over the standard NUMA model.
I don't know if we have PL readers of this blog, but I would love to hear their thoughts, if so!
Showing posts with label specifications. Show all posts
Showing posts with label specifications. Show all posts
Wednesday, 7 March 2018
Thursday, 12 October 2017
Deriving assumptions and constraints
In the past few blog entries, I focused on issues of "specification": to what extent are we able to specify the behavior our systems guarantee, the behavior we expect clients to respect, or other kinds of assumptions we might be making about the setting, peak loads, and so forth?
Today I thought I might ask a closely related question: could formal theorem-proving tools, like the Ivy prover used by my friends at Tel Aviv University, or the NuPRL system that Bob Constable's group here at Cornell created, be used to "extract" a specification, including any assumptions or constraints the solution imposes on applications that use it?
I should mention that while these two theorem proving systems use high level logic languages, not all such systems are quite so mathematical in approach. If you prefer Java as your coding language, Microsoft's Dafny would be another system where you could pose my question. In fact, Dafny really embodies the main idea behind this blog posting, but approaches it the question in a slightly different way. In Dafny, when you specify a component of a system, you encode any preconditions or invariants as assertions in a special notation that goes into the documentation for the associated module and methods. Later, when compiling your code, Dafny requires you to prove that the method actually respects the constraints that you expressed this way. So Dafny doesn't automate specification, per se, but it does enforce that a method must respect its specification, and it can sometimes automatically prove that this property holds. If so, you won't need to do anything more at all. Further, if your users later violate an assumption, Dafny would refuse to compile their code, ensuring that your module will be used only as intended.
The problem of automatically figuring out what these specifications should include looks super hard, but is fascinating to me: an ideal topic for research, if you have the math and type-theory background (or are willing to learn: nobody is born knowing that stuff...)
So here's the setting. Suppose I have a method for computing some function, F(x), such as "it computes x/2". Now, assume that I decide to run it purely with integer arithmetic. When will method F() be correct? Well, for this simple example, it will work for even values of x. Had I been using Dafny, it might refuse to compile my code without some help, such as "assert even(x)" as a precondition (the definition of even(x) could be something like x%2 == 0, for an integer x).
So Dafny wouldn't necessarily compile code with an error in it, but it often wouldn't know why the code isn't correct. The question becomes: could a theorem prover have figured this out for me? With this very simple example, the answer is "sort of." Take a theorem prover, and tell it that F is a "lambda" that maps from x to x/2. Now define the argument x to be of type integer, and tell it that the arithmetic operator is of type (integer, integer) => integer.
If you tell NuPRL or Ivy to "verify" this code, it should fail, just as Dafny should fail, giving an example such as "x=1", and meaning "with 1 as its input, F(1) gives an undefined result". Another possibility, for situations where the prover understands that integer division rounds down, would to try and verify the invariant that F(X)*2 = X. This should fail, with the example F(1)=0.
So now we know that our function doesn't "work" as intended. What we really want is for the system to suggest "Have you considered requiring that X must be even?"
So this would be an automated derivation of an assumption, or of a constraint on the inputs. (For this blog posting, we can assume that assumption and constraint are synonyms, although there are some PL communities that use the terms in slightly different ways.)
How hard is to automate the inference of assumptions? With current programming languages, it can be very difficult, for several reasons. A core issue is specificity and naturalness. Notice first that because false implies anything, there is a very simple universal constraint, but it renders the problem totally useless. This rules out any kind of simple way of solving the problem. So we want a non-trivial solution.
Next, consider that specifications can involve multiple kinds of formalisms: multiple areas of mathematics. For example, over the course of my career I've worked with systems that have real-time guarantees, protocols in which you typically specify a convergence guarantee, more classic temporal logic properties, such as consistency for state-machine replication. Years ago, one of my students (Kryzs Ostrowski) made the point that there aren't any programming languages in which all three of these "models" would easily fit. He argued for a different form of type checking, but setting that to the side, the bottom line is that if you code in a language where temporal logic is relatively easy to express (like Dafny), you probably won't be able to specify real-time properties, or probabilistic convergence properties. Each style of property has a different most natural style of formalism, and they don't necessary compose in obvious ways.
The same goes for having a system automatically infer specifications: the odds are that any given formalism will be expressive enough to capture and perhaps infer at least some kinds of specifications in its own formalism, but that it won't even be able to "understand" properties that are outside its normal scope of coverage.
This makes specification of the automatic-specification-derivation question itself tricky. A really good derivation of assumptions would factor out each distinct element, so that we would have a small list of them, each "speaking" about a distinct aspect of the runtime environment. But a theorem prover, lacking a human notion of what it means to be distinct and natural, is much more likely to extract some single messy condition for safety, and perhaps a second messy condition for liveness ("total" correctness can be viewed as having two aspects: "nothing bad happens", and "if condition X holds, then something good will eventually happen").
Of course, if English was useful for describing this goal, it would have been much easier. We basically want a normal human reader of the specification to be given a list of preconditions (requirements the caller must respect), each separately intuitive and sensible: "The program will work if (1) The inputs are even numbers. (2) No input is negative. (3) No input exceeds 2^16-1..." So getting from some single condition for correctness, if we had one, into a cleanly refactored form that feels right to human users will be a puzzle. Then we would want to specify post-conditions, again in an easily understood form, and invariants.
But while these easy cases are probably very feasible, any general approach to extracting a specification purely in temporal logic is guaranteed to be hard. Taking a favorite classic paper: I would love to see someone explore extracting the specification of uniform agreement (consensus). In principle, doing so should "derive" the famous Chandra and Toueg <>W conditions: consensus with N>2 members, of which at most one is faulty, can be achieved if the failure detection input has the property that eventually, it permanently stabilizes in a state where some correct process is never again suspected of being faulty by any correct process. A really powerful system might even be able to give a result for the more general case of N members and T failures, and derive that N > 2T+1.
If you follow this blog, you've noticed that I'm obsessed with our new Derecho system. For a system like Derecho, what could a tool of this kind derive? We think we know the actual specification (we understand our own protocols well), but it would be fun to see a surprising "angle" that we haven't considered. And you can't rule out such a thing happening: Derecho is a complex engineered piece of software, and even if we think we understand the conditions for progress and safety, perhaps there are aspects of the environment that Derecho depends upon, and that we haven't thought much about. For example, what are we assuming about the network layer (RDMA, in the case of Derecho)? What are we assuming about the SSD storage units? Are there any timing requirements?
Today I thought I might ask a closely related question: could formal theorem-proving tools, like the Ivy prover used by my friends at Tel Aviv University, or the NuPRL system that Bob Constable's group here at Cornell created, be used to "extract" a specification, including any assumptions or constraints the solution imposes on applications that use it?
I should mention that while these two theorem proving systems use high level logic languages, not all such systems are quite so mathematical in approach. If you prefer Java as your coding language, Microsoft's Dafny would be another system where you could pose my question. In fact, Dafny really embodies the main idea behind this blog posting, but approaches it the question in a slightly different way. In Dafny, when you specify a component of a system, you encode any preconditions or invariants as assertions in a special notation that goes into the documentation for the associated module and methods. Later, when compiling your code, Dafny requires you to prove that the method actually respects the constraints that you expressed this way. So Dafny doesn't automate specification, per se, but it does enforce that a method must respect its specification, and it can sometimes automatically prove that this property holds. If so, you won't need to do anything more at all. Further, if your users later violate an assumption, Dafny would refuse to compile their code, ensuring that your module will be used only as intended.
The problem of automatically figuring out what these specifications should include looks super hard, but is fascinating to me: an ideal topic for research, if you have the math and type-theory background (or are willing to learn: nobody is born knowing that stuff...)
So here's the setting. Suppose I have a method for computing some function, F(x), such as "it computes x/2". Now, assume that I decide to run it purely with integer arithmetic. When will method F() be correct? Well, for this simple example, it will work for even values of x. Had I been using Dafny, it might refuse to compile my code without some help, such as "assert even(x)" as a precondition (the definition of even(x) could be something like x%2 == 0, for an integer x).
So Dafny wouldn't necessarily compile code with an error in it, but it often wouldn't know why the code isn't correct. The question becomes: could a theorem prover have figured this out for me? With this very simple example, the answer is "sort of." Take a theorem prover, and tell it that F is a "lambda" that maps from x to x/2. Now define the argument x to be of type integer, and tell it that the arithmetic operator is of type (integer, integer) => integer.
If you tell NuPRL or Ivy to "verify" this code, it should fail, just as Dafny should fail, giving an example such as "x=1", and meaning "with 1 as its input, F(1) gives an undefined result". Another possibility, for situations where the prover understands that integer division rounds down, would to try and verify the invariant that F(X)*2 = X. This should fail, with the example F(1)=0.
So now we know that our function doesn't "work" as intended. What we really want is for the system to suggest "Have you considered requiring that X must be even?"
So this would be an automated derivation of an assumption, or of a constraint on the inputs. (For this blog posting, we can assume that assumption and constraint are synonyms, although there are some PL communities that use the terms in slightly different ways.)
How hard is to automate the inference of assumptions? With current programming languages, it can be very difficult, for several reasons. A core issue is specificity and naturalness. Notice first that because false implies anything, there is a very simple universal constraint, but it renders the problem totally useless. This rules out any kind of simple way of solving the problem. So we want a non-trivial solution.
Next, consider that specifications can involve multiple kinds of formalisms: multiple areas of mathematics. For example, over the course of my career I've worked with systems that have real-time guarantees, protocols in which you typically specify a convergence guarantee, more classic temporal logic properties, such as consistency for state-machine replication. Years ago, one of my students (Kryzs Ostrowski) made the point that there aren't any programming languages in which all three of these "models" would easily fit. He argued for a different form of type checking, but setting that to the side, the bottom line is that if you code in a language where temporal logic is relatively easy to express (like Dafny), you probably won't be able to specify real-time properties, or probabilistic convergence properties. Each style of property has a different most natural style of formalism, and they don't necessary compose in obvious ways.
The same goes for having a system automatically infer specifications: the odds are that any given formalism will be expressive enough to capture and perhaps infer at least some kinds of specifications in its own formalism, but that it won't even be able to "understand" properties that are outside its normal scope of coverage.
This makes specification of the automatic-specification-derivation question itself tricky. A really good derivation of assumptions would factor out each distinct element, so that we would have a small list of them, each "speaking" about a distinct aspect of the runtime environment. But a theorem prover, lacking a human notion of what it means to be distinct and natural, is much more likely to extract some single messy condition for safety, and perhaps a second messy condition for liveness ("total" correctness can be viewed as having two aspects: "nothing bad happens", and "if condition X holds, then something good will eventually happen").
Of course, if English was useful for describing this goal, it would have been much easier. We basically want a normal human reader of the specification to be given a list of preconditions (requirements the caller must respect), each separately intuitive and sensible: "The program will work if (1) The inputs are even numbers. (2) No input is negative. (3) No input exceeds 2^16-1..." So getting from some single condition for correctness, if we had one, into a cleanly refactored form that feels right to human users will be a puzzle. Then we would want to specify post-conditions, again in an easily understood form, and invariants.
But while these easy cases are probably very feasible, any general approach to extracting a specification purely in temporal logic is guaranteed to be hard. Taking a favorite classic paper: I would love to see someone explore extracting the specification of uniform agreement (consensus). In principle, doing so should "derive" the famous Chandra and Toueg <>W conditions: consensus with N>2 members, of which at most one is faulty, can be achieved if the failure detection input has the property that eventually, it permanently stabilizes in a state where some correct process is never again suspected of being faulty by any correct process. A really powerful system might even be able to give a result for the more general case of N members and T failures, and derive that N > 2T+1.
If you follow this blog, you've noticed that I'm obsessed with our new Derecho system. For a system like Derecho, what could a tool of this kind derive? We think we know the actual specification (we understand our own protocols well), but it would be fun to see a surprising "angle" that we haven't considered. And you can't rule out such a thing happening: Derecho is a complex engineered piece of software, and even if we think we understand the conditions for progress and safety, perhaps there are aspects of the environment that Derecho depends upon, and that we haven't thought much about. For example, what are we assuming about the network layer (RDMA, in the case of Derecho)? What are we assuming about the SSD storage units? Are there any timing requirements?
Monday, 18 September 2017
What we can learn about specifications from ZooKeeper's asynchronous mode, and its unsafe ForceSync=no option?
At the time of this writing, ZooKeeper is surely the world's most widely used data replication tool. You run it on a few machines, normally 3, and it offers a file system API with very strong guarantees to the user. In fact, if configured to do so, ZooKeeper implements the Paxos specification: Leslie Lamport's formalism of the properties required for correct state machine replication. (My post-doc, Weijia Song, points out that actually, the Zookeeper Atomic Broadcast, ZAB, isn't necessarily a true Paxos protocol, but the issue he raises is very subtle, so I'll set that to the side. For our purposes here, ZAB is close enough).
In a recent blog posting, we discussed some of the missing aspects of that very specification. As a result, when I read the ZooKeeper documentation, I was intrigued to realize that the documentation more or less urges that the system be configured to violate Paxos! In fact the document is short, and easy to read, so have a look if you are skeptical.
You'll learn about all sorts of parameters that represent ZooKeeper's response to those missing specification elements, such as how to deal with disks that fill up completely, or avoiding inconsistency in the list of servers running the ZooKeeper service.
And then, in the middle of the same document, you run into a fascinating option: there is a small section called "Unsafe configuration options" that explains that "The following options can be useful, but be careful when you use them. The risk of each is explained along with the explanation of what the variable does." Then we read about an option called ForceSync: "If this option is set to no, ZooKeeper will not require updates to be synced to the media." There is no discussion of risks at all.
Some people know about this but think of it in terms of a broader approach to "using Zookeeper asynchronously". Used asynchronously, Zookeeper lets you start a series of operations but either ignore their termination, or at least not wait one by one. Of course flow control always kicks in eventually, to prevent congestion, but you end up with a stream of requests. In this mode it is nearly universal that you would also set ForceSync=no.
So how safe are such actions?
Elsewhere, on the ZooKeeper blog, Flavio Junquera writes that the system would perfectly well if this option is used, and that it can offer big speedups. He comments that for safety, there are several options: "You could consider using write barriers, or battery-backed raid SSD". The write barrier remark relates to a Linux system call, "fsync". A battery-backed raid SSD is a type of SSD storage with a DRAM cache that can hold pending writes in memory (in DRAM), but with battery backup so that if power fails, the pending writes will definitely complete. Then behind the DRAM are a set of SSD storage units arranged to handle transfers in parallel, so that the aggregate bandwidth might be enough to keep up with the DRAM transfer rates.
On StackOverflow and elsewhere, you can easily find threads encouraging you to configure ZooKeeper with ForceWrites=no, and assuring the reader that nobody has ever observed any bad consequences.
In effect, there is very little discussion of risks, except in the sense of "yes, you should definitely use this feature, but remember to also do these other things...."
So what's the issue, and why is it interesting?
At the core of any Paxos implementation is the transaction log where Paxos stores its state. In Derecho, this takes the form of replicated data residing in the replicated C++ objects defined by the developer. In classic Paxos, it was a list of log entries associated with the "acceptor role". Most people understand this to have been an append-only disk file, but my colleague and friend Robbert van Renesse, a Paxos expert, questions that assumption. He thinks that Leslie was deliberately vague about where the logs live, with the intent that it could equally well be used as an in-memory atomic multicast. Derecho does exactly that: it has one protocol, with two configuration options, and you get to pick. Durable storage on disk gives you a durable Paxos, and in-memory storage, a form of atomic multicast with total ordering and fault-tolerance.
The same is true in ZooKeeper, in which performance centers on the speed of the ZooKeeper transaction log. You need to tell it where you want the log to reside. Some popular options include placing it in RamDisk (in memory), or on a real disk, or perhaps an SSD. Above you saw recommendations that it be on a battery-backed raid SSD.
The problem is that if you just put the log on a normal disk or even a normal SSD disk, you get Paxos guarantees of durability... but you also see a heck of a big slowdown. Partly this is because DMA to an SSD is quite slow compared to copying in memory. But the bigger issue is that each time you do an SSD write, if you actually wait for the write to fully complete ("a forced sync"), you pay a full millisecond just waiting.
Even with concurrency this limits the typical SSD configuration of ZooKeeper to about 1000 write operations per second.
Early in the ZooKeeper story, the developers ran into this issue, and added a new option: ForceSync=no. With it, ZooKeeper "on its own" ceases to be a true Paxos log, because it will build a backlog of in-memory updates queued up to be written to disk, and won't actually carry out those updates instantly. But it gains hugely in performance: 50,000 writes per second become completely feasible. A 50x speedup... at what cost?
This is where those comments about battery-backed SSDs and write barriers enter the picture. And this is the puzzle: in fact, you can use ZooKeeper safely in this mode, at no cost and no risk at all. But it depends on your perception of cost, and of risk.
Lets start by setting ForceWrites=no but ignoring the helpful advice. ZooKeeper will be buggy. But, to be bit by this particular bug two things have to happen. First, you need to have a service that crashes and develops amnesia about a batch of committed transactions (updates) that were pending at the time of the crash. And second, someone or something needs to notice.
The point about "someone noticing" is the key to why so many applications get away with setting ForceSync=no, and yet pay no attention to Flavio's advice. Think about the sequence of events for an application using ZooKeeper. Some application is about not to complete something important, like launching the rocket ship. So it writes to the ZookKeeper log "... two, one, ignition!" and presses the launch button.
Exactly as this occurs, the power goes out, and on recovery, the system has no record that the button was about to get pushed. So we have an inconsistency that Paxos normally doesn't permit: Lamport requires that Paxos must never forget a committed transaction, meaning that once the application is told the commit has occurred, Paxos has an obligation to not lose it.
But this is not a likely failure sequence! The amnesia part, sure, that really is likely. A bit like with a normal Linux file system: if a program crashes before calling fsync, the last bytes it wrote could easily be lost (maybe even the last few thousand). We know that, and learn to call fsync. But someone actually caring, about that specific operation, yet neglecting to manually call fsync? Seems very unlikely...
So here we have ZooKeeper acting... like Linux file systems normally act! In fact, you can manually call fsync anytime you like in ZooKeeper, so if you do need it, there it is. That's the write-barrier approach.
The battery-backed raid SSD option is less common.
So who is wrong: Leslie, for including this rule in the specification? The good user, who learns to call fsync when necessary? Or the bad user, for recklessly breaking the properties of Paxos, all for a lousy 50x or 100x speedup?
As a builder, I have to feel sympathy for any developer who wants the speed. And I honestly question that Paxos specification. Maybe the requirement really is too strong! Couldn't it be reexpressed in terms of fsync: "no committed request will ever be lost if fsync was invoked, and completed after the commit?"
In fact the interesting issue here is that when ForceSync=no, ZooKeeper simply imposes an extra obligation on the behavior of the developer (use fsync, or confirm that you have the right kind of specialized SSD). As we discussed in that prior blog entry, Paxos already imposes obligations on its users, and doesn't express those either. Why is this different?
Yet I also understand Leslie. I've asked him about this, and he thinks developers will just get it wrong. They want the speed, because otherwise they look bad, so they flip this switch, but do something for extra speed in a situation where it really isn't appropriate.
Here in a college town, with students who definitely drive unsafely and fast, I get it.
How many of the developers who push ZooKeeper's insane speed button actually know what they are doing, and think about when to manually call fsync? Yet on the other hand, how many of their applications would break if the ZooKeeper storage subsystem were to slow down by 50x or 100x?
So you tell me: should systems follow the ZooKeeper lead?
Seriously: what do you think? Should Derecho support ForceSync=no?
In a recent blog posting, we discussed some of the missing aspects of that very specification. As a result, when I read the ZooKeeper documentation, I was intrigued to realize that the documentation more or less urges that the system be configured to violate Paxos! In fact the document is short, and easy to read, so have a look if you are skeptical.
You'll learn about all sorts of parameters that represent ZooKeeper's response to those missing specification elements, such as how to deal with disks that fill up completely, or avoiding inconsistency in the list of servers running the ZooKeeper service.
And then, in the middle of the same document, you run into a fascinating option: there is a small section called "Unsafe configuration options" that explains that "The following options can be useful, but be careful when you use them. The risk of each is explained along with the explanation of what the variable does." Then we read about an option called ForceSync: "If this option is set to no, ZooKeeper will not require updates to be synced to the media." There is no discussion of risks at all.
Some people know about this but think of it in terms of a broader approach to "using Zookeeper asynchronously". Used asynchronously, Zookeeper lets you start a series of operations but either ignore their termination, or at least not wait one by one. Of course flow control always kicks in eventually, to prevent congestion, but you end up with a stream of requests. In this mode it is nearly universal that you would also set ForceSync=no.
So how safe are such actions?
Elsewhere, on the ZooKeeper blog, Flavio Junquera writes that the system would perfectly well if this option is used, and that it can offer big speedups. He comments that for safety, there are several options: "You could consider using write barriers, or battery-backed raid SSD". The write barrier remark relates to a Linux system call, "fsync". A battery-backed raid SSD is a type of SSD storage with a DRAM cache that can hold pending writes in memory (in DRAM), but with battery backup so that if power fails, the pending writes will definitely complete. Then behind the DRAM are a set of SSD storage units arranged to handle transfers in parallel, so that the aggregate bandwidth might be enough to keep up with the DRAM transfer rates.
On StackOverflow and elsewhere, you can easily find threads encouraging you to configure ZooKeeper with ForceWrites=no, and assuring the reader that nobody has ever observed any bad consequences.
In effect, there is very little discussion of risks, except in the sense of "yes, you should definitely use this feature, but remember to also do these other things...."
So what's the issue, and why is it interesting?
At the core of any Paxos implementation is the transaction log where Paxos stores its state. In Derecho, this takes the form of replicated data residing in the replicated C++ objects defined by the developer. In classic Paxos, it was a list of log entries associated with the "acceptor role". Most people understand this to have been an append-only disk file, but my colleague and friend Robbert van Renesse, a Paxos expert, questions that assumption. He thinks that Leslie was deliberately vague about where the logs live, with the intent that it could equally well be used as an in-memory atomic multicast. Derecho does exactly that: it has one protocol, with two configuration options, and you get to pick. Durable storage on disk gives you a durable Paxos, and in-memory storage, a form of atomic multicast with total ordering and fault-tolerance.
The same is true in ZooKeeper, in which performance centers on the speed of the ZooKeeper transaction log. You need to tell it where you want the log to reside. Some popular options include placing it in RamDisk (in memory), or on a real disk, or perhaps an SSD. Above you saw recommendations that it be on a battery-backed raid SSD.
The problem is that if you just put the log on a normal disk or even a normal SSD disk, you get Paxos guarantees of durability... but you also see a heck of a big slowdown. Partly this is because DMA to an SSD is quite slow compared to copying in memory. But the bigger issue is that each time you do an SSD write, if you actually wait for the write to fully complete ("a forced sync"), you pay a full millisecond just waiting.
Even with concurrency this limits the typical SSD configuration of ZooKeeper to about 1000 write operations per second.
Early in the ZooKeeper story, the developers ran into this issue, and added a new option: ForceSync=no. With it, ZooKeeper "on its own" ceases to be a true Paxos log, because it will build a backlog of in-memory updates queued up to be written to disk, and won't actually carry out those updates instantly. But it gains hugely in performance: 50,000 writes per second become completely feasible. A 50x speedup... at what cost?
This is where those comments about battery-backed SSDs and write barriers enter the picture. And this is the puzzle: in fact, you can use ZooKeeper safely in this mode, at no cost and no risk at all. But it depends on your perception of cost, and of risk.
Lets start by setting ForceWrites=no but ignoring the helpful advice. ZooKeeper will be buggy. But, to be bit by this particular bug two things have to happen. First, you need to have a service that crashes and develops amnesia about a batch of committed transactions (updates) that were pending at the time of the crash. And second, someone or something needs to notice.
The point about "someone noticing" is the key to why so many applications get away with setting ForceSync=no, and yet pay no attention to Flavio's advice. Think about the sequence of events for an application using ZooKeeper. Some application is about not to complete something important, like launching the rocket ship. So it writes to the ZookKeeper log "... two, one, ignition!" and presses the launch button.
Exactly as this occurs, the power goes out, and on recovery, the system has no record that the button was about to get pushed. So we have an inconsistency that Paxos normally doesn't permit: Lamport requires that Paxos must never forget a committed transaction, meaning that once the application is told the commit has occurred, Paxos has an obligation to not lose it.
But this is not a likely failure sequence! The amnesia part, sure, that really is likely. A bit like with a normal Linux file system: if a program crashes before calling fsync, the last bytes it wrote could easily be lost (maybe even the last few thousand). We know that, and learn to call fsync. But someone actually caring, about that specific operation, yet neglecting to manually call fsync? Seems very unlikely...
So here we have ZooKeeper acting... like Linux file systems normally act! In fact, you can manually call fsync anytime you like in ZooKeeper, so if you do need it, there it is. That's the write-barrier approach.
The battery-backed raid SSD option is less common.
So who is wrong: Leslie, for including this rule in the specification? The good user, who learns to call fsync when necessary? Or the bad user, for recklessly breaking the properties of Paxos, all for a lousy 50x or 100x speedup?
As a builder, I have to feel sympathy for any developer who wants the speed. And I honestly question that Paxos specification. Maybe the requirement really is too strong! Couldn't it be reexpressed in terms of fsync: "no committed request will ever be lost if fsync was invoked, and completed after the commit?"
In fact the interesting issue here is that when ForceSync=no, ZooKeeper simply imposes an extra obligation on the behavior of the developer (use fsync, or confirm that you have the right kind of specialized SSD). As we discussed in that prior blog entry, Paxos already imposes obligations on its users, and doesn't express those either. Why is this different?
Yet I also understand Leslie. I've asked him about this, and he thinks developers will just get it wrong. They want the speed, because otherwise they look bad, so they flip this switch, but do something for extra speed in a situation where it really isn't appropriate.
Here in a college town, with students who definitely drive unsafely and fast, I get it.
How many of the developers who push ZooKeeper's insane speed button actually know what they are doing, and think about when to manually call fsync? Yet on the other hand, how many of their applications would break if the ZooKeeper storage subsystem were to slow down by 50x or 100x?
So you tell me: should systems follow the ZooKeeper lead?
Seriously: what do you think? Should Derecho support ForceSync=no?
Thursday, 7 September 2017
Inadequacy of the Paxos specification, and what we can learn from the issue
In a blog ten days ago, I discussed the issue of specifications that omit coverage for cases that actually arise in real systems. Since then two colleagues who follow the blog asked for examples to illustrate the issues, so I thought I might say a few more words on this, focusing on the classic specification of Paxos: Leslie Lamport's solution to the State Machine Replication problem (also sometimes called Consensus, or Uniform Agreement).
The traditional specification of Paxos has the following elements:
For example, suppose that Paxos isn't the real repository for data but is playing an intermediary role: the program using the Paxos service might itself be a replicated database, or some other form of replicated service that wants updates delivered in a deterministic order.
But notice how hard it would be to check a Paxos specification for adequacy. We would need a fairly elaborate (and adequate) specification of the environment, and of our larger goals. Otherwise, questions such as flow-control or other aspects of bounding resource consumption, or of client state, could never even be posed. So there is sense of chicken and egg: to understand if a Paxos specification is adequate, we really need an adequate specification of the setting where Paxos will be used, so that we can study the questions it poses about the Paxos service per-se.
I'll stop on that point, but there is more one can say about adequacy of specifications. A good topic for some other posting down the road...
The traditional specification of Paxos has the following elements:
- A specified set of participants.
- An assignment of roles {leader, acceptor, learner} to the participants. Each can have more than one role, and we often think of external clients as adding two additional roles: {command-initiator, command-consumer}.
- A leader runs a protocol for putting new commands into the Paxos log.
- An acceptor holds a Paxos log (an ordered list of slots, each of which can be empty, or can hold a command), and information about which commands are known to have committed. Any given acceptor might have gaps: slots for which it lacks the committed command (on top of this, there is also a somewhat subtle failure case in which a slot will permanently be left empty, so that every acceptor would have a gap at that spot).
- A learner runs a protocol for computing the full list of committed commands and their ordering. Any single acceptor might have gaps in its log, so the learner does this by merging logs in order to fill those gaps.
- Paxos really says nothing at all about command initiators and consumers, except that the initiator waits for a response to the request that the command be posted (in doing so, Paxos eliminates what we sometimes refer to as a causal order obligation, in which a system is expected to track and respect ordering on pending asynchronous actions).
- A rule for what it means for a command to be valid (non-triviality).
- Agreement on ordering.
- Durability: in any state where a Paxos service responds to "learn" requests, it needs to return the entire list of previously ordered commands.
Many authors just focus on the three bolded properties. Yet notice that from this set of five elements, we can easily discern a whole series of additional, unspecified aspects:
- There is a Paxos reconfiguration protocol, but it doesn't introduce additional specification elements, except to change the set of participants. Yet there are several aspects one would normally wish to see addressed:
- Malkhi has convincingly argued that one should terminate a membership epoch before starting actions in the next epoch. This avoids having a command that was initiated in epoch k commit much later, perhaps in epoch k+1. While Lamport has often said that this isn't necessarily a bad thing, Malkhi's point is that a delayed commit can be confusing, because many systems operate in a configuration-sensitive way.
- A new member of a Paxos acceptor group should probably not have an initially empty log. A means of performing state transfer to it is thus required. Simply copying some existing log to the joiner is incorrect, because by doing so, a command that previously lacked a quorum and hence was uncommitted (Paxos has a scenario in which it leaves a slot "empty") can become committed because duplicating a log effectively duplicates a vote for that command.
- When Paxos restarts after all its members crash, the protocol doesn't specify the rule for figuring out the proper initial configuration for the restarted service (this matters with dynamic membership).
- The specification says nothing about flow-control, yet if a Paxos protocol has no flow control mechanism at all, a quorum of acceptors could advance unboundedly far into the future relative to a stalled or failed acceptor. This might mean that the faulty acceptor has no feasible way to catch up later, and in effect, would decrease the resilience of the service: rather than having N members, we would have to think of it as having just N-1.
- The specification says nothing about sizes of objects (size of commands), yet acceptors will presumably have bounded amounts of memory, and might not be able to accept arbitrarily large objects. Solving this isn't necessarily hard (one could have commands that point to external objects), but then the objects would be less replicated than the commands, and one has to ask whether that somehow violates the durability property.
- The specification says nothing about fairness or other quality of service properties, such as timeliness of response. Yet real systems need fairness when many clients share a Paxos service and all the clients want a fair-share of access. In fact, one can then ask what specific notion of fairness is desired: should it be round-robin (like in Derecho)? Or should some clients be allowed to send 2x more commands than others, because they happen to be busier? Should a slower client be "delayed" by activity of a faster client?
- I mentioned that Paxos seemingly excludes situations where clients might issue a series of requests, without waiting for replies. In practice, this is common (clients often "stream" requests). We would want the client ordering to be respected by the system: if a client sends request A, then B, Paxos should preserve the A happened before B relationship.
- At Google, the Paxos owner (in fact the leader of the team responsible for the Chubby service) pointed out to me that his big issue is concerned with wide area deployments of Paxos, which introduces a whole set of issues Lamport never considered:
- Proper specification of a hierarchical Paxos. Guerraoui and Pedone and Quema all have looked at this question, primarily in connection with Ring-Paxos protocols.
- Heavy tailed behaviors. Chubby struggles to deal with very delayed data that can be caused by overloaded or damaged WAN links.
- One way to get around "late" data is to design systems that assume they have correct and current data, for example using locks or leases. Chubby does this, but it turns out that when one does so, getting WAN service instances to release their read locks so that the data can be updated, or preventing them from renewing those leases, can be very slow. This might violate a specification that requires fast normal read behavior, but also requires a fast way to be able to update "rarely changed" configuration parameters or program versions or other forms of WAN data that does change now and then.
For example, suppose that Paxos isn't the real repository for data but is playing an intermediary role: the program using the Paxos service might itself be a replicated database, or some other form of replicated service that wants updates delivered in a deterministic order.
- Do we expect that such a service would always be able to use the identical order to the Paxos log? What does this imply about the specification the client service must respect?
- On restart from crashes, we now have two forms of state: state in the durable Paxos logs, and state in the database service replicas. How should these be reconciled?
- We won't want the Paxos state to grow without bounds, so we will need to truncate the Paxos logs. There is a truncate protocol in Paxos, but what obligations fall upon the client service that wishes to make use of that truncate command? How does truncation interplay with failure cases that might arise?
But notice how hard it would be to check a Paxos specification for adequacy. We would need a fairly elaborate (and adequate) specification of the environment, and of our larger goals. Otherwise, questions such as flow-control or other aspects of bounding resource consumption, or of client state, could never even be posed. So there is sense of chicken and egg: to understand if a Paxos specification is adequate, we really need an adequate specification of the setting where Paxos will be used, so that we can study the questions it poses about the Paxos service per-se.
I'll stop on that point, but there is more one can say about adequacy of specifications. A good topic for some other posting down the road...
Tuesday, 29 August 2017
The adequacy of specifications
I had coffee with a visitor yesterday: Professor Eva Kuhn from the Technical University in Vienna. Our conversation was focused on the power, and limitations, of new methods for creating correct solutions to distributed computing problems.
As you probably know, for many years I've been in dialog with a number of programming language researchers (notably Bob Constable, Mooly Sagiv and Noam Rimsky, although the full list would be much longer and would include Leslie Lamport, Nancy Lynch, Jay Lorch and many others), all specialists on a new way of generating provably correct distributed computing systems and protocols from formal specifications. I'm not an expert on this topic myself -- my close collaborator Robbert van Renesse is far more knowledgeable than me, and actually works with such tools himself. Call me an enthusiast.
The methodology they've worked with is roughly as follows. Using temporal logic or a similar abstract mathematical representation, one creates a description of the problem in terms of sets (the members might be understood as computing nodes, processes, variables, the network itself -- the designer gets to decide), operations upon them, and statements about them. In this way we can model a distributed collection of computers, exchanges of messages between processes running upon them, and even crashes.
Next, one specifies a desired behavior, such as uniform agreement (the abstract problem underlying consensus protocols such as Paxos, including the versions we built into Derecho). In some sense this step describes a "goal", but not the method for achieving the goal. Think of the specification as a set of constraints, assumptions, invariants: properties that characterize a correct solution. Ideally, the behavior would have a safety component ("the solution only does good things, in the following sense...") and a liveness component ("provided that the following assumptions hold, the solution always terminates"). But some protocols aren't always live, and sometimes the conditions under which they are live are difficult to pin down, so this second aspect isn't necessarily feasible.
At any rate, in the penultimate step, one specifies the desired protocol itself, but still in a logic formalism. This is done by expressing the behavior of the protocol as a sequence of operations in the underlying framework -- for example, as a set of temporal logic "actions" on the underlying sets, carefully limited so that any "distributed" operation is performed using our abstracted versions of primitives that make sense in real networks. For example, the standard Paxos protocol, with its leader-based rounds used to construct ballots and contend for slots in the Paxos log, would be transformed into a series of set operations that match the behavior of the leader, the local copies of the logs at each of the acceptor processes, and so forth. The lowest level operations would be formal versions of message send and receive primitives.
With this in hand, the next step is to use a theorem prover like NuPRL (Constable's system) or Ivy (the one used at Tel Aviv University) to prove that the abstractly-specified protocol implements the abstractly-formalized behavioral specification. For example, in the case of Paxos, such a proof would show that for any feasible mix of roles (leader, acceptor, etc), and for every reachable protocol state, the correctness invariants hold. We would also want to show that from any initial state, some decision states are always reachable, but of course this is not always possible. For one thing, the FLP impossibility prevents us from creating a protocol in which a decision is guaranteed to occur within finite time, but in fact there are similar cases in which progress can't occur, namely situations that might involve a crash of a majority of the machines, or a partitioning of the network. For example, if you were to launch a consensus algorithm in a setting where more than half the nodes have crashed, clearly it wouldn't be able to reach consensus. As mentioned above, in the ideal case you actually specify assumptions under which progress can occur ("we assume that at least a majority of the processes are operational and remain operational throughout the execution of the protocol"), but it isn't always as easy as you might expect to specify those assumptions. So sometimes, this aspect is not addressed.
These NuPRL or Ivy (or TLA+, Dafny, Coq, Larch...) proofs are semi-manual. There is a proof-checking step, typically done using a technique called model checking (basically, the system enumerates reachable states and verifies that the invariants hold for all such states). Then there are higher level theorems that can offer short-cuts: general proof cases that were previously proved and checked that essentially represent forms of meta-reasoning, covering a class of behaviors. These allow the checker to avoid repeatedly model-checking basic steps and to instead model-check the pattern, and then look for instances of that pattern. Finally, when the checker stalls, a human can intervene and help it find the proof (or perhaps modify the protocol or the target environment specification, to make it easier to establish the desired property).
The meta-proofs (the higher level ones) are very interesting and necessary, because they potentially address cases that cannot be model-checked by exhaustively enumerating every reachable state. For example, suppose that some protocol can generate unbounded runs of states, but a proof exists that every reachable state satisfies a given property. With that "meta" proof in hand, we don't need to examine every reachable state in order to know that the property always holds, and this might let us make a true statement about the protocol that references the meta-property. In contrast, had we tried to examine every reachable state, the checker would have failed, since the runs are unbounded, hence the number of states needing to be checked is unbounded.
In practice, the power of a tool like Ivy or NuPRL centers on this kind of meta-reasoning, and the sophistication of the tactics used to match proof requirements to the library of meta-proofs. Someday, these tactics may approach the sophistication of a human logician, and in fact NuPRL has already been used to semi-automatically solve some deep open problems in logic! But there are many cases it would not yet be able to tackle.
When checkers fail, they sometimes can exhibit a counterexample: perhaps, a run in which two processes enter "decision" states but hold different outcome values, violating consensus. But they can also simply fail to find a proof. This is because a powerful enough specification language can encode undecidable questions, hence one simply cannot automate the entire proof task: there are guaranteed to be some problems on which a prover can neither conclude that a statement is true, nor false. Moreover, for any finite amount of resources (space, computer time) there are problems that would take much more space, or much more time, to model check. So for several reasons, the checker might stall. If it succeeds, though, the result is that we have a proof for our abstract protocol specification: we can show that it solves the problem, as specified.
An interesting point, tangential to what I really want to say here, is that one could perhaps extract minimum conditions for progress (a form of weakest precondition), in the manner common in PL correctness proofs of a few decades ago. This would automate extraction of assumptions needed to prove "conditional liveness": if the precondition holds, then progress will occur. To me that would be amazing, and would automate a step that Chandra and Toueg first proposed for consensus nearly 20 years ago (the famous <>W oracle). If you love theory and languages, do consider tackling this challenge!
But staying "on message", the last step with a prover such as Ivy or NuPRL is to extract a provably correct program in C or O'CaML from the proof itself. That is, given a specification of the problem, and a specification of the protocol, and a proof that the given protocol solves the problem, these tools let you push a button and automatically extract the corresponding code in an executable form, after which you simply compile and run it! Ideally, the compiler used should be proved correct (there is a proved compiler for a subset of C), and the operating system itself be proved correct (like SEL4), and the hardware verified too (using tools like Verilog) and the foundry that made the chips... well, one goes as far as one can. In fact any chain of technologies has its limitations. But let's not fuss over the obvious.
Professor Kuhn works with people developing safety critical systems for self-driving cars, control of potentially dangerous equipment, and so forth, and for her, this new methodology was fascinating. In fact she isn't the first person I've talked to about this: Chris Hobbs, at QNX, and his colleague Peter Shook, are also extremely interested in the potential of such tools. By taking the programmer out of the loop and extracting code directly from a proof. we seemingly eliminate a weakness in many kinds of control systems, where one historically would hire a team to design a solution, but then would depend on people to write the required code, after which you use a method such as the "B method" to try an prove the code correct. The resulting human-generated proofs are only as good as the human team carrying them out, and the worry always exists that they might have failed to check some important case. With a computer-generated proof, there are computable "checking" methods that can quickly establish whether or not every case was model-checked.
And yet even with automated extraction, issues remain. Can every solvable problem be tackled in this way? Over coffee, Professor Kuhn and I talked about two concerns.
First, there are solvable problems for which a model-checker might run low on space or time and throw up its hands, and hence that could be solved in principle, but in fact might not be amenable to formal treatment even so. So one can imagine situations in which there is some important task, like controlling the flaps on an airplane wing, a good solution that our engineering colleagues want to implement, and a hand-built proof of correctness that "seems" adequate, but for which there isn't any feasible fully-machine checked counterpart, because our computers might not be powerful enough, or perhaps because our techniques for generating model-checked proofs might not have the needed meta-proof methods at hand.
A related issue was raised by Hobbs and Shook at QNX: If a proof (and for that matter, the corresponding C program) is not "natural" in appearance, a human skeptic might not be easily convinced that it is correct. Thus there are also model-checked proofs that might be rejected by a team tasked with confirming that the airplane is safe to fly: the computer says "yes, here is the proof" but the skeptic in the team might worry that if no human can read and fully understand that proof, it could be flawed in some systematic way and yet this would be overlooked.
That concern leads directly to the second question Professor Kuhn and I found intriguing. Our conversation ended on a related form of impasse: suppose that the original problem specification itself is somehow inadequate? For example, one could imagine a specification for behavior of flaps on an airplane wing that leaves out some important case that can actually arise, and hence fails to pin down the correct behavior in that case. Such a specification leaves undefined the correct behavior for some actual situations that might arise in the real world, although perhaps it covers "most" cases and hence might seem complete and useful: you could still generate code, look at examples, trace the logic, and see that for those examples the code behaves properly. The lurking danger would be that because there were unspecified but real cases, examples could also exist in which the behavior would be different than intended, because the specification neglected to cover them.
Thus we would want to be sure that the specification itself was adequate in the sense of fully specifying every case that could really arise in practice. This, though, seems to be a somewhat less fully solved problem. Indeed, it seems to pose an impossible requirement!
I've been shown some work that looks at specifications, and the question is a classic one: large communities are hard at work on the topic, and have been for decades. The issue is that the "adequacy of a specification" problem itself seems to be undecideable. The intuition is sort of obvious: if one could decide all possible adequacy situations, what would stop me from encoding some simple undecideable problem (such as the halting problem), and then using the test of adequacy to solve the undecideable problem? Seemingly, nothing stops me from doing this. Thus adequacy-testing should itself be undecideable. I bet someone has proved this, although I don't think I've ever seen such a paper. I need to read more of the PL literature.
At any rate, what we see here is that on the one hand, our field seems to be at the edge of a major advance (automated synthesis of provably correct solutions to safety-critical systems problems), but on the other hand, is also approaching a natural and final form of impossibility: the risk that for important cases, it may turn out to be impossible to verify that the specification itself is "complete".
There is reason for hope. There are many situations in which if one is given a program and must answer a question about it, the task cannot be solved because the given program might encode an undecideable task. Yet when we use computational methods to generate programs, we can often prove that our methods only generate sound programs.
Could we solve the adequacy problem in this manner? For example, is there a way to generate specifications through some kind of dialog with the developer, that would only generate adequate specifications with full coverage of the problem domain? This, I think, should be possible. The resulting solution might not be able to specify every problem you can dream up, but for the things it could specify, we would know that the specification doesn't overlook any possible scenarios.
Perhaps the practical class of critical control systems doesn't actually require the ability to specify control tasks that encode undecideable questions. If so, then perhaps every needed critical control solution can be created. This would finesse the issue: even though there may be ways to encode undecideability into the same formalism, our more limited use of the methodology would never attempt to do the impossible.
My hope is that we are rapidly heading towards this kind of happy outcome... with all the progress on proofs using NuPRL an Ivy (and other systems like TLA+, Dafny, Larch and Coq), we'll know pretty soon.
As you probably know, for many years I've been in dialog with a number of programming language researchers (notably Bob Constable, Mooly Sagiv and Noam Rimsky, although the full list would be much longer and would include Leslie Lamport, Nancy Lynch, Jay Lorch and many others), all specialists on a new way of generating provably correct distributed computing systems and protocols from formal specifications. I'm not an expert on this topic myself -- my close collaborator Robbert van Renesse is far more knowledgeable than me, and actually works with such tools himself. Call me an enthusiast.
The methodology they've worked with is roughly as follows. Using temporal logic or a similar abstract mathematical representation, one creates a description of the problem in terms of sets (the members might be understood as computing nodes, processes, variables, the network itself -- the designer gets to decide), operations upon them, and statements about them. In this way we can model a distributed collection of computers, exchanges of messages between processes running upon them, and even crashes.
Next, one specifies a desired behavior, such as uniform agreement (the abstract problem underlying consensus protocols such as Paxos, including the versions we built into Derecho). In some sense this step describes a "goal", but not the method for achieving the goal. Think of the specification as a set of constraints, assumptions, invariants: properties that characterize a correct solution. Ideally, the behavior would have a safety component ("the solution only does good things, in the following sense...") and a liveness component ("provided that the following assumptions hold, the solution always terminates"). But some protocols aren't always live, and sometimes the conditions under which they are live are difficult to pin down, so this second aspect isn't necessarily feasible.
At any rate, in the penultimate step, one specifies the desired protocol itself, but still in a logic formalism. This is done by expressing the behavior of the protocol as a sequence of operations in the underlying framework -- for example, as a set of temporal logic "actions" on the underlying sets, carefully limited so that any "distributed" operation is performed using our abstracted versions of primitives that make sense in real networks. For example, the standard Paxos protocol, with its leader-based rounds used to construct ballots and contend for slots in the Paxos log, would be transformed into a series of set operations that match the behavior of the leader, the local copies of the logs at each of the acceptor processes, and so forth. The lowest level operations would be formal versions of message send and receive primitives.
With this in hand, the next step is to use a theorem prover like NuPRL (Constable's system) or Ivy (the one used at Tel Aviv University) to prove that the abstractly-specified protocol implements the abstractly-formalized behavioral specification. For example, in the case of Paxos, such a proof would show that for any feasible mix of roles (leader, acceptor, etc), and for every reachable protocol state, the correctness invariants hold. We would also want to show that from any initial state, some decision states are always reachable, but of course this is not always possible. For one thing, the FLP impossibility prevents us from creating a protocol in which a decision is guaranteed to occur within finite time, but in fact there are similar cases in which progress can't occur, namely situations that might involve a crash of a majority of the machines, or a partitioning of the network. For example, if you were to launch a consensus algorithm in a setting where more than half the nodes have crashed, clearly it wouldn't be able to reach consensus. As mentioned above, in the ideal case you actually specify assumptions under which progress can occur ("we assume that at least a majority of the processes are operational and remain operational throughout the execution of the protocol"), but it isn't always as easy as you might expect to specify those assumptions. So sometimes, this aspect is not addressed.
These NuPRL or Ivy (or TLA+, Dafny, Coq, Larch...) proofs are semi-manual. There is a proof-checking step, typically done using a technique called model checking (basically, the system enumerates reachable states and verifies that the invariants hold for all such states). Then there are higher level theorems that can offer short-cuts: general proof cases that were previously proved and checked that essentially represent forms of meta-reasoning, covering a class of behaviors. These allow the checker to avoid repeatedly model-checking basic steps and to instead model-check the pattern, and then look for instances of that pattern. Finally, when the checker stalls, a human can intervene and help it find the proof (or perhaps modify the protocol or the target environment specification, to make it easier to establish the desired property).
The meta-proofs (the higher level ones) are very interesting and necessary, because they potentially address cases that cannot be model-checked by exhaustively enumerating every reachable state. For example, suppose that some protocol can generate unbounded runs of states, but a proof exists that every reachable state satisfies a given property. With that "meta" proof in hand, we don't need to examine every reachable state in order to know that the property always holds, and this might let us make a true statement about the protocol that references the meta-property. In contrast, had we tried to examine every reachable state, the checker would have failed, since the runs are unbounded, hence the number of states needing to be checked is unbounded.
In practice, the power of a tool like Ivy or NuPRL centers on this kind of meta-reasoning, and the sophistication of the tactics used to match proof requirements to the library of meta-proofs. Someday, these tactics may approach the sophistication of a human logician, and in fact NuPRL has already been used to semi-automatically solve some deep open problems in logic! But there are many cases it would not yet be able to tackle.
When checkers fail, they sometimes can exhibit a counterexample: perhaps, a run in which two processes enter "decision" states but hold different outcome values, violating consensus. But they can also simply fail to find a proof. This is because a powerful enough specification language can encode undecidable questions, hence one simply cannot automate the entire proof task: there are guaranteed to be some problems on which a prover can neither conclude that a statement is true, nor false. Moreover, for any finite amount of resources (space, computer time) there are problems that would take much more space, or much more time, to model check. So for several reasons, the checker might stall. If it succeeds, though, the result is that we have a proof for our abstract protocol specification: we can show that it solves the problem, as specified.
An interesting point, tangential to what I really want to say here, is that one could perhaps extract minimum conditions for progress (a form of weakest precondition), in the manner common in PL correctness proofs of a few decades ago. This would automate extraction of assumptions needed to prove "conditional liveness": if the precondition holds, then progress will occur. To me that would be amazing, and would automate a step that Chandra and Toueg first proposed for consensus nearly 20 years ago (the famous <>W oracle). If you love theory and languages, do consider tackling this challenge!
But staying "on message", the last step with a prover such as Ivy or NuPRL is to extract a provably correct program in C or O'CaML from the proof itself. That is, given a specification of the problem, and a specification of the protocol, and a proof that the given protocol solves the problem, these tools let you push a button and automatically extract the corresponding code in an executable form, after which you simply compile and run it! Ideally, the compiler used should be proved correct (there is a proved compiler for a subset of C), and the operating system itself be proved correct (like SEL4), and the hardware verified too (using tools like Verilog) and the foundry that made the chips... well, one goes as far as one can. In fact any chain of technologies has its limitations. But let's not fuss over the obvious.
Professor Kuhn works with people developing safety critical systems for self-driving cars, control of potentially dangerous equipment, and so forth, and for her, this new methodology was fascinating. In fact she isn't the first person I've talked to about this: Chris Hobbs, at QNX, and his colleague Peter Shook, are also extremely interested in the potential of such tools. By taking the programmer out of the loop and extracting code directly from a proof. we seemingly eliminate a weakness in many kinds of control systems, where one historically would hire a team to design a solution, but then would depend on people to write the required code, after which you use a method such as the "B method" to try an prove the code correct. The resulting human-generated proofs are only as good as the human team carrying them out, and the worry always exists that they might have failed to check some important case. With a computer-generated proof, there are computable "checking" methods that can quickly establish whether or not every case was model-checked.
And yet even with automated extraction, issues remain. Can every solvable problem be tackled in this way? Over coffee, Professor Kuhn and I talked about two concerns.
First, there are solvable problems for which a model-checker might run low on space or time and throw up its hands, and hence that could be solved in principle, but in fact might not be amenable to formal treatment even so. So one can imagine situations in which there is some important task, like controlling the flaps on an airplane wing, a good solution that our engineering colleagues want to implement, and a hand-built proof of correctness that "seems" adequate, but for which there isn't any feasible fully-machine checked counterpart, because our computers might not be powerful enough, or perhaps because our techniques for generating model-checked proofs might not have the needed meta-proof methods at hand.
A related issue was raised by Hobbs and Shook at QNX: If a proof (and for that matter, the corresponding C program) is not "natural" in appearance, a human skeptic might not be easily convinced that it is correct. Thus there are also model-checked proofs that might be rejected by a team tasked with confirming that the airplane is safe to fly: the computer says "yes, here is the proof" but the skeptic in the team might worry that if no human can read and fully understand that proof, it could be flawed in some systematic way and yet this would be overlooked.
That concern leads directly to the second question Professor Kuhn and I found intriguing. Our conversation ended on a related form of impasse: suppose that the original problem specification itself is somehow inadequate? For example, one could imagine a specification for behavior of flaps on an airplane wing that leaves out some important case that can actually arise, and hence fails to pin down the correct behavior in that case. Such a specification leaves undefined the correct behavior for some actual situations that might arise in the real world, although perhaps it covers "most" cases and hence might seem complete and useful: you could still generate code, look at examples, trace the logic, and see that for those examples the code behaves properly. The lurking danger would be that because there were unspecified but real cases, examples could also exist in which the behavior would be different than intended, because the specification neglected to cover them.
Thus we would want to be sure that the specification itself was adequate in the sense of fully specifying every case that could really arise in practice. This, though, seems to be a somewhat less fully solved problem. Indeed, it seems to pose an impossible requirement!
I've been shown some work that looks at specifications, and the question is a classic one: large communities are hard at work on the topic, and have been for decades. The issue is that the "adequacy of a specification" problem itself seems to be undecideable. The intuition is sort of obvious: if one could decide all possible adequacy situations, what would stop me from encoding some simple undecideable problem (such as the halting problem), and then using the test of adequacy to solve the undecideable problem? Seemingly, nothing stops me from doing this. Thus adequacy-testing should itself be undecideable. I bet someone has proved this, although I don't think I've ever seen such a paper. I need to read more of the PL literature.
At any rate, what we see here is that on the one hand, our field seems to be at the edge of a major advance (automated synthesis of provably correct solutions to safety-critical systems problems), but on the other hand, is also approaching a natural and final form of impossibility: the risk that for important cases, it may turn out to be impossible to verify that the specification itself is "complete".
There is reason for hope. There are many situations in which if one is given a program and must answer a question about it, the task cannot be solved because the given program might encode an undecideable task. Yet when we use computational methods to generate programs, we can often prove that our methods only generate sound programs.
Could we solve the adequacy problem in this manner? For example, is there a way to generate specifications through some kind of dialog with the developer, that would only generate adequate specifications with full coverage of the problem domain? This, I think, should be possible. The resulting solution might not be able to specify every problem you can dream up, but for the things it could specify, we would know that the specification doesn't overlook any possible scenarios.
Perhaps the practical class of critical control systems doesn't actually require the ability to specify control tasks that encode undecideable questions. If so, then perhaps every needed critical control solution can be created. This would finesse the issue: even though there may be ways to encode undecideability into the same formalism, our more limited use of the methodology would never attempt to do the impossible.
My hope is that we are rapidly heading towards this kind of happy outcome... with all the progress on proofs using NuPRL an Ivy (and other systems like TLA+, Dafny, Larch and Coq), we'll know pretty soon.
Subscribe to:
Posts (Atom)