Magical Thinking and the Logical Foundations of BlockChains

During the past few years, I've been exposed to an unrelenting drumbeat for BlockChains.  The level of enthusiasm for this model, and the commercial mania around it, have all the elements of a "market bubble".  Just yesterday I saw a quote from a BlockChain/CyberCoin billionaire who believes that "BlockChain will replace the Internet."  Really?  But search for that phrase and you'll actually find that this guy is saying something many people believe.  Rational or not, there is a huge community totally convinced that the future will be a giant BlockChain.

The BlockChain buzz was evident at the recent conference I attended, where one speaker told us about a Berkeley spin-off based on BlockChain: Oasis, which just landed $45M in first-round "seed" funding.  Just think about that for a moment: how can such a number be justified?  I'm a skeptic.

Oasis apparently plans to build a secure infrastructure using BlockChain as the storage solution, but entirely secure from the ground up.  Presumably this is one reason Oasis needed so much cash: most companies these days just run on a public cloud like Azure or Amazon (or any of the others).  Building from the ground up will be expensive, but would let Oasis avoid a pitfall other startups share: because its competitors depend on existing datacenters, they are exposed to whatever security flaws those cloud platforms embody.

But can one build a secure data center from the ground up?  Let's focus purely on storage, since this seems to be the essence of the Oasis plan.  Could one build a new kind of secure data center that (only) provides secure storage using BlockChain, built from the ground up?

The first step is to reject the permissionless BlockChain model, which is too weak to guarantee freedom from rollbacks even years after a transaction seemingly commits: permissionless BlockChain systems with anonymous servers are insecure by design.  We want a minimal BlockChain solution, but if you take minimal to mean "anonymous, globally replicated, permissionless", my answer is that "it can't be done: it is impossible to create a trustworthy platform with that mix of properties and technologies."

Fortunately, the permissioned model avoids this risk. Moreover, it seems reasonable to assume that if the goal is to offer a data-center BlockChain product, the data center operator can control which machines can operate the solution.  This moves us from the BitCoin style of anonymous, amorphic, fully decentralized BlockChain to a more standard model of append-only files used by customers like banks.

Next, we should perhaps reject a standard cloud that offers encrypted append-only files. This is an interesting step in the analysis because a block chain really is just a secure append-only file, no matter what anyone might tell you (secured using SHA 256 hashes or similar block hashes, with proof-of-work if the system is permissionless, and then with the signatures entangled to prevent tampering).  Any file system could play that role, if you code the needed logic to generate records formatted this way and with the required chain of attestation.  Amazon and Azure and other cloud companies already offer extremely secure storage layers, including BlockChain services. But as noted, they do depend on other elements of the respective datacenter systems.  So out with the old, and in with the new!

Now, without knowing anything about the proprietary protocols that Oasis is presumably designing,  I can't say anything about how they plan to guarantee correctness.  But I can tell you how I would do it.  I would use a form of Paxos, and because I would want extreme speed, would go with the version of durable Paxos that we implemented in Cornell's Derecho system.  If I were chief architect at Oasis, I might want to build my own software (hence not use Derecho), but I would certainly adopt the Paxos specification, and prove that my software implements it.

Of course being a Derecho zealot, I'm going to make the case that using Derecho might be the smart move, even if you might have preferred to roll your own.

First, I should note that by using Paxos, Derecho is able to leverage decades of work on  proofs of correctness -- Derecho was implemented by fusing a  proved-correct version of Paxos  integrated with a proved-correct version of the virtual synchrony membership management model and a new reliable (but not atomic) multicast layer.  Then all of the data movement steps were mapped to the available storage (SSD or 3-D XPoint) and communications technologies (RDMA or TCP) in an efficient way.  Finally, Derecho uses specialized optimizations for code paths that turn out to be performance-critical.

Next, it is worth noting that Derecho is open source, hence can benefit from community contributions over time, and also that the system is extremely fast -- the fast such system ever created.  Further, it actually achieves minimal bounds for Paxos (Derecho's protocols are "optimal" in a formal sense).  Of course one can talk about smaller constants and so forth, but given the speed of the system, there is an obvious case to be made that the constants aren't showing any sign of being unreasonably large.  So Derecho is a genuinely interesting option!  Heck, maybe my students and I should try and raise $50M or so and jump into the commercial space!  

But now we run into the first of a series of issues: the protocols and proofs we are leveraging were all created in the usual way: on paper, by hand.  The mapping didn't modify the underlying logic, yet it required to adapt them to modern networking is by hand, too, and hence also needed to be proved by hand.  The same can be said about our dozens of optimizations.

Is there really a sensible way to argue that all of these hand-written proofs be accepted as somehow being "more trustworthy" than Amazon AWS or Azure?  After all, those are companies are serious about specifications too, and further, both have invested hundreds of millions of dollars in their testing and Q/A process.  Derecho is remarkably robust, and we would point to all those proofs as part of the reason, but even so, we do find bugs in our logic.

Now, if I had the money, one option might be to harden Derecho.  Aggressive testing, deep quality assurance and better documentation would be a breeze.   Starting with such a strong prototype, we could quickly end up with a professional-quality tool.  In fact I actually hope to do this, in the next year or so, if Derecho users are able to chip in to help with the costs.

But perhaps you still wouldn't be satisfied.  And indeed, today's state of the art goes much further: the very best approach is to only run code extracted from a machine-checked proof.  In effect, we compile the proof into the running system and take the developers entirely off the development path.

This, though, turns out to be infeasible for software as elaborate as Derecho, and would be even harder for whatever Oasis really plans to build.  The issue here is that as of today, the provers can't handle the style of code that we needed to use in order to create Derecho, and any full data-center infrastructure would have 10x more such code, and perhaps far more than just 10x.

Today's best provers actually can handle automated extraction of Paxos code from correctness proofs (this has been done using NuPRL here at Cornell, or IOA and Larch in Nancy Lynch's group at MIT, or IronFleet, using Dafny at Microsoft).  The resulting solutions are very robust in the sense that the logical proof structures that result are rock solid -- for what they cover.  Unfortunately, however, the resulting code is incredibly slow compared to Derecho.  Moreover, infrastructure aspects are much harder to formalize than data replication and consistency, so in some sense, Paxos is the "easy" part of the story.  Can we specify the system, fully?  Is the specification itself bullet-proof?  Bootstrap?  Other management tasks?  These steps are much harder than many people would expect.  They may not even be possible, in some cases!

This same pattern is evident in many projects that have formalized aspects of operating systems or runtime environments.  At MIT, Nick Zeldovich famously proved a very simple file system correct a few years ago.  It ran on Linux, but there is a Linux u-kernel called SEL4 that has been proved correct, and while it doesn't cover all of Linux, SEL4 probably has enough stuff in it to support Nick's provably correct file system.

Then you could perhaps use the proved version of the C compiler to compile the thing (C++ is considered to be too complex for existing provers).  Even better would be to just build the whole thing in a language like RUST or Dafny, where proof is much more central to the coding and compilation model.  With such help, you may actually manage to create a proved solution, for parts of your full system.  

But without exception, you'll end up with slow code compared to the best possible, and will have solved just a portion of the entire datacenter infrastructure.  We are decades from having data-center scale, provably correct , ultra-performant software systems.  Perhaps we'll never get there.

Moreover, even if we did manage to overcome these barriers, we would run into further questions.

One big issue is the hardware.  Think about any hardware component in the entire data center.  The routers.  Printers. Digital telephone systems.  Storage devices.

$45M may seem like a huge amount of money, but in fact it is a tiny drop in the bucket when you consider that companies like Intel spend billions on their VLSI chip fabrication factories.  So there is simply no question that Oasis will end up using components some other company created.

The problem is that these components tend to be software-defined, and this is becoming more and more of a standard story: Almost all hardware components have general-purpose, highly capable processors within them.  An entire separate computer, with its own memory, network interfaces and code.

Indeed, if you needed one CPU and DRAM unit just to operate the hardware, why not include two on the same board, or chip?  Who would notice?  And if you do this, why not drop malicious code into the second unit?  Your printer company may not even realize that it is selling compromised devices: I've heard of network chips that had entire secondary networking infrastructures built in, operated by entire stealth operating systems.  You can monitor your network as closely as you like.  You would never notice the stealth network, and its control logic!

So you can perhaps make the higher layers provably secure, but this issue of trust in the hardware limits the degree that the resulting system could be secure.

If you run a secure solution on compromised hardware, all bets are off.  The situation is a bit better if you trust the hardware: Intel has an approach called SGX that can do a bit better, and perhaps Oasis plans to leverage it, but if so, they will face performance challenges.  Sadly, SGX is quite slow.

But suppose they pull all of this off: a ground-up datacenter solution, minimal trust in the hardware, offering a BlockChain storage layer to customers.  Now we run into a new puzzle: the issue arises of how to draw the boundary between the trusted storage solution and the customer's application.

The problem here has to do with composing a trusted application with a trusted storage layer through some form of less-trusted layer of intermediary logic, like the runtime associated with the programming language.  Modern applications are coded in standard languages like Java, Python, C++, Ruby.  They use databases from big vendors like Oracle, web servers like Apache, and so forth... and each of brings its own millions of lines of logic and its own runtime environment.  Those presumably have flaws, hence an attacker could potentially compromise the application by compromising some element of the compiler or runtime, even if other aspects of the datacenter BlockChain storage solution magically were iron-clad.

And this is why I'm a skeptic: I don't see how such a picture can be secured, not today, and probably not in my lifetime.

I actually do believe in security, but I think that in modern systems, we get much more protection from diversity and multiple layers of monitoring than we do from automated techniques like verification.  We should definitely do verification where we can -- for systems like Derecho, it offers a path that can slash bug rates and greatly improve confidence in the correctness of the system relative to the promises it can legitimately make.  But to me we oversell the power of verification and proofs if we go further and allow people to believe that we have discovered a magic way to carry this idea to the limits and "prove the whole thing", whatever that thing may be.  BlockChains don't change this reality.

The Oasis folks will presumably read this blog, and I should emphasis that it isn't a personal criticism.  I'm a huge fan of the Berkeley security team and have been amazed by their accomplishments.  Amazing work has been done.  But even so, and without being hostile in any way at all, I do think we all share a need to be frank with the public about what technology can, and cannot, accomplish.

BlockChains are being oversold as a trivial way to get perfect security -- not by Oasis, but by the popular technology press, which seems to have a very dim understanding of the concept.  The press seems to think BlockChains are somehow "more" than secure file systems.  Yet if anything, they are "less"!

Perhaps we are seeing a superposition of two elements.  Clearly, we do have a community that was unaware of the concept of a tamper-proof append-only log protected using cryptography.  All sorts of folks who work in government, health care, manufacturing clearly feel that this is a revelation, and offers an answer to all their security worries.  And quite possibly some were actually not aware that we can use file systems in secure ways -- I'm glad they know, now, and if BlockChain helps them conceive of this, I'm all for it.

Then we have hype, driven by cryptocurrency valuations in the stratosphere, a technology press endlessly eager for the next big thing, and investors keen to make a killing.  In this marketplace, I see a lot of value that companies can bring to the table, particularly ones with exciting ideas for packaging this stuff to be useful, and some of this value is very real: HyperLedger and Ethereum and related tools are genuinely powerful.

But just the same, we need to stop claiming that BlockChain is a revolutionary invention.

My worry is that by overselling the same old file systems to a naïve community of infrastructure owners, we may end up with systems that are actually less secure than what they replace.  After all, a platform like Azure is actually remarkably secure today, managed professionally by a company obsessed with security (and nobody is paying me to say this, by the way!), and has such a diversity of technologies deployed that compromising it in a major way would be quite hard.  If some hospital were to abandon that and jump to BlockChain as its file system, the illusion of security may have replaced much stronger real security.  True, today's reality has its limits, but in fact  I would be far more comfortable seeing medical records hosted on Azure or AWS, than abandoning these professional solutions in favor of a storage product that uses BlockChain as a magic wand to solve all problems.

But clearly, the current climate (especially the technology press) is prone to magical thinking, and a bit weak on just what BlockChains are, and how they work, and what their logical foundations turn out to be.  And in light of that, I suppose that the amazingly high first round of Oasis investment makes a kind of sense.  A bubble?  Definitely.  And yet all valuations are measures of market sentiment.  So perhaps not an unreasonable bubble, given the modern business climate and the craze that BlockChain has engendered.

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?

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.

Moving AI to the edge

In today's data centers, a dominant paradigm shapes machine learning and AI systems: massive amounts of data are collected, cleaned, and stored into some form of database or collection of files.  Then machine learning tools are used to train a model on the observed data, and finally the resulting model is used for a while in the edge application.  All of this takes time, so the edge applications operate using stale data, at least to some degree.

In online AI/Ml systems, like smart highways controlling smart cars, smart homes, or the smart power grid, a pervasive need for instant responsiveness based on the most current data is a distinguishing characteristic: today's standard cloud systems can definitely react to new events extremely rapidly (100ms or less is the usual goal), but because the edge runs on cached data -- in this situation, cached models -- and these platforms can't update their models promptly, they will continue to use a stale model long after something fundamental has changed, invalidating it. 

So why would we care about stale models?  The term model, as used by the ML community, refers to any concise representation of knowledge.  For example, on a highway, knowledge of a particular truck's behavior (its apparent route, history of speeds and lane changes, perhaps any observations of risks such as a tire that could be shredding, or a piece of cargo that might not be properly tied down) are all part of the model.  In a continuous learning setting, the model shapes behavior for all the smart cars in the vicinity.  In a smart power grid, the model is our estimate of the state of the grid; if the grid starts to show an oscillatory imbalance or signs of a shortage of power, the model can evolve in milliseconds, and the grid control algorithms need to adjust accordingly.  Yesterday's model, or even the one from ten seconds ago, might not be acceptable.

What will it take to move AI to the edge?

• The AI/ML community will need to figure out what aspects of their problems really need to run on the edge, and are incorrectly situated on the standard backend today.  Coding at the edge won't be the same as coding for the backend, so work will be required.  This suggests that many applications will need to be split into online and offline aspects, with the online parts kept as slim as possible.  The offline components will be easier to implement because they run in a more standard way.
• We need programming tools and platforms for edge-oriented AI/ML tools.  I'm betting that Derecho can be the basis of such a solution, but I also think it will take a while to reach that point.  We'll need to understand what edge-hosted AI/ML tools will actually look like: how will they represent, store, and access machine-learned models?  How big are these models, and what data rates arise?  Where are the low-latency paths, and how low does  latency need to be?
• We may need to integrate hardware accelerators into the infrastructure: if a system does vision, it probably wants to use GPU accelerators for image segmentation, tagging and for operations such as rotation, alignment, debluring, 3-D scene reconstruction, etc.  FPGA components offer a second rapid model, more focused on searching HTML text or other "byte stream" objects.  FPGA accelerators are also useful for doing quick cryptographic operations.  There could easily be other kinds of ASICs too: DFFT units, quantum thinkers, you name it. 
• All of these pieces need to synchronize properly and be easy to program in a "correct" way...

I'm fascinated by this whole area.  If it interests you too,  send me a note:  perhaps we can find ways to team up!

Will smart memory be the next big thing?

We're fast approaching a new era of online machine learning and online machine-learned behavior: platforms that will capture real-time data streams at high data rates, process the information instantly, and then act on the output of the processing stage.  A good example would be a smart highway that tells cars what to expect up around the next curve, or a real-time television feed integrated with social networking tools (like a world-cup soccer broadcast that lets the viewers control camera angles while their friends join from a remote location).

If you ask how such systems will need to be structured, part of the story is familiar: as cloud-hosted services capturing data from sensors of various kinds (I'm including video cameras here), crunching on it, then initiating actions. 

A great example of such a service is Microsoft's Cosmos data farm.  This isn't a research platform but there have been talks on it at various forums.  The company organized a large number of storage and compute nodes (hundreds of thousands) into a data warehouse that absorbs incoming objects,  then replicates them onto a few SSD storage units (generally three replicas per object, with the replication pattern fairly randomized to smooth loads, but in such a way that the replicas are on fault-independent machines: ones that live in different parts of the warehouse and are therefore unlikely to crash simultaneously).

Once the data is securely stored, Cosmos computes on it: it might compress or resize an image or video, or it could deduplicate, or run an image segmentation program.  This yields intermediary results, which it also replicates, stores, and then might further process: perhaps, given the segmented image, it could run a face recognition program to automatically tag people in a photo.  Eventually, the useful data is served back to the front-end for actions (like the smart highway that tells cars what to do).  Cold but valuable data is stored to a massive backend storage system, like Microsoft's Pelican shingled storage server.  Unneeded intermediary data is deleted to make room for new inputs.

Thus Cosmos has a lot in common with Spark, the famous data processing platform, except on a much larger scale, and with an emphasis on a pipeline of transformations rather than on MapReduce.

If we step way back, we can start to perceive Cosmos as an example of a smart memory system: it remembers things, and also can think about them (process them), and could potentially query them too, although as far as I know Cosmos and Spark have limited interactive database query functionality.  But you could easily imagine a massive storage system of this kind with an SQL front-end, and with some form of internal schema, dynamically managed secondary index structures, etc.

With such a capability, a program could interrogate the memory even as new data is received and stored into it.  With Cornell's Derecho system, the data capture and storage steps can be an asynchronous pipeline that would still guarantee consistency.  Then, because Derecho stores data into version vectors, queries can run asynchronously too, by accessing specific versions or data at specific times.  It seems to me that the temporal style of indexing is particularly powerful.

The interesting mix here is massive parallelism, and massive amounts of storage, with strong consistency... and it is especially interesting that in Derecho, the data is all moved asynchronously using RDMA transfers.  Nobody has to wait for anything, and queries can be done in parallel.

Tomorrow's machine learning systems will surely need this kind of smart memory, so for those of us working in systems, I would say that smart memory architectures jump out as a very exciting next topic to explore.  How should such a system be organized, and what compute model should it support? As you've gathered, I think Cosmos is already pretty much on the right track (and that Derecho can support this, even better than Cosmos does).  How can we query it? (Again, my comment about SQL wasn't haphazard: I would bet that we want this thing to look like a database).  How efficiently can it use the next general of memory hardware: 3-D XPoint, phase-change storage, high-density RAID-style SSD, RDMA and GenZ communication fabrics?

Check my web page in a few years: I'll let you know what we come up with at Cornell...

On systematic errors in complex computer programs

Society as a whole, including many computing professionals, seems to assume that mistakes made by unsupervised deep learning and other forms of machine-learning will be like Heisenbugs: rare, random, and controllable through a more professional code development and testing process. This belief underlies a growing tendency to trust computing systems that embody unknown (indeed, unknowable) machine-learned behaviors.

Why is this a concern?  

In many parts of computer science, there is a belief in "ultimate correctness": a perception that if we merely formalize our goals and our algorithms and successfully carry out a proof that our code accomplishes the goals, then we will have created a correct artifact.  If the goals covered a set of safety objectives, then the artifact should be safe to use, up to the quality of our specification.  Highly professional development practices and extensive testing strengthen our confidence; model-checking or other forms of machine-checked proofs that run on the real software carry this confidence to the point at which little more can be said, if you trust the specification.

Yet we also know how unrealistic such a perspective can be.  Typical computing systems depend upon tens or hundreds of millions of lines of complex code, spread over multiple modules, perhaps including firmware programs downloaded into the hardware.  All of this might then be deployed onto the cloud, and hence dependent on the Internet, and on the cloud data-center's thousands of computers. The normal behavior of such programs resides somewhere in the cross-product of the individual states of the component elements: an impossibly large space of possible configurations. 

While we can certainly debug systems through thorough testing, software is never even close to flawless: by some estimates, a bug might lurk in every few tens or hundreds of lines of logic.  The compiler and the operating system and various helper programs are probably buggy too.  Testing helps us gain confidence that these latent bugs are rarely exercised under production conditions, not that the code is genuinely correct.

Beyond what is testable we enter the realm of Heisen-behaviors: irreproducible oddities that can be impossible to explain: perhaps caused by unexpected scheduling effects, or by cosmic rays that flip bits, or by tiny hardware glitches.  The hardware itself is often better modelled as being probabilistic than deterministic: 1 + 1 certainly should equal 2, but perhaps sometimes the answer comes out as 0, or as 3.  Obviously, frequent problems of that sort would make a machine sufficiently unreliable that we would probably repair or replace it.  But an event happening perhaps once a week?  Such problems often pass unnoticed.

Thus, ultimate correctness is elusive; we know this, and we've accommodated to the limitations of computing systems by doing our best to fully specify systems, holding semi-adversarial code reviews aimed at finding design bugs, employing clean-room development practices, then red-team testing, then acceptance testing, then integration testing.  The process works surprisingly well, although patches and other upgrades commonly introduce new problems, and adapting a stable existing system to operate on new hardware or in a new setting can reveal surprising unnoticed issues that were concealed or even compensated for by the prior pattern of use, or by mechanisms that evolved specifically for that purpose.

The puzzle with deep learning and other forms of unsupervised or semi-supervised training is that we create systems that lack a true specification.  Instead, they have a self-defined behavioral goal: reinforcement learning trains a system to respond to situations resembling ones it has seen before by repeating whatever response dominated in the training data.  In effect: "when the traffic light turns yellow, drive very fast."

Thus we have a kind of autonomously-learned specification, and because the specification is extracted automatically by training against a data set, the learned model is inherently shaped by the content of the data set.

Train such a system on a language sample in which plurals always end in "s", and it won't realize that "cattle" and "calamari" are plural.  Train it on images in which all the terrorists have dark hair and complexions, and the system will learn that anyone with dark hair or skin is a potential threat.  Teach it to drive in California, where every intersection either has stop signs on one or both streets, or has a traffic signal, and it won't understand how to drive in Europe, where many regions use a "priority to the right" model, whereby incoming traffic (even from a small street) has priority over any traffic from the left (even if from a major road). 

Machine learning systems trained in this way conflate correlation with causation.  In contrast, human learning teases out causal explanations from examples.  The resulting knowledge is different from a knowledge model learned by training today's machine learning technologies, no matter how impressive the machine learning system's ability to do pattern matching.

Human knowledge also understands time, and understands that behavior must evolve over time.  Stephen Gould often wrote about being diagnosed as a young adult with a fatal circulatory cancer.  Medical statistics of the period gave him a life expectancy of no more than a few months, perhaps a year at best.  But as it happened, a new medication proved to be a true magic bullet: he was cured.   The large-population statistics were based on prior treatments and hence not predictive of the outcomes for those who received this new treatment.  The story resonated in Gould's case because in his academic life, he studied "punctuated equilibria", which are situations in which a population that has been relatively static suddenly evolves in dramatic ways: often, because of some significant change in the environment.  Which is precisely he point.

Those who fail to learn from the past are doomed to repeat it.  But those who fail to appreciate that the past may not predict the future are also doomed.  Genuine wisdom comes not from raw knowledge, but also from the ability to reason about novel situations in robust ways.

Machine learning  systems tend to learn a single set of models at a time.  They squeeze everything into a limited collection of models, which blurs information if the system lacks a needed category: "drives on the left", or "uses social networking apps".  Humans create models, revise models, and are constantly on the lookout for exceptions.  "Is  that really a  pile of  leaves, or has the cheetah realized it can hide in a pile of leaves?  It never did that before.  Clever cheetah!"   Such insights once were of life-or-death importance.

Today, a new element enters the mix: systematic error in which a system is programmed to learn a pattern, but overgeneralizes and consequently behaves incorrectly every time a situation arises that exercises the erroneous generalization.  Systematic error is counterintuitive, and perhaps this explains our seeming inability to recognize the risk: viewing artificially intelligent systems as mirrors of ourselves, we are blind to the idea that actually, they can exhibit bizarre and very non-random misbehavior.  Indeed, it is in the nature of this form of machine learning to misbehave in unintuitive  ways!

My concern is this: while we've learned to create robust solutions from somewhat unreliable components, little of what we know about reliability extends to this new world of machine-learning components that can embody systematic error, model inadequacies, or an inability to adapt and learn as conditions evolve.  This exposes us to a wide range of new failure modalities never before seen, and that could challenge the industry and the computer science community to overcome.  We lack systematic ways to recognize and respond to these new kinds of systematic flaws.

Systematic error also creates new and worrying attack surfaces that hackers and others might exploit.  Knowing how a machine learning system is trained, a terrorist might circulate some photoshopped images of him or herself with very pale makeup and light brown or blond hair, to bind other biometrics that are harder to change (like fingerprints, corneal patterns) with interpretations suggesting "not a threat".  Knowing how a self-driving car makes decisions, a hacker might trick it into driving into a pylon.

Welcome to the new world of complex systems with inadequate artificial intelligences.  The public places far too much confidence in these systems, and our research community has been far too complacent.  We need to open our eyes to the risks, and to teach the public about them, too.  

C++ just grew up, and wow, what a change!

When I was first learning to program (longer ago than I should admit, but this would have been around 1975), I remember what a revelation it was to start working in C, after first teaching myself languages like Basic, PL/I, SNOBOL and Fortran.  Back then, those were the choices.

When you code in C, you can literally visualize the machine instructions that the compiler will generate.  In fact most C programmers learn to favor loops like these:

     while(--n) { ... do something ... }

or even

    do { ... something ... } while(--n);

because when you code in this style, you know that the compiler will take advantage of the zero/non-zero condition code left in the processor register after doing the --n decrement, and hence will generate one fewer instruction than with a for-loop, where you generally end up with an increment/decrement followed by a separate test.

I fell in love with C.  What an amazing shift of perspective: a language that actually lets you control everything!

Ok, admittedly, only a computer science nut could care.  But as it happens, this little example gets to the core of something important about computer systems: we tend to want our systems to be as functional as possible, but also to want them to be as minimal as possible and as fast as possible.  That tension is at the core of the best systems research: you want a maximally expressive component in which every non-essential element is removed, so that the remaining logic can be executed blindingly rapidly (or with amazing levels of concurrency, or perhaps there are other goals).  This sense of minimalism, though, is almost akin to an artistic aesthetic.  Code in C was beautiful in a way that code in PL/I never, ever, was able to match.

Our programming languages have somewhat lost that purity.  When I first learned Python and Java and then C#, their raw power impressed me enormously.  Yet there is also something a little wrong, a little fast-and-loose, about these technologies: they are insanely expensive.  First, they encourage enormous numbers of very small method calls, which entail pushing return addresses and arguments to the stack, doing maybe two instructions worth of work, and then popping the environment.  Next, because of automated memory management, object creation is cheap and easy, yet costly, and there are unpredictable background delays when garbage collection runs.  Even if you code in a style that preallocates all the objects you plan to use, these costs arise anyhow, because the runtime libraries make extensive use of them.  Finally, the very powerful constructs they offer tend to make a lot of use of runtime introspection features: polymorphism, dynamic type checking, and dynamic request dispatch.  All are quite expensive.

But if you are a patient person, sometimes you get to relive the past.  Along came C++ 11, which has gradually morphed to C++ 14, with C++ 17 around the corner.  These changes to C++ are not trivial, but they are a revelation: for the first time, I feel like I'm back in 1975 programming in C and thinking hard about how many instructions I'm asking the compiler to generate for me. 

I'll start by explaining what makes the new C++ so great, but then I'll complain a little about how very hard it has become to learn and to use.

• A normal program spends a remarkable amount of time pushing stuff onto the stack and popping it back off.  This includes arguments passed by value or even by reference (in Java and C# a reference is like a pointer), return addresses, registers that might be overwritten, etc.  Then the local frame needs to be allocated and initialized, and then your code can run.  So, remember that cool C program that looked so efficient back in 1975?  In fact it was spending a LOT of time copying!  You can ask: how much of that copying was really needed?
  
  In C++  these costs potentially vanish.  There is a new notation for creating an alias: if a method foo() has an argument declared this way: foo(int& x), then the argument x will be captured as an alias to the integer passed in.  So the compiler doesn't need to push the value of x, and it won't even need to push a pointer: it literally accesses the caller's x, which in turn could also be an alias, etc. 
  
  With a bit of effort, foo itself will expand inline, and if foo is recursive but uses some form of constant expression to decide the recursion depth or pattern, the compiler can often simulate the recursive execution and generate just the data-touching code from the unwound method.
• With polymorphic method calls in Java and C#, a runtime dispatch occurs when the system needs to figure out the actual dynamic types of the variables used in a method invocation and match that to a particular entry point.  In C++, you get the same behavior but the actual resolution that matches caller and callee occurs at compile time.  Thus at runtime, only data-touching code runs, which is far faster.
• Although C++ now has dynamic memory management, it comes from a library implementing what are called smart pointers, which are reference-counter objects that C++ creates and automatically manages: when such an object goes out of scope, the compiler calls the destructor method and it decrements the reference count on the object, and then automatically destroys the object itself once the count goes to 0.  This gives a remarkable degree of control over memory allocation and deallocation, once you become familiar with the required coding style.  In fact you can take full control and reach a point where no dynamic allocation or garbage collection would ever take place: you preallocate objects and keep old copies around for reuse.  The libraries, unlike the ones in Java and C#, don't create objects on their own, hence the whole thing actually works.
• C++ can do a tremendous amount of work at compile time, using what are called constant expression evaluation and variadic template expansions.  Basically, the compile-time behavior of the language is that of a full program that you get to write, and that generates the code that will really execute at runtime.  All the work of type checking occurs statically,  many computations are carried out by the compiler and don't need to be performed at runtime, and you end up with very complex .h header files, but remarkably "thin" executables

So with so much fantastic control, what's not to love?

• The syntax of C++ has become infuriatingly difficult to understand: a morass of angle braces and & operators and pragmas about constants and constant expressions that actually turn out to matter very much.
• The variadic template layer is kind of weird: it does a syntax-directed style of recursion in which there are order-based matching operations against what often looks, at a glance, like an ambiguous set of possible matching method invocations.  A misplaced comma can lead the compiler off on an infinite loop.  At best, you feel that you are coding in a bizarre fusion of Haskall or O'CaML with the old C++, which honestly doesn't make for beautiful code.
• As a teacher who enjoys teaching object oriented Java classes, I'm baffled by the basic question of how one would teach this language to a student.  For myself, it has taken two years to start to feel comfortable with the language.  I look forward to seeing a really good textbook!  But I'm not holding my breath.
• The language designers have been frustratingly obtuse in some ways.  For example, and this is just one of many, there are situations in which one might want to do compile-time enumerations over the public members of a class, or to access the actual names the programmer used for fields and methods.  For obscure religious reasons that date back to the dark ages, the standards committee has decided that these kinds of things are simply evil and must never, ever, be permitted. 
  
  Why are they needed?  Well, in Derecho we have persistent template classes and would normally want to name the files that hold the persisted data using the name of the variable the data corresponds to, which would be some sort of scoped name (the compile-time qualified path) and then the variable name.  No hope. 
  
  And one wants to iterate the fields in order to automatically serialize the class.  Nope. 
  
  And one wants to iterate over the methods because this would permit us to do fancy kinds of type checking, like to make sure the client invoking a point-to-point method isn't accidentally invoking a multicast entry point.  Sorry, guy.  Not gonna happen.
• The language designers also decided not to support annotations, like the @ notation in Java, or the C# [ something ] notation that you can attach to a class.  This is a big loss: annotations are incredibly useful in polymorphic code, and as C++ gets more and more powerful, we get closer and closer to doing compile-time polymorphic logic.  So why not give us the whole shebang?
• There isn't any way to stash information collected at compile time.  So for example, one could imagine using variadic templates to form a list of methods that have some nice property, such as being read-only or being multicast entry points.  That list would be a constexpr: generated at compile time.  But they just don't let you do this.  No obvious reason for the limitation.

I could complain at greater length, but I'll stop with the remark that even with its many limitations, and even with the practical problem that compilers have uneven support for the C++ 17 features, the language on a tear and this is clearly the one language that will someday rule them all.

In our work on Derecho, we've become C++ nuts (lead by Matt Milano, an absolutely gifted C++ evangelist and the ultimate C++ nut).  Our API is not trivial and the implementation is quite subtle.  Yet under Matt's guidance, 95% of that implementation involves compile-time logic.  The 5% left that has to be done at runtime is incredibly "thin" code, like the while(--n) { ... } loop: code that genuinely has to execute at that point in time, that actually touches data.  And because this code tends to be very efficient and very highly optimized, just a few instructions often suffice.  All of Derecho may be just instructions away from the RDMA NIC taking control and moving bytes.

Wow...  I feel like it is 1975 again (except that there is no way to fool myself into believing that I'm 20 years old.  Sigh)  But at least we can finally write efficient systems code, after decades of writing systems code in languages that felt like plush goose-down quilts: thick and soft, and nowhere near reality...

Systems engineering viewed as a science

At Cornell University, where I've done my research and taught since 1982, we've always had a reputation for being a top theory department, and because Cornell is relatively small compared to some of our peers, and because many of my colleagues are famous for rigorous systems theory, this reputation includes systems.  I wouldn't call it a bad thing: I actually like to specify protocols as carefully as possible and to tease out a correctness argument, and my work has often benefitted from rigor.

And yet I'm reminded of something Roger Needham loved to stress.  You've probably heard the story, but Roger headed the most widely known systems group in Europe for many years, at Cambridge University, and he went on to found the Microsoft Research Laboratory in Cambridge.

Roger's health finally failed, and his colleagues gathered to celebrate Roger's accomplishments.  This came near the end of his life, when the cancer he was suffering from had left him very frail.  As a result, Roger was unable to physically attend, but he did send a video, and in this video we see him in a wheelchair holding an engineer's hard hat on his lap.  He starts out by saying a few words about his career (which included a wide range of work, some very theoretical, some very practical).  And then he puts the hat on.  Roger looks directly at the camera and says that he hasn't very long now, and wants people to remember him this way: wearing a hard hat, very much the engineer. 

For Roger, computer systems research is an engineering discipline first: that our primary obligation is to really build the things we invent, and to build production quality software that people will really want to use.  Roger loved ideas, but for him, an unimplemented idea was inferior to a working one, and a working system that people use was the gold standard.  Throughout his career, Roger repeatedly acknowledged the value of rigor and used theoretical tools to achieve rigor.  But the key thing is that for him, theory in the systems arena was a tool, secondary to the actual engineering work itself.  The real value resided in the artifact: the working system.

For me this was one of the most iconic images in my entire career: Roger wearing that hat and underscoring that we are at our best when we build things of high value: useful things, beautifully designed concrete implementations.  And there is a genuine esthetic of systems creation too: a meaningful sense in which great systems are beautiful things. 

Today, I see a huge need to elevate our view of systems engineering: rather than thinking of it as mere implementation work, we need to begin to appreciate the science and beauty of great systems work.  There is an inherent value to this act of creation: building really good software, that solves some really hard problem, and having it work, and be used.  We're at our best when we create artifacts.

When I visit people at the French air traffic control agency, I'm kind of awed that the software we built for them in 1990 is still working today without a single unmanaged failure, in 27 years.  The NYSE floor trading system I developed ran the show for ten years, and there was never a single disruption to trading in all that time.  Every time you install Oracle, watch closely: in the middle of the install script Oracle sets up my old Isis toolkit system as its network management tool.  And this has worked for nearly 30 years.  Nobody phones me to ask how to fix obscure bugs.  (Of course, once Derecho is finally out there, I bet many will call to ask how to migrate to it).

We built these really difficult engineered infrastructures with incredibly demanding specifications, came up with a beautiful and elegant model (virtual synchrony, which turns out to be a variation on the Paxos state machine replication model), and it actually worked!  This is as good as it gets.

Our field continues to struggle with the tension between its mathematically-oriented theory side and its roots in systems engineering.  One sees this again and again.  Papers are brushed to the side by conferences because the contributions are primarily about sound engineering and great performance: "minor and incremental" aspects in the eyes of some PC member (who has probably never coded a large C++ program in his life)!  Funding programs somehow assume that the massive data collection infrastructures that will be needed as hosting environments for their fancy new machine learning technologies are trivial and will just build themselves.  You write a reference letter for a student, and back comes an email query: yes, ok, the student is a gifted distributed systems engineer.  But do they have a talent for theory?  And if not, where's the originality?  I've become accustomed to that sinking feeling of needing to translate my enthusiasm for systems engineering to make sense to a person who just doesn't understand the creativity and originality that the best systems research demands.

So here's my little challenge to the community: we need to start going out of our way to seek out and accept papers on the best systems, and to deliberately validate and celebrate the systems engineering side of the field as we do so.  Over time, we need to recreate a culture of artifacts: by deliberate choice, we need to tilt the field back towards valuing systems to a greater degree.  Roger was right: we're at our best when we wear those hard hats. 

A few concrete suggestions:

• Let's start to write papers that innovate by revealing clever ways to build amazing things.
• Those of us in a position to do so should press program committees to set aside entire sessions to highlight real systems: practical accomplishments that highlight the underlying science of systems engineering. 
• We should be giving awards to the best academic systems research work.  Somehow, over time, prizes like the ACM software systems prize started going purely to massive projects done by big teams in industry (which is fine, if ACM wants to orient the prize that way).  But we also need prizes to recognize the best systems built in academic and research settings.  

Why do these things?  Because we're at our best when we create working code, and when we teach others to appreciate the elegance of the code itself: the science behind the engineering.  Systems building is what we do, and we should embrace that underlying truth.