atomic.v 1.23 KB
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1
2
(* Logically atomic triple *)

Ralf Jung's avatar
Ralf Jung committed
3
4
From iris.base_logic Require Export fancy_updates.
From iris.program_logic Require Export hoare weakestpre.
Zhen Zhang's avatar
Zhen Zhang committed
5
6
7
8
From iris.prelude Require Export coPset.
Import uPred.

Section atomic.
9
  Context `{irisG Λ Σ} (A: Type).
Zhen Zhang's avatar
Zhen Zhang committed
10

Ralf Jung's avatar
Ralf Jung committed
11
12
13
  (* TODO RJ: IMHO it would make more sense to have the outer mask first, after all, that's what the shifts "starts" with. *)
  (* TODO RJ: Don't define atomic_triple_base; everybody should only ever use atomic_triple anyway. *)
  (* TODO RJ: We probably will want to make `A` an implicit parameter. *)
14
  Definition atomic_triple_base
Zhen Zhang's avatar
Zhen Zhang committed
15
16
17
             (α: A  iProp Σ) (* atomic pre-condition *)
             (β: A  val _  iProp Σ) (* atomic post-condition *)
             (Ei Eo: coPset) (* inside/outside masks *)
18
19
20
21
22
23
             (e: expr _) P Q : iProp Σ :=
    ((P ={Eo, Ei}=>  x:A,
                       α x 
                       ((α x ={Ei, Eo}= P) 
                        ( v, β x v ={Ei, Eo}= Q x v))
     ) - {{ P }} e @  {{ v, ( x: A, Q x v) }})%I.
Zhen Zhang's avatar
Zhen Zhang committed
24

25
26
  (* logically atomic triple: <x, α> e @ E_i, E_o <v, β x v> *)
  Definition atomic_triple α β Ei Eo e := ( P Q, atomic_triple_base α β Ei Eo e P Q)%I.
Zhen Zhang's avatar
Zhen Zhang committed
27
28
29

  Arguments atomic_triple {_} _ _ _ _.
End atomic.