Homework (Week 3) Term 2, 2021 Announcements Course Outline Course Schedule Ed Forum Glossary Maths Resources Moodle - Lecture Recordings Assignment 0 Spec TeX Guide Web Submission Assignment 1 Spec TeX Guide Web Submission Assignment 2 Spec Web Submission Java Resources Monitors Video Multithreading Video Semaphores Video Volatile Video Web Tutorials Week 1 Homework Thursday Slides Condensed Thursday Slides Wednesday Slides Condensed Wednesday Slides Week 2 Homework Thursday Code Thursday Notes Thursday Slides Condensed Thursday Slides Wednesday Code Week 3 Homework Promela Code Thursday Code Thursday Slides Condensed Thursday Slides Wednesday Slides Condensed Wednesday Slides Week 4 Homework Thursday Code Thursday Slides Condensed Thursday Slides Wednesday Code and Notes Wednesday Slides Condensed Wednesday Slides Week 5 Homework Thursday Slides Condensed Thursday Slides Wednesday Code and Notes Wednesday Slides Condensed Wednesday Slides Week 7 Homework Thursday Notes Thursday Slides Condensed Thursday Slides Wednesday Notes Wednesday Slides Condensed Wednesday Slides Week 8 Homework Thursday Slides Condensed Thursday Slides Wednesday Code Wednesday Slides Condensed Wednesday Slides Week 9 Homework Thursday Notes Thursday Slides Wednesday Notes Wednesday Slides Condensed Wednesday Slides Week 10 Old Exams Thursday Slides Wednesday Notes Wednesday Slides Old Exam Papers final05s2 final06s2 final07s2 final08s2 final09s2 final10s2 final11s2 final13s2 final14s2 final17s2 Homework (Week 3) Table of Contents 1. Manna-Pnueli Algorithm (2 marks) 2. Szymanski's Algorithm (5 marks) 3. Peterson's algorithm (5 marks) Submission: Due on Thursday, 24th of June, 4pm Sydney Time. Please submit using the CSE Give System either online or via this command on a CSE terminal: give cs3151 hw3 hw3.pdf
Please put all your answers in one PDF file called hw3.pdf. Use of LaTeX is encouraged but not required. Please make your answers as concise as possible. 1 Manna-Pnueli Algorithm (2 marks) Recall the Manna-Pnueli algorithm from Lecture 3. Recall that the if condition and body must be executed as one atomic step. If this were not the case, find an interleaving that violates mutual exclusion. That is, split the if condition into two steps (condition and body) and find an execution such that both processes end up in their critical section simultaneously. 2 Szymanski's Algorithm (5 marks) In this Promela code archive you will find a Promela model of Szymanski's algorithm for three processes, broken down to satisfy LCR, with a particular choice of test order for the various \(\mathbf{await}\) statements. This choice happens to satisfy mutual exclusion and eventual entry (as you may check in Spin), but as mentioned in the lectures, not all choices do. The task here is to twiddle with the test orders and figure out which orderings break the algorithm and which don't. You don't need to test all permutations, but do answer these questions: Can you find any reorderings that break mutual exclusion and/or eventual entry? (You should be able to find at least one). Are there any \(\mathbf{await}\mbox{s}\) that don't seem sensitive to reordering at all? What if you you reorder the tests for all the \(\mathbf{await}\mbox{s}\) in the exact same way? And finally, based on any error trails you obtain, can you form an educated guess about why the test order matters? Explain your findings, informally and in your own words. 3 Peterson's algorithm (5 marks) In the Wednesday lecture of Week 3, Johannes started sketching an assertion network for the two-process version of Peterson's algorithm. This is as far as he got: == Process P ==
forever do
{ ??? }
p1: non-critical section;
{ ??? }
p2: wantp := true;
{ ??? }
p3: last := 1;
{ ??? }
p4: await(wantq = false ∨ last = 2);
{ wantp = true ∧ (wantq = false ∨ last = 2 ∨ Q@q3)}
p5: critical section;
{ ??? }
p6: wantp := false
== Process Q ==
forever do
{ ??? }
q1: non-critical section;
{ ??? }
q2: wantq := true;
{ ??? }
q3: last := 2;
{ ??? }
q4: await(wantp = false ∨ last = 1);
{ wantq = true ∧ (wantp = false ∨ last = 1 ∨ P@p3)}
q5: critical section;
{ ??? }
q6: wantq := false
This presentation shows the program and its associated assertion network together. The idea is that above each location (e.g. q1), the assertion for that location is written in curly brackets. Fill in the missing assertions. Show that the resulting assertion networks for P and Q are inductive and interference free. If you change the assertions at p5 and q5, make sure they still satisfy mutual exclusion; that is, it should hold that: \[ \mathcal{P}(p_5) \wedge \mathcal{Q}(q_5) \wedge P@p_5 \wedge Q@q_5 \Rightarrow \bot \] 2021-08-05 tor 15:45 Announcements RSS
