Homework (Week 5) 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 5) Table of Contents 1. Reasoning about message passing (4 marks) 2. For an extra challenge (1 marks) 3. Philosophers (4 marks) 4. Fair Merge (4 marks) Submission: Due on Thursday, 15th of July, 4pm Sydney Time. Please submit using the CSE Give System either online or via this command on a CSE terminal: give cs3151 hw5 hw5.pdf philosophers.pml merge.pml
Develop solutions to each of the following problems in Promela, in a separate Promela file. 1 Reasoning about message passing (4 marks) Look at the Levin & Gries-style proof for Example 2 of the Week 5 Wednesday slides. In a similar vein, use the Levin & Gries method to prove \(\{\mathtt{True}\}\;P\;\{x + y = 3\}\), where \(P = P_1 || P_2 || P_3\) is the closed product of the following three processes: Submit your answer in a pdf file called hw5.pdf. 2 For an extra challenge (1 marks) Can you do the previous question using only one shared variable in your assertion network? 3 Philosophers (4 marks) Develop a solution for the dining philosophers problem using only message passing, under the additional restriction that each channel must be connected to exactly one sender and exactly one receiver. By way of a hint, the following things do not work: Having only 5 processes, one for each philosopher. Having only 5 channels, one for each fork. Configure the solution to run forever, in a 5 philosopher scenario. Put all your work in a file called philosophers.pml. Do not include any other files. 4 Fair Merge (4 marks) Develop an algorithm to merge two sequences of data. A process called merge is given three channel parameters of type byte, receives data on two input channels and interleaves the data on the output channel, such that if the two inputs are sorted (in ascending order), then the output is sorted. Try to implement a fair merge that is free from starvation of both input channels when possible. This means that you should try to make sure every input stream is always eventually read from. This requirement will sometimes be impossible to reconcile with the sortedness requirement. If so, keeping the outputs sorted takes priority. For example, if the two input channels transmit infinite streams of 1:s and 2:s, respectively, no 2:s should be sent on the output channel. Assume that the value 255 is a special EOF signal, and no further data will be sent on a channel after EOF is sent. Your merge process should terminate if all data has been transmitted. Assume that an EOF will be sent at the end of the data stream (if it ends). Put all your work in a file called merge.pml. Do not include any other files. 2021-08-05 tor 15:45 Announcements RSS
