-
Home
- Model checking concurrent
- Model checking concurrent
- Modeling concurrent processes:
In the following, consider an arbitrary number of philosophers.
Three philosophers is only a special case.
- Assume we number the forks, and each philosopher picks upforks in numerical order.
Because the table is round, this implies that if mostphilosophers pick up the left fork first, that one will instead
pick up the right fork first.This is a well-known strategy for avoiding deadlock.
Is that strategy weakly fair? Strongly fair?
- Consider the strategy of acquiring forks in numerical orderand releasing them in the opposite order.
Compare its behavior in SPIN's simulation modewith SPIN's built-in weak fairness enforcement turned
off vs. on.
- That particular strategy is neither weakly nor strongly fair,in general.
(It is weakly fair when there are only 2 or 3 philosophers.)For example, it allows for one philosopher to repeatedly
grabs and drop forks, while the others do nothing.
The following is an example of the distinction between deadlock and
livelock. Consider two people walking in a hallway towardseach other.
The hallway is wide enough for two people to pass.Of interest is what happens when the two people meet in the hall.
When meeting on the same (left/right) side of the corridor,a polite strategy is to step to the other side of the hallway.
A more belligerent strategy is to wait for the other person to move.With two polite people there is the possibility of livelock, while
with two belligerent people there is the possibility of deadlock.(As an aside, note that one polite and one belligerent person
together in a hall don't have any problems.)
- Model the livelock problem in Promela.
Use SPIN to demonstrate that your Promela program in fact modelsthe problem.
- Model the deadlock problem in Promela.
Use SPIN to demonstrate that your Promela program in fact modelsthe problem.
A key to modeling the problem is to abstract away the unnecessary
details. In particular, there is no need to model the peoplewalking down the hall, as nothing interesting happens then.
Similarly, the hallway can be modeled as being only wide enoughfor two people to pass.
By these restrictions, we reduce the data to only four possibilities:each of the two people can be on either of two sides of the hall.
Keeping the state space small allows SPIN to solve moreproblems, solve them faster, and report traces that are more
succinct and, thus, easier to understand.
The following is one of the many ways to code this.
/* Code assumes these two values add to two. */
#define NUM_BELLIGERENT 2#define NUM_POLITE 0
/* Indicates position of two people.* Values: 0 or 1, for two sides of hall.
* 2 means unitilized.*/
int position[2]= 2;
active [NUM_BELLIGERENT]proctype belligerent()
{/* Non-deterministically set up starting position. */
if:: true ->position[_pid] = 0;:: true ->position[_pid] = 1;fi;
/* Wait for other person to initialize. */position[1 - _pid] != 2;do
:: position[1 - _pid]== position[_pid] ->/* Wait for other person to move. */
skip;:: else ->/* Success. */
break;od;
}active [NUM_POLITE] proctype polite(){
/* Non-deterministically set up starting position. */if
:: true ->position[_pid] = 0;:: true ->position[_pid] = 1;fi;
/* Wait for other person to initialize. */position[1 - _pid] != 2;do
:: position[1 - _pid]== position[_pid] ->/* Move to other side. */
position[_pid]= 1 - position[_pid];:: else ->/* Success. */
break;od;
}
The process scheduler in an operating system is a typical example of
where we are concerned with fairness. If we have multiple processesrunning on a single processor, we break time into finitely-long
intervals during which we execute one of the processes.We'd like to ensure that each process gets a ``fair''
share of the CPU time.
Your model should have an ``OS'' process
(the scheduler) and multiple ``user'' processes, usingthis framework.The user processes are non-terminatingthey always want
to get the CPU's next time slice.
I.e. , the user processes will be continually
enabled from the perspective of your own scheduler,although not from that of SPIN.
But, we aren't modeling the user computation, those processesjust print a message.
Your scheduler, which is also non-terminating,somehow picks among the processes which will execute.
-
- Write a scheduler which does not exhibit weak fairness.
I.e. , it is possible for one process
not to make progress.However, do not write a trivial scheduler that simplyalways picks one process and never the other.
- Use SPIN to verify that your scheduler doesn't allow deadlock.
- Use SPIN to demonstrate that your scheduler does not exhibit
weak fairness.
-
- Write a scheduler which does exhibit weak fairness,
i.e. ,
that each process is guaranteed to make progress.Do not use SPIN's built-in weak fairness enforcement,
rather your scheduling algorithm must somehow enforce thatcondition.
- Consider if we added a progress label to the user
proctype ,
inside its loop.Why is this insufficient for SPIN to verify the weak fairness?
- Describe how we could modify the program to verify the weak
fairness. You do not need to implement this.Use only the features of Promela/Spin we've covered so far.
(Soon, we'll introduce new features that allow asimpler and better approach.)
- The simplest such scheduler is one that non-deterministicallychooses which process is scheduled next.
- The simplest such scheduler just alternates between thetwo processes.Adding a progress label to, say, only process A allows SPINto verify that A makes progress. But that says nothing
about B making progress.Adding a progress label to both A and B allows SPIN
to verify that
at least one of A and B
makes progress, both not necessarily both.With what we've seen, here's two possible ways to use SPINto convince ourselves that the code is weakly fair.
- Add a progress label to only process A. SPIN verifies thatA must gets turns. Then add a progress label to only
process B. SPIN verifies that B must get turns.Thus, both A and B must get turns.Unfortunately, this requires two separate verifications.Also, editing the code inbetween the verifications is
error-prone, as it is easy to forget to delete the firstprogress label.
- Add code, probably to the scheduler, that keeps track ofthe scheduling choices. Add logic and assertions to
check if this behavior is correct.It is easy to check, for example, that the processesare indeed strictly alternated. Or, more flexibly,
that after 100 scheduling choices, both processes werescheduled at least once. But, it is tricky to capture
the idea that each will eventually get scheduled.Adding substantial code for verification is alwaysundesirable because we must separately reason that this
additional code is correct and doesn't interfere withthe original behavior.
Source:
OpenStax, Model checking concurrent programs. OpenStax CNX. Oct 27, 2005 Download for free at http://cnx.org/content/col10294/1.3
Google Play and the Google Play logo are trademarks of Google Inc.
