From e2681e43cc7849d66425d5bc93565e9e177d229a Mon Sep 17 00:00:00 2001 From: Rutger Broekhoff Date: Wed, 24 Jun 2026 19:29:28 +0200 Subject: Initial commit --- theories/lmpmc_queue_proof.v | 362 +++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 362 insertions(+) create mode 100644 theories/lmpmc_queue_proof.v (limited to 'theories/lmpmc_queue_proof.v') diff --git a/theories/lmpmc_queue_proof.v b/theories/lmpmc_queue_proof.v new file mode 100644 index 0000000..fa732cc --- /dev/null +++ b/theories/lmpmc_queue_proof.v @@ -0,0 +1,362 @@ +From iris.program_logic Require Import atomic. +From iris.heap_lang Require Import notation proofmode. +From iris.algebra.lib Require Import excl_auth. +From iris.base_logic.lib Require Import invariants. +From iris.base_logic.lib Require Import invariants mono_nat mono_list. +From iris_named_props Require Import custom_syntax. + +From lmpmc Require fin_queue_spec lmpmc_queue_spec. +From lmpmc Require Import upstream util. + +Section lmpmc_queue. + Context {fq : fin_queue_spec.fin_queue_hl}. + + Definition new : val := λ: <>, + let: "ℓ_q" := fq.(fin_queue_spec.new) #() in ("ℓ_q", "ℓ_q"). + + Definition enqueue : val := (* passing arguments [ℓ_enq data] *) + fq.(fin_queue_spec.enqueue). + + Definition try_dequeue : val := rec: "go" "ℓ_q" := + match: fq.(fin_queue_spec.try_dequeue) "ℓ_q" with + InjL "v" => + SOME "v" + | InjR "mℓ_nextq" => + match: "mℓ_nextq" with + NONE => NONE + | SOME "ℓ_nextq" => "go" "ℓ_nextq" + end + end. + + Definition link : val := (* passing arguments [ℓ_enq1 ℓ_deq2] *) + fq.(fin_queue_spec.finalize). + + Section proofs. + Context `{!heapGS Σ} {fqp : fin_queue_spec.fin_queue_iris Σ fq}. + + Record node := Node { ℓ_node : loc; vs_node : list val }. + Add Printing Constructor node. + Definition linked_single_queue_repr (n : node) (mℓ_nextq : option loc) : iProp Σ := + fqp.(fin_queue_spec.queue_repr fq) n.(ℓ_node) n.(vs_node) (loc_to_val <$> mℓ_nextq). + + Definition chain := list node. + Definition queue_repr ℓ_deq ℓ_enq (cvs : list val) : iProp Σ := + ∃ (c : chain), + ⌜length c > 0⌝ ∗ ⌜ℓ_node <$> head c = Some ℓ_deq⌝ ∗ + ⌜ℓ_node <$> last c = Some ℓ_enq⌝ ∗ ⌜cvs = c ≫= vs_node⌝ ∗ + [∗ list] i ↦ l ∈ c, linked_single_queue_repr l (ℓ_node <$> c !! S i). + + #[global] Instance queue_repr_timeless ℓ_deq ℓ_enq cvs : Timeless (queue_repr ℓ_deq ℓ_enq cvs) := _. + + Lemma new_spec : + {{{ True }}} + new #() + {{{ (ℓ_deq ℓ_enq : loc), RET (#ℓ_deq, #ℓ_enq); queue_repr ℓ_deq ℓ_enq [] }}}. + Proof. + iIntros (Φ _) "HΦ". iUnfold new. wp_pures. + wp_apply (fqp.(fin_queue_spec.new_spec fq) with "[//]"). + iIntros (ℓ) "H". wp_pures. iModIntro. iApply "HΦ". + unfold queue_repr. iExists [Node ℓ []]. + iFrame. iSimplifyEq. by iSplit; first (iPureIntro; lia). + Qed. + + Lemma enqueue_spec (ℓ_enq : loc) (data : val) : + ⊢ <<{ ∀∀ ℓ_deq cvs, queue_repr ℓ_deq ℓ_enq cvs }>> + enqueue #ℓ_enq data @ ∅ + <<{ queue_repr ℓ_deq ℓ_enq (cvs ++ [data]) | RET #() }>>. + Proof. + iIntros "%Φ AU". iUnfold enqueue. + + wp_bind (fin_queue_spec.enqueue _ _ _)%E. + awp_apply fqp.(fin_queue_spec.enqueue_spec fq). + rewrite /atomic_acc /=. + iMod "AU" as "(%ℓ_deq & %cvs & (%c & %Hclen & %Hhead & %Hlast & %Hcvs & Hqs) & Hclose)". + iModIntro. + + destruct (last c) as [n_last|] eqn:Hlastn; last done. + iExists n_last.(vs_node). + + apply last_Some in Hlastn as [c' ->]. + iDestruct (big_sepL_insert_acc _ _ (length c') with "Hqs") as "[Hnode Hrepr]". + { by rewrite lookup_app_r // Nat.sub_diag. } + iSimplifyEq. iUnfold linked_single_queue_repr in "Hnode". + + rewrite lookup_app_r; last lia. + replace (S (length c') - length c') with 1 by lia. + simplify_eq/=. iFrame. + + iSplit. + - iDestruct "Hclose" as "[Hclose _]". + iIntros "Hnode". + iDestruct ("Hrepr" with "[Hnode //]") as "Hrepr". + rewrite list_insert_id; last first. + { by rewrite lookup_app_r // Nat.sub_diag. } + iMod ("Hclose" with "[$Hrepr]") as "AU". + { by rewrite last_snoc. } + done. + - iDestruct "Hclose" as "[_ Hclose]". + iIntros "Hnode". + + set n_last' := Node n_last.(ℓ_node) (n_last.(vs_node) ++ [data]). + set c := c' ++ [n_last']. + + iDestruct ("Hrepr" with "[Hnode]") as "Hrepr". + { rewrite /linked_single_queue_repr /=. + replace (ℓ_node n_last) with n_last'.(ℓ_node) by done. + by replace (vs_node n_last ++ [data]) with n_last'.(vs_node). } + + iMod ("Hclose" with "[Hrepr]") as "HΦ". + { unfold queue_repr. iExists c. repeat iSplit; try done. + - iPureIntro. rewrite length_app /=. lia. + - iPureIntro. rewrite /c. by destruct c'; simplify_eq/=. + - iPureIntro. by rewrite /c last_snoc. + - iPureIntro. by rewrite /c !bind_app /= !app_nil_r app_assoc. + - rewrite insert_app_r_alt // Nat.sub_diag /=. + iApply (big_sepL_mono with "Hrepr"). + { iIntros (i n Hi) "Hrepr". + rewrite -list_lookup_fmap fmap_app. + replace (ℓ_node <$> [n_last]) with (ℓ_node <$> [n_last']) by done. + by rewrite -fmap_app list_lookup_fmap. } } + + iModIntro. iApply "HΦ". + Qed. + + Lemma try_dequeue_spec (ℓ_deq : loc) : + ⊢ <<{ ∀∀ ℓ_enq cvs, queue_repr ℓ_deq ℓ_enq cvs }>> + try_dequeue #ℓ_deq @ ∅ + <<{ queue_repr ℓ_deq ℓ_enq (tail cvs) | RET (val_opt_hl (head cvs)) }>>. + Proof. + revert ℓ_deq. iLöb as "IH". iIntros (ℓ_deq Φ) "AU". wp_rec. + + awp_apply (fqp.(fin_queue_spec.try_dequeue_spec fq)). + rewrite /atomic_acc /=. + iMod "AU" as "(%ℓ_enq & %cvs & (%c & %Hclen & %Hhead & %Hlast & %Hcvs & Hqs) & Hclose)". iModIntro. + + destruct c as [|n_head c']; first done. + iDestruct (big_sepL_cons with "Hqs") as "[Hnode Hqs]". + simpl. destruct (c' !! 0) as [n_next|] eqn:Hnextq. + - iExists n_head.(vs_node), (Some #n_next.(ℓ_node)). iSplitL "Hnode"; last iSplit. + + simplify_eq/=. by rewrite /linked_single_queue_repr /=. + + simplify_eq/=. iIntros "Hnode". iDestruct "Hclose" as "[Hclose _]". + pose c := n_head :: c'. + iAssert (linked_single_queue_repr n_head (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode". + { by rewrite /linked_single_queue_repr /= Hnextq. } + iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs". + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head ++ c' ≫= vs_node)) with "[$Hqs //]" as "Hrepr". + by iMod ("Hclose" with "Hrepr") as "Hrepr". + + simplify_eq/=. iIntros "Hnode". + destruct n_head.(vs_node) as [|x vs_head'] eqn:Hvs_head. + * simplify_eq/=. iDestruct "Hclose" as "[Hclose _]". + + iDestruct (fqp.(fin_queue_spec.queue_fin_obtain fq) with "Hnode") as "#Hfin". + + pose c := n_head :: c'. + iAssert (linked_single_queue_repr n_head (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode". + { by rewrite /linked_single_queue_repr /= Hnextq Hvs_head /=. } + iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs". + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head ++ c' ≫= vs_node)) with "[$Hqs //]" as "Hrepr". + rewrite Hvs_head /=. iMod ("Hclose" with "Hrepr") as "AU". iModIntro. wp_pures. + clear c c' Hclen Hlast Hnextq Hvs_head. + + awp_apply "IH". rewrite /atomic_acc /=. + iMod "AU" as "(%ℓ_enq' & %cvs' & (%c'' & _ & %Hhead' & %Hlast' & %Hcvs' & Hqs') & Hclose)". + destruct c'' as [|n_head' c'']; first done. + iDestruct (big_sepL_cons with "Hqs'") as "[Hq0 Hqs']". simplify_eq/=. + iEval (rewrite /linked_single_queue_repr /=) in "Hq0". + rewrite -Hhead'. + iDestruct (fqp.(fin_queue_spec.queue_fin_agree fq) with "Hfin Hq0") as %[Hhead Hc'']. + destruct (c'' !! 0) as [n_next'|] eqn:Hc''head; last done. simplify_eq/=. + rewrite -Hc''. clear Hhead' Hc'' n_next n_head. + assert (Hc''len : length c'' > 0). { by apply lookup_lt_Some in Hc''head. } + + iAssert (queue_repr n_next'.(ℓ_node) ℓ_enq' (c'' ≫= vs_node)) with "[$Hqs']" as "Hrepr'". + { iPureIntro. repeat split; try done. + - by rewrite head_lookup Hc''head. + - enough (last c'' = last (n_head' :: c'')) as ->; first done. + destruct c''; first done. by rewrite last_cons_cons. } + + iModIntro. iFrame. iSplit. + -- iIntros "(%d & %Hdlen & %Hdhead & %Hdlast & %Hdvs & Hrepr)". + rewrite Hhead /=. simplify_eq/=. + pose c := n_head' :: d. + iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hq0]" as "Hq0". + { by rewrite /linked_single_queue_repr /= Hhead /= -head_lookup Hdhead /=. } + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hq0 Hrepr]" as "Hrepr". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr (ℓ_node n_head') ℓ_enq' (c'' ≫= vs_node)) with "[$Hrepr]" as "Hrepr". + { iPureIntro. repeat split; try done. + - unfold c. simpl. lia. + - unfold c. rewrite -Hdlast. by destruct d. + - unfold c. rewrite Hdvs. simplify_eq/=. + by rewrite Hhead. } + by iMod ("Hclose" with "Hrepr") as "AU". + -- iIntros "(%d & %Hdlen & %Hdhead & %Hdlast & %Hdvs & Hrepr)". + rewrite Hhead /=. simplify_eq/=. + pose c := n_head' :: d. + iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hq0]" as "Hq0". + { by rewrite /linked_single_queue_repr /= Hhead /= -head_lookup Hdhead /=. } + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hq0 Hrepr]" as "Hrepr". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr (ℓ_node n_head') ℓ_enq' (tail (c'' ≫= vs_node))) with "[$Hrepr]" as "Hrepr". + { iPureIntro. repeat split; try done. + - unfold c. simpl. lia. + - unfold c. rewrite -Hdlast. by destruct d. + - unfold c. rewrite Hdvs. simplify_eq/=. + by rewrite Hhead. } + by iMod ("Hclose" with "Hrepr") as "AU". + * simplify_eq/=. iDestruct "Hclose" as "[_ Hclose]". + + pose n_head' := Node (ℓ_node n_head) vs_head'. + pose c := n_head' :: c'. + + iAssert (linked_single_queue_repr n_head' (ℓ_node <$> c !! S 0)) with "[Hnode]" as "Hnode". + { by rewrite /linked_single_queue_repr /= Hnextq /=. } + iAssert ([∗ list] i↦n ∈ c', linked_single_queue_repr n (ℓ_node <$> c !! S (S i)))%I with "[Hqs //]" as "Hqs". + iAssert ([∗ list] i↦n ∈ c, linked_single_queue_repr n (ℓ_node <$> c !! S i))%I with "[Hnode Hqs]" as "Hqs". + { iApply big_sepL_cons. iFrame. } + iAssert (queue_repr n_head.(ℓ_node) ℓ_enq (vs_node n_head' ++ c' ≫= vs_node)) with "[$Hqs]" as "Hrepr". + { iPureIntro. repeat split; try done. by destruct c'. } + + iMod ("Hclose" with "Hrepr") as "Hrepr". + iModIntro. wp_pures. iApply "Hrepr". + - destruct c'; last done. simplify_eq/=. iClear "Hqs". + rewrite app_nil_r. clear Hclen. + iExists n_head.(vs_node), None. iSplitL "Hnode". + + by rewrite /linked_single_queue_repr /=. + + iSplit. + * iIntros "Hrepr". iDestruct "Hclose" as "[Hclose _]". + iMod ("Hclose" with "[Hrepr]") as "AU". + { iExists [n_head]. iFrame. + repeat iSplit; try done. + - iPureIntro. simpl. lia. + - simpl. by rewrite app_nil_r. } + done. + * iIntros "Hrepr". iDestruct "Hclose" as "[_ Hclose]". + set n_head' := Node n_head.(ℓ_node) (tail n_head.(vs_node)). + iMod ("Hclose" with "[Hrepr]") as "HΦ". + { iExists [n_head']. iFrame. + repeat iSplit; try done. + - iPureIntro. simpl. lia. + - simpl. by rewrite app_nil_r. } + destruct n_head.(vs_node) as [|v vs']; + iModIntro; wp_pures; iApply "HΦ". + Qed. + + (** Linking two queues: + * _______________ _______________ + * / Q1 \ / Q2 \ + * ℓ_deq1 ... ℓ_enq1 <> ℓ_deq2 ... ℓ_enq2 + * \ \ link op args / / + * \ \____________/ / + * \ Q1 <> Q2 / + * \______________________________/ + *) + Lemma link_spec (ℓ_enq1 ℓ_deq2 : loc) : + ⊢ <<{ ∀∀ (b : bool) ℓ_deq1 ℓ_enq2 cvs1 cvs2, queue_repr ℓ_deq1 ℓ_enq1 cvs1 ∗ + if b then queue_repr ℓ_deq2 ℓ_enq2 cvs2 else ⌜ℓ_deq1 = ℓ_deq2 ∧ ℓ_enq1 = ℓ_enq2⌝ }>> + link #ℓ_enq1 #ℓ_deq2 @ ∅ + <<{ if b then queue_repr ℓ_deq1 ℓ_enq2 (cvs1 ++ cvs2) else True | RET #() }>>. + Proof. + iIntros "%Φ AU". iUnfold link. + + wp_bind (fin_queue_spec.finalize _ _ _)%E. + awp_apply fqp.(fin_queue_spec.finalize_spec fq). + rewrite /atomic_acc /=. + iMod "AU" as (b ℓ_deq1 ℓ_enq2 cvs1 cvs2) "[[(%c1 & %Hclen1 & %Hhead1 & %Hlast1 & %Hcvs1 & Hqs1) Hqs2] Hclose]". + iModIntro. + + destruct (last c1) as [n_last1|] eqn:Hlastn1; last done. + iExists n_last1.(vs_node). + + apply last_Some in Hlastn1 as [c1' ->]. + iDestruct (big_sepL_app with "Hqs1") as "[Hqs1 Hnode]". + iSimplifyEq. iDestruct "Hnode" as "[Hnode _]". + rewrite Nat.add_0_r. + + rewrite lookup_ge_None_2 /=; last first. + { rewrite length_app /=. lia. } + iUnfold linked_single_queue_repr in "Hnode". + iSimplifyEq. iFrame. + + iSplit. + - iDestruct "Hclose" as "[Hclose _]". + iIntros "Hnode". + + iAssert (linked_single_queue_repr n_last1 (ℓ_node <$> (c1' ++ [n_last1]) !! S (length c1'))) with "[Hnode]" as "Hnode". + { rewrite /linked_single_queue_repr !lookup_app_r; last lia. + by assert (S (length c1') - length c1' = 1) as -> by lia. } + + iDestruct (big_sepL_snoc with "[$Hqs1 $Hnode]") as "Hqs1'". + + iPoseProof ("Hclose" with "[$Hqs1' $Hqs2]") as "Hqs". + { iPureIntro. repeat split; try done. by rewrite last_app. } + done. + + - iDestruct "Hclose" as "[_ Hclose]". + iIntros "Hnode". + + destruct b; last by iApply "Hclose". + iDestruct "Hqs2" as "(%c2 & %Hclen2 & %Hhead2 & %Hlast2 & %Hcvs2 & Hqs2)". + + pose c := (c1' ++ [n_last1]) ++ c2. + + iAssert (linked_single_queue_repr n_last1 (ℓ_node <$> c !! S (length c1'))) with "[Hnode]" as "Hnode". + { rewrite /linked_single_queue_repr /c !lookup_app_r; try (rewrite length_app /=; lia). + rewrite length_app /=. assert (S (length c1') - (length c1' + 1) = 0) as -> by lia. + rewrite -head_lookup Hhead2 //=. } + + iDestruct (big_sepL_mono with "Hqs1") as "Hqs1". + { iIntros (i l Hi) "Hrepr". + iAssert (linked_single_queue_repr l (ℓ_node <$> c !! S i))%I with "[Hrepr]" as "Hrepr". + { rewrite /c lookup_app_l // length_app /=. apply lookup_lt_Some in Hi. lia. } + iExact "Hrepr". } + + iDestruct (big_sepL_snoc with "[$Hqs1 $Hnode]") as "Hqs1'". + + iDestruct (big_sepL_mono with "Hqs2") as "Hqs2". + { iIntros (i l Hi) "Hrepr". + iAssert (linked_single_queue_repr l (ℓ_node <$> c !! S (length (c1' ++ [n_last1]) + i)))%I with "[Hrepr]" as "Hrepr". + { rewrite /c length_app /= lookup_app_r length_app /=; last lia. + by assert (S i = S (length c1' + 1 + i) - (length c1' + 1)) as -> by lia. } + iExact "Hrepr". } + iSimplifyEq. + + iDestruct (big_sepL_app with "[$Hqs1' $Hqs2]") as "Hqs". fold c. + rewrite -bind_app -/c. + iMod ("Hclose" with "[Hqs]") as "HΦ". + { iFrame. iPureIntro. repeat split; try done. + - rewrite /c !length_app /=. lia. + - rewrite /c head_app. case_match; last done. congruence. + - rewrite /c last_app. case_match; last done. congruence. } + iModIntro. iApply "HΦ". + Qed. + + End proofs. + +End lmpmc_queue. + +Definition lmpmc_queue_hl (fq : fin_queue_spec.fin_queue_hl) : lmpmc_queue_spec.lmpmc_queue_hl. +Proof. + by refine {| lmpmc_queue_spec.new := new; + lmpmc_queue_spec.enqueue := enqueue; + lmpmc_queue_spec.try_dequeue := try_dequeue; + lmpmc_queue_spec.link := link |}. +Defined. + +Definition lmpmc_queue_iris `{!heapGS Σ} + (fq : fin_queue_spec.fin_queue_hl) + (fqp : fin_queue_spec.fin_queue_iris Σ fq) : lmpmc_queue_spec.lmpmc_queue_iris Σ (lmpmc_queue_hl fq). +Proof. + by refine (lmpmc_queue_spec.LmpmcQueueIris _ _ + (lmpmc_queue_hl fq) _ _ + new_spec + enqueue_spec + try_dequeue_spec + link_spec). +Defined. + +#[global] Typeclasses Opaque queue_repr. -- cgit v1.3