Exercises


  • 7.1 What action trace violates the following safety property?

     property PS = (a->(b->PS|a->PS)|b->a->PS).

  • 7.2 A lift has a maximum capacity of ten people. In the model of the lift control system, passengers entering a lift are signaled by an enter action and passengers leaving the lift are signaled by an exit action. Specify a safety property in FSP which when composed with the lift will check that the system never allows the lift that it controls to have more than ten occupants.

  • 7.3 Specify a safety property for the car park problem of Chapter 5, which asserts that the car park does not overflow. Specify a progress property which asserts that cars eventually enter the car park. If car departure is lower priority than car arrival, does starvation occur?

  • 7.4 In an operating system, a binary semaphore is used to control access to the console. The console is used by user processes and system processes. Construct a model of this system and investigate the scheduling conditions under which user processes may be denied access to the console.

  • 7.5 Implement the system modeled in exercise 7.4 in Java using the ThreadPanel and NumberCanvas classes for display. Can you induce starvation in a user thread by giving it a lower scheduling priority using Thread.setPriority()? If not, can you explain why starvation does not occur?

  • 7.6 Two warring neighbors are separated by a field with wild berries. They agree to permit each other to enter the field to pick berries, but also need to ensure that only one of them is ever in the field at a time. After negotiation, they agree to the following protocol.

  • When one neighbor wants to enter the field, he raises a flag. If he sees his neighbor’s flag, he does not enter but lowers his flag and tries again. If he does not see his neighbor’s flag, he enters the field and picks berries. He lowers his flag after leaving the field.

  • Model this algorithm for two neighbors, n1 and n2. Specify the required safety property for the field and check that it does indeed ensure mutually exclusive access. Specify the required progress properties for the neighbors such that they both get to pick berries given a fair scheduling strategy. Are there any adverse circumstances in which neighbors would not make progress? What if the neighbors are greedy?

  • (Hint: The following FSP can be used to model the flags.)

        const True = 1    const False = 0    range Bool = False..True    set BoolActions =         {setTrue,setFalse,[False],[True]}    BOOLVAR = VAL[False],    VAL[v:Bool] = ( setTrue -> VAL[True]                  | setFalse -> VAL[False]                  | [v] -> VAL[v]                  ). ||FLAGS = (flag1:BOOLVAR||flag2:BOOLVAR).

  • 7.7 Peterson’s Algorithm for two processes (Peterson, G.L., 1981)

  • Fortunately for the neighbors in exercise 7.6, Gary Peterson visits one day and explains his algorithm to them. He explains that, in addition to the flags, the neighbors must share a turn indicator which can take the values 1 or 2. This is used to avoid potential deadlock.

  • When one neighbor wants to enter the field, he raises his flag and sets the turn indicator to indicate his neighbor. If he sees his neighbor’s flag and it is his neighbor’s turn, he may not enter but must try again later. Otherwise, he can enter the field and pick berries and must lower his flag after leaving the field.

  • For instance, neighbor n1 behaves as shown below, and neighbor n2 behaves symmetrically.

     while (true) {       flag1 = true; turn = 2;       while (flag2 and turn==2) {};       enterField; pickBerries;        flag1 = false; }

  • Model Peterson’s Algorithm for the two neighbors. Check that it does indeed avoid deadlock and satisfy the mutual exclusion (safety) and berry-picking (progress) properties.

  • (Hint: The following FSP can be used to model the turn indicator.)

     set CardActions = {set1,set2,[1],[2]} CARDVAR = VAL[1], VAL[i:Card] = ( set1 -> VAL[1]               | set2 -> VAL[2]               | [i] -> VAL[i]               ).

  • 7.8 Implement Peterson’s Algorithm as modeled in exercise 7.7.




Concurrency(c) State Models & Java Programs
Concurrency: State Models and Java Programs
ISBN: 0470093552
EAN: 2147483647
Year: 2004
Pages: 162

flylib.com © 2008-2017.
If you may any questions please contact us: flylib@qtcs.net