Homework (Week 7) 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 7) Table of Contents 1. Compositional Verification, I (6 marks) 2. Compositional Verification, II (6 marks) Submission: Due on Thursday, 22nd of July, 4pm Sydney Time. Please submit using the CSE Give System either online or via this command on a CSE terminal: give cs3151 hw6 hw6.pdf
Please put all your answers in one PDF file called hw6.pdf. Use of LaTeX is encouraged but not required. Please make your answers concise. 1 Compositional Verification, I (6 marks) The compositional method requires channels to be unidirectional, connecting at most two processes. For systems where channels connect three or more processes, the compositional proof method is unsound, as the following "proof" will illustrate. Recall the following synchronous message passing system, that we verified using the Levin & Gries method in homework 5: Use the compositional method to prove the following bogus Hoare triple: \[ \{ \top \}\ P_1\ \|\ P_2\ \|\ P_3\ \{ \bot \}\] Hint: make the local annotations at the terminal locations contradict each other, then use the consequence rule. That would still be a valid Hoare triple if \(P_1\ \|\ P_2\ \|\ P_3\) didn't terminate. Just to be sure, use the AFR method to check that \(P_1\ \|\ P_2\ \|\ P_3\) is deadlock-free. You don't have to be explicit about how your proof obligations are discharged, but do show your assertion network, how and when you update your local auxiliary variables, and your global invariant. 2 Compositional Verification, II (6 marks) For bidirectional channels—i.e., channels that two processes can both send and receive on—the compositional proof method is instead embarrasingly incomplete, as the following exercise demonstrates. Sketch a proof using your choice of Levin & Gries, AFR or Floyd's method of the following Hoare triple: \[ \{ \top \}\ P_1\ \|\ P_2\ \{ x=1 \}\] Again, you don't have to be explicit about how your proof obligations are discharged, but do show how you annotate the transition diagrams. Now attempt to prove \[ \{ \top \}\ P_1\ \|\ P_2\ \{ x=1 \}\] using the compositional proof method. Argue that it's impossible to do so. You don't have to formally prove that it's impossible, but Vincent should find your argument convincing. 2021-08-05 tor 15:45 Announcements RSS
