On a Method of Multiprogramming

In this monograph we investigate sets of sequential programs that are executed concurrently. Therefore we shall start with an elaboration of the two key elements in this description of our subject, viz. “execution of a sequential program” and “concurrent execution (of programs)”.

Since in this monograph we will be studying the design of concurrently executed sequential programs, we need a notation for sequential programs in the first place. At this point we have made a very traditional choice by adopting Dijkstra’s Guarded Command Language, which was first defined in [Dij76]. Its distinguishing features are notational and mathematical austerity, and the incorporation of nondeterminacy in sequential programs. In our study of multiprogramming, nondeterminacy will hardly play a rôle, but mathematical austerity will do so all the more. We will briefly describe this program notation, which we expect to offer no problem to anyone familiar with ALGOL60, Pascal, or even C. We will discuss its semantics in more detail, anticipating in our discussion that in later chapters sequential programs will be considered in cooperation with other ones rather than in isolation.

In the previous chapter, the notion of an assertion in a sequential program has been introduced, and we have seen how sequential programs can be annotated with assertions in such a way that the annotation precisely reflects our proof obligations. We have also seen how this effectively protects us against operational reasoning, and how it aids in coming to firm grips with sequential programs. All these virtues become even more important now that we are on the verge of taking multiprograms into account, i.e. entire sets of cooperating sequential programs to be executed simultaneously.

At the end of the previous chapter, we charged the reader with an impossible task, viz. to prove, with the Core rules of the Owicki/Gries theory, that the little multiprogram Pre: x = 0A: x = x + 1B: x = x + 1 establishes postcondition x = 2. This impossibility, which we shall prove in a moment, is really disturbing, first, because from an operational point of view it is absolutely obvious that the final state satisfies x = 2, and, second, because it makes us wonder how many other surprises there are in store for us. (To reassure the reader, things will turn out reasonably well.)

Let us consider a multiprogram with N components, each containing M atomic statements and, hence, M assertions, and let us count how much work is involved in proving the correctness of the annotation of such a multiprogram. First of all, there are M × N assertions in the game. Secondly, for each individual assertion we have to check its local correctness — counting for 1 — and its global correctness — counting for M × (N-1). As a result, the total amount of proof obligations to be fulfilled equals % MathType!MTEF!2!1!+-% feaaguart1ev2aaatCvAUfeBSjuyZL2yd9gzLbvyNv2CaerbuLwBLn% hiov2DGi1BTfMBaeXatLxBI9gBaerbd9wDYLwzYbItLDharqqtubsr% 4rNCHbGeaGqiVu0Je9sqqrpepC0xbbL8F4rqqrFfpeea0xe9Lq-Jc9% vqaqpepm0xbba9pwe9Q8fs0-yqaqpepae9pg0FirpepeKkFr0xfr-x% fr-xb9adbaqaaeGaciGaaiaabeqaamaabaabaaGcbaGaamytaiaays% W7cqGHxdaTcaaMe8UaamOtaiabgEna0kaaysW7caGGOaGaaGymaiab% gUcaRiaad2eacaaMe8Uaey41aqRaaGjbVlaacIcacaWGobGaeyOeI0% IaaGymaiaacMcacaGGPaaaaa!4D39! $$M\; \times \;N \times \;(1 + M\; \times \;(N - 1)) $$ which is quadratic in the size — i.e. the number of atomic statements — of the multiprogram. Even for a modestly sized program with M = 7 and N = 5, the workload already consists of % MathType!MTEF!2!1!+-% feaaguart1ev2aaatCvAUfeBSjuyZL2yd9gzLbvyNv2CaerbuLwBLn% hiov2DGi1BTfMBaeXatLxBI9gBaerbd9wDYLwzYbItLDharqqtubsr% 4rNCHbGeaGqiVu0Je9sqqrpepC0xbbL8F4rqqrFfpeea0xe9Lq-Jc9% vqaqpepm0xbba9pwe9Q8fs0-yqaqpepae9pg0FirpepeKkFr0xfr-x% fr-xb9adbaqaaeGaciGaaiaabeqaamaabaabaaGcbaGaaGymaiaac6% cacaaIWaGaaGymaiaaiwdaaaa!3993! $$1.015$$ proofs to be carried out. This is definitely far beyond what can be expected from a human being. Even an automatic proof system would quickly be defeated by such a quadratic explosion. The main cause of this explosion is the necessity to prove the global correctness of assertions.

This short chapter will, as a matter of fact, be at the heart of one of our main techniques for the formal derivation of multiprograms. This technique will consist in a stepwise strengthening of a too-weakly annotated multi-program, i.e. of a multiprogram that cannot be handled with just the Core rules of the Owicki/Gries theory. Each individual strengthening step will always be guided by the desire to turn one or more assertions into correct ones, i.e. correct ones according to the Core. When, after a series of such strengthenings, the entire annotation has become correct in the Core — if ever! —, the design process has come to an end, because then — by the postulate of Weakening the Annotation — the original annotation is correct as well. In this chapter we shall focus on how to strengthen the annotation so as to make a single assertion correct (in the Core).

Now that most of the groundwork has been done, the time has come to show the formalism at work. We shall give a number of rather unrelated examples, some of which are relevant enough to acquire the status of theorems. We start with the theorems, which happen to be the simpler exercises, and we conclude with slightly more sophisticated examples, which enable us to pay attention to the design of a-posteriori proofs, an activity that is quite similar to our ultimate goal: the design of multiprograms.

Most multiprograms are designed with the aim of having the components cooperate on a common task. The common task may vary from a large-scale computation divided over the various components to an orderly scheduling of the access of components to scarce common resources. Almost all applications will require information exchange — communication — between components, and almost always will the need arise for tuning the relative speeds — i.e. for synchronization — of the components. Indeed, a component that is about to perform an addition, might have to be delayed until the addends have arrived, and a component that is about to need a printer, might have to “wait” if no printer is free.

In the early decades of computing, when the speed of electronic circuitry had outgrown that of mechanical peripheral devices by some orders of magnitude, the demand for “parallelism” became louder and louder, because it was becoming more and more urgent for economic reasons. And, indeed, the excessively expensive circuitry of the time could, instead of being idle while waiting for the input of a slow card reader, much more beneficially be deployed for serving other customers of the computer installation. The idea of several programs running “simultaneously” on a single installation had been born.

In the foregoing chapters we have seen a number of examples of how to use the technique of Strengthening the Annotation to show that a given, too-weakly annotated multiprogram is correct. There we strengthened the original annotation in a number of steps, until it became correct in the Core. Here, in this chapter, we will do exactly the same, be it not for a completed program, but for a program still to be completed. That is, along with a stronger annotation, new, additional code will see the light as well, and that is what we call program development. We have to admit, though, that in this first exercise not too much additional code will be developed, on the one hand because the current example is very simple and on the other hand because, in general, a development that is carried out with caution does not introduce more than needed.

This is the last chapter of the first half of this text. In the second half we will almost exclusively be occupied with program derivation, using the vocabulary and the techniques introduced so far. There is, however, one final issue that we have hardly touched upon, viz. the problem of how to make programs more fine-grained. We already alluded to this issue when specifying the problem of Concurrent Vector Writing, but now the time has come to become a little more articulate about it.

This chapter forms a true divide in this monograph, in that the preceding part was mainly concerned with the description of multiprograms whereas the following part will deal with their construction. What we did so far was introduce and discuss a body of concepts, techniques, and rules of thumb that together form the basic ingredients for our method of multiprogramming. Since these ingredients are rather scattered over the various chapters, it seems appropriate that, on this divide of the book, we give a brief and rough summary of them. And this, indeed, is the primary purpose of these “Yellow Pages”.

As a matter of fact, this chapter is not really about the Safe Sluice. It has more of a methodological flavour, mainly because it tells the story of how a method can emerge from a careful study of a judiciously chosen, simple algorithm like the Safe Sluice. For us, authors, the exploration of this algorithm created the first evidence that the Owicki/Gries theory could, somehow, effectively be put at work for the formal derivation of multi-programs [Fei87]. The original theme of that exploration was to compare the various correctness proofs that, at the time, we could give for the Safe Sluice. Here, we are happy to have the opportunity to let the reader share in this experience, and to show how seemingly tiny little details can give rise to unforeseen developments.

Ever since the emergence of Dekker’s mutual exclusion algorithm for two components and Dijkstra’s for an arbitrary number of components [Dij65], the search for new, better or different such algorithms has continued. It took the computing community about twenty years to come up with a beautiful — because genuinely simple — mutual exclusion algorithm for two components. It is the one invented by G.L. Peterson [Pet81], and we shall be glad to discuss it here, not only because of its compelling elegance but also because we think that each educated computing scientist should be familiar with all the ins and outs of this algorithm.

As mentioned before, the concept of mutual exclusion has, ever since the early days of computing, been recognized as a central issue in taming the complexity brought about by multiprograms run on a shared installation. The reason why it became a central issue is that the primitive statements provided by actual machinery often were — and are — far too finegrained to make multiprogramming practically feasible. Thus, the mutual exclusion problem, i.e. the problem of how to build (arbitrary) coarsegrained atomic statements out of finer-grained ones, did become an urgent one. In its canonical form, the problem is:

Given a number of components, each of the form

% MathType!MTEF!2!1!+-% feaaguart1ev2aaatCvAUfeBSjuyZL2yd9gzLbvyNv2CaerbuLwBLn% hiov2DGi1BTfMBaeXatLxBI9gBaerbd9wDYLwzYbItLDharqqtubsr% 4rNCHbGeaGqiVu0Je9sqqrpepC0xbbL8F4rqqrFfpeea0xe9Lq-Jc9% vqaqpepm0xbba9pwe9Q8fs0-yqaqpepae9pg0FirpepeKkFr0xfr-x% fr-xb9adbaqaaeGaciGaaiaabeqaamaabaabaaGcbaGaaiOkaiaacU% facaWGUbGaam4yaiaadohacaGG7aGaam4yaiaadohacaGGDbaaaa!3DD2!

$$*[ncs;cs] $$

synchronize them in such a way that at any moment in time, at most one component is engaged in its

cs

- fragment.

A frequently recurring theme in the area of communication is the transmission of information from one place to another while there is no buffering facility in between. Such situations, for instance, occur in electronic circuits where wires must carry signals from one end to the other. The problem also pops up when synchronous communication has to be implemented by asynchronous means. The algorithms that take care of such a “bufferless” information transmission are known as handshake protocols, and they are at the heart of the (physical) realization of communication and synchronization between otherwise autonomous computer installations. Also, they are nowadays beneficially used as a starting point for the construction of asynchronous circuitry [Mar96].

This monograph emphasizes the construction of correct (multi)programs. However, along with every program comes the question of “performance”, addressing such aspects as efficiency, demand on storage space, degree of parallelism, communication density, robustness, etc.. Although these issues definitely fall outside the scope of this text, we nevertheless wish to include a very modest touch on them.

The problem of the parallel linear search is a nice little paradigm that was first communicated to us in the mid 1980s by Ernst-Rüdiger Olderog. The problem can be used to illustrate a variety of phenomena that come with parallelism, and in this capacity it is one of the running examples in [AO91]. In [Kna92] we can find a first formal derivation of the algorithm, a derivation that is carried out in the UNITY formalism [CM88].

Almost all of our multiprograms come with an initial state, as embodied by the precondition “Pre” in our schemes. In one way or another this initial state has to be established before any component can start executing its code. So here is a synchronization problem to be dealt with.

There is a rule that says: “Avoid duplication of volatile information.”†. Disobedience of this rule may have disastrous consequences for an organization, whether it is just a computer system or a human society. Information — in the broadest sense of the word — that is widely diffused and then needs to be changed, may require a gigantic update operation, and — perhaps worse — may be unreliable or just wrong at all those places where the update operation has not been effectuated yet. (Changing all telephone numbers in the Netherlands, in the mid 1990s, was an enormous operation, which took a whole year. The transition of a lot of European currencies to the euro is an almost frightening prospect. The millennium problem, caused by an untraceable diffusion of an erroneous date field, will cost society billions and billions of dollars.)

At the end of Chapter 19 we promised to return to the initialization problem after having dealt with co-components, and in this chapter we will do so. We do not repeat the problem statement here, but resume our development at what we called “A (hopeless) stepping stone” ; this time, however, we omit the “hopeless”:

This example has been inspired by a problem from the field of real-time data processing. The rationale for that problem can be found in [Lam77, KR93]. Here we will only sketch it in brief. The problem concerns the following little two-component multiprogram

In the history of parallel computing, many synchronization primitives have been proposed, but only few have acquired a prominent position. A set of primitives that do have acquired such a position are C.A. R. Hoare’s so-called CSP-constructs [Hoa78, Hoa85]. (CSP is an acronym for “Communicating Sequential Processes”.) The constructs gracefully combine communication — i.e. information transfer — and synchronization. Below we describe them, briefly and informally.

We consider a multiprogram with a positive and finite number of components. Component i has a private boolean variable y.i and it does just one thing, namely it performs one as yet unknown assignment to this variable. The problem is to synchronize the components in such a way that they all terminate and leave the system in a final state satisfying† (0) % MathType!MTEF!2!1!+-% feaaguart1ev2aaatCvAUfeBSjuyZL2yd9gzLbvyNv2CaerbuLwBLn% hiov2DGi1BTfMBaeXatLxBI9gBaerbd9wDYLwzYbItLDharqqtubsr% 4rNCHbGeaGqiVu0Je9sqqrpepC0xbbL8F4rqqrFfpeea0xe9Lq-Jc9% vqaqpepm0xbba9pwe9Q8fs0-yqaqpepae9pg0FirpepeKkFr0xfr-x% fr-xb9adbaqaaeGaciGaaiaabeqaamaabaabaaGcbaGaaiikaiaaic% dacaGGPaGaaGzbVpaaamaabaGaai4iaiaadQgacaGG6aGaaiOoaiaa% dMhacaGGUaGaamOAaaGaayzkJiaawQYiaiabg2da9iaaigdaaaa!42D5! $$ \left\langle {\# j::y.j} \right\rangle = 1 $$

As we already pointed out earlier, the concept of mutual exclusion historically was one of the first concepts for dealing with the enormous complexity brought about by the concurrent execution of cooperating sequential programs. Along with the emergence of the concept, the quest for mutual exclusion algorithms began, and a continuous stream of such algorithms has seen the light, ever since the first general mutual exclusion algorithm was conceived [Dij65]. (For an overview, the reader may consult [Ray86].)

In Chapter 17 we addressed the problem of phase synchronization — also known as “barrier synchronization” — for the case of two components. The main purpose of that chapter was to show program derivation at work in a simple setting and to discuss various methodological issues. It should not be surprising that, as this text progresses, we become interested in more “scaled-up” problems, problems closer to everyday practice so to speak. Therefore in this chapter we will tackle, as an example, the problem of barrier synchronization for an arbitrary but fixed number of components, and show how it can be solved through an intermediary in the shape of a monitor or a bus. In the next chapter we will then develop an algorithm for barrier synchronization that is fully distributed, i.e. that is intended for an architecture where the components are located in the nodes of a — sparsely connected — network. The overall intention of these examples is to show program derivation at work in a less simple setting and on a variety of potential machine architectures. In addition, the problem of barrier synchronization all by itself has proved to be important enough, because of its applications in areas where components are to proceed in a “lock-step-like” fashion.

There is a rather wide-spread belief that the design of distributed algorithms requires methods that are quite different from those used for the design of shared-variable algorithms. This is an unfortunate misunderstanding. In previous chapters we already showed the development of a number of small distributed algorithms, and in this chapter we will try to dispel the misunderstanding more rigorously by presenting the design of a non-trivial, fully distributed algorithm for phase synchronization (an algorithm which most likely is beyond what can operationally be conceived and comprehended).

A typical architecture that one encounters is that of a number of computers located in the nodes of a sparsely connected, but otherwise arbitrary network. One of the difficulties with such an architecture is that the flow of control and the information exchange between the various computers are not always easily orchestrated, simply because the network is so arbitrary. This brings about the so-called routing problem. There are, however, at least two general ways to reduce these difficulties.

Along with the rise of large-scale distributed systems, a number of new-problems and algorithmic paradigms saw the light. One of these was the problem of so-called quiescence detection, which led to the wider class of so-called distributed snapshot algorithms. Roughly speaking, distributed snapshot algorithms have to detect, in a distributed fashion, whether a system has entered a state in which no relevant things will happen any more. What is relevant very much depends on the specifics of the problem. For instance, in a self-stabilizing system, i.e. a system that stabilizes towards some pre-specified state, one might be interested in whether that state has been reached. The so-called termination detection algorithms, which were the first algorithms of this class to attract the attention of computing scientists, are to detect whether a distributed computation proper has arrived at a final state, i.e. has terminated.

The Alternating Bit Protocol is an algorithm for the correct transmission of a data stream from one place to another via so-called “faulty channels”. Here, a faulty channel is a kind of medium that can garble, duplicate or lose data in some well-specified ways. This protocol has raised a lot of interest ever since its emergence [BSW69]. It is discussed, specified, and provided with correctness proofs abundantly in the established literature. However, in spite of this reputation, the general understanding of the algorithm is at an extremely low level: most computing scientists “know” the Alternating Bit Protocol in the sense that they have heard of it, but only a few can explain it. This is a pity for such a fundamental algorithm.

This last technical chapter is not really about Peterson’s algorithm, although it may reinforce the beauty of that design. What this chapter really is about, is a serious and fundamental criticism that one may have of the method of multiprogramming proposed in this book. The method is invariably driven by the requirement of partial correctness, thereby largely neglecting the aspect of individual progress, or “liveness”. Of course, we do have some rules of thumb that prevent us from excluding progress beforehand, the most notable one being to choose the annotation and the induced guards as weak as possible. But how good is this? Is there a mathematical underpinning? The answer is simple: there isn’t!

Now that all the work has been done, in particular by the reader who traveled this far, we may start pondering on what has been achieved and what has not, and on what we explored and on what we ignored. Let us first discuss two technical subjects that are intrinsically related to concurrency, but that we decided to leave alone. They pertain to speeding up computations and to aspects of communication.