As my asignment I have to verify something on Dekker's algorithm - but with 3 pr开发者_如何转开发ocesses -
I can only find original version for 2 processes.
The goal is not the algorithm but it's implementation and verification in SMV System http://www.cs.cmu.edu/~modelcheck/smv.html
You should probably ask the course staff, but you can use two Dekker mutexes to achieve three-process mutex. Processes 0 and 1 compete to acquire mutex A; the holder of mutex A and process 2 compete to acquire mutex B, whose holder is allowed to run a critical section.
// Dekkers algorithm version3
system:
boolean t1WantsToEnter=false;
boolean t2WantsToEnter=false;
startThreads;//initialize and launch all threads
Thread T1;
void main();{
while(!done);
{
t1WantsToEnter=true;
while(t2WantsToEnter); //wait
//critical section cokde
t1WantsToEnter=false;
//code outside critical section
Thread T2;
void main();{
while(!done);
{
t2WantsToEnter=true;
while(t1WantsToEter);//wait
//critical section code
t2WantsToEnter=false;
//code outside critical section
// if u want to know how this code is executed using RAM diagram,
// Dekkers algorithm version3
system:
boolean t1WantsToEnter = false;
boolean t2WantsToEnter = false;
startThreads; // initialize and launch all threads
// Thread T1
void main() {
while(!done);
{
t1WantsToEnter = true;
while(t2WantsToEnter) { // wait
// critical section cokde
t1WantsToEnter = false;
}
// code outside critical section
} // end outer while
} // end Thread T1
// Thread T2
void main() {
while(!done);
{
t2WantsToEnter = true;
while (t1WantsToEter) { //wait
// critical section code
t2WantsToEnter =false;
}
// code outside critical section
} // end outer while
} // end Thread T2
精彩评论