| << Chapter < Page | Chapter >> Page > |
Run this code several times and observe its behavior.
What is the state space for this code?
As desired, the program will always exit if
dist reaches either of its
limit values.
Is it equivalent to change the
<= and
>= to
== in this example?
Why or why not?
Yes. As mentioned, because of the
else clause, the loop
will terminate once the distance is out of range. Since thedistance is only ever changed by 1 on an iteration, it is
sufficient to check just the boundary conditions of the range.
While equivalent, it is probably a not good idea to make this change, since its correctness is dependent on other factors.
What is Promela's equivalent of the following
C conditional statement?
if (
condition )
then_stmt ;
else
else_stmt ;
if
::
condition ->
then_stmt ;
:: else ->
else_stmt ;
fi;
What is Promela's equivalent of the following
C loop statement?
while (
condition )
body_stmt ;
do
::
condition ->
body_stmt ;
:: else ->break;
do;
The previous examples illustrate what happens where there is a choice among guarded statements and at least one is enabled. What if noneare enabled? In that case, that process is blocked, and it halts execution until it is no longer blocked.
Create a Promela program illustrating synchronization and looping in the following way.One process counts down a global variable, until it reaches zero.Another process waits for the count to be zero to print a message.Run your program in "Interactive" mode and confirm that the second process is blocked, and thus does nothing, until the countreaches zero.
show int count = 5;
active proctype count_down(){
do:: count>0 ->count--;
:: else ->break;
od;}
active proctype wait(){
count == 0 ->printf("I'm done waiting!\n");
} We have so far seen very simple interactions between processes, using shared variables for communication and guarded statementsfor synchronization. This sections delves further into the possible interactionsand introduces some additional Promela syntax for that.
While blocking is an essential tool in designing concurrent programs, since it allows process to synchronize, it also introduces thepossibility of deadlock, when all processes are blocked. Since deadlock is a common problem in concurrent programs,we will later see how to verify whether a program can deadlock .
Create a small Promela program that can deadlock. The program need not do anything computationally interesting.Run your program to see that it can get stuck.
There are many possible programs, but the following is a simple example.
show int x = 1;
active[2]proctype wait()
{x == 0 ->printf("How on earth did x become 0?!?\n");
} One standard concurrent programming technique that uses guarded statements is locking . While details of its use are beyond thescope of this module, we'll provide a quick review. Locks are used when there is some resource or critical section of code that we want to control access to. For example, only one process at a timeshould be able to write data to a specific file, lest the file get intermingled inconsistently. To ensure this, the processmust acquire the lock associated with writing this file before it can do the operation, and then must release it.
Notification Switch
Would you like to follow the 'Model checking concurrent programs' conversation and receive update notifications?
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|
|