Spec (Warm-up Assignment) Term 2, 2020 Announcements Course Outline Course Schedule Glossary Maths Resources Moodle - BB Collab Piazza Forum 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 Monday Board Recording Slides Condensed Slides Thursday Code Slides Condensed Slides Week 2 Homework Thursday Slides Condensed Slides Week 3 Homework Monday Brownies Promela Samples Slides Condensed Slides Thursday Code Slides Condensed Slides Week 4 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 5 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 7 Homework Monday Slides Condensed Slides Thursday Slides Condensed Slides Week 8 Homework Monday Slides Thursday Slides Week 9 Homework Monday Slides Thursday Slides Week 10 Notes Spec (Warm-up Assignment) Table of Contents 1. Task 2. Deliverables 3. Testing 4. Submission Instructions This assignment is worth 10% and due before the Thursday lecture of Week 3. that is, Thursday June 18th, 17:59:59 local time Sydney. The purpose of this assignment is to ensure that every student in this course is familiar with the tools we will be using for the two major assignments. This assignment has to be done individually. The task involving Spin is supposed to be relatively easy. Finding the assertion network however can be hard. This component serves to (a) re-inforce understanding of the Owicki/Gries method and (b) provide a modest challenge. 1 Task Consider the following algorithm presented in Ben-Ari's notation. Use Spin to verify that Algorithm Y is a solution to the critical section problem. Address all four desiderata given in lecture 2. Encode Algorithm Y as a parallel composition of two transition diagrams. Define an assertion network \(Q\) such that the assertions at the locations representing the critical sections express mutual exclusion. Prove that \(Q\) is inductive. (It is ok to focus on the processes after the initialisation of \(b\). It is not ok to make the assertions at the entry locations unreasonably strong.) Prepare a report that explains your findings. Make it concise and convincing. Liam will have to read almost 50 of them. 2 Deliverables algY.pml faithful implementations of Algorithm Y in Promela. algY.pdf A PDF of your report. Diagrams may be hand-drawn but prose must be typeset, preferably with LaTeX (although not mandatory). List your student ID near the top of the document. The document should describe your efforts, incorporate the previous deliverables, quote some output of Spin as evidence if that is helpful, and contain the Owicki/Gries-style proof. 3 Testing Submissions will be tested on CSE servers. Spin's command line interface is already available. A compatible version of the ispin GUI will be accessible for vlab users with this command: % ~cs3151/bin/ispin
4 Submission Instructions The give command to be run is: % give cs3151 assn0 algY.pml algY.pdf
You may also use the online give interface to submit. Beware of rather tight submission size limits. 2020-08-06 Thu 03:32 Announcements RSS
