Plan
School of Computing and Information Systems
SWEN90004 Modelling Complex Software Systems
Concurrency Workshop 4, Week 5, Semester 1, 2021
Concurrency in FSP
This workshop should give you experience with modelling concurrent processes in FSP, and using the model checking functionality available in LTSA. The FSP code used in exercises 1 and 6 can be found on the LMS under Workshops.
The exercises
1. Magee and Kramer define the following model of a shared resource:
RESOURCE = (acquire -> release -> RESOURCE).
USER = (acquire -> use -> release -> USER).
||RESOURCE_SHARE = (a:USER || b:USER || {a,b}::RESOURCE).
(This is available on the LMS in file resource-user.lts.) Based on the definition of RESOURCE, show that the following two processes are not equivalent, by finding a trace that is in one process but not the other:
||ONE = (a:RESOURCE || b:RESOURCE).
||TWO = ({a,b}::RESOURCE).
Try to answer this question by pure reasoning; then check out the LTS models. Note that, in case of independent composite processes, LTSA allows you to select only the components. To generate the LTS models, first select ONE from the drop-down menu on the toolbar, and then select Build ! Compose from the menu. Inspect this model. Then do the same for TWO. (Recall that {a,b}.acquire means that either process a or b can engage in acquire, but not both together.)
2. Consider the following modified version of RESOURCE SHARE:
||RESOURCE_SHAREv2 = (a:USER || b:USER || a:RESOURCE || b:RESOURCE).
What is the di↵erence between RESOURCE SHARE and RESOURCE SHAREv2? Come up with a trace that is in one process but not the other.
3. Create a new process called RESOURCE SHAREv3 that models a single resource shared under mutually exclusive access by a set of N users, where N=5. Model this process so that modifying the number of users is straightforward. (If there are too many states for LTSA to draw something useful, use a smaller N to check that your solution works.)
4. Recall that the STOP, END, and ERROR are all special pre-defined process in FSP that describe process termination.
Generate the LTS for ONESHOT = (once -> STOP).
Then generate the LTS for this following modified version: ONESHOT = (once -> ERROR). Finally, generate the LTS for ONESHOT = (once -> END).
What do you notice about the di↵erent LTS models for the three process descriptions?
5. Perform deadlock analyses on three models described in Exercise 4. This can be done by selecting Check ! Safety from the LTSA menu.
What do you notice about the di↵erent outputs from this analysis?
6. The Dining Philosophers example, discussed in lecture Con.07, deadlocks if all philosophers pick up their right fork at the same time. This deadlocking model is:
PHIL = (sitdown -> right.get -> left.get -> eat
-> left.put -> right.put -> arise -> PHIL).
FORK = (get -> put -> FORK).
||DINERS(N=5)
= forall [i:0..N-1]
( phil[i]:PHIL
|| {phil[i].left,phil[((i-1)+N)%N].right}::FORK
).
The source for this is available on the LMS, in file dining-philosophers.lts.
Model a BUTLER process that, when composed with the model above, permits a maximum of four philosophers to sit down. Demonstrate that this system avoids deadlock, and explain why this is the case.
Challenge Task
If you get this far and want to be challenged further, try the following task.
7. According to the semantics of FSP, each process defines a labelled transition system. Two processes are said to be strongly equivalent when their labelled transition systems are iso- morphic (Magee & Kramer page 394, Section C.6.1). Processes that are strongly equivalent have the property that they can be substituted for one another in any system constructed as a composition of one of those processes, without a↵ecting the behaviour of the system with respect to strong equivalence. That is, if P is strongly equivalent to Q, then (P || X) is strongly equivalent to (Q || X) for all processes X. Decide whether the processes P and Q, defined below, are strongly equivalent. Justify your answer.
P = (a -> b -> P | a -> c -> P).
Q = (a -> (b -> Q | c -> Q)).