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

3
From iris.program_logic Require Export hoare weakestpre pviewshifts.
Zhen Zhang's avatar
Zhen Zhang committed
4
5
6
7
From iris.prelude Require Export coPset.
Import uPred.

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

10
  Definition atomic_triple_base
Zhen Zhang's avatar
Zhen Zhang committed
11
12
13
             (α: A  iProp Σ) (* atomic pre-condition *)
             (β: A  val _  iProp Σ) (* atomic post-condition *)
             (Ei Eo: coPset) (* inside/outside masks *)
14
15
16
17
18
19
             (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
20

21
22
  (* 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
23
24
25

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