Homework (Week 2) 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 2) Table of Contents 1. No skip (4 marks) 2. Dekker's Algorithm (8 marks) Submission: Due on Thursday, 17th of June, 4pm Sydney Time. Please submit using the CSE Give System either online or via this command on a CSE terminal: give cs3151 hw2 hw2.pdf hw2.pml
1 No skip (4 marks) Consider the following trivial Promela model: byte x = 0;
active proctype P() {
x = 1;
x = 2;
x = 3;
}
ltl skip_2 { <>(x == 1 until x == 3) }
Here we would be surprised if the value of x becomes 3 immediately after being 1. Yet Spin verifies that the property skip_2 holds. Explain why this model nonetheless satisfies skip_2. Also, give an LTL formula that better captures the intent stated above. Submit your answer in a PDF file called hw2.pdf. Use of LaTeX is encouraged but not required. Please make your answers as concise as possible 2 Dekker's Algorithm (8 marks) Dekker's algorithm (aka attempt 5 from the lectures) was presented with two processes. This question explores whether it generalises successfully to three (or more) processes. Write a Promela model for Dekker's algorithm with three processes. Use the same general idea for the pre- and post-protocol with wantX variables and a turn counter (you'll need three wantX:s and three distinct turn values). Make sure your Promela model obeys the limited critical inference restriction. Use Spin to check if your generalisation of Dekker's algorithm satisfies mutual exclusion and eventual entry. Include the LTL properties you used in your Promela file, along with /* comments */ explaining what verification options you used and what the result was. Submit your answer in a Promela file called hw2.pml Hint 1: Feel free to assume that this Promela header file is present in the same directory as your .pml file, if you want to use the same critical section boilerplate as in the lectures. Hint 2: The limited critical inference restriction also applies to the guards of do and if statements. In particular, the following does not obey limited critical inference, because wantp and wantq cannot be checked atomically. do
:: wantp -> ...
:: wantq -> ...
:: else -> ...
od
2021-08-05 tor 15:45 Announcements RSS
