3.1 Modeling Concurrency

3.1 Modeling Concurrency

In the previous chapter, we modeled a process abstractly as a state machine that proceeds by executing atomic actions, which transform its state. The execution of a process generates a sequence (trace) of atomic actions. We now examine how to model systems consisting of multiple processes.

The first issue to consider is how to model the speed at which one process executes relative to another. The relative speed at which a process proceeds depends on factors such as the number of processors and the scheduling strategy – how the operating system chooses the next process to execute. In fact, since we want to design concurrent programs which work correctly independently of the number of processors and the scheduling strategy, we choose not to model relative speed but state simply that processes execute at arbitrary relative speeds. This means that a process can take an arbitrarily long time to proceed from one action to the next. We abstract away from execution time. This has the disadvantage that we can say nothing about the real-time properties of programs but has the advantage that we can verify other properties independently of the particular configuration of the computer and its operating system. This independence is clearly important for the portability of concurrent programs.

The next issue is how to model concurrency or parallelism. Is it necessary to model the situation in which actions from different processes can be executed simultaneously by different processors in addition to the situation in which concurrency is simulated by interleaved execution? We choose always to model concurrency using interleaving. An action a is concurrent with another action b if a model permits the actions to occur in either the order a → b or the order b → a. Since we do not represent time in the model, the fact that the event a actually occurs at the same time as event b does not affect the properties we can assert about concurrent executions.

Finally, having decided on an interleaved model of concurrent execution, what can we say about the relative order of actions from different processes in the interleaved action trace representing the concurrent program execution? We know that the actions from the same process are executed in order. However, since processes proceed at arbitrary relative speeds, actions from different processes are arbitrarily interleaved. Arbitrary interleaving turns out to be a good model of concurrent execution since it abstracts the way processors switch between processes as a result of external interrupts. The timing of interrupts relative to process execution cannot in general be predetermined since actions in the real world cannot be predicted exactly – we cannot foretell the future.

The concurrent execution model in which processes perform actions in an arbitrary order at arbitrary relative speeds is referred to as an asynchronous model of execution. It contrasts with the synchronous model in which processes perform actions in simultaneous execution steps, sometimes referred to as lock-step.

3.1.1 Parallel Composition

If P and Q are processes then (P||Q) represents the concurrent execution of P and Q. The operator || is the parallel composition operator.

Parallel composition yields a process, which is represented as a state machine in the same way as any other process. The state machine representing the composition generates all possible interleavings of the traces of its constituent processes. For example, the process:

 ITCH = (scratch->STOP).

has a single trace consisting of the action scratch. The process:

 CONVERSE = (think->talk->STOP).

has the single trace think→talk. The composite process:

 ||CONVERSE_ITCH = (ITCH || CONVERSE).

has the following traces:

 think→talk→scratch think→scratch→talk scratch→think→talk

The state machines corresponding to ITCH, CONVERSE and CONVERSE_ITCH are depicted in Figure 3.2. The state machine representing the composition is formed by the Cartesian product of its constituents. For example, if ITCH is in state(i) and CONVERSE is in state(j), then this combined state is represented by CONVERSE_ITCH in state(<i, j>). So if CONVERSE has performed the think action and is in state(1) and ITCH performs its scratch action and is in state(1) then the state representing this in the composition is state(<1,1>). This is depicted as state(4) of the composition. We do not manually compute the composite state machines in the rest of the book, since this would be tedious and error-prone. Compositions are computed by the LTSA tool and the interested reader may use it to verify that the compositions depicted in the text are in fact correct.

Figure 3.2: Composition CONVERSE_ITCH.

From Figure 3.2, it can be seen that the action scratch is concurrent with both think and talk as the model permits these actions to occur in any order while retaining the constraint that think must happen before talk. In other words, one must think before talking but one can scratch at any point!

Composite process definitions are always preceded by || to distinguish them from primitive process definitions. As described in the previous chapter, primitive processes are defined using action prefix and choice while composite processes are defined using only parallel composition. Maintaining this strict distinction between primitive and composite processes is required to ensure that the models described by FSP are finite.

As a further example, the following processes model a clock radio which incorporates two independent activities: a clock which ticks and a radio which can be switched on and off. The state machine for the composition is depicted in Figure 3.3.

Figure 3.3: Composition CLOCK_RADIO.

 CLOCK = (tick->CLOCK). RADIO = (on->off->RADIO). ||CLOCK_RADIO = (CLOCK || RADIO).

