6.826—Principles of Computer Systems 2000 Handout 17. Formal Concurrency 1 17. Formal Concurrency In this handout we take a more formal view of concurrency than in handout 14 on practical concurrency. Our goal is to be able to prove that a general concurrent program implements a spec. We begin with a fairly precise account of the non-atomic semantics of Spec, though our treatment is less formal than the one for atomic semantics in handout 9. Next we explain the general method for making large atomic actions out of small ones (easy concurrency) and prove its correctness. We continue with a number of examples of concurrency, both easy and hard: mutexes, condition variables, read-write locks, buffers, and non-atomic clocks. Finally, we give fairly careful proofs of correctness for some of the examples. Non-atomic semantics of Spec We have already seen that a Spec module is a way of defining an automaton, or state machine, with transitions corresponding to the invocations of external atomic procedures. This view is sufficient if we only have functions and atomic procedures, but when we consider concurrency we need to extend it to include internal transitions. To properly model crashes, we introduced the idea of atomic commands that may not be interrupted. We did this informally, however, and since a crash “kills” any active procedure, we did not have to describe the possible behaviors when two or more procedures are invoked and running concurrently. This section describes the concurrent semantics of Spec. The most general way to describe a concurrent system is as a collection of independent atomic actions that share a collection of variables. If the actions are A1, ..., An then the entire system is just the ‘or’ of all these actions: A1 [] ... [] An. In general only some of the actions will be enabled, but for each transition the system non-deterministically chooses an action to execute from all the enabled actions. Usually, however, we find it convenient to carry over into the concurrent world as much of the framework of sequential computing as possible. To this end, we model the computation as a set of threads (also called ‘tasks’ or ‘processes’), each of which executes a sequence of atomic actions; we denote threads by variables h, h', etc. To define its sequence, each thread has a state variable called its ‘program counter’ $pc, and each of its actions has the form (h.$pc = a) => c, so that c can only execute when h’s program counter equals a. Different actions have different values for a, so that at most one action of a thread is enabled at a time. Each action advances the program counter with an assignment of the form h.$pc := ß, thus enabling the thread’s next action. It’s important to understand there is nothing truly fundamental about threads, that is, about organizing the state transitions into sets such that at most one action is enabled in each set. We do so because we can then carry forward much of what we know about sequential computing into the concurrent world. In fact, we want to achieve our performance goals with as little concurrency as possible, since concurrency is confusing and error-prone. 6.826—Principles of Computer Systems 2000 Handout 17. Formal Concurrency 2 We now explain how to use this view to understand the non-atomic semantics of Spec. Non-atomic commands and threads Unlike an atomic command, a non-atomic command cannot be described simply as a relation between states and outcomes, that is, an atomic transition. The simple example, given in handout 14, of a non-atomic assignment x := x + 1 executed by two threads should make this clear: the outcome can increase x by 1 or 2, depending on the interleaving of the transitions in the two threads. Rather, a non-atomic command corresponds to a sequence of atomic transitions, which may be interleaved with the sequences of other commands executing concurrently. To describe this interleaving, we use labels and program counters. We also need to distinguish the various threads of concurrent computation. Intuitively, threads represent sequential processes. Roughly speaking, each point in the program between two atomic commands is assigned a label. Each thread’s program counter $pc takes a label as its value,1 indicating where that thread is in the program, that is, what command it is going to execute next. Spec threads are created by top level THREAD declarations in a module. They make all possible concurrency explicit at the top level of each module. A thread is syntactically much like a procedure, but instead of being invoked by a client or by another procedure, it is automatically invoked in parallel initially, for every possible value of its arguments.2 When it executes a RET (or reaches the end of its body), a thread simply makes no more transitions. However, threads are often written to loop indefinitely. Spec does not have COBEGIN or FORK constructs, as many programming languages do, these are considerably more difficult to define precisely, since they are tangled up with the control structure of the program. Also, because one Spec thread starts up for every possible argument of the THREAD declaration, they tend to be more convenient for most of the specifications and code in this course. To keep the thread from doing anything until a certain point in the computation (or at all), use an initial guard for the entire body as in the Sieve example below. A thread is named by the name in the declaration and the argument values. Thus, the threads declared by THREAD Foo(bool) = ..., for example, would be named Foo(true) and Foo(false) The names of local variables are qualified by both the name of the thread that is the root of the call stack, and by the name of the procedure invoked.3 In other words, each procedure in each thread has its own set of local variables. So for example, the local variable p in the Sieve example appears in the state as Sieve(0).p, Sieve(1).p, .... If there were a PROC Foo called by Sieve with a local variable baz, the state might be defined at Sieve(0).Foo.baz, Sieve(1).Foo.baz, .... The pseudo-names $a, $x, and $pc are qualified only by the thread. 1 The variables declared by a program are not allowed to have labels as their values, hence there is no Label type. 2 This differs from the threads in Java, in Modula 3, or in many C implementations. These languages start a computation with one thread and allow it to create and destroy