ex_05_parallel_add_mul.v 2.64 KB
Newer Older
Robbert Krebbers's avatar
Robbert Krebbers committed
1
2
3
4
5
6
7
8
9
10
(**
In this exercise we consider a variant of the previous exercise. We have a
reference which is initially 0 and two threads running in parallel. One thread
increases the value of the reference by 2, whereas the other multiples the
value of the reference by two. An interesting aspect of this exercise is that
the outcome of this program is non-deterministic. Depending on which thread runs
first, the outcome is either 2 or 4.

Contrary to the earlier exercises, this exercise is nearly entirely open.
*)
Hai Dang's avatar
Hai Dang committed
11
From iris.algebra Require Import auth frac_auth excl.
Robbert Krebbers's avatar
Robbert Krebbers committed
12
13
From iris.base_logic.lib Require Import invariants.
From iris.heap_lang Require Import proofmode notation lib.par.
Ralf Jung's avatar
Ralf Jung committed
14
From exercises Require Import ex_03_spinlock.
Robbert Krebbers's avatar
Robbert Krebbers committed
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35

Definition parallel_add_mul : expr :=
  let: "r" := ref #0 in
  let: "l" := newlock #() in
  (
    (acquire "l";; "r" <- !"r" + #2;; release "l")
  |||
    (acquire "l";; "r" <- !"r" * #2;; release "l")
  );;
  acquire "l";;
  !"r".

(** In this proof we will make use of Boolean ghost variables. *)
Section proof.
  Context `{!heapG Σ, !spawnG Σ, !inG Σ (authR (optionUR (exclR boolC)))}.

  (** The same helping lemmas for ghost variables that we have already seen in
  the previous exercise. *)
  Lemma ghost_var_alloc b :
    (|==>  γ, own γ ( (Excl' b))  own γ ( (Excl' b)))%I.
  Proof.
Hai Dang's avatar
Hai Dang committed
36
37
38
    iMod (own_alloc ( (Excl' b)   (Excl' b))) as (γ) "[??]".
    - by apply auth_both_valid.
    - by eauto with iFrame.
Robbert Krebbers's avatar
Robbert Krebbers committed
39
40
41
42
43
44
45
  Qed.

  Lemma ghost_var_agree γ b c :
    own γ ( (Excl' b)) - own γ ( (Excl' c)) -  b = c .
  Proof.
    iIntros "Hγ● Hγ◯".
    by iDestruct (own_valid_2 with "Hγ● Hγ◯")
Hai Dang's avatar
Hai Dang committed
46
      as %[<-%Excl_included%leibniz_equiv _]%auth_both_valid.
Robbert Krebbers's avatar
Robbert Krebbers committed
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
  Qed.

  Lemma ghost_var_update γ b' b c :
    own γ ( (Excl' b)) - own γ ( (Excl' c)) ==
      own γ ( (Excl' b'))  own γ ( (Excl' b')).
  Proof.
    iIntros "Hγ● Hγ◯".
    iMod (own_update_2 _ _ _ ( Excl' b'   Excl' b') with "Hγ● Hγ◯") as "[$$]".
    { by apply auth_update, option_local_update, exclusive_local_update. }
    done.
  Qed.

  (** *Difficult exercise*: come up with a suitable invariant and prove the spec
  of [parallel_add_mul]. In this proof, you should use Boolean ghost variables,
  and the rules for those as given above. You are allowed to use any number of
  Boolean ghost variables. *)
  Definition parallel_add_mul_inv (r : loc) (γ1 γ2 : gname) : iProp Σ :=
    True%I. (* exercise: replace [True] with something meaningful. *)

  Lemma parallel_add_mul_spec :
    {{{ True }}} parallel_add_mul {{{ z, RET #z;  z = 2  z = 4  }}}.
  Proof.
    (* exercise *)
  Admitted.
End proof.