Commit 696f0dbb authored by Zhen Zhang's avatar Zhen Zhang

introduce srv

parent 583562b5
......@@ -23,7 +23,7 @@ Section flat_combiner.
Definition doOp: val :=
λ: "f" "o",
match: !"o" with
InjL "req" => "o" <- InjR ("f" "o")
InjL "req" => "o" <- InjR ("f" "req")
| InjR "_" => #()
......@@ -5,7 +5,7 @@ From iris.prelude Require Import functions.
From iris.algebra Require Import upred_big_op.
From iris.program_logic Require Import saved_prop sts.
From iris.heap_lang Require Import proofmode.
From flatcomb Require Import protocol.
From flatcomb Require Import protocol flat.
Class flatG Σ := FlatG {
flat_stsG :> stsG Σ sts
......@@ -37,3 +37,16 @@ Section proof.
Definition flat_ctx (γ: gname) (l : loc) : iProp Σ :=
( (heapN N) heap_ctx sts_ctx γ N (flat_inv l))%I.
Definition init (l: loc) :=
( γ, flat_ctx γ l sts_ownS γ {[ Init ]} )%I.
Definition req (lo: val) P :=
( γ req (l: loc), lo = #l l InjLV req P req sts_ownS γ {[ Req ]} {[ White ]})%I.
Lemma doOp_spec (l f o: val) P:
Φ: val iProp Σ,
(* lock l *)
req o P
WP doOp f o {{ Φ }}.
From iris.program_logic Require Export weakestpre.
From iris.proofmode Require Import invariants ghost_ownership.
From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import frac excl dec_agree.
Definition srv : val :=
rec: "srv" "f" "p" :=
match: !"p" with
InjL "x" => "p" <- InjR ("f" "x");; "srv" "f" "p"
| InjR "_" => "srv" "f" "p"
Definition mk_srv : val :=
λ: "f",
let: "l" := newlock #() in
let: "p" := ref (InjR #0)%V in
Fork (srv "f" "p");;
rec: "wait" "x" :=
acquire "l";;
"p" <- InjL "x"
match: !"p" with
InjR "r" => "p" <- #0 ;; "r"
| InjL "_" => "wait" "x"
(* play with some algebraic structure to see what fit ... *)
Definition srvR := prodR fracR (dec_agreeR val).
Lemma srv_coincide: (x1 x2: val) (q1 q2: Qp), ((q1, DecAgree x1) (q2, DecAgree x2)) x1 = x2.
intros x1 x2 q1 q2 H. destruct (decide (x1 = x2))=>//.
exfalso. destruct H as [H1 H2].
simpl in H2. apply dec_agree_op_inv in H2.
by inversion H2.
Lemma srv_update: (x1 x2: val), (1%Qp, DecAgree x1) ~~> (1%Qp, DecAgree x2).
Proof. intros. by apply cmra_update_exclusive. Qed.
(* define the gFunctors *)
Class srvG Σ := FlatG { srv_tokG :> inG Σ srvR }.
Definition srvΣ : gFunctors := #[GFunctor (constRF srvR)].
Instance subG_srvΣ {Σ} : subG srvΣ Σ srvG Σ.
Proof. intros [?%subG_inG _]%subG_inv. split; apply _. Qed.
Section proof.
Context `{!heapG Σ, !lockG Σ, !srvG Σ} (N : namespace).
Markdown is supported
0% or
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment