“Concurrent Buns” – A chef’s guide to concurrency verification

Sequential recipes

Consider the recipe for making breakfast that is presented in Figure 1, below. An arrow from one step to another indicates that the first step must be completed before the second may commence. The recipe, as presented, fails to convey the fact that many of the steps can be swapped around. For instance, the bowl of cereal can be prepared at any convenient time during the proceedings, provided it is done before the milk is poured. Similarly, it doesn’t matter whether we put oil in the pan first, or turn on the stove.

A sequential recipe for breakfast

Figure 1: A sequential recipe for breakfast

This presentation is fine for those occasions when there is only one chef preparing breakfast. After all, they can only do one thing at a time, so while they might enjoy the freedom to shift instructions around, doing so is not actually going to make them any quicker.

The situation in which this presentation really does become inadequate is when our chef has a friend to help him. The chef ought to be able to delegate some work to his friend (perhaps the preparation of the cereal) and in doing so, speed up the entire process. However, our recipe does not allow the steps to overlap in this way. While it doesn’t insist that the same person performs all of the tasks, it does require each step to commence only once the previous one has completed. So even with twenty people to help him, our chef can’t prepare breakfast any faster (assuming he sticks rigidly to this recipe).

Concurrent recipes

Consider, then, the alternative presentation given in Figure 2, below. Here we make explicit which steps can be done concurrently. For instance, the recipe insists that by the time we pour the eggs into the pan, we have put oil in the pan, put the pan on the stove, turned on the stove and prepared the eggs, but it doesn’t mention the order in which those activities can be performed, there being no arrow between those steps in the recipe. Similarly, the cereal preparation can be seen to be largely independent of the egg-scrambling process; this is, of course, as it should be. Only occasionally must the recipe enforce ordering; for instance, the eggs must be cracked before they can be whisked. We can think of our sequential recipe of Figure 1 as a special case of this concurrent recipe.

A concurrent recipe for breakfast
Figure 2: A concurrent recipe for breakfast

This recipe is highly suitable for a team of chefs. In fact, up to five chefs may be usefully employed, because at the start of the recipe, the work is split five ways. One chef is tasked with putting oil in the pan, another with putting the pan on the stove (this might make the first chef’s job slightly harder!) and yet another with lighting the stove. The fourth chef gets busy with the eggs, and the fifth takes care of the cereal. By the time the eggs are being scrambled, only two chefs will be busy (one doing the scrambling, the other still sorting out the cereal), but when it’s time to serve the eggs, a third can leap into action once more, to turn off the stove while the eggs are being served and seasoned.

Verification

One downside of writing concurrent recipes is that it’s harder to see that the recipe is correct, because the recipe is so much more complicated. The recipe allows the stove to be turned off before the eggs are served, or afterwards. Is that ok? Probably. If our cereal chef is particularly enthuastic, it’s conceivable that she will have finished the cereal preparation before the other chefs have got their aprons on. Conversely, the recipe also allows the cereal preparation to be left right until the end, or, indeed, anywhere in between. Do all of these interpretations of the recipe lead to the intended result? Ought we to consider all the possible ways in which the recipe can be executed, in order to be sure that the recipe won’t lead to food poisoning or a burnt kitchen?

We could do so in this small example. But consider a somewhat larger recipe that can employ n chefs and gives each a sequence of k tasks to do. It can be shown that there are roughly n^{nk} different ways of carrying out the recipe. If you consider that the number of ways of doing a recipe that assigns ten chefs a sequence of ten tasks each is comparable to the number of atoms in the observable universe, you’ll see that it is utterly untractable to verify the recipe in such a simplistic way.

Computers

Finally, let us shift focus to computers for a moment. The recipe is our metaphor for a computer program, while a chef is a processor in a computer. Old computers would contain only one processor, hence programs written in the style of Figure 1 were fine, but nowadays having two or more processors in a computer is commonplace. Accordingly, more and more programs are being written in the style of Figure 2, in order to take advantage of having multiple processors.

It is silly to talk of recipes that comprise a hundred tasks and employ ten chefs. But it’s not silly when we talk of computer programs: they are routinely measured not in hundreds of lines of code, but tens of thousands. Furthermore, it’s a bit silly to contemplate verifying that a recipe won’t burn down a kitchen, because no sensible chef would allow that to happen. Nevertheless, computers have no idea how to be sensible, for they are mindless, idiotic machines that would gladly set themselves on fire if told to do so. Accordingly, we need to make computer programs absolutely idiot-proof. Finally, it is rather silly to talk of verifying recipes in the first place, because it’s not the end of the world if your breakfast gets burnt. Some computer programs, on the other hand, have far greater responsibilities that include keeping aeroplanes in the air, and radioactive chemicals from nuclear power stations out of the air. While it’s a bit daft to spend hours checking that your breakfast will always be edible, it’s of paramount importance that these kinds of computer programs are free from bugs.

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out /  Change )

Google photo

You are commenting using your Google account. Log Out /  Change )

Twitter picture

You are commenting using your Twitter account. Log Out /  Change )

Facebook photo

You are commenting using your Facebook account. Log Out /  Change )

Connecting to %s