Project Ideas

Further Exercises and Project Ideas Using Uppaal.

• A list with 27 suggested exercises is available here.
• The book “The little book of semaphores” by Allen B. Downey presents semaphore-based solutions to many concurrency problems, ranging from classical ones (like the barbershop) to tricky and obscure problems (like the Sushi bar). All of these problems are a suitable source of student projects on modelling and verification using Uppaal. (The pointer to Downey’s book is courtesy of Frits Vaandrager.)
• Using Uppaal (or the Concurrency Workbench, if you prefer) model the mutual exclusion algorithm proposed by Murray A. Eisenbeng and Michael R. McGuire (“Further comments on Dijkstra’s concurrent programming control problem”, Communications of the ACM 15(11):999 (November 1972)) for three processes, and establish that the algorithm does guarantee mutual exclusion. The code for process i is given below.

do {
 // Acquire lock
 while(1) {
   flag[i] = WantIn;
   j = turn;
   while (j != i) {
     if (flag[j] != idle)
       j = turn;
     else
       j = (j + 1) % n;
   }
   flag[i] = InCS;
   j = 0;
   while ((j < n) && (j == i || flag[j] != InCS))
     j++;
   if ((j >= n) && (turn == i || flag[turn] == Idle))
     break; // Acquired lock, Leave while loop
 }
 turn = i;
 -- Critical Section --
 // Release Lock
 j = (turn + 1) % n;
 while (flag[j] == Idle)
   j = (j + 1) % n;
 turn = j;
 flag[i] = Idle;
 -- Remainder Section
} while (1);

The shared variable turn is initialized to a number between 0 and n-1 (inclusive). All elements of the flag array are initialized to Idle. A process can be in any state in the set {Idle, WantIn, InCS}.