5. Principles of Model Checking. Baier_ Joost (2008) (811406), страница 21
Текст из файла (страница 21)
. ..(Hint: Choose an appropriate communication mechanism.)(c) Outline the transition system A1 A2 A3 C.Exercise 2.4. Show that the handshaking operator that forces two transition systems tosynchronize over their common actions (see Definition 2.26 on page 48) is associative. That is,show that(TS1 TS2 )TS3 = TS1 (TS2 TS3 )where TS1 , TS2 , TS3 are arbitrary transition systems.Exercise 2.5. The following program is a mutual exclusion protocol for two processes due toPnueli [118].
There is a single shared variable s which is either 0 or 1, and initially 1. Besides,each process has a local Boolean variable y that initially equals 0. The program text for processPi (i = 0, 1) is as follows:l0: loop forever dobeginl1: Noncritical sectionl2: (yi , s) := (1, i);l3: wait until ((y1−i = 0) ∨ (s = i));l4: Critical sectionl5: yi := 0end.Here, the statement (yi , s) := (1, i); is a multiple assignment in which variable yi := 1 and s := iis a single, atomic step.84Modelling Concurrent SystemsQuestions:(a) Define the program graph of a process in Pnueli’s algorithm.(b) Determine the transition system for each process.(c) Construct their parallel composition.(d) Check whether the algorithm ensures mutual exclusion.(e) Check whether the algorithm ensures starvation freedom.The last two questions may be answered by inspecting the transition system.Exercise 2.6.
Consider a stack of nonnegative integers with capacity n (for some fixed n).(a) Give a transition system representation of this stack. You may abstract from the values onthe stack and use the operations top, pop, and push with their usual meaning.(b) Sketch a transition system representation of the stack in which the concrete stack content isexplicitly represented.Exercise 2.7.
Consider the following generalization of Peterson’s mutual exclusion algorithmthat is aimed at an arbitrary number n (n 2) processes. The basic concept of the algorithmis that each process passes through n “levels” before acquiring access to the critical section. Theconcurrent processes share the bounded integer arrays y[0..n−1] and p[1..n] with y[i] ∈ { 1, . .
. , n }and p[i] ∈ { 0, . . . , n−1 }. y[j] = i means that process i has the lowest priority at level j, andp[i] = j expresses that process i is currently at level j. Process i starts at level 0. On requestingaccess to the critical section, the process passes through levels 1 through n−1. Process i waits atlevel j until either all other processes are at a lower level (i.e., p[k] < j for all k = i) or anotherprocess grants process i access to its critical section (i.e., y[j] = i). The behavior of process i is inpseudocode:while true do.
. . noncritical section . . .forall j = 1, . . . , n−1 dop[i] := j;y[j] := i;wait until (y[j] = i) ∨od. . . critical section . . .p[i] := 0;odQuestions:0<kn,k=ip[k] < jExercises85(a) Give the program graph for process i.(b) Determine the number of states (including the unreachable states) in the parallel compositionof n processes.(c) Prove that this algorithm ensures mutual exclusion for n processes.(d) Prove that it is impossible that all processes are waiting in the for-iteration.(e) Establish whether it is possible that a process that wants to enter the critical section waitsad infinitum.Exercise 2.8.
In channel systems, values can be transferred from one process to another process.As this is somewhat limited, we consider in this exercise an extension that allows for the transferof expressions. That is to say, the send and receive statements c!v and c?x (where x and v are ofthe same type) are generalized into c!expr and c?x, where for simplicity it is assumed that expris a correctly typed expression (of the same type as x). Legal expressions are, e.g., x ∧ (¬y ∨ z)for Boolean variables x, y, and z, and channel c with dom(c) = { 0, 1 }. For integers x, y, and aninteger-channel c, |2x + (x − y)div17| is a legal expression.Question: Extend the transition system semantics of channel systems such that expressions areallowed in send statements.(Hint: Use the function η such that for expression expr, η(expr ) is the evaluation of expr underthe variable valuation η.)Exercise 2.9.
Consider the following mutual exclusion algorithm that uses the shared variablesy1 and y2 (initially both 0).Process P1 :while true do. . . noncritical section . . .y1 := y2 + 1;wait until (y2 = 0) ∨ (y1 < y2 ). . . critical section . . .y1 := 0;odProcess P2 :while true do. . . noncritical section . . .y2 := y1 + 1;wait until (y1 = 0) ∨ (y2 < y1 ). . . critical section .
. .y2 := 0;odQuestions:(a) Give the program graph representations of both processes. (A pictorial representation suffices.)(b) Give the reachable part of the transition system of P1 P2 where y1 2 and y2 2.(c) Describe an execution that shows that the entire transition system is infinite.(d) Check whether the algorithm indeed ensures mutual exclusion.86Modelling Concurrent Systems(e) Check whether the algorithm never reaches a state in which both processes are mutuallywaiting for each other.(f) Is it possible that a process that wants to enter the critical section has to wait ad infinitum?Exercise 2.10. Consider the following mutual exclusion algorithm that was proposed 1966 [221]as a simplification of Dijkstra’s mutual exclusion algorithm in case there are just two processes:1 Boolean array b(0;1) integer k, i, j,2 comment This is the program for computer i, which may beeither 0 or 1, computer j =/= i is the other one, 1 or 0;3 C0: b(i) := false;4 C1: if k != i then begin5 C2: if not b(j) then go to C2;6else k := i; go to C1 end;7else critical section;8b(i) := true;9remainder of program;10go to C0;11endHere C0, C1, and C2 are program labels, and the word “computer” should be interpreted as process.Questions:(a) Give the program graph representations for a single process.
(A pictorial representationsuffices.)(b) Give the reachable part of the transition system of P1 P2 .(c) Check whether the algorithm indeed ensures mutual exclusion.Exercises87Exercise 2.11. Consider the following two sequential hardware circuits C1 and C2 :C1 :yANDxNOTANDORC2 :yANDNOTNOTr1ANDORANDr1r2(a) Give the transition system representation TS(C1 ) of the circuit C1 .(b) Let TS(C2 ) be the transition system of the circuit C2 .
Outline the transition system TS(C1 )⊗TS(C2 ).Exercise 2.12.Consider the following leader election algorithm: For n ∈ N, n processesP1 , . . . , Pn are located in a ring topology where each process is connected by an unidirectionalchannel to its neighbor in a clockwise manner.To distinguish the processes, each process is assigned a unique identifier id ∈ {1, . . . , n}. The aimis to elect the process with the highest identifier as the leader within the ring. Therefore eachprocess executes the following algorithm:send (id);while (true) doreceive (m);if (m = id ) then stop;if (m > id ) then send (m);odinitially set to process’ idprocess is the leaderforward identifier(a) Model the leader election protocol for n processes as a channel system.(b) Give an initial execution fragment of TS([P1 |P2 |P3 ]) such that at least one process hasexecuted the send statement within the body of the whileloop.
Assume for 0 < i 3, thatprocess Pi has identifier idi = i.Chapter 3Linear-Time PropertiesFor verification purposes, the transition system model of the system under considerationneeds to be accompanied with a specification of the property of interest that is to beverified. This chapter introduces some important, though relatively simple, classes ofproperties.
These properties are formally defined and basic model-checking algorithmsare presented to check such properties in an automated manner. This chapter focuses onlinear-time behavior and establishes relations between the different classes of propertiesand trace behavior.
Elementary forms of fairness are introduced and compared.3.1DeadlockSequential programs that are not subject to divergence (i.e., endless loops) have a terminalstate, a state without any outgoing transitions. For parallel systems, however, computations typically do not terminate—consider, for instance, the mutual exclusion programstreated so far. In such systems, terminal states are undesirable and mostly represent adesign error.
Apart from “trivial” design errors where it has been forgotten to indicatecertain activities, in most cases such terminal states indicate a deadlock. A deadlock occurs if the complete system is in a terminal state, although at least one component is in a(local) nonterminal state. The entire system has thus come to a halt, whereas at least onecomponent has the possibility to continue to operate. A typical deadlock scenario occurswhen components mutually wait for each other to progress.8990Linear-Time PropertiesTrLight 1redαβgreenTrLight 2redαTrLight 1 || TrLight 2βgreenred , red Figure 3.1: An example of a deadlock situation.Example 3.1.Deadlock for Fault Designed Traffic LightsConsider the parallel composition of two transition systemsTrLight 1 TrLight 2modeling the traffic lights of two intersecting roads.
Both traffic lights synchronize bymeans of the actions α and β that indicate the change of light (see Figure 3.1). Theapparently trivial error to let both traffic lights start with a red light results in a deadlock.While the first traffic light is waiting to be synchronized on action α, the second trafficlight is blocked, since it is waiting to be synchronized with action β.Example 3.2.Dining PhilosophersThis example, originated by Dijkstra, is one of the most prominent examples in the fieldof concurrent systems.Deadlock91Stick1P1P2Stick0Stick2P0P3Stick4P4Stick3Five philosophers are sitting at a round table with a bowl of rice in the middle. For thephilosophers (being a little unworldly) life consists of thinking and eating (and waiting,as we will see).
To take some rice out of the bowl, a philosopher needs two chopsticks.In between two neighboring philosophers, however, there is only a single chopstick. Thus,at any time only one of two neighboring philosophers can eat. Of course, the use of thechopsticks is exclusive and eating with hands is forbidden.Note that a deadlock scenario occurs when all philosophers possess a single chopstick.The problem is to design a protocol for the philosophers, such that the complete system isdeadlock-free, i.e., at least one philosopher can eat and think infinitely often. Additionally,a fair solution may be required with each philosopher being able to think and eat infinitelyoften.
The latter characteristic is called freedom of individual starvation.The following obvious design cannot ensure deadlock freedom. Assume the philosophersand the chopsticks are numbered from 0 to 4. Furthermore, assume all following calculations be “modulo 5”, e.g., chopstick i−1 for i=0 denotes chopstick 4, and so on.Philosopher i has stick i on his left and stick i−1 on his right side. The action request i,iexpress that stick i is picked up by philosopher i. Accordingly, request i−1,i denotes theaction by means of which philosopher i picks up the (i−1)th stick. The actions release i,iand release i−1,i have a corresponding meaning.The behavior of philosopher i (called process Phil i ) is specified by the transition systemdepicted in the left part of Figure 3.2. Solid arrows depict the synchronizations with thei-th stick, dashed arrows refer to communications with the i−1th stick.
![](https://s.studizba.com/z.php?f=/templates/si/i/noavatar.png&w=100&h=100&t=1"){kind=avatar}
