关键词 > COMP3151/9154

COMP3151/9154 Homework 3

发布时间：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 3)

Due: 9:00 am Mon 19 June 2023

Submission: Please put all your answers in one PDF file. 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. Solu- tions 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. Mutual exclusion: Use Spin to show that the following Manna-Pnueli program, discussed in lectures, is not correct if we do not treat the if statements as atomic.

Manna-Pnueli Algorithm

integer wantp, wantq — 0, 0

forever do

p1 non-critical section

p2 if wantq = -1

then wantp — -1 else wantp — 1

p3 await wantq wantp p4 critical section

p5 wantp — 0

forever do

non-critical section if wantp = -1

then wantq — 1

else wantq — -1

await wantq -wantp critical section

wantq — 0

(To do this, rewrite the if statement so that it satisfies the Limited Crit- ical Reference assumption. ) What about the await statements? Does it matter if they are atomic or not? (Give a reason for your answer.)

2. Hoare Logic: Show the correctness of the following Hoare logic assertion (a variant of the example we discussed in class)

{True}i = 0; s = 0; while i 三 n do {s = s+i; i = i+1 } {s = n()}

where all variables are of type Integer. To do so, show that the following assertions for the transitions are correct:

. {True} i = 0 {i = 0}

. {i = 0} s = 0 {i ≤ n + 1 ∧ s =

. {i ≤ n + 1 ∧ s = = s + i {i ≤ n ∧ s =

. {i ≤ n ∧ s = = i + 1 {i ≤ n + 1 ∧ s =

. {i ≤ n + 1 ∧ s = =

Use the method from the Notes on Floyd’s method to give the detailed translation of these statements to a formula, and prove that the formula is valid. The point of this exercise is to emphasize that the correctness of these sorts of statements can essentially be calculated mechanically, modulo the validity checking (Validity checking itself might be hard once quantifiers or more complicated mathematics are involved.)

3. Floyd’s method: Consider the Counters example, with just one process.

n ← 0

i ← 1

while i ≤ 10 do {x ← n;

x ← x + 1; n ← x;

i ← i + 1}

Apply Floyd’s method to prove that this terminates with n = 10.

4. Owicki-Gries: Consider again the Counters example, but now with two processes (each with local variables i and x, so that n is the only shared variable) . Apply the Owicki-Gries method to prove that this terminates with 2 ≤ n ≤ 20.