关键词 > COMP3151/9154
COMP3151/9154 Homework 2
发布时间：2023-08-24
Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit
COMP3151/9154
Homework (Week 2)
Due: 9:00 am Tue 13 June 2023
Submission: Please put all your answers in one PDF file called hw2.pdf . Use of LaTeX is encouraged but not required. Please make your answers as concise as possible. This homework should not be more than a few pages. See the course Moodle page for the submission location. Late submissions will not be accepted. Solutions to this homework will be discussed in the tutorial immediately following the due date, and your participation mark will depend on your ability to present your answer if called upon in the tutorial.
1. Suppose x,y,z are variables shared with other processes.
(a) The following statement inside a process will not run atomically in most programming languages, although that is how SPIN will treat it.
Rewrite the statement as a sequence of statements that satisfy the lim- ited critical reference restriction, so that SPIN simulates the expected behaviour:
x = y + z
(b) Explain why we should not consider the guards in the following nonde- terministic program as satisfying the limited critical reference assumption:
if
:: x > 0 → x = 0
:: y > 0 → x = 0
:: z > 0 → y = 0
:: else → skip
fi
(c) Consider two ways we could rewrite the program in (b). The first one reads the variables into local copies before the if statement. The second considers the cases one by one, using nested if statements. Do these two approaches have the same meaning in a concurrent setting?
2. We discussed in class that the COUNTERS program has a run where n = 2 at termination. Use SPIN to discover a run on which this happens, and then write a brief explanation of how this is possible. (Don’t just repeat the whole interleaving, try to give a succinct description of what is going on.)
3. Write SPIN specifications for the following, and use SPIN to determine whether they are true of the COUNTERS program. (Hint, in some cases, you may need to use SPIN to check the negation of the property!)
(a) If ever n = 10, we will have n ≥ 10 at all future times.
(b) If ever n = 10 and process 1 has terminated, then the final value of n will be at least 10.
(c) There is a run where at some point of time, n = 10 and both processes have i = 6.
4. Consider a situation where a row of n male frogs face off against a row of n female frogs at opposite ends of a bridge, with enough space between them for one frog. They would all like to get to the other side. Frogs can make the following two types of moves: (1) if there is an empty space immediately ahead of them, move into it, and (2) if there is a frog ahead of them, and an empty space immediately after that frog, jump over the one ahead and land in the empty space. (For the purposes of this exercise frogs are not allowed to jump on top of other frogs, and can’t jump over more than one frog.) Model this scenario in Promela for n = 3, and use Spin’s counter-example capabilities to find a sequence of moves that get all the frogs across to the other side of the bridge from where they start. (Submit both your Promela code and a succinct description of the solution.)
Frog Puzzle:
✒←✑
One Step of the Frog Puzzle (after the second female hops over the first) :
✓M✏✓M✏✓M✏✓M✏
Final State of the Frog Puzzle:
✓✏✓✏✓✏✓✏
✓✏✓✏F
✓M✏
5. Consider the following concurrent program:
|
var wantp , wantq ← False, False |
|
|
forever do p1 wantp ← True; p2 await wantq = False; p3 wantp ← False |
forever do q1 wantq ← True; q2 await wantp = False; q3 wantq ← False |
Draw its state transition diagram.
