Hello, dear friend, you can consult us at any time if you have any questions, add WeChat: daixieit

Tutorial 3: Verification

CSSE7610

The exercises below are from Chapter 4 of M. Ben-Ari Principles of Concurrent and Distributed Programming (second edition), 2006.

1. Prove invariants for the first attempt algorithm (from Week 2’s lectures) and use them to show that mutual exclusion holds.

2. Prove the following invariants of Dekker’s algorithm and use them to prove that Dekker’s algorithm satisfies mutual exclusion.

(1) turn = 1 ∨ turn = 2

(2) p3..5 ∨ p8..10 ⇔ wantp

(3) q3..5 ∨ q8..10 ⇔ wantq

Hint: for (2) prove the following two propositions in terms of ⇒:

(i) p3..5 ∨ p8..10 ⇒ wantp

(ii) wantp ⇒ p3..5 ∨ p8..10

3. Extend the proof of mutual exclusion of Dekker’s algorithm from Question 2 to show that ¬ (p8..10 ∧ q8..10) is an invariant.

Use this to prove that the following are also invariants of Dekker’s algo-rithm. (These invariants are required to prove starvation freedom.)

(4) q10 ⇒ turn = 1

(5) p10 ⇒ turn = 2

(6) p4..6 ∧ turn = 2 ⇒ q2..9

(7) q4..6 ∧ turn = 1 ⇒ p2..9

4. Argue whether or not the following hold:

(a) (✷A ∧ ✷B) ⇔ ✷(A ∧ B)

(b) (✸A ∨ ✸B) ⇔ ✸(A ∨ B)

(c) (✷A ∨ ✷B) ⇔ ✷(A ∨ B)

(d) (✸A ∧ ✸B) ⇔ ✸(A ∧ B)

5. The temporal operator leads to, denoted ❀, is defined as: A ❀ B is true in a state si if and only if for all states sj , j ≥ i, if A is true in sj , then B is true in some state sk , k ≥ j. Express ❀ in terms of the other temporal operators.