Examples of traces generated by the state machine of Figure 3.3 are given below. The LTSA Animator can be used to generate such traces.

 on→tick→tick→off→tick→tick→tick→on→off→... tick→on→off→on→off→on→off→tick→on→tick→...

The parallel composition operator obeys some simple algebraic laws:

 Commutative: (P||Q) = (Q||P) Associative: (P||(Q||R)) = ((P||Q)||R) = (P||Q||R).

Taken together these mean that the brackets can be dispensed with and the order that processes appear in the composition is irrelevant.

3.1.2 Shared Actions

The examples in the previous section are all compositions of processes with disjoint alphabets. That is, the processes in a composition do not have any actions in common. If processes in a composition do have actions in common, these actions are said to be shared. Shared actions are the way that process interaction is modeled. While unshared actions may be arbitrarily interleaved, a shared action must be executed at the same time by all the processes that participate in that shared action. The following example is a composition of processes that share the action meet.

 BILL = (play -> meet -> STOP). BEN  = (work -> meet -> STOP). ||BILL_BEN = (BILL || BEN).

The possible execution traces of the composition are:

 play→work→meet work→play→meet

The unshared actions, play and work, are concurrent and thus may be executed in any order. However, both of these actions are constrained to happen before the shared action meet. The shared action synchronizes the execution of the processes BILL and BEN. The state machine for the composite process is depicted in Figure 3.4.

Figure 3.4: Composition BILL_BEN.

The next example consists of a process that manufactures an item and then signals that the item is ready for use by a shared ready action. A user can only use the item after the ready action occurs.

 MAKER = (make->ready->MAKER). USER  = (ready->use->USER). ||MAKER_USER = (MAKER || USER).

From Figure 3.5, it can be seen that the following are possible execution traces:

 make→ready→use→make→ready→... make→ready→make→use→ready→...

Figure 3.5: Composition MAKER_USER.

After the initial item is manufactured and becomes ready, manufacture and use can proceed in parallel since the actions make and use can occur in any order. However, it is always the case that an item is made before it is used since the first action is make in all traces. The second trace shows that two items can be made before the first is used. Suppose that this is undesirable behavior and we do not wish the MAKER process to get ahead in this way. The solution is to modify the model so that the user indicates that the item is used. This used action is shared with the MAKER who now cannot proceed to manufacture another item until the first is used. This second version is shown below and in Figure 3.6.

 MAKERv2 = (make->ready->used->MAKERv2). USERv2  = (ready->use->used->USERv2). ||MAKER_USERv2 = (MAKERv2 || USERv2).

Figure 3.6: Composition MAKER_USERv2.

The interaction between MAKER and USER in this second version is an example of a handshake, an action which is acknowledged by another. As we see in the chapters to follow, handshake protocols are widely used to structure interactions between processes. Note that our model of interaction does not distinguish which process instigates a shared action even though it is natural to think of the MAKER process instigating the ready action and the USER process instigating the used action. However, as noted previously, an output action instigated by a process does not usually form part of a choice while an input action may.

The examples of synchronization so far are between two processes; however, many processes can engage in a shared action. The next example illustrates the use of multi-party synchronization in a small manufacturing system which produces two different parts and assembles the parts into a product. Assembly cannot take place until both parts are ready. Again, makers are not permitted to get ahead of users. The state machine is depicted in Figure 3.7.

 MAKE_A   = (makeA->ready->used->MAKE_A). MAKE_B   = (makeB->ready->used->MAKE_B). ASSEMBLE = (ready->assemble->used->ASSEMBLE). ||FACTORY = (MAKE_A || MAKE_B || ASSEMBLE).

Figure 3.7: Composition FACTORY.

Since a parallel composition of processes is itself a process, called a composite process, it can be used in the definition of further compositions. We can restructure the previous example by creating a composite process from MAKE_A and MAKE_B as follows:

 MAKE_A = (makeA->ready->used->MAKE_A). MAKE_B = (makeB->ready->used->MAKE_B). ||MAKERS = (MAKE_A || MAKE_B).

The rest of the factory description now becomes:

 ASSEMBLE = (ready->assemble->used->ASSEMBLE). ||FACTORY = (MAKERS || ASSEMBLE).

The state machine remains that depicted in Figure 3.7. Substituting the definition for MAKERS in FACTORY and applying the commutative and associative laws for parallel composition stated in the last section results in the original definition for FACTORY in terms of primitive processes. The LTSA tool can also be used to confirm that the same state machine results from the two descriptions.

3.1.3 Process Labeling

Given the definition of a process, we often want to use more than one copy of that process in a program or system model. For example, given the definition for a switch:

 SWITCH = (on->off->SWITCH).

we may wish to describe a system that is the composition of two distinct switches. However, if we describe this system as (SWITCH||SWITCH), the composition is indistinguishable from a single switch since the two switch processes synchronize on their shared actions on and off. We must ensure that the actions of each SWITCH process are not shared, i.e. they must have disjoint labels. To do this we use the process labeling construct.

a:P prefixes each action label in the alphabet of P with the label “a”.

A system with two switches can now be defined as:

 ||TWO_SWITCH = (a:SWITCH || b:SWITCH).

The state machine representation for the processes a:SWITCH and b:SWITCH is given in Figure 3.8. It is clear that the alphabets of the two processes are disjoint, i.e. {a.on, a.off} and {b.on, b.off}.

Figure 3.8: Process labeling in TWO_SWITCH.

Using a parameterized composite process, SWITCHES, we can describe an array of switches in FSP as follows:

 ||SWITCHES(N=3) =(forall[i:1..N] s[i]:SWITCH).

An equivalent but shorter definition is:

 ||SWITCHES(N=3) =(s[i:1..N]:SWITCH).

Processes may also be labeled by a set of prefix labels. The general form of this prefixing is as follows:

{a₁,..,a_x}::P replaces every action label n in the alphabet of P with the labels a₁.n,...,a_x.n. Further, every transition (n->Q) in the definition of P is replaced with the transitions ({a₁.n,...,a_x.n}->Q).

We explain the use of this facility in the following example. The control of a resource is modeled by the following process:

 RESOURCE = (acquire->release->RESOURCE).

and users of the resource are modeled by the process:

 USER = (acquire->use->release->USER).

We wish to model a system consisting of two users that share the resource such that only one user at a time may be using it (called “mutual exclusion”). The two users may be modeled using process labeling as a:USER and b:USER. This means that there are two distinct actions (a.acquire and b.acquire) to obtain the resource and similarly two actions to free it (a.release and b.release). Consequently, RESOURCE must be labeled with the set {a,b} to yield these transitions. The composition is described below.

 ||RESOURCE_SHARE =       (a:USER || b:USER || {a,b}::RESOURCE).

The state machine representations of the processes in the RESOURCE_SHARE model are depicted in Figure 3.9. The effect of process labeling on RESOURCE can be clearly seen. The composite process graph shows that the desired result of allowing only one user to use the resource at a time has been achieved.

Figure 3.9: Process labeling in RESOURCE_SHARE.

A perceptive reader might notice that our model of the RESOURCE alone would permit one user to acquire the resource and the other to release it! For example, it would permit the following trace:

 a.acquire →b.release →...

However, each of the USER processes cannot release the resource until it has succeeded in performing an acquire action. Hence, when the RESOURCE is composed with the USER processes, this composition ensures that only the same user that acquired the resource can release it. This is shown in the composite process RESOURCE_SHARE in Figure 3.9. This can also be confirmed using the LTSA Animator to run through the possible traces.

3.1.4 Relabeling

Relabeling functions are applied to processes to change the names of action labels. The general form of the relabeling function is:

 /{newlabel_1/oldlabel_1,...newlabel_n/oldlabel_n}. 

Relabeling is usually done to ensure that composite processes synchronize on the desired actions. A relabeling function can be applied to both primitive and composite processes. However, it is generally used more often in composition.

A server process that provides some service and a client process that invokes the service are described below:

 CLIENT = (call->wait->continue->CLIENT). SERVER = (request->service->reply->SERVER).

As described, the CLIENT and SERVER have disjoint alphabets and do not interact in any way. However, using relabeling, we can associate the call action of the CLIENT with the request action of the SERVER and similarly the reply and wait actions. The composition is defined below.

 ||CLIENT_SERVER = (CLIENT || SERVER)                   /{call/request, reply/wait}.

The effect of applying the relabeling function can be seen in the state machine representations of Figure 3.10. The label call replaces request in the description of SERVER and reply replaces wait in the description of CLIENT.

Figure 3.10: Relabeling in CLIENT_SERVER.

An alternative formulation of the client – server system is described below using qualified or prefixed labels.

 SERVERv2 = (accept.request            ->service->accept.reply->SERVERv2). CLIENTv2 = (call.request            ->call.reply->continue->CLIENTv2). ||CLIENT_SERVERv2 = (CLIENTv2 || SERVERv2)                     /{call/accept}.

