T-106.420 Concurrent programming Example solution for homework assignment 1

1. (a) (x = 5 ∧ y = 2)

(b) Six possible execution orders:

S_{1}; S_{2}; S_{3}; ⊧ (x = 5 ∧ y = 2) S_{1}; S_{3}; S_{2}; ⊧ (x = 2 ∧ y = −3) S_{2}; S_{1}; S_{3}; ⊧ (x = 2 ∧ y = −3) S_{2}; S_{3}; S_{1}; ⊧ (x = 2 ∧ y = −3) S_{3}; S_{1}; S_{2}; ⊧ (x = 2 ∧ y = −3) S_{3}; S_{2}; S_{1}; ⊧ (x = −11 ∧ y = −8)

(c) The await statement never executes. The other statement sets x to − 3. The whole co statement deadlocks with (x = −3 ∧ y = 5)

2. (a) Yes. The final value of x is zero. The last statement executes first, then the other two (in either order).

(b) S_{1}(fails); S_{2}(fails); S_{3}; ⊧ (x = 5) S_{2}(fails); S_{1}(fails); S_{3}; ⊧ (x = 5) S_{1}(fails); S_{3}; S_{2}; ⊧ (x = 2) S_{2}(fails); S_{3}; S_{1}; ⊧ (x = 3) S_{3}; S_{1}; S_{2}; ⊧ (x = 0) S_{3}; S_{2}; S_{1}; ⊧ (x = 0)

3. Initial values that work, and the corresponding final values:

x = {−1, 0, 1} ⊧ x = {−1, 0, 1}

Altogether 6 possible histories.

{(x < −1)} ⊧ S_{1} and S_{3} deadlocks {(x > 1)} ⊧ S_{2} and S_{3} deadlocks