Skip to content
GitLab
Commit 49861c8d authored by Zhen Zhang's avatar Zhen Zhang
Browse files

proved a general version; although the mask is still a bit funky

parent 62d9ffd7
Hide whitespace changes
Inline Side-by-side
sync.v
View file @ 49861c8d
......@@ -111,87 +111,77 @@ Section generic.
Proof. apply _. Qed.
Definition atomic_triple'
(α: val → iProp Σ)
(β: val → A → A → val → iProp Σ)
(Ei Eo: coPset)
(f x: val) γ : iProp Σ :=
(∀ P Q, (∀ g g' r, (P ={Eo, Ei}=> gFrag γ g) ★
(gFrag γ g' ★ β x g g' r ={Ei, Eo}=> Q r))
(∀ P Q, (∀ g, (P ={Eo, Ei}=> gFrag γ g ★ α x) ★
(∀ g' r, gFrag γ g' ★ β x g g' r ={Ei, Eo}=> Q r))
-★ {{ P }} f x {{ Q }})%I.
Lemma update_a: ∀ x x': A, (gFullR x ⋅ gFragR x) ~~> (gFullR x' ⋅ gFragR x').
Proof.
intros x x'.
Admitted.
Proof. Admitted.
Definition mk_sync' : val :=
λ: "init" "f_seq",
let: "l" := "init" #() in
let: "lk" := newlock #() in
λ: "x",
acquire "lk";;
let: "v" := "f_seq" "l" "x" in
release "lk";;
"v".
Definition sync : val :=
λ: "f_cons" "f_seq",
let: "l" := "f_cons" #() in
let: "s" := mk_sync #() in
"s" ("f_seq" "l").
Definition seq_spec (f: val) ϕ β :=
∀ (x : val) (g g': A) (Φ: val → iProp Σ) (l: loc),
heapN ⊥ N →
heap_ctx ★ ϕ l g ★ (∀ r g', ϕ l g' -★ β x g g' r -★ Φ r)
⊢ WP f #l x {{ Φ }}.
Definition seq_spec (f: val) (ϕ: val → A → iProp Σ) α β :=
∀ (Φ: val → iProp Σ) (l: val),
{{ True }} f l {{ f', ■ (∀ (x: val) (Φ: val → iProp Σ) (g: A),
heapN ⊥ N →
heap_ctx ★ ϕ l g ★ α x ★ (∀ (v: val) (g': A), ϕ l g' -★ β x g g' v -★ |={⊤}=> Φ v)
⊢ WP f' x {{ Φ }} )}}.
Lemma atomic_spec (f_cons f_seq: val) ϕ β:
heapN ⊥ N → seq_spec f_seq ϕ β →
heap_ctx
⊢ WP mk_sync' f_cons f_seq {{ f, ∃ γ, ∀ x, □ atomic_triple' β ⊤ ⊤ f x γ }}.
Proof.
(* iIntros (HN) "#Hh". repeat wp_let. *)
(* wp_alloc l1 as "Hl1". *)
(* wp_alloc l2 as "Hl2". *)
(* iVs (own_alloc (gFullR (#0, #0) ⋅ gFragR (#0, #0))) as (γ) "Hγ"; first by done. *)
(* wp_let. *)
(* iDestruct (own_op with "Hγ") as "[Hfull Hfrag]". *)
(* iAssert (∃ x1 x2, l1 ↦ x1 ★ l2 ↦ x2 ★ gFull γ (x1, x2))%I with "[-Hfrag]" as "HR". *)
(* { iExists #0, #0. by iFrame. } *)
(* wp_bind (newlock _). iApply newlock_spec=>//. *)
(* iFrame "Hh". *)
(* iFrame "HR". *)
(* iIntros (lk γ') "#Hlk". *)
(* wp_let. *)
(* iClear "Hfrag". (* HFrag should be handled to user? *) *)
(* iVsIntro. iExists γ. iAlways. *)
(* rewrite /is_pcas. *)
(* iIntros (a b P Q) "#H". *)
(* iAlways. iIntros "HP". *)
(* repeat wp_let. *)
(* wp_bind (acquire _). *)
(* iApply acquire_spec. *)
(* iFrame "Hlk". iIntros "Hlked Hls". *)
(* iDestruct "Hls" as (x1 x2) "(Hl1 & Hl2 & HFulla)". *)
(* wp_seq. *)
(* wp_bind ((pcas_seq _) _). *)
(* iApply (pcas_seq_spec with "[Hlked HP Hl1 Hl2 HFulla]"); try auto. *)
(* iFrame "Hh". rewrite /ϕ. iCombine "Hl1" "Hl2" as "Hl". *)
(* instantiate (H2:=(x1, x2)). iFrame. *)
(* iIntros (v xs') "[Hl1 Hl2] Hβ". *)
(* wp_let. wp_bind (release _). wp_let. *)
(* iDestruct ("H" $! (x1, x2) xs' v) as "[Hvs1 Hvs2]". *)
(* iVs ("Hvs1" with "HP") as "Hfraga". (* XXX: this Hfraga might be too strong *) *)
(* iCombine "HFulla" "Hfraga" as "Ha". *)
(* iVs (own_update with "Ha") as "Hb". *)
(* { instantiate (H3:=(gFullR xs' ⋅ gFragR xs')). *)
(* apply update_a. eauto. } *)
Definition cons_spec (f: val) (g: A) ϕ :=
∀ Φ: val → iProp Σ,
(∀ (l: val) (γ: gname), ϕ l g -★ gFull γ g -★ gFrag γ g -★ Φ l)
⊢ WP f #() {{ Φ }}.
(* (* I should have full access to lk now ... shit *) *)
(* iAssert (∃ lkl: loc, #lkl = lk ★ lkl ↦ #true)%I as "Hlkl". *)
(* { admit. } *)
(* iDestruct "Hlkl" as (lkl) "[% Hlkl]". subst. *)
(* wp_store. (* now I just simply discard the things ... *) *)
(* iDestruct (own_op with "Hb") as "[HFullb HFragb]". *)
(* iVs ("Hvs2" with "[Hβ HFragb]"). *)
(* { rewrite /gFrag. by iFrame. } *)
(* by iVsIntro. *)
Admitted.
Lemma atomic_spec (f_cons f_seq: val) (ϕ: val → A → iProp Σ) α β:
∀ (g0: A),
heapN ⊥ N → seq_spec f_seq ϕ α β → cons_spec f_cons g0 ϕ →
heap_ctx
⊢ WP sync f_cons f_seq {{ f, ∃ γ, gFrag γ g0 ★ ∀ x, □ atomic_triple' α β ⊤ ⊤ f x γ }}.
Proof.
iIntros (g0 HN Hseq Hcons) "#Hh". repeat wp_let.
wp_bind (f_cons _). iApply Hcons.
iIntros (l γ) "Hϕ HFull HFrag".
wp_let. wp_bind (mk_sync _).
iApply mk_sync_spec_wp=>//.
iAssert (∃ g: A, ϕ l g ★ gFull γ g)%I with "[-HFrag]" as "HR".
{ iExists g0. by iFrame. }
iFrame "Hh HR".
iIntros (s) "#Hsyncer".
wp_let. rewrite /is_syncer /seq_spec.
wp_bind (f_seq _). iApply wp_wand_r. iSplitR; first by iApply (Hseq with "[]")=>//.
iIntros (f) "%".
iApply wp_wand_r. iSplitR; first by iApply "Hsyncer".
iIntros (v) "#Hrefines".
iExists γ. iFrame. iIntros (x).
iAlways. rewrite /atomic_triple'.
iIntros (P Q) "#Hvss".
rewrite /refines.
iDestruct "Hrefines" as "#Hrefines".
iSpecialize ("Hrefines" $! (of_val x) x P Q).
iApply ("Hrefines" with "[]"); first by rewrite to_of_val.
iAlways. iIntros "[HR HP]". iDestruct "HR" as (g) "[Hϕ HgFull]".
(* we should view shift at this point *)
iDestruct ("Hvss" $! g) as "[Hvs1 Hvs2]".
iApply pvs_wp.
iVs ("Hvs1" with "HP") as "[HgFrag Hα]".
iVsIntro.
iApply H0=>//. (* H0 name is horrible *)
iFrame "Hh Hϕ Hα". iIntros (ret g') "Hϕ' Hβ".
iCombine "HgFull" "HgFrag" as "Hg".
iVs (own_update with "Hg") as "[HgFull HgFrag]".
{ apply update_a. }
iSplitL "HgFull Hϕ'".
- iExists g'. by iFrame.
- by iVs ("Hvs2" $! g' ret with "[HgFrag Hβ]"); first by iFrame.
Qed.
End triple.
End generic.
......@@ -207,46 +197,54 @@ Section atomic_pair.
else #false.
Local Opaque pcas_seq.
Definition α (x: val) : iProp Σ := (∃ a b: val, x = (a, b)%V)%I.
Definition ϕ (l1 l2: loc) (xs: val * val) : iProp Σ := (l1 ↦ fst xs ★ l2 ↦ snd xs)%I.
Definition ϕ (ls: val) (xs: val * val) : iProp Σ :=
(∃ l1 l2: loc, ls = (#l1, #l2)%V ★ l1 ↦ fst xs ★ l2 ↦ snd xs)%I.
Definition β (a b: val) (xs xs': val * val) (v: val) : iProp Σ :=
(■ ((v = #true ∧ fst xs = a ∧ snd xs = a ∧ fst xs' = b ∧ snd xs' = b) ∨
(v = #false ∧ (fst xs ≠ a ∨ snd xs ≠ a) ∧ xs = xs')))%I.
Definition β (ab: val) (xs xs': val * val) (v: val) : iProp Σ :=
(■ ∃ a b: val,
ab = (a, b)%V ∧
((v = #true ∧ fst xs = a ∧ snd xs = a ∧ fst xs' = b ∧ snd xs' = b) ∨
(v = #false ∧ (fst xs ≠ a ∨ snd xs ≠ a) ∧ xs = xs')))%I.
Local Opaque β.
Lemma pcas_seq_spec (a b: val) (xs xs': val * val) ls:
∀ (Φ: val → iProp Σ) (l1 l2: loc),
heapN ⊥ N → to_val ls = Some (#l1, #l2)%V →
heap_ctx ★ ϕ l1 l2 xs ★ (∀ v xs', ϕ l1 l2 xs' -★ β a b xs xs' v -★ Φ v)
⊢ WP pcas_seq ls (a, b) {{ Φ }}.
Lemma pcas_seq_spec: seq_spec N pcas_seq ϕ α β.
Proof.
rewrite /ϕ.
iIntros (Φ l1 l2 HN Hls) "(#Hh & (Hl1 & Hl2) & HΦ)".
wp_value. iVsIntro.
wp_seq. repeat wp_let.
subst. wp_proj. wp_load.
wp_proj. wp_op=>[?|Hx1na].
rewrite /seq_spec.
intros Φ l.
iIntros "!# _". wp_seq. iVsIntro. iPureIntro. clear Φ.
iIntros (x Φ g HN) "(#Hh & Hg & Hα & HΦ)".
rewrite /ϕ /α.
iDestruct "Hg" as (l1 l2) "(% & Hl1 & Hl2)".
iDestruct "Hα" as (a b) "%".
subst. destruct g as (x1, x2). simpl.
wp_let. wp_proj. wp_load. wp_proj.
wp_op=>[?|Hx1na].
- subst.
wp_if. wp_proj. wp_load. wp_proj.
wp_op=>[?|Hx2na]. subst.
+ wp_if. wp_proj. wp_proj. wp_store. wp_proj. wp_proj. wp_store.
iDestruct ("HΦ" $! #true (b, b)) as "H".
iApply ("H" with "[Hl1 Hl2]"); first by iFrame.
iDestruct ("HΦ" $! #true (b, b)) as "HΦ".
iApply ("HΦ" with "[Hl1 Hl2]").
{ iExists l1, l2. by iFrame. }
rewrite /β.
iPureIntro. left. eauto.
iPureIntro. exists a, b. split; first done. left. eauto.
+ wp_if.
iDestruct ("HΦ" $! #false xs) as "H".
iApply ("H" with "[Hl1 Hl2]"); first by iFrame.
iDestruct ("HΦ" $! #false (a, x2)) as "H".
iApply ("H" with "[Hl1 Hl2]").
{ iExists l1, l2. by iFrame. }
rewrite /β.
iPureIntro. right. eauto.
iPureIntro. exists a, b. split; first done. right. eauto.
- subst.
wp_if.
iDestruct ("HΦ" $! #false xs) as "H".
iApply ("H" with "[Hl1 Hl2]"); first by iFrame.
iDestruct ("HΦ" $! #false (x1, x2)) as "H".
iApply ("H" with "[Hl1 Hl2]").
{ iExists l1, l2. by iFrame. }
rewrite /β.
iPureIntro. right. eauto.
iPureIntro. exists a, b. split; first done. right. eauto.
Qed.
Definition is_pcas γ (f: val): iProp Σ :=
......
Supports Markdown
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