atomic.v 4.24 KB
Newer Older
1
From iris.bi Require Export bi updates.
2
From iris.bi.lib Require Import fixpoint laterable.
3
From stdpp Require Import coPset.
4
From iris.proofmode Require Import tactics.
5
6
Set Default Proof Using "Type".

7
8
9
10
11
12
13
14
15
16
(** atomic_update as a fixed-point of the equation
   AU = ∃ P. ▷ P ∗ □ (▷ P ==∗ α ∗ (α ==∗ AU) ∧ (β ==∗ Q))
 *)
Section definition.
  Context `{BiFUpd PROP} {A B : Type}
    (α : A  PROP) (* atomic pre-condition *)
    (β : A  B  PROP) (* atomic post-condition *)
    (Eo Em : coPset) (* outside/module masks *)
    (Φ : A  B  PROP) (* post-condition *)
  .
17

18
19
20
  Definition atomic_shift (P P' : PROP) : PROP :=
    ( ( E, Eo  E  P ={E, EEm}=  x, α x 
          ((α x ={EEm, E}= P')  ( y, β x y ={EEm, E}= Φ x y)))
21
22
    )%I.

23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
  Lemma atomic_shift_mono P P1 P2:
     (P1 - P2) -  (atomic_shift P P1 - atomic_shift P P2).
  Proof.
    iIntros "#HP12 !# #AS !# * % HP".
    iMod ("AS" with "[% //] HP") as (x) "[Hα Hclose]".
    iModIntro. iExists x. iFrame "Hα". iSplit.
    - iIntros "Hα". iDestruct "Hclose" as "[Hclose _]".
      iApply "HP12". iApply "Hclose". done.
    - iIntros (y) "Hβ". iDestruct "Hclose" as "[_ Hclose]".
      iApply "Hclose". done.
  Qed.

  Definition atomic_update_pre (Ψ : ()  PROP) (_ : ()) : PROP :=
    ( (P : PROP),  P  atomic_shift ( P) (Ψ ()))%I.

  Local Instance atomic_update_pre_mono : BiMonoPred atomic_update_pre.
  Proof.
    constructor.
    - iIntros (P1 P2) "#HP12". iIntros ([]) "AU".
      iDestruct "AU" as (P) "[HP AS]". iExists P. iFrame.
      iApply (atomic_shift_mono with "[HP12]"); last done.
      iAlways. iApply "HP12".
    - intros ??. solve_proper.
  Qed.

  Definition atomic_update_def :=
    bi_greatest_fixpoint atomic_update_pre ().
End definition.

(** Seal it *)
Definition atomic_update_aux : seal (@atomic_update_def). by eexists. Qed.
Definition atomic_update `{BiFUpd PROP} {A B : Type} := atomic_update_aux.(unseal) PROP _ A B.
Definition atomic_update_eq :
  @atomic_update = @atomic_update_def := atomic_update_aux.(seal_eq).

(** Lemmas about AU *)
59
Section lemmas.
Robbert Krebbers's avatar
Robbert Krebbers committed
60
  Context `{BiFUpd PROP} {A B : Type}.
61
62
63
  Implicit Types (α : A  PROP) (β: A  B  PROP) (P : PROP) (Φ : A  B  PROP).

  Local Existing Instance atomic_update_pre_mono.
64

65
66
  (** The ellimination form: an accessor *)
  Lemma aupd_acc α β Eo Em Φ E :
67
    Eo  E 
68
    atomic_update α β Eo Em Φ -
69
    |={E, EEm}=>  x, α x 
70
71
      ((α x ={EEm, E}= atomic_update α β Eo Em Φ) 
       ( y, β x y ={EEm, E}= Φ x y)).
72
  Proof using Type*.
73
74
75
    rewrite atomic_update_eq {1}/atomic_update_def /=. iIntros (HE) "HUpd".
    iPoseProof (greatest_fixpoint_unfold_1 with "HUpd") as "HUpd".
    iDestruct "HUpd" as (P) "(HP & Hshift)".
76
    iMod ("Hshift" with "[% //] HP") as (x) "[Hα Hclose]".
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
    iModIntro. iExists x. iFrame.
  Qed.

  Global Instance aupd_laterable α β Eo Em Φ :
    Laterable (atomic_update α β Eo Em Φ).
  Proof.
    rewrite /Laterable atomic_update_eq {1}/atomic_update_def /=. iIntros "AU".
    iPoseProof (greatest_fixpoint_unfold_1 with "AU") as (P) "[HP #AS]".
    iExists P. iFrame. iIntros "!# HP !>".
    iApply greatest_fixpoint_unfold_2. iExists P. iFrame "#∗".
  Qed.

  Lemma aupd_intro P α β Eo Em Φ :
    Em  Eo  Laterable P 
    P -
     (P - |={Eo, EoEm}=>  x, α x 
      ((α x ={EoEm, Eo}= P)  ( y, β x y ={EoEm, Eo}= Φ x y))) -
    atomic_update α β Eo Em Φ.
  Proof.
    rewrite atomic_update_eq {1}/atomic_update_def /=.
    iIntros (??) "HP #AU".
    iApply (greatest_fixpoint_coind _ (λ _, P)); last done. iIntros "!#" ([]) "HP".
    iDestruct (laterable with "HP") as (P') "[HP' #HPi]". iExists P'. iFrame.
    iIntros "!#" (E HE) "HP'". iDestruct ("HPi" with "HP'") as ">HP {HPi}".
    iApply fupd_mask_frame_diff_open; last
      iMod ("AU" with "HP") as (x) "[Hα Hclose] {AU}"; [done..|].
    iModIntro. iExists x. iFrame. iSplit.
    - iDestruct "Hclose" as "[Hclose _]". iIntros "Hα".
      iApply fupd_mask_frame_diff_close; last (by iApply "Hclose"); done.
    - iDestruct "Hclose" as "[_ Hclose]". iIntros (y) "Hβ".
      iApply fupd_mask_frame_diff_close; last (by iApply "Hclose"); done.
108
109
  Qed.
End lemmas.