Commit 390663b1 authored by Simon Friis Vindum's avatar Simon Friis Vindum

Simplify MS-queue code

parent 4911a6e6
......@@ -64,7 +64,6 @@ theories/logrel/F_mu_ref_conc/examples/stack/FG_stack.v
theories/logrel/F_mu_ref_conc/examples/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/queue/common.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/MS_queue_alt.v
theories/logrel/F_mu_ref_conc/examples/queue/CG_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_variant.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_original.v
......@@ -96,6 +95,7 @@ theories/logatom/flat_combiner/peritem.v
theories/logatom/flat_combiner/atomic_sync.v
theories/logatom/flat_combiner/misc.v
theories/logatom/snapshot/spec.v
theories/logatom/snapshot/atomic_snapshot.v
theories/logatom/conditional_increment/spec.v
theories/logatom/conditional_increment/cinc.v
theories/logatom/rdcss/rdcss.v
......
From iris.proofmode Require Import tactics.
From iris.program_logic Require Import weakestpre.
From iris_examples.logrel.F_mu_ref_conc Require Import examples.lock.
From iris.program_logic Require Import adequacy ectxi_language.
From iris.proofmode Require Import tactics.
......@@ -44,14 +43,14 @@ Definition MS_dequeue :=
(LetIn
(* n = *) (Load (Var 2 (* head *)))
(LetIn
(* c = *) (getValue (Unfold (Load ((Var 0 (* n *))))))
(* c = *) (Snd (getValue (Unfold (Load ((Var 0 (* n *)))))))
(Case
(Unfold (Load (Load (Snd (Var 0 (* c *)))))) (* Get next node after sentinel *)
(Unfold (Load (Load (Var 0 (* c *))))) (* Get next node after sentinel *)
(* Snd n = InjL Unit => *)
none (* The queue is empty, return none *)
(* Snd n = InjR n' => *)
(If
(CAS (Var 5 (* head *)) (Var 2 (* n *)) (Load (Snd (Var 1 (* c *)))))
(CAS (Var 5 (* head *)) (Var 2 (* n *)) (Load (Var 1 (* c *))))
(some (getValue (Fst (Var 0 (* n' *)))))
(App (Var 3 (* try *)) Unit)
)
......@@ -185,8 +184,6 @@ Definition MS_queue_original : expr :=
))).
Section MS_queue.
Context `{heapIG Σ, cfgSG Σ}.
(* Check the types of the various functions. *)
Lemma getValue_type Γ τ e :
......@@ -202,10 +199,9 @@ Section MS_queue.
econstructor.
{ repeat econstructor. }
econstructor.
{ apply getValue_type.
{ econstructor. apply getValue_type.
eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
}
repeat econstructor. }
econstructor.
- eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor.
......
......@@ -143,25 +143,6 @@ Section Queue_refinement.
iExistsFrame.
Qed.
Lemma insert_node γ κ ω toS toT s ι n m :
m !! s = None -
own κ ( (to_agree <$> m) : nodeUR) -
map_map γ κ toS toT m -
nodeInv γ κ ι ω toS toT s n
==
own κ ( (to_agree <$> (<[s := (ι, ω, n)]> m)) : nodeUR)
map_map γ κ toS toT (<[s := (ι, ω, n)]> m)
node_mapsto κ s ι ω n.
Proof.
iIntros "% auth mon sentInv".
iMod (own_update with "auth") as "[auth frag]".
{ apply (mapUR_alloc _ s). rewrite lookup_fmap. rewrite a. done. }
rewrite fmap_insert.
iFrame.
iApply big_sepM_insert; first done.
iExistsFrame.
Qed.
Lemma auth_node_mapsto_Some γ m s ι ω n :
own γ ( (to_agree <$> m) : nodeUR) -
node_mapsto γ s ι ω n -
......@@ -432,6 +413,7 @@ Section Queue_refinement.
simpl.
iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [SndCtx])).
iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
......@@ -452,12 +434,13 @@ Section Queue_refinement.
iApply wp_pure_step_later; auto. iNext. simpl.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [CaseCtx _ _])).
iAsimpl.
iApply (wp_bind (fill [UnfoldCtx])).
iApply (wp_bind (fill [LoadCtx])).
iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
......@@ -544,7 +527,6 @@ Section Queue_refinement.
iAsimpl.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])).
iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts".
simpl.
......
......@@ -121,25 +121,6 @@ Section Queue_refinement.
by iExistsFrame.
Qed.
Lemma insert_node γ κ toS s ι n m :
m !! s = None -
own κ ( (to_agree <$> m) : nodeUR) -
map_map γ κ toS m -
nodeInv γ κ ι toS s n
==
own κ ( (to_agree <$> (<[s := (ι, n)]> m)) : nodeUR)
map_map γ κ toS (<[s := (ι, n)]> m)
node_mapsto κ s ι n.
Proof.
iIntros "% auth mon sentInv".
iMod (own_update with "auth") as "[auth frag]".
{ apply (mapUR_alloc _ s). rewrite lookup_fmap. rewrite a. done. }
rewrite fmap_insert.
iFrame.
iApply big_sepM_insert; first done.
iExistsFrame.
Qed.
Lemma auth_node_mapsto_Some γ m s ι n :
own γ ( (to_agree <$> m) : nodeUR) -
node_mapsto γ s ι n -
......@@ -417,6 +398,7 @@ Section Queue_refinement.
iApply (load_sentinel with "[$]"). iNext. iIntros (s ι sOut) "(#sMapsto & nodeState)".
iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [SndCtx])).
iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
......@@ -435,12 +417,13 @@ Section Queue_refinement.
iApply wp_pure_step_later; auto. iNext. simpl.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [CaseCtx _ _])).
iAsimpl.
iApply (wp_bind (fill [UnfoldCtx])).
iApply (wp_bind (fill [LoadCtx])).
iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iAsimpl.
iApply wp_value. simpl.
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
......@@ -523,7 +506,6 @@ Section Queue_refinement.
iAsimpl.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])).
iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts".
simpl.
......
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