atomic.v 816 Bytes
Newer Older
Zhen Zhang's avatar
Zhen Zhang committed
1 2 3 4 5
From iris.program_logic Require Export hoare weakestpre pviewshifts ownership.
From iris.prelude Require Export coPset.
Import uPred.

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

8
  Definition atomic_triple_base
Zhen Zhang's avatar
Zhen Zhang committed
9 10 11
             (α: A  iProp Σ)
             (β: A  val _  iProp Σ)
             (Ei Eo: coPset)
12 13 14 15 16 17
             (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
18

19 20
  (* 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
21 22 23

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