Objectives

• To understand how concurrency can be modelled in FSP processes.
• To have an appreciation of the state space explosion introduced by concurrency.
• To understand further the phenomenon of interference between threads and race hazards
• To learn basic elements of the Java Threads API, including starting threads.

Preparation

• revise the Threads and Concurrency lectures and second half of Ch 2 and all of Ch 3 (of Magee&Kramer.
• have a look at the ThreadDemoTerm.java and CountDownTerm.java program and familiarize yourself with their structure and use of the API.
• revise the exercises in the previous session (including the Homework!), and get ready any questions you might have from it.
• remember to bring a pen and paper for the Tutorial Exercises.

Tutorial Exercises

1. Discuss any outstanding issues from the previous session (including Homework).

2. Consider the following process definitions:

      P = (a -> b -> P).
      Q = (c -> b -> Q).
      ||S1 = (P || Q).
      S2 = (a -> c -> b -> S2 | c -> a -> b -> S2).
   

   Generate traces for ||S1 and S2. Can one generate a different trace from the other? Are the processes the same? Why?

3. Use the following rules to show that P||Q is indeed the same as S2. Let A and B denote the alphabets of processes X = x -> X' and Y = y -> Y' and C be the intersection of A and B. Then:

   X||Y = x -> (X' || Y')        , if x=y (and are in C)     (P1)
   X||Y = (x -> (X' || y->Y')      
          |y -> (x->X' || Y'))   , if x,y are not in C       (P2)
   X||Y = x -> (X' || y->Y')     , if y is in C and x is not (P3)
   X||Y = y -> (x->X' || Y')     , if x is in C and y is not (P3')
   

4. The actions of a process repeatedly incrementing a counter variable can be modelled by the FSP process
   INCCTR = (loadCtr -> inc -> storeCtr -> rest -> INCCTR).
   Note that here we do not model the value of the counter. Two such process operating in parallel (updating the same counter, cf. Race.java) can be modelled as:
   ||INCCTR = (a:INCCTR || b:INCCTR).
   1. Check that the following trace can be generated by ||INCCTR.
      a.loadCtr -> a.inc -> b.loadCtr -> a.storeCtr -> b.inc -> b.storeCtr
      Hint: produce a sequenece of independent state transitions in a:INCCTR and b:INCCTR that reproduces this trace.

   2. Assuming that the following actions represent the corresponding machine instructions:
      loadCtr: load contents of the address Ctr into register A
      inc: increment register A
      storeCtr: store contents of register A into memory location Ctr
      rest: branch back to the loadCtr instruction.
      and the value of Ctr was initially 0, what would it be after the above trace is executed (assume that b:INCCTR updates register B instead of A).

   3. If there was the intention that every time a storeCtr action was performed, the value of Ctr was incremented by 1, would ||INCCTR preserve this behaviour? What if the event rest took 10³ machine cycles (and the other events took only one)? What if it took 10⁹ cycles?

5. Consider the following process definitions.

         P1 = (x1 -> P1).
         ||P1_2 = (a1:P1 || a2:P1).
         P2 = (x1 -> x2 -> P2).
         ||P2_2 = (a1:P2 || a2:P2).
         ||P2_3 = (a1:P2 || a2:P2 || a3:P2).
   

   How many states do each of these processes have? If we defined in the above fashion ||Px_y, i.e. y independent process with x states combined in parallel, how many states would this process have?

   Note: if you do Build -> compose for these processes in the LTSA tool, you can check your answer on the Output pane!

6. (Ex 3.3 Magee & Kramer) Extend the model of the client-server program so that the server can use two clients.

   SERVERv2 = (accept.request -> service -> accept.reply -> SERVERv2).
   CLIENTv2 = (call.request -> call.reply -> continue -> CLIENTv2).
   ||CLIENT_SERVERv2 = (CLIENTv2 || SERVERv2) / {call/accept}.
   

   Hint: prefix the CLIENT prcesses and then do the renaming.

7. Consider the following process definition:

   COUNTDOWN (N=3)   = (start -> COUNTDOWN[N]),
   COUNTDOWN[i:0..N] = ( when (i>0)  tick -> COUNTDOWN[i-1]
                       | when (i==0) beep -> STOP
                       | stop -> STOP).
   

   The CountDownTerm.java program is meant to be an implementation of this. The main program thread performs the stop action; it only performs this if the counter thread, which performs the tick and beep actions, is not running:

   if (c.counter.isAlive()) 
     c.stop(); // sets c.counter to null then prints "stop"
   

   Why does this not prevent the erroneous behaviour ... tick tick stop beep? That is, the program can produce the output:

     ...
     tick:(count=1)
     stop
     beep
   

   What (if any) erroneous behaviour does the guard prevent?

   Hint: in the above situation, the main thread performs the actions:

   isAlive[1] -> ctr.write[0] -> print.stop
   (call to c.counter.isAlive() returns 1, sets counter to null and prints stop) and the counter thread performs the actions (for the last iteration):
   ctr.read[1] -> print.tick -> threadExit (i.e. reads counter as non-null, prints tick and terminates)
   Note that isAlive() will only return 0 after threadExit is performed. What interleaving of these actions can cause the above behaviour?

Laboratory Exercises

1. (Ex 3.1 Magee & Kramer) In the LTSA tool, verify that the processes ||S1 and S2 are identical, i.e. that they generate equivalent LTS.

      P = (a -> b -> P).
      Q = (c -> b -> Q).
      ||S1 = (P || Q).
   
      S2 = (a -> c -> b -> S2 | c -> a -> b -> S2).
      ||S2 = S2
   

   Hint: load each of the two processes in separate tools. Build -> Compile and Build -> Compose each. Now Build -> Minimize ||S2.

2. In the tool with ||S1, select Options -> Multiple LTS in Draw Window. In the Draw pane, select all processes (you will need to drag the top one away to see the others - see the relevant section of Help -> Manual for more information). Run ||S1 and observe the transitions in the component and combined LTS diagrams.

3. The CountDownTerm.java program has a race hazard caused by the stop action being performed by the the main thread. Rewrite the program so that the start and stop actions are performed by the counter thread. (Hint: remove the code for starting, sleeping and stopping in main(). The creation and starting of counter is moved to the constructor. The run() method initially calls start(); it calls stop() after t iterations, where t is a random number in the range 0..N+1 -- you can reuse the code in main() to setup the random number for this purpose).

   You will notice now that the main thread stops much earlier, but the java CountDownTerm process does not terminate until the counter thread does.

4. The program ThreadDemoTerm.java uses a sub-class of the Thread class called ThreadTerm to create a thread. Rewrite the program in the alternate way in which a thread may be created, i.e. by a class which implements the Runnable class. Hint: use CountDownTerm.java as an example.

5. Extend ThreadDemoTerm.java so that it creates three threads.

Homework

1. Implement a version of CountDownTerm.java which uses a sub-class of theThread class to create the thread. Hint: Initialize counter = this; in the constructor, rename start() to startE() (this will also need to be modified) and stop() to stopE(). As it is in another class, main() will have to access N etc through the object c.

2. Verify the second part to your answer in Tutorial Exercise 7 by removing the guard if (c.counter.isAlive()) in CountDownTerm.java and running the program.

3. Model the situation in Tutorial Exercise 7 by as a composite FSP process ||COUNTDOWNEND. Verify that the erroneous traces can be reproduced by your model.

   Hint: model the last iteration of the while loop of run() only in the process COUNTER with alphabet {ctr.read[0..1], print.tick, threadExit} . The process MAIN has the alphabet {isAlive[0..1], ctr.write[0], print.stop}. Model the value of initially non-null counter in the process CTR with alphabet {ctr.read[0..1], ctr.write[0]}. Finally, model the thread state in a process THREADSTATE with alphabet {isAlive[0..1], threadExit}.

4. Follow up your revision of concurrent processes by studying on the LTSA tool some examples from Chapter 3 of the textbook (see Howework Q2 from the previous session). Observe the relationship between the LTS of the composite process with that of the component processes. Observe the transitions in the component processes as you run the composite process. Suggested examples are ||SWITCHES, ||RESOUCE_SHARE, ||CLIENT_SERVERv2 and ||THREAD.

5. (Ex 3.7 Magee & Kramer: play with applets!) Modify the ThreadDemo.java program so that it consists of three rotating threads. You will also need to download ThreadPanel.java.

Challenge Exercise!