3. Verification of sequential and concurrent programs. Apt_ Olderog (3rd edition) (2010) (811405), страница 5

Просмтор этого файла доступен только зарегистрированным пользователям. Но у нас супер быстрая регистрация: достаточно только электронной почты!

Текст из файла (страница 5)

Such programsare usually difficult to design, and errors are more a rule than an exception. Of course, we also consider sequential programs because they occur ascomponents of concurrent ones.341 Introduction1.1 An Example of a Concurrent ProgramTo illustrate the subtleties involved in the design of concurrent programsconsider the following simple problem, depicted in Figure 1.1.Problem Let f be a function from integers to integers with a zero. Write aconcurrent program ZERO that finds such a zero.Fig. 1.1 Zero search of a function f : integer → integer split into two subproblemsof finding a positive zero and a nonpositive zero.The idea is to solve the problem by splitting it into two subproblems thatcan be solved independently, namely finding a positive and a nonpositivezero.

Here z is called a positive zero of f if z > 0 and f (z) = 0, and it iscalled a nonpositive zero if z ≤ 0 and f (z) = 0. We are now looking forsequential programs S1 and S2 solving the two subproblems such that theparallel execution of S1 and S2 solves the overall problem. We write [S1 kS2 ]for a parallel composition of two sequential programs S1 and S2 . Executionof [S1 kS2 ] consists of executing the individual statements of S1 and S2 inparallel.

The program [S1 kS2 ] terminates when both S1 and S2 terminate.Solution 1Consider the following program S1 :1.1 An Example of a Concurrent Program5S1 ≡ f ound := false; x := 0;while ¬f ound dox := x + 1;f ound := f (x) = 0od.S1 terminates when a positive zero of f is found. Similarly, the followingprogram S2 terminates when a nonpositive zero of f is found:S2 ≡ f ound := false; y := 1;while ¬f ound doy := y − 1;f ound := f (y) = 0od.Thus the programZERO-1 ≡ [S1 kS2 ],the parallel composition of S1 and S2 , appears to be a solution to the problem.Note that the Boolean variable f ound can be accessed by both componentsS1 and S2 . This shared variable is used to exchange information about termination between the two components.⊓⊔Indeed, once ZERO-1 has terminated, one of the variables x or y storesa zero of f , and ZERO-1 has solved the problem.

Unfortunately, ZERO-1need not terminate as the following scenario shows. Let f have only one zero,a positive one. Consider an execution of ZERO-1, where initially only theprogram’s first component S1 is active, until it terminates when the zero off is found. At this moment the second component S2 is activated, f ound isreset to false, and since no other zeroes of f exist, f ound is never reset totrue.

In other words, this execution of ZERO-1 never terminates.Obviously our mistake consisted of initializing f ound to false twice —oncein each component. A straightforward solution would be to initialize f oundonly once, outside the parallel composition. This brings us to the followingcorrected solution.Solution 2LetS1 ≡ x := 0;while ¬f ound dox := x + 1;f ound := f (x) = 0od61 IntroductionandS2 ≡ y := 1;while ¬f ound doy := y − 1;f ound := f (y) = 0od.ThenZERO-2 ≡ f ound := false; [S1 kS2 ]should be a solution to the problem.⊓⊔But is it actually? Unfortunately we fooled the reader again. Supposeagain that f has exactly one zero, a positive one, and consider an executionof ZERO-2 where, initially, its second component S2 is activated until itenters its loop.

From that moment on only the first component S1 is executeduntil it terminates upon finding a zero. Then the second component S2 isactivated again and so f ound is reset to false. Now, since no other zeroesof f exist, f ound is never reset to true and this execution of ZERO-2 willnever terminate! Thus, the above solution is incorrect.What went wrong? A close inspection of the scenario just presented revealsthat the problem arose because f ound could be reset to false once it wasalready true. In this way, the information that a zero of f was found gotlost.One way of correcting this mistake is by ensuring that f ound is never resetto false inside the parallel composition.

For this purpose it is sufficient toreplace the unconditional assignmentf ound := f (x) = 0by the conditional one:if f (x) = 0 then f ound := true fiand similarly with the assignment f ound := f (y) = 0. Observe that thesechanges do not affect the meaning of the component programs, but they alterthe meaning of the parallel program.We thus obtain the following possible solution.Solution 3LetS1 ≡ x := 0;1.1 An Example of a Concurrent Program7while ¬f ound dox := x + 1;if f (x) = 0 then f ound := true fiodandS2 ≡ y := 1;while ¬f ound doy := y − 1;if f (y) = 0 then f ound := true fiod.ThenZERO-3 ≡ f ound := false; [S1 kS2 ]should be a solution to the problem.⊓⊔But is it really a solution? Suppose that f has only positive zeroes, andconsider an execution of ZERO-3 in which the first component S1 of the parallel program [S1 kS2 ] is never activated.

Then this execution never terminateseven though f has a zero.Admittedly, the above scenario is debatable. One might object that anexecution sequence in which one component of a parallel program is neveractivated is illegal. After all, the main reason for writing parallel programsis to have components executed in parallel. The problem here concerns thedefinition of parallel composition.

We did not exactly specify its meaning andare now confronted with two different versions.The simpler definition says that an execution of a parallel program [S1 kS2 ]is obtained by an arbitrary interleaving of the executions of its componentsS1 and S2 . This definition does not allow us to make any assumption of therelative speed of S1 and S2 . An example is the execution of the above scenariowhere only one component is active.The more demanding definition of execution of parallel programs requiresthat each component progress with a positive speed.

This requirement ismodeled by the assumption of fairness meaning that every component of aparallel program will eventually execute its next instruction. Under the assumption of fairness ZERO-3 is a correct solution to the zero search problem.In particular, the execution sequence of ZERO-3 discussed above is illegal.We now present a solution that is appropriate when the fairness hypothesisis not adopted.

It consists of building into the program ZERO-3 a schedulerwhich ensures fairness by forcing each component of the parallel program toeventually execute its next instruction. To this end, we need a new programming construct, await B then R end, allowing us to temporarily suspendthe execution of a component.

Informally, a component of a parallel programexecutes an await statement if the Boolean expression B evaluates to true.81 IntroductionStatement R is then immediately executed as an indivisible action; during itsexecution all other components of the parallel program are suspended. If Bevaluates to false, then the component executing the await statement itselfis suspended while other components can proceed. The suspended componentcan be retried later.In the following program we use an additional shared variable turn thatcan store values 1 and 2 to indicate which component is to proceed.Solution 4LetS1 ≡ x := 0;while ¬f ound doawait turn = 1 then turn := 2 end;x := x + 1;if f (x) = 0 then f ound := true fiodandS2 ≡ y := 1;while ¬f ound doawait turn = 2 then turn := 1 end;y := y − 1;if f (y) = 0 then f ound := true fiod.ThenZERO-4 ≡ turn := 1; f ound := false; [S1 kS2 ]should be a solution to the problem when the fairness hypothesis is notadopted.¤To better understand this solution, let us check that it is now impossible to execute only one component unless the other has terminated.

Indeed,with each loop iteration, turn is switched. As a consequence, no loop bodycan be executed twice in succession. Thus a component can be activateduninterruptedly for at most “one and a half” iterations. Once it reaches theawait statement the second time, it becomes suspended and progress can nowbe achieved only by activation of the other component. The other componentcan always proceed even if it happens to be in front of the await statement.In other words, execution of ZERO-4 now alternates between the components.

But parallelism is still possible. For example, the assignments to xand y can always be executed in parallel.1.1 An Example of a Concurrent Program9But is ZERO-4 really a solution to the problem? Assume again that fhas exactly one positive zero. Consider an execution sequence of ZERO-4in which the component S1 has just found this zero and is about to execute the statement f ound := true.

Instead, S2 is activated and proceedsby one and a half iterations through its loop until it reaches the statement await turn = 2 then turn := 1 end. Since turn = 1 holds from thelast iteration, S2 is now blocked. Now S1 proceeds and terminates withf ound := true. Since turn = 1 is still true, S2 cannot terminate but remains suspended forever in front of its await statement. This situation iscalled a deadlock.To avoid such a deadlock, it suffices to reset the variable turn appropriatelyat the end of each component.

This leads us to the following solution.Solution 5LetS1 ≡ x := 0;while ¬f ound doawait turn = 1 then turn := 2 end;x := x + 1;if f (x) = 0 then f ound := true fiod;turn := 2andS2 ≡ y := 1;while ¬f ound doawait turn = 2 then turn := 1 end;y := y − 1;if f (y) = 0 then f ound := true fiod;turn := 1.ThenZERO-5 ≡ turn := 1; f ound := false; [S1 kS2 ]is a deadlock-free solution to the problem when the fairness hypothesis is notadopted.⊓⊔Can you still follow the argument? We assure you that the above solutionis correct. It can, moreover, be improved. By definition, an execution of anawait statement, await B then R end, temporarily blocks all other components of the parallel program until execution of R is completed. Reducing101 Introductionthe execution time of the statement R decreases this suspension time andresults in a possible speed-up in a parallel execution.

Here such an improvement is possible —the assignments to the variable turn can be taken out ofthe scope of the await statements. Thus we claim that the following programis a better solution to the problem.Solution 6LetS1 ≡ x := 0;while ¬f ound dowait turn = 1;turn := 2;x := x + 1;if f (x) = 0 then f ound := true fiod;turn := 2andS2 ≡ y := 1;while ¬f ound dowait turn = 2;turn := 1;y := y − 1;if f (y) = 0 then f ound := true fiod;turn := 1and let as beforeZERO-6 ≡ turn := 1; f ound := false; [S1 kS2 ].Here wait B is an instruction the execution of which suspends a componentif B evaluates to false and that has no effect otherwise.⊓⊔The only difference from Solution 5 is that now component S2 can beactivated —or as one says, interfere— between wait turn = 1 and turn := 2of S1 , and analogously for component S1 .

We have to show that such aninterference does not invalidate the desired program behavior.First consider the case when S2 interferes with some statement not containing the variable turn. Then this statement can be interchanged with the1.2 Program Correctness11statement turn := 2 of S1 , thus yielding an execution of the previous program ZERO-5. Otherwise, we have to consider the two assignments turn := 1of S2 .

The first assignment turn := 1 (inside the loop) cannot be executedbecause immediately before its execution turn = 2 should hold, but by ourassumption S1 has just passed wait turn = 1. However, the second assignment turn := 1 could be executed. But then S2 terminates, so f ound is trueand S1 will also terminate —immediately after finishing the current loopiteration. Just in time —in the next loop iteration it would be blocked!To summarize, activating S2 between wait turn = 1 and turn := 2 of S1does not lead to any problems. A similar argument holds for activating S1 .Thus Solution 6 is indeed correct.1.2 Program CorrectnessThe problem of zero search seemed to be completely trivial, and yet severalerrors, sometimes subtle, crept in.

Характеристики

Список файлов книги