Using Temporal Logic to Specify Properties: Homework Exercises 1.3 2005/05/09 08:51:26 GMT-5 2005/10/06 15:44:38.203 GMT-5 John Greiner greiner@cs.rice.edu Ian Barland ian@cs.rice.edu Moshe Vardi vardi@cs.rice.edu John Greiner greiner@cs.rice.edu Ian Barland ian@cs.rice.edu Moshe Vardi vardi@cs.rice.edu Give an English translation of the following LTL formulae. Try to give a natural wording for each, not just a transliteration of the logical operators. (◇ r →(pUr)) □ (q→□ ¬p ) ``p is true before r.'' ``p is false after q.'' In the following, give an LTL formula that formalizes the given English wording. If the English is subject to any ambiguity, as it frequently is, describe how you are disambiguating it, and why. ``p is true.'' ``p becomes true before r.'' ``p will happen at most once.'' ``p will happen at most twice.'' ``The light always blinks.'' Use the following proposition: p = the light is on. ``The lights of a traffic signal always light in the following sequence: green, yellow, red, and back to green, etc., with exactly one light on at any time.'' ¶ Use the following propositions: g = the green light is on, y = the yellow light is on, and r = the red light is on. This looks so simple and obvious, right? Unfortunately, it is ambiguous. The simple answer, p, says it's true right now. But, the likelier intended meaning is that it's always true, □p. This can be reworded as ``p becomes true while r is still false.'' (¬rW(p∧¬r)) The version of LTL we use cannot capture the notion of something being true for exactly one state. Instead, we must instead think in terms of something being true for ``a while''. Using that idea, we'll reword the original English into more explicit, long-winded forms. ¶ ``p will happen at most once'' becomes ``p is false for a while, then it may become true for a while, then it may become false forever.'' It LTL, that can be written as (¬pW(pW□ ¬p )). ¶ Repeating that pattern, ``p will happen at most twice'' becomes (¬pW(pW(¬pW(pW□ ¬p )))). Here are three progressively simpler solutions which are equivalent. □ ((p→◇¬p)∧(¬p→◇p)) (□ (pU¬p) ∧□ (¬pUp) ) (□ ◇ p ∧□ ◇ ¬p ) There are many ways to write this, but here's one. It states that whenever the green light is on, no other light is on, and it will stay on until the yellow one is on. Note that this implies the red light won't come on before the yellow one. What happens when the other lights are on is entirely parallel. Finally, at least one light is on. ¶ □ ((g→((¬y∧¬r)∧(gUy)))∧(y→((¬r∧¬g)∧(yUr)))∧(r→((¬g∧¬y)∧(rUy)))∧(g∨y∨r)) Recall the Dining Philosophers Problem from the previous homework. Using temporal logic, formally specify the following desired properties of solutions to the D.P. Problem. Use the following logic variables, where 0 ≤ i < N : l i : Philosopher i has his/her left fork. r i : Philosopher i has his/her left fork. For each question, your answer should cover exactly the given condition -- nothing more or less. You may assume N 3 . No fork is ever claimed to be held by two philosophers simultaneously. Philosopher i gets to eat (at least once). Each philosopher gets to eat infinitely often. The philosophers don't deadlock. (The main difficulty is to conceptualize and restate ``deadlock'' within this specific model in terms of the available logic variables.) ¶ You may assume philosophers pick up two forks in some order, eat, and drop both forks. The philosophers don't deadlock. (The main difficulty is to conceptualize and restate ``deadlock'' within this specific model in terms of the available logic variables.) ¶ You may not assume philosophers pick up two forks in some order, eat, and drop both forks. For example, one might pick up a single fork and then drop it. Or, the philosophers might be lazy and never pick up a fork. Describe a D.P. Problem run in which philosophers don't deadlock, but it is not the case that each philosopher gets to eat infinitely often. □ (¬ ( l 0 ∧ r 2 ) ∧¬ ( l 1 ∧ r 0 ) ∧¬ ( l 2 ∧ r 1 ) ) ◇ ( l i ∧ r i ) (□ ◇ ( l 0 ∧ r 0 ) ∧□ ◇ ( l 1 ∧ r 1 ) ∧□ ◇ ( l 2 ∧ r 2 ) ) Here are two solutions. □ (¬ ( l 0 ∧ l 1 ∧ l 2 ) ∧¬ ( r 0 ∧ r 1 ∧ r 2 ) ) □ ◇ (( l 0 ∧ r 0 )∨( l 1 ∧ r 1 )∨( l 2 ∧ r 2 )) This simply says that it never gets stuck in one particular fork configuration. There would be many if statements, one per configuration, and this is abbreviated. ¶ □ ((( l 0 ∧ l 1 ∧ l 2 )→◇ ¬ ( l 0 ∧ l 1 ∧ l 2 ) )∧((¬ l 0 ∧ l 1 ∧ l 2 ∧¬ r 2 )→◇ ¬ (¬ l 0 ∧ l 1 ∧ l 2 ∧¬ r 2 ) )∧…) There are many possibilities. One is where philosopher 0 repeatedly eats, grabbing the forks so quickly that neither other philosopher has a chance to grab one that is shared with him. They following algorithm is an attempt to implement mutual exclusion for two processes. Here, each process is willing to defer to the other. (It also introduces Promela's goto, which lets you branch to a label; this is an alternate way of implementing loops and other control flow.) Verify whether the algorithm is correct or not. Verify using SPIN's built-in checks, without using temporal logic. Verify using temporal logic. If it is incorrect, find a shortest possible trace when it fails. 1 int x, y, z; 2 3 active[2] proctype user() 4 { 5 int me = _pid+1; /* me is 1 or 2. */ 6 7 L1: 8 x = me; 9 if 10 :: (y != 0 && y != me) -> goto L1 /* Try again. */ 11 :: (y == 0 || y == me) /* Continue... */ 12 fi; 13 14 z = me; 15 if 16 :: (x != me) -> goto L1 /* Try again. */ 17 :: (x == me) /* Continue... */ 18 fi; 19 20 y = me; 21 if 22 :: (z != me) -> goto L1 /* Try again. */ 23 :: (z == me) /* Continue... */ 24 fi; 25 26 /* Entering critical section. */ 27 /* ... */ 28 29 /* Leaving critical section. */ 30 } As usual, we must check that no more than one process is in the critical section at a time. We can our usual code in_crit++; assert(in_crit == 1); in_crit--; and declaring in_crit global. This code passes verification, but warns us that this code isn't necessarily even executed! For a critical section protocol to be valid, it must also guarantee that each process eventually enters the critical section. Since the gotos create a control flow loop, we can check this by looking for non-progress cycles, labeling the critical section as progress.

The shortest counter-example trace. For brevity, the local values of me are not shown, since they cannot vary.

Using temporal logic, we can create a formula that describe our desired behavior: ``Eventually, each process gets to the critical section, but not both at the same time.'' One such formula is (◇ p ∧◇ q ∧□ ¬ (p∧q) ) where we define #define p (user[0]@crit) #define q (user[1]@crit) and define the label crit in the critical section. This is a Promela version of an algorithm once recommended by a major computer manufacturer. As you can see, like many other mutual exclusion algorithms that have been proposed, it is flawed. The following is pseudocode for an attempt to implement critical sections for n processes. It is based on the idea that processes take numbers, and the one with the lowest number proceeds next. This algorithm has one small flaw. Your task is to find and fix the flaw. In particular, show the following steps of this process. Implement this algorithm in Promela, and show the resulting code. Include any code added for verification purposes, although that is counts towards the next problem's score. Show the use(s) of SPIN to verify that there is a flaw and to determine what the flaw is. Briefly describe the flaw. Fix the flaw in the code, and show either the fix or the resulting code. Again, include any code added for the next problem's verification. Show the use(s) of SPIN to verify your final implementation. Hints: First, do not radically change the algorithm. There is a straightforward solution that only changes/adds a line or two. Second, do not overly serialize the code. Since the entry protocol's for loop is already serialized, this really means that each each process should be able to calculate max concurrently. Shared variable declarations. /* Is Pi choosing a number? */ boolean choosing[n]; /* Pi's number, or 0 if Pi has none. */ unsigned int number[n]; Global initialization. Occurs once, before any process attempts to enter its critical section. /* No process has a number. */ for all j ∈ {0,…,n-1} number[j] = 0; Critical section entry protocol, for process i. I.e., each process has the following code immediately before its critical section. ¶ /* Choose Pi's number. */ choosing[i] = true; number[i] = max(number[0],number[1],…,number[n-1]) + 1; choosing[i] = false; /* For all other processes, … */ for all j ∈ {0,…,i-1, i+1,…,n-1} in some serial order /* Wait if the other process is currently choosing. */ while (choosing[j]) /* nothing */ ; /* Wait if the other process has a number and comes ahead of us. */ if ((number[j] > 0) && (number[j] < number[i])) while (number[j] > 0) /* nothing */ ; Note that, because of the if's test, it is equivalent to allow j to get the value i in this loop, as well. Although less intuitive, that simplifies the loop. Critical section exit protocol, for process i. I.e., each process has the following code immediately after its critical section. /* Clear Pi's number. */ number[i] = 0; The problem with the given code is that the concurrent max computations does not necessarily result in each element of number[] being unique. Uniqueness is assumed by the following conditional to prioritize the processes: if ((number[j] > 0) && (number[j] < number[i])) One of the hints precludes changing the max calculation to produce uniqueness. So, we need a way to prioritize processes when they receive the same number. This is most easily accomplished by using their process IDs: if ((number[j] > 0) && ((number[j] < number[i]) || ((number[j] == number[i]) && j<i))) Of course, …j>i… is also fine.