 Process
Analysis Toolkit (PAT) 3.5
Help |
In this tutorial, we use the dining philosopher example,
which traditionally is a classic CSP model, to demonstrate how to
model and verify systems. The model uses CSP features like alphabetized parallel
composition. Moreover, in order to prove property of the system, a number
of fairness constraints are involved. The following is the problem description. In 1971, Edsger Dijkstra set an examination question on a
synchronization problem where five computers competed for access to five
shared tape drive peripherals. Soon afterwards the problem was retold by Tony
Hoare as the dining philosophers' problem. The five philosophers sit at a
circular table with a large bowl of spaghetti in the center. A fork is placed
in between each philosopher, and as such, each philosopher has one fork to his
or her left and one fork to his or her right. As spaghetti is difficult to
serve and eat with a single fork, it is assumed that a philosopher must eat
with two forks. The philosopher can only use the fork on his or her immediate
left or right. It is further assumed that the philosophers are so stubborn
that a philosopher only put down the forks after eating. The problem is
generalized as N philosophers sitting around a round table. #define N
5; The above defines a global constant named N, of value 5, which denotes
the number of philosophers. Next, we model each object in the system as one
process. There are two sets of objects, i.e., the philosophers and the
forks. Phil(i) = get.i.(i+1)%N -> get.i.i -> eat.i -> put.i.(i+1)%N
-> put.i.i -> Phil(i); We assume that the philosophers and forks are numbered from 0 to
N-1, as shown in the figure. The above models a philosopher.
Phil is the process name and i is a process parameter which
informally denotes the i-th philosopher. Event get.i.(i+1)%N models the
event of i-th philosopher picking up the fork on his right hand side. % is the
standard mod operator. Event get.i.i models the event of i-th philosopher
picking up the fork on his left hand side. Event eat.i models the event
of i-th philosopher eating. Event put.i.(i+1)%N models the event of
putting down the fork from the right hand side. Event put.i.i models the
event of putting down the fork from the left hand side. Informally
speaking, the philosopher picks up the forks, eats, and then puts down the
forks. We remark all these events have no attached program, and hence, they may
serve as synchronization barriers. Notice that an event name may be composed of
process parameters or even global variables. Fork(x) = get.x.x -> put.x.x -> Fork(x) [] get.(x-1)%N.x ->
put.(x-1)%N.x -> Fork(x); The above models the other objects in the system, namely the forks. At the
top level, the process is modeled using a (external) choice "[]".
Informally, it states that the fork can be picked up by the philosopher on the
left or the one on the right. Notice that the events shared the same name
with those in process Phil(i). College() =
||x:{0..N-1}@(Phil(x)||Fork(x)); The above models the system. "||" is the parallel composition
operator. The above is equivalent to the following: Phil(0) || Fork(0) ||
Phil(1) || Fork(1) || ... || Phil(N-1) || Fork(N-1). The semantics of the
"||" operator is that all processes execute in parallel. What's more, if
an event (without attached program) is shared by multiple processes (i.e., the
process's alphabet contains this event), then all those processes must
synchronize on the event. For instance, the event get.0.1 can only occur
when process Phil(0) and process Fork(1) both engage in the event.
Implementation() = College()
\{get.0.0,get.0.1,put.0.0,put.0.1,eat.1,get.1.1,get.1.2,put.1.1, put.1.2,eat.2,get.2.2,get.2.3,put.2.2,put.2.3,eat.3,get.3.3,get.3.4,put.3.3,put.3.4,eat.4,get.4.4,get.4.0,put.4.4,put.4.0}; The above defines a process which behaves exactly as process
College() excepts that all events but eat.0 are hidden. The
operator "\" reads as "hide". Specification() = eat.0 ->
Specification(); The above defines a process which repeatedly engages in event eat.0. Its role
will be explained in detail later. The above completes the modeling of the
system. Next, we analyze the system by asserting different properties. #assert College() deadlockfree; The above asserts that process College() is deadlock-free, where
"deadlockfree" is a reserved keyword. A system is deadlock-free if
and only if the system will never enter a state while there is no further moves.
#assert College() |= []<>
eat.0; The above asserts that process College() satisfies the LTL property
which reads "always eventually eat.0 is engaged". Or equivalently, the 0-th
philosopher shall not starve to death. Notice that instead of a proposition, an
event is used as part of the LTL. We found that this is particularly useful
for event-based specifications. #assert Implementation() refines Specification(); The above demonstrates a different kind of assertion. Instead of using LTL,
it asserts that process Implementation() (traces) refines process
Specification(). In other words, all traces of process
Implementation() must be allowed by process Specification().
Because the only traces of Specification() are finite sequences of event
eat.0. This assertion simply states that it is possible in process
Implementation() that the 0-philosopher eats (possibly infinitely).
Notice there is a range of other refinement relationships as well.
We are now ready to verify the system. Open the Verifier (by clicking
Verification or pressing F7) and
double-click the first assertion: "#assert
College() deadlockfree;". The following message is printed in the
output window. ********Verification Result******** ********Verification
Setting******** ********Verification
Statistics******** The first part of the message states the verification result, i.e., the
assertion is not valid. A trace which leads to the deadlock state is printed.
The second part of the message reveals details on the analysis technique. The
last part provides statistics on the number of system states/transitions
explored, the search depth and time/memory usage. Notice
that because PAT is implemented in C#, the memory usage is only
estimated because of garbage collection. The printed trace reveals a deadlock situation where each and every
philosopher holds one fork and waits. A counterexample produced by the verifier
often reveals a bug in the model (and probably in the system). Often, the
model needs to be modified and re-verified. There are multiple ways in this case
to avoid the deadlock situation. The following models one of the ways. Process Phil0() is different from Phil(0) in that the forks are
picked up in a different order. Re-open the Verifier and double click the
assertion stating that College_deadlockfree() is deadlock free. This verifier
reports that the assertion is true. Now, double-click the assertion "#assert
College_deadlockfree() |= []<> eat.0;". The following is printed. The highlighted part of the trace forms a loop. In this counterexample trace,
the 1-th philosopher keeps picking up the forks and eating, whereas the 0-th
philosopher keeps waiting all the time. By a simple argument, it can be shown
that this is not a fair trace! Now, selecting the option "Event-level weak
fairness" and click Verify again, a longer trace is printed as a counterexample
this time. Simulate this trace and you will see a complicated loop. The reason
is that weak fairness guarantees that if an action is always enabled, eventually
it occurs. However, in this model, because a philosopher shared forks with his
neighbors, if one of his neighbors is infinitely faster than he is, the fork is
not always there, instead, it is only repeatedly there. To avoid this situation,
we need (at least) event-level strong fairness! Now, selecting the option
"Event-level strong fairness" and click Verify again. The assertion is
proved.
There are several interesting properties about the problem.
One is a dangerous possibility of deadlock when every philosopher holds a left
fork and waits perpetually for a right fork. The other is starvation. A
philosopher may starve for different reasons, e.g., system deadlock, greedy
neighbor, etc. In the following, we model the problem in PAT.
The
Assertion (College() deadlockfree) is NOT valid.
The following trace leads to a deadlock
situation.
<init -> get.0.1 -> get.0.0
-> eat.0 -> put.0.1 -> get.1.2 -> get.1.1 -> eat.1 ->
put.0.0 -> get.4.0 -> put.1.2 -> get.2.3 -> put.1.1 ->
get.0.1 -> get.1.2 -> get.3.4>
Admissible Behavior:
All
Search Engine: First Witness Trace
using Depth First Search
System
Abstraction: False
Visited
States:59
Total
Transitions:61
Time
Used:0.0041809s
Estimated Memory
Used:8897.464KB
Copyright © 2007-2012 Semantic Engineering Pte. Ltd.