Modelling and Verification 2009
First Mini-project

Bureaucratic Information

Literature

Before starting with the mini-project, read Chapter 7 (Introduction and Section 7.2). Note that there is a typo in the pseudocode for Hyman's algorithm in Exercise 7.3 on page 146 (see the errata list for more information).

First Mini-Project: Verification of Mutual Exclusion Algorithms

Before you start working on this mini-project, you should You are asked to provide a very brief report about how you solved the tasks below. There is no need to write any introduction or any additional text, just complete all the tasks below and copy and paste your implementations directly into the report. The report should be delivered as a PDF document.

Your tasks are as follows.

  1. Form a group of at most three students. Write the names and email addresses of all members of your group on the front page of your report.
  2. Model Dekker's algorithm for mutual exclusion in the tool of your choice (the pseudocode of the algorithm can be found here). Copy and paste the CWB or CWB-NC code in your report.
  3. Suggest a high-level specification (Spec) of a mutual exclusion algorithm, write it into your report, and compare it with your implementation (Impl) with respect to the following equivalences/preorders: (a) strong bisimilarity, (b) weak bisimilarity, (c) weak trace equivalence and (d) weak trace preorder.
  4. Write the verification results you achieved in your report and, for each of the equivalences/preorders, comment on why you think the outcome was as it was. Based on these experiments, can you conclude that Dekker's algorithm is correct (i.e. that it guarantees mutual exclusion)?
  5. Model Hyman's algorithm for mutual exclusion in the tool of your choice. (The pseudocode is available below or in Exercise 7.3 on page 146 in the book - note that the book contains an error in the pseudocode on line 5, which has been corrected in the errata list.) Copy and paste the code into your report.
  6. Repeat steps 3 and 4 for Hyman's algorithm. Can you conclude that this algorithm is correct? If not, provide a trace leading to a situation where both processes are in the critical section at the same time. Write your results in the report.
  7. Finish your report by briefly commenting on what was your experience working with the tool.
  8. Compile a single PDF file and post the file on the intranet by the stated deadline.

Hyman's Algorithm (for two processes i=0 and i=1):

while (true) {

< noncritical section >

bi := true

while (k != i) {

while (b1-i) {}

k := i

}

< critical section >

bi := false

}

Notice that there are 3 shared variables: b0 , b1 , and k.