Commit 7ae12caf authored by Zhen Zhang's avatar Zhen Zhang

More docs

parent 630bae21
From iris.program_logic Require Export weakestpre hoare. From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import dec_agree frac. From iris.algebra Require Import dec_agree frac.
From iris_atomic Require Import atomic sync misc. From iris_atomic Require Import atomic sync misc.
Definition syncR := prodR fracR (dec_agreeR val). Definition syncR := prodR fracR (dec_agreeR val). (* track the local knowledge of ghost state *)
Class syncG Σ := sync_tokG :> inG Σ syncR. Class syncG Σ := sync_tokG :> inG Σ syncR.
Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)]. Definition syncΣ : gFunctors := #[GFunctor (constRF syncR)].
...@@ -40,7 +39,7 @@ Section atomic_sync. ...@@ -40,7 +39,7 @@ Section atomic_sync.
( (v: val) (g': A), ( (v: val) (g': A),
ϕ l g' - β x g g' v ={E}= Φ v) ϕ l g' - β x g g' v ={E}= Φ v)
WP f' x @ E {{ Φ }} )}}. WP f' x @ E {{ Φ }} )}}.
(* XXX (zhen): The linear VS in the above post-condition is for the final step (* The linear view shift in the above post-condition is for the final step
of computation. The client side of such triple will have to prove that the of computation. The client side of such triple will have to prove that the
specific post-condition he wants can be lvs'd from whatever threaded together specific post-condition he wants can be lvs'd from whatever threaded together
by magic wands. The library side, when proving seq_spec, will always have by magic wands. The library side, when proving seq_spec, will always have
...@@ -69,9 +68,7 @@ Section atomic_sync. ...@@ -69,9 +68,7 @@ Section atomic_sync.
iIntros (f') "#Hsynced". iIntros (f') "#Hsynced".
iExists γ. iFrame. iExists γ. iFrame.
iIntros (x). iAlways. iIntros (x). iAlways.
rewrite /atomic_triple'.
iIntros (P Q) "#Hvss". iIntros (P Q) "#Hvss".
rewrite /synced.
iSpecialize ("Hsynced" $! P Q x). iSpecialize ("Hsynced" $! P Q x).
iIntros "!# HP". iApply wp_wand_r. iSplitL "HP". iIntros "!# HP". iApply wp_wand_r. iSplitL "HP".
- iApply ("Hsynced" with "[]")=>//. - iApply ("Hsynced" with "[]")=>//.
...@@ -92,9 +89,8 @@ Section atomic_sync. ...@@ -92,9 +89,8 @@ Section atomic_sync.
apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. } apply cmra_update_exclusive. by rewrite pair_op dec_agree_idemp. }
iVs ("Hvs2" with "[Hg1 Hβ]"). iVs ("Hvs2" with "[Hg1 Hβ]").
{ iExists g'. iFrame. } { iExists g'. iFrame. }
iVsIntro. iSplitL "Hg2 Hϕ'". iVsIntro. iSplitL "Hg2 Hϕ'"; last done.
* iExists g'. by iFrame. iExists g'. by iFrame.
* done.
- iIntros (?) "?". by iExists g0. - iIntros (?) "?". by iExists g0.
Qed. Qed.
......
(* Flat Combiner *)
From iris.program_logic Require Export weakestpre saved_prop. From iris.program_logic Require Export weakestpre saved_prop.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
......
(* Miscellaneous lemmas *)
From iris.program_logic Require Export weakestpre. From iris.program_logic Require Export weakestpre.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang Require Import proofmode notation.
From iris.algebra Require Import auth frac gmap dec_agree upred_big_op. From iris.algebra Require Import auth frac gmap dec_agree upred_big_op.
From iris.prelude Require Import countable. From iris.prelude Require Import countable.
From iris.program_logic Require Import auth. From iris.program_logic Require Import auth.
Import uPred. Import uPred.
Section lemmas. Section lemmas.
Lemma op_some: {A: cmraT} (a b: A), Some a Some b = Some (a b).
Proof. done. Qed.
Lemma invalid_plus: (q: Qp), ¬ (1 + q)%Qp.
Proof.
intros q H.
apply (Qp_not_plus_q_ge_1 q).
done.
Qed.
Lemma pair_l_frac_update (g g': val):
((1 / 2)%Qp, DecAgree g) ((1 / 2)%Qp, DecAgree g) ~~> ((1 / 2)%Qp, DecAgree g') ((1 / 2)%Qp, DecAgree g').
Proof.
repeat rewrite pair_op dec_agree_idemp.
rewrite frac_op' Qp_div_2.
eapply cmra_update_exclusive.
done.
Qed.
Lemma pair_l_frac_op (p q: Qp) (g g': val):
(((p, DecAgree g') (q, DecAgree g'))) ~~> ((p + q)%Qp, DecAgree g').
Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
Lemma pair_l_frac_op' (p q: Qp) (g g': val): Lemma pair_l_frac_op' (p q: Qp) (g g': val):
((p + q)%Qp, DecAgree g') ~~> (((p, DecAgree g') (q, DecAgree g'))). ((p + q)%Qp, DecAgree g') ~~> (((p, DecAgree g') (q, DecAgree g'))).
Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed. Proof. by rewrite pair_op dec_agree_idemp frac_op'. Qed.
......
(* Coarse-grained syncer *)
From iris.program_logic Require Export weakestpre hoare. From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang proofmode notation.
From iris.heap_lang Require Import proofmode notation.
From iris.heap_lang.lib Require Import spin_lock. From iris.heap_lang.lib Require Import spin_lock.
From iris.algebra Require Import dec_agree frac. From iris.algebra Require Import dec_agree frac.
From iris_atomic Require Import sync. From iris_atomic Require Import sync.
......
(* Syncer spec *)
From iris.program_logic Require Export weakestpre hoare. From iris.program_logic Require Export weakestpre hoare.
From iris.heap_lang Require Export lang. From iris.heap_lang Require Export lang.
From iris.heap_lang Require Import proofmode notation. From iris.heap_lang Require Import proofmode notation.
......
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