Commit b5522319 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 ...@@ -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/stack/refinement.v
theories/logrel/F_mu_ref_conc/examples/queue/common.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.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/CG_queue.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_variant.v theories/logrel/F_mu_ref_conc/examples/queue/refinement_variant.v
theories/logrel/F_mu_ref_conc/examples/queue/refinement_original.v theories/logrel/F_mu_ref_conc/examples/queue/refinement_original.v
......
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
From iris.program_logic Require Import weakestpre. 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.program_logic Require Import adequacy ectxi_language.
From iris.proofmode Require Import tactics. From iris.proofmode Require Import tactics.
...@@ -44,14 +43,14 @@ Definition MS_dequeue := ...@@ -44,14 +43,14 @@ Definition MS_dequeue :=
(LetIn (LetIn
(* n = *) (Load (Var 2 (* head *))) (* n = *) (Load (Var 2 (* head *)))
(LetIn (LetIn
(* c = *) (getValue (Unfold (Load ((Var 0 (* n *)))))) (* c = *) (Snd (getValue (Unfold (Load ((Var 0 (* n *)))))))
(Case (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 => *) (* Snd n = InjL Unit => *)
none (* The queue is empty, return none *) none (* The queue is empty, return none *)
(* Snd n = InjR n' => *) (* Snd n = InjR n' => *)
(If (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' *))))) (some (getValue (Fst (Var 0 (* n' *)))))
(App (Var 3 (* try *)) Unit) (App (Var 3 (* try *)) Unit)
) )
...@@ -185,8 +184,6 @@ Definition MS_queue_original : expr := ...@@ -185,8 +184,6 @@ Definition MS_queue_original : expr :=
))). ))).
Section MS_queue. Section MS_queue.
Context `{heapIG Σ, cfgSG Σ}.
(* Check the types of the various functions. *) (* Check the types of the various functions. *)
Lemma getValue_type Γ τ e : Lemma getValue_type Γ τ e :
...@@ -202,10 +199,9 @@ Section MS_queue. ...@@ -202,10 +199,9 @@ Section MS_queue.
econstructor. econstructor.
{ repeat econstructor. } { repeat econstructor. }
econstructor. econstructor.
{ apply getValue_type. { econstructor. apply getValue_type.
eapply (TUnfold _ _ (TNodeBody τ (TVar 0))). eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor. repeat econstructor. }
}
econstructor. econstructor.
- eapply (TUnfold _ _ (TNodeBody τ (TVar 0))). - eapply (TUnfold _ _ (TNodeBody τ (TVar 0))).
repeat econstructor. repeat econstructor.
......
...@@ -143,25 +143,6 @@ Section Queue_refinement. ...@@ -143,25 +143,6 @@ Section Queue_refinement.
iExistsFrame. iExistsFrame.
Qed. 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 : Lemma auth_node_mapsto_Some γ m s ι ω n :
own γ ( (to_agree <$> m) : nodeUR) - own γ ( (to_agree <$> m) : nodeUR) -
node_mapsto γ s ι ω n - node_mapsto γ s ι ω n -
...@@ -432,6 +413,7 @@ Section Queue_refinement. ...@@ -432,6 +413,7 @@ Section Queue_refinement.
simpl. simpl.
iApply wp_pure_step_later; auto. iNext. iAsimpl. iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply (wp_bind (fill [LetInCtx _])). iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [SndCtx])).
iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])). iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)". iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
...@@ -452,12 +434,13 @@ Section Queue_refinement. ...@@ -452,12 +434,13 @@ Section Queue_refinement.
iApply wp_pure_step_later; auto. iNext. simpl. iApply wp_pure_step_later; auto. iNext. simpl.
iApply wp_value. iApply wp_value.
iApply wp_pure_step_later; auto. iNext. iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [CaseCtx _ _])). iApply (wp_bind (fill [CaseCtx _ _])).
iAsimpl. iAsimpl.
iApply (wp_bind (fill [UnfoldCtx])). iApply (wp_bind (fill [UnfoldCtx])).
iApply (wp_bind (fill [LoadCtx])). iApply (wp_bind (fill [LoadCtx])).
iApply (wp_bind (fill [LoadCtx])). iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl. iApply wp_value. simpl.
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)". iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
...@@ -544,7 +527,6 @@ Section Queue_refinement. ...@@ -544,7 +527,6 @@ Section Queue_refinement.
iAsimpl. iAsimpl.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])). iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])).
iApply (wp_bind (fill [LoadCtx])). iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl. iApply wp_value. simpl.
iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts". iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts".
simpl. simpl.
......
...@@ -121,25 +121,6 @@ Section Queue_refinement. ...@@ -121,25 +121,6 @@ Section Queue_refinement.
by iExistsFrame. by iExistsFrame.
Qed. 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 : Lemma auth_node_mapsto_Some γ m s ι n :
own γ ( (to_agree <$> m) : nodeUR) - own γ ( (to_agree <$> m) : nodeUR) -
node_mapsto γ s ι n - node_mapsto γ s ι n -
...@@ -417,6 +398,7 @@ Section Queue_refinement. ...@@ -417,6 +398,7 @@ Section Queue_refinement.
iApply (load_sentinel with "[$]"). iNext. iIntros (s ι sOut) "(#sMapsto & nodeState)". iApply (load_sentinel with "[$]"). iNext. iIntros (s ι sOut) "(#sMapsto & nodeState)".
iApply wp_pure_step_later; auto. iNext. iAsimpl. iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply (wp_bind (fill [LetInCtx _])). iApply (wp_bind (fill [LetInCtx _])).
iApply (wp_bind (fill [SndCtx])).
iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])). iApply (wp_bind (fill [UnfoldCtx; CaseCtx _ _])).
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)". iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
...@@ -435,12 +417,13 @@ Section Queue_refinement. ...@@ -435,12 +417,13 @@ Section Queue_refinement.
iApply wp_pure_step_later; auto. iNext. simpl. iApply wp_pure_step_later; auto. iNext. simpl.
iApply wp_value. iApply wp_value.
iApply wp_pure_step_later; auto. iNext. iApply wp_pure_step_later; auto. iNext.
iApply wp_value.
iApply wp_pure_step_later; auto. iNext.
iApply (wp_bind (fill [CaseCtx _ _])). iApply (wp_bind (fill [CaseCtx _ _])).
iAsimpl.
iApply (wp_bind (fill [UnfoldCtx])). iApply (wp_bind (fill [UnfoldCtx])).
iApply (wp_bind (fill [LoadCtx])). iApply (wp_bind (fill [LoadCtx])).
iApply (wp_bind (fill [LoadCtx])). iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext. iAsimpl.
iApply wp_value. simpl. iApply wp_value. simpl.
iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv". iInv nodesN as (m) "[>authM bigSep]" "closeNodesInv".
iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)". iDestruct (node_lookup with "authM bigSep sMapsto") as "(sentInv & authM & bigSep)".
...@@ -523,7 +506,6 @@ Section Queue_refinement. ...@@ -523,7 +506,6 @@ Section Queue_refinement.
iAsimpl. iAsimpl.
iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])). iApply (wp_bind (fill [CasRCtx (LocV _) (LocV _)])).
iApply (wp_bind (fill [LoadCtx])). iApply (wp_bind (fill [LoadCtx])).
iApply wp_pure_step_later; auto. iNext.
iApply wp_value. simpl. iApply wp_value. simpl.
iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts". iApply (wp_load_frac with "hdPtPts"). iNext. iIntros "hdPtPts".
simpl. 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