G52CON: Exercise 6, CTL

Consider the concurrent program consisting of the two processes shown below:

// Process 1				// Process 2

while(true) {                           while(true) {
    r1 = turn;                              r2 = turn;
    if (!r1) {                              if (r2) {
        <crit1>;                                <crit2>;
        turn = true;                            turn = false;
    }                                       }
}                                       }

	      // Shared datastructures
	      boolean turn = r1 = r2 = false;

States are described by the following propositional variables:

• t  for turn equals true;
• r₁ for r1 equals true;
• r₂  for r2 equals true;
• c₁ for process 1 is in its critical section;
• c₂ for process 2 is in its critical section.

The starting state is s₀ = (¬t, ¬r₁, ¬r₂, ¬c₁, ¬c₂). Each process performs the following sequence of actions: copy the value of variable turn into its local variable r1 or r2; evaluate the if statement; depending on the outcome, either do its critical section and set turn to be true (false), or return to the first step. Actions can be arbitrarily interleaved. As usual we assume that assignment is an atomic operation. If we are in a state where for example r₁ holds and t does not and process 1 executes atomic action  r1 = turn we make a transition to a state where ¬r₁ holds. In this example we can also assume that evaluating the if statement is an atomic operation since the value of the local variable can't be changed by another process. So if we are in the state where ¬r₁ holds and process 1 evaluates the condition of its if statement, we move to a state where c₁ is true.

Questions:

1. Draw the state transition diagram.
2. Write a CTL formula expressing the following property: it is impossible that r1 is true and process 1 is in its critical section. Is this formula true at the start state of the transition system you drew? Justify your answer using the truth definition for CTL formulas.
3. Write a CTL formula expressing the property of non-strict scheduling: process 1 and process 2 don't always take turns at entering critical section, but instead for example process 1 can go into critical section several times in a row. (Hint: you may need to use Until operator.) Is this formula true at the start state of the transition system you drew? Justify your answer using the truth definition for CTL formulas.