First Mini-project

- The mini-project is supposed to be solved in groups of two or
three students and short reports should be posted on the intranet by
the stated deadline.
**Late submissions will not be accepted.** - The solutions of different groups must be independent and sharing
parts of the code or the text of the report is
**strictly forbidden**. - The mini-project will account for 30% of your final mark for the course.
- The deadline for delivering the first mini-project is Wednesday, 6 May, at 23:00.

- have read the introduction and Section 7.2 in the book and
- have installed and can run either the CWB or the CWB-NC (recommended) on your laptop.

Your tasks are as follows.

- 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.
- 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.
- 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.
- 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)?
- 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.
- 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.
- Finish your report by briefly commenting on what was your experience working with the tool.
- 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 >

b_{i} := true

while (k != i) {

while (b_{1-i}) {}

k := i

}

< critical section >

b_{i} := false

}

*Notice that there are 3 shared variables: b _{0} , b_{1} , and k.*