| << Chapter < Page | Chapter >> Page > |
The previous examples modeled two people simultaneously updating the
same bank account, one making a deposit, and one a withdrawal.What if we had even more simultaneous updates?
Let's focus only on deposits, so each is doing the same action.Rather than duplicating code with multiple
proctype 's (say,
deposit1 ,
deposit2 , and
deposit3 ),
Promela allows us toabstract that, as in the following:
1 /* Number of copies of the process to run. */
2 #define NUM_PROCS 33
4 /* A variable shared between all processes. */5 show int z = 0;
67 active[NUM_PROCS] proctype increment()8 {
9 show int new_z;10
11 new_z = z;12 new_z++;
13 z = new_z;14 }
We've abstracted the variables' names, but otherwise,
increment is the same as the
previous
deposit .
The first substantial change is that we are starting three processes,rather than two, each with a copy of the same code.
The bracket notation in the
proctype declaration indicates
how many copies of that code are to be used.The number of copies must be given by a constant,
and it is good practice to name that constant as shown.
Although vastly simplified, this is also the core of our
web-based flight reservation system example .
The shared variable
z would represent the number of booked seats.
We can also ask questions likeWhat is the probability that we end
with
z having the value 3?How would you solve this?
Divide the number of traces meeting this condition by the total number of conceivable traces.
However, this assumes that each possible trace is equally likelya dangerous assumption! In real life, with a particular operating system and hardware, sometraces might be much more common than others. For example, it mightbe very unlikely (but possible) that two context switches would occur only a smallnumber of instructions apart. So, a more realistic answer would bebased upon a statistical analysis of repeated runs.
But an even more preferable answer is to say that this is a trick question!Rather than thinking of our concurrent system as being probabilistic,it is often better to stop short and merely call it non-deterministic . For example, if processes are distributed across the internet,then which trace occurs might depend on network traffic, which in turn might depend on such vagaries asthe day's headlines, orhow many internet routers are experimenting with a new algorithm, orwhether somebody just stumbled over an ethernet cord somewhere. In practice, we can't come up with any convincing distributionon how jobs get scheduled. Moreover, sometimes we want to cover adversarial schedules(such as guarantees of how our web server protocol acts during denial-of-service attack).
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|