3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 65
Текст из файла (страница 65)
From the more recent version of CSP from Hoare [1985] we use twoconcepts here: communication channels instead of process names and outputguards in the alternatives of repetitive commands. Hoare’s CSP is also thekernel of the programming language OCCAM (see INMOS [1984]) used fordistributed transputer systems.In Section 11.2 we define the semantics of distributed programs by formalizing the effect of a synchronous communication.
In particular, synchronouscommunication may lead to deadlock, a situation where some processes of adistributed program wait indefinitely for further communication with otherprocesses.Distributed programs can be transformed in a direct way into nondeterministic programs, without the use of control variables. This transformationis studied in detail in Section 11.3. It is the key for a simple proof theoryfor distributed programs which is presented in Section 11.4. As in Chapter 9,we proceed in three steps and consider first partial correctness, then weaktotal correctness which ignores deadlocks, and finally total correctness. As acase study we prove in Section 11.5 the correctness of a data transmissionproblem.11.1 Syntax37511.1 SyntaxDistributed programs consist of a parallel composition of sequential processes.So we introduce first the notion of a process.Sequential ProcessesA (sequential ) process is a statement of the formS ≡ S0 ; do ⊓⊔mj=1 gj → Sj od,where m ≥ 0 and S0 , .
. ., Sm are nondeterministic programs as defined inChapter 10. S0 is the initialization part of S anddo ⊓⊔mj=1 gj → Sj odis the main loop of S. Note that there may be further do loops inside S. Byconvention, when m = 0 we identify the main loop with the statement skip.Then S consists only of the nondeterministic program S0 . Thus any nondeterministic program is a process. Also, when the initialization part equalsskip, we drop the subprogram S0 from a process.The g1 , . . ., gm are generalized guards of the formg ≡ B; αwhere B is a Boolean expression and α an input/output command or i/ocommand for short, to be explained in a moment.
If B ≡ true, we abbreviatetrue; α ≡ α.The main loop terminates when all Boolean expressions within its generalizedguards evaluate to false.Input/output commands refer to communication channels or channels forshort. Intuitively, such channels represent connections between the processesalong which values can be transmitted.
For simplicity we assume the following:• channels are undirected; that is, they can be used to transmit values inboth directions;• channels are untyped; that is, they can be used to transmit values of different types.An input command is of the form c?u and an output command is of theform c!t where c is a communication channel, u is a simple or subscriptedvariable and t is an expression.37611 Distributed ProgramsAn input command c?u expresses the request to receive a value along thechannel c. Upon reception this value is assigned to the variable u.
An outputcommand c!t expresses the request to send the value of the expression t alongchannel c. Each of these requests is delayed until the other request is present.Then both requests are performed together or synchronously. In particular,an output command cannot be executed independently. The joint executionof two i/o commands c?u and c!t is called a communication of the value of talong channel c to the variable u.While values of different types can be communicated along the same channel, each individual communication requires two i/o commands of a matchingtype.
This is made precise in the following definition.Definition 11.1. We say that two i/o commands match when they refer tothe same channel, say c, one of them is an input command, say c?u, and theother an output command, say c!t, such that the types of u and t agree. Wesay that two generalized guards match if their i/o commands match.⊓⊔Two generalized guards contained in two different processes can be passedjointly when they match and their Boolean parts evaluate to true. Thenthe communication between the i/o commands takes place. The effect of acommunication between two matching i/o commands α1 ≡ c?u and α2 ≡ c!tis the assignment u := t.
Formally, for two such commands we defineEff (α1 , α2 ) ≡ Eff (α2 , α1 ) ≡ u := t.For a process S let change(S) denote the set of all simple or array variablesthat appear in S on the left-hand side of an assignment or in an input command, let var(S) denote the set of all simple or array variables appearing inS, and finally let channel(S) denote the set of channel names that appear inS. Processes S1 and S2 are called disjoint if the following condition holds:change(S1 ) ∩ var(S2 ) = var(S1 ) ∩ change(S2 ) = ∅.We say that a channel c connects two processes Si and Sj ifc ∈ channel(Si ) ∩ channel(Sj ).Distributed ProgramsNow, distributed programs are generated by the following clause for parallelcomposition:S ::= [S1 k.
. .kSn ],where for n ≥ 1 and sequential processes S1 , . . ., Sn the following two conditions are satisfied:11.1 Syntax377(i) Disjointness: the processes S1 , . . ., Sn are pairwise disjoint.(ii) Point-to-Point Connection: for all i, j, k such that 1 ≤ i < j < k ≤ nchannel(Si ) ∩ channel(Sj ) ∩ channel(Sk ) = ∅holds.Condition (ii) states that in a distributed program each communication channel connects at most two processes. Note that as in previous chapters wedisallow nested parallelism.A distributed program [S1 k. . .kSn ] terminates when all of its processes Siterminate. This means that distributed programs may fail to terminate because of divergence of a process or an abortion arising in one of the processes.However, they may also fail to terminate because of a deadlock.
A deadlockarises here when not all processes have terminated, none of them has endedin a failure and yet none of them can proceed. This will happen when allnonterminated processes are in front of their main loops but no pair of theirgeneralized guards matches.We now illustrate the notions introduced in this section by two examples.To this end, we assume a new basic type character which stands for symbols from the ASCII character set. We consider sequences of such charactersrepresented as finite sections of arrays of type integer → character.Example 11.1. We now wish to write a programSR ≡ [SENDERkRECEIVER],where the process SENDER sends to the process RECEIVER a sequence ofM (M ≥ 1) characters along a channel link.
We assume that initially thissequence is stored in the section a[0 : M − 1] of an array a of type integer→ character in the process SENDER. Upon termination of SR we wantthis sequence to be stored in the section b[0 : M − 1] of an array b of typeinteger → character in the process RECEIVER, see Figure 11.1.The sequential processes of SR can be defined as follows:SENDER ≡ i := 0; do i 6= M ; link!a[i] → i := i + 1 od,RECEIVER ≡ j := 0; do j 6= M ; link?b[j] → j := j + 1 od.The processes first execute independently of each other their initializationparts i := 0 and j := 0. Then the first communication along the channel link occurs with the effect of b[0] := a[0]. Subsequently both processesindependently increment their local variables i and j. Then the next communication along the channel link occurs with the effect of b[1] := a[1].
Thischaracter-by-character transmission from a into b proceeds until the processes SENDER and RECEIVER have both executed their main loops Mtimes. Then i = j = M holds and SR terminates with the result that the37811 Distributed ProgramsFig. 11.1 Sending characters along a channel.character sequence in a[0 : M − 1] has been completely transmitted intob[0 : M − 1]. Note that in the program SR the sequence of communicationsbetween SENDER and RECEIVER is uniquely determined.⊓⊔Example 11.2. We now wish to transmit and process a sequence of characters.
To this end, we consider a distributed programTRANS ≡ [SENDERkFILTERkRECEIVER].The intention now is that the process FILTER pass all the characters fromSENDER to RECEIVER with the exception that it delete from the sequenceall blank characters, see Figure 11.2.As before, the sequence of characters is initially stored in the sectiona[0 : M − 1] of an array a of type integer → character in the processSENDER. The process FILTER has an array b of the same type serving asan intermediate store for processing the character sequence and the processRECEIVER has an array c of the same type to store the result of the filteringprocess.
For coordinating its activities the process FILTER uses two integervariables in and out pointing to elements in the array b.The processes of TRANS are defined as follows:SENDER ≡i := 0; do i 6= M ; input!a[i] → i := i + 1 od,FILTER ≡in := 0; out := 0; x := ‘ ’;do x 6= ‘∗’; input?x →if x = ‘ ’ → skip⊓⊔ x 6= ‘ ’ → b[in] := x;in := in + 1fi⊓⊔ out 6= in; output!b[out] → out := out + 1od,11.1 Syntax379Fig.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