The relabeling function /{call/accept} replaces any label prefixed by accept with the same label prefixed by call. Thus accept.request becomes call.request and accept.reply becomes call.reply in the composite process CLIENT_SERVERv2. This relabeling by prefix is useful when a process has more than one interface. Each interface consists of a set of actions and can be related by having a common prefix. If required for composition, interfaces can be relabeled using this prefix as in the client – server example.

3.1.5 Hiding

When applied to a process P, the hiding operator {a₁..a_x} removes the action names a₁..a_x from the alphabet of P and makes these concealed actions “silent”. These silent actions are labeled tau. Silent actions in different processes are not shared.

The hidden actions become unobservable in that they cannot be shared with another process and so cannot affect the execution of another process. Hiding is essential in reducing the complexity of large systems for analysis purposes since, as we see later, it is possible to minimize the size of state machines to remove tauactions. Hiding can be applied to both primitive and composite processes but is generally used in defining composite processes. Sometimes it is more convenient to state the set of action labels which are visible and hide all other labels.

When applied to a process P, the interface operator @{a₁..a_x} hides all actions in the alphabet of P not labeled in the set a₁..a_x.

The following definitions lead to the state machine depicted in Figure 3.11:

 USER = (acquire->use->release->USER)        \{use}. USER = (acquire->use->release->USER)        @{acquire,release}.

Figure 3.11: Hiding applied to USER.

Minimization of USER removes the hidden tau action to produce a state machine with equivalent observable behavior, but fewer states and transitions (Figure 3.12). LTSA can be used to confirm this.

Figure 3.12: Minimized LTS for USER.

3.1.6 Structure Diagrams

We have used state machine diagrams to depict the dynamic behavior of processes. State machine diagrams represent the dynamic process operators, action prefix and choice. However, these diagrams do not capture the static structure of a model. While the result of applying parallel composition can be described as a state machine (since it is a process), the parallel composition expression itself is not represented. Parallel composition, relabeling and hiding are static operators that describe the structure of a model in terms of primitive processes and their interactions. Composition expressions can be represented graphically as shown in Figure 3.13.

Figure 3.13: Structure diagram conventions.

A process is represented as a box with visible actions shown as circles on the perimeter. A shared action is depicted as a line connecting two action circles, with relabeling if necessary. A line joining two actions with the same name indicates only a shared action since relabeling is not required. A composite process is the box enclosing a set of process boxes. The alphabet of the composite is again indicated by action circles on the perimeter. Lines joining these circles to internal action circles show how the composite’s actions are defined by primitive processes. These lines may also indicate relabeling functions if the composite name for an action differs from the internal name. Those actions that appear internally, but are not joined to a composite action circle, are hidden. This is the case for action a inside S in Figure 3.13. The processes inside a composite may, of course, themselves be composite and have structure diagram descriptions.

We sometimes use a line in a structure diagram to represent a set of shared actions that have a common prefix label. The line is labeled with the prefix rather than explicitly by the actions. The example in Figure 3.14 uses the single-slot buffer of section 2.1.3 to construct a buffer that can store two values. A definition of the single-slot buffer is given below.

 range T = 0..3 BUFF = (in[i:T]->out[i]->BUFF).

Figure 3.14: Two-slot buffer TWOBUF.

Each of the labels in the diagram of Figure 3.14 – in, out and a.out –represents the set of labels in[i:T], out[i:T] and a.out[i:T], respectively.

Sometimes we omit the label on a connection line where it does not matter how relabeling is done since the label does not appear in the alphabet (interface) of the composite. For example, in Figure 3.14, it would not matter if we omitted the label a.out and used b.in/a.out instead of a.out/b.in as shown. We also omit labels where all the labels are the same, i.e. no relabeling function is required.

Lastly, we use a diagrammatic convention to depict the common situation of resource sharing as described in section 3.1.3. The resource-sharing model is repeated in Figure 3.15 together with its structure diagram representation. The resource is not anonymous as before; it is named printer. Sharing is indicated by enclosing a process in a rounded rectangle. Processes, which share the enclosed process, are connected to it by thick lines. The lines in Figure 3.15 could be labeled a.printer and b.printer; however these labels are omitted as a relabeling function is not required.

Figure 3.15: Resource-sharing PRINTER_SHARE.