Commit bbaecef4 by Jaehwang Jung

strengthen spmc_mp_spec

parent 3f48de33
 ... ... @@ -40,32 +40,36 @@ Definition spmc_mp : expr := let: "flag" := new [ #1] in "flag" <- #0 ;; Fork (Q.(enqueue) ["q"; #1] ;; Q.(enqueue) ["q"; #2] ;; "flag" <-ʳᵉˡ #1 ) ;; Fork (Q.(dequeue) ["q"]);; (repeat: !ᵃᶜ "flag") ;; Q.(dequeue) ["q"]. Fork (**) (**) (Q.(enqueue) ["q"; #1] ;; (**) (**) Q.(enqueue) ["q"; #2] ;; (**) (**) "flag" <-ʳᵉˡ #1 ) ;; (**) (**) Fork (**) (Q.(dequeue) ["q"]);; (**) (**) (**) (repeat: !ᵃᶜ "flag") ;; (**) (**) Q.(dequeue) ["q"] (**) (**) . (** Invariant on the queue state: A successful dequeue consumes a token [◯ 1] and there are only 2 such tokens. *) (** Invariant on the queue state: - A successful dequeue consumes a token [◯ 1]. - There are only 2 such tokens. - Only the values 1 or 2 are enqueued. *) Definition MPInv γg γm q : vProp := ∃ G, Q.(QueueInv) γg q G ∗ ⎡ own γm (● 2%nat) ⎤ ∗ ⎡ own γm (◯ (size G.(com))) ⎤ ⎡ own γm (◯ (size G.(com))) ⎤ ∗ ⌜ ∀ e eV v, G.(Es) !! e = Some eV → eV.(ge_event) = Enq v → v = 1 ∨ v = 2 ⌝ . (** The flag location transfers the knowledge about the enqueue events. *) Definition FlagProtocol γg q s (v : val) : vProp := match s with | false => ⌜v = #0⌝ | true => ⌜v = #1⌝ ∗ ∃ G M e1 e2 eV1 eV2 v1 v2, | true => ⌜v = #1⌝ ∗ ∃ G M e1 e2 eV1 eV2, Q.(QueueLocal) qN γg q G M ∗ ⌜ e1 ≠ e2 ∧ G.(Es) !! e1 = Some eV1 ∧ G.(Es) !! e2 = Some eV2 ∧ eV1.(ge_event) = Enq v1 ∧ eV2.(ge_event) = Enq v2 ∧ eV1.(ge_event) = Enq 1 ∧ eV2.(ge_event) = Enq 2 ∧ e1 ∈ M ∧ e2 ∈ M ⌝ end. Definition FlagInterp γg q : interpO Σ boolProtocol := ... ... @@ -79,7 +83,7 @@ Global Instance FlagInterp_persistent γg q s l γl t b v V : Proof. destruct b; apply _. Qed. Lemma spmc_mp_spec tid : {{{ True }}} spmc_mp @ tid; ⊤ {{{ v, RET #v; ⌜0 < v⌝ }}}. {{{ True }}} spmc_mp @ tid; ⊤ {{{ v, RET #v; ⌜v = 1 ∨ v = 2⌝ }}}. Proof using All. iIntros (Φ) "_ Post". rewrite /spmc_mp. ... ... @@ -98,7 +102,7 @@ Proof using All. as (γf ?) "FPW". iDestruct (GPS_iSP_SWWriter_Reader with "FPW") as "#FPR". iMod (inv_alloc mpinvN _ (MPInv γg γm q) with "[QI ●m]") as "#I". { iNext. iExists ∅. iFrame "QI". iDestruct "●m" as "[\$ \$]". } { iNext. iExists ∅. iFrame "QI". iDestruct "●m" as "[\$ \$]". done. } (* enqueuing thread *) wp_apply (wp_fork with "[FPW]"); [done|..]. ... ... @@ -106,9 +110,9 @@ Proof using All. (* enqueue 1 *) iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]". awp_apply (enqueue_spec with "⊒V QL"); [solve_ndisj|done|]. iInv mpinvN as (G1) "(QI & >●m & >◯m)". iInv mpinvN as (G1) "(QI & >●m & >◯m & >%Hv)". iAaccIntro with "QI". { iFrame. iIntros "QI !> !>". iExists _. iFrame. } { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. } iIntros (V1 G1' enqId1 enq1 Venq1 M1') "(QI & #⊒V1 & #QL1 & %F) !>". set (eV1 := mkGraphEvent enq1 Venq1 M1') in *. rewrite /is_enqueue in F. ... ... @@ -117,18 +121,20 @@ Proof using All. { subst enqId1. rewrite EsG1'. apply lookup_app_1_eq. } iDestruct (view_at_elim with "⊒V1 QL1") as "{QL QL1} QL1". iSplitR "FPW". { iNext. iExists G1'. rewrite -ComG1'. iFrame. } iIntros "_". wp_seq. { iNext. iExists G1'. rewrite -ComG1'. iFrame. iPureIntro. rewrite EsG1'. intros ??? [?|[-> <-]]%lookup_app_1; [by eapply Hv|]. injection 1 as <-. by left. } clear Hv. iIntros "_". wp_seq. (* enqueue 2 *) awp_apply (enqueue_spec with "⊒V QL1"); [solve_ndisj|done|]. iInv mpinvN as (G2) "(QI & >●m & >◯m)". iInv mpinvN as (G2) "(QI & >●m & >◯m & >%Hv)". rewrite QueueInv_graph_master_acc. iDestruct "QI" as "[>Gm QI]". iDestruct (graph_master_consistent with "Gm") as %EGC. iPoseProof (QueueLocal_graph_snap with "QL1") as "Gs". iDestruct (graph_master_snap_included with "Gm Gs") as %SubG1'2. iSpecialize ("QI" with "[\$Gm]"). iAaccIntro with "QI". { iFrame. iIntros "QI !> !>". iExists _. iFrame. } { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. } iIntros (V2 G2' enqId2 enq2 Venq2 M2') "(QI & #⊒V2 & #QL2 & %F) !>". set (eV2 := mkGraphEvent enq2 Venq2 M2') in *. rewrite /is_enqueue in F. ... ... @@ -137,7 +143,9 @@ Proof using All. { subst enqId2. rewrite EsG2'. apply lookup_app_1_eq. } iDestruct (view_at_elim with "⊒V2 QL2") as "{QL2} QL2". iSplitR "FPW". { iNext. iExists G2'. rewrite -ComG2'. iFrame. } { iNext. iExists G2'. rewrite -ComG2'. iFrame. iPureIntro. rewrite EsG2'. intros ??? [?|[-> <-]]%lookup_app_1; [by eapply Hv|]. injection 1 as <-. by right. } iIntros "_". wp_seq. (* set the flag *) iApply (GPS_iSP_SWWrite flagN (FlagInterp γg q) (FlagInterp γg q false) ... ... @@ -145,7 +153,7 @@ Proof using All. [solve_ndisj|done|done|by right|done|..]. { simpl. iSplitL; [|done]. iIntros "!> * % !>". iSplitR; [done|]. iExists G2', M2', enqId1, enqId2, eV1, eV2, _, _. iFrame "QL2". iExists G2', M2', enqId1, enqId2, eV1, eV2. iFrame "QL2". iPureIntro. split_and!; [| |done|done|done| |done]. - subst enqId1 enqId2. have ? : (length (Es G1) < length (Es G1')). ... ... @@ -163,22 +171,22 @@ Proof using All. { iIntros "!>" (?). iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]". awp_apply (dequeue_spec with "⊒V QL"); [solve_ndisj|]. iInv mpinvN as (G) "(QI & >●m & >◯m)". iInv mpinvN as (G) "(QI & >●m & >◯m & >%Hv)". iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC". iAaccIntro with "QI". { iFrame. iIntros "QI !> !>". iExists _. iFrame. } { iFrame. iIntros "QI !> !>". iExists _. iFrame. done. } iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #⊒V' & #QL' & %F) !>". iSplitL; last by iIntros. iNext. iExists G'. set (dV := mkGraphEvent deq Vdeq M') in *. destruct F as (SubG' & SubM' & HVin & HVcomm & [CASE|CASE]). - destruct CASE as (_&_&_&_&_& ComG' &_). rewrite ComG'. iFrame. - destruct CASE as (_&_&_&_& NoSo & _ & _ & ComG' & _). - destruct CASE as (_& -> &_& EsG' &_& ComG' &_). rewrite ComG'. iFrame. iPureIntro. rewrite EsG'. intros ??? [?|[-> <-]]%lookup_app_1; [by eapply Hv|done]. - destruct CASE as (_& -> & -> &_& NoSo & EsG' &_& ComG' & _). iFrame. iCombine "◯m ◯m1" as "◯m". rewrite ComG' size_union. + rewrite size_singleton (comm plus). iFrame. + rewrite size_singleton (comm plus). iFrame. iPureIntro. rewrite EsG'. intros ??? [?|[-> <-]]%lookup_app_1; [by eapply Hv|done]. + apply disjoint_singleton_l. rewrite -(bsq_cons_so_com _ QC). by apply NoSo. } iIntros "_". wp_seq. ... ... @@ -202,13 +210,13 @@ Proof using All. iClear "IH FPR FPR'". iDestruct "FI" as "[-> QL]". iExists 1. iSplit; [done|]. simpl. iIntros "!> !>". wp_seq. iDestruct "QL" as (G0 M0 ??????) "(#QL & %NEe12 & %HeV1 & %HeV2 & %Henq1 & %Henq2 & %HM1 & %HM2)". iDestruct "QL" as (G0 M0 ????) "(#QL & %NEe12 & %HeV1 & %HeV2 & %Henq1 & %Henq2 & %HM1 & %HM2)". iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]". iApply (wp_step_fupd _ _ _ _ (∀ _, _ -∗ _)%I with "[\$Post]"); [auto..|]. awp_apply (dequeue_spec with "⊒V QL"); [solve_ndisj|]. iInv mpinvN as (G) "(QI & >●m & >◯m)". iInv mpinvN as (G) "(QI & >●m & >◯m & >%Hv)". iDestruct (QueueInv_QueueConsistent with "QI") as "#>%QC". rewrite QueueInv_graph_master_acc. iDestruct "QI" as "[>Gm QI]". ... ... @@ -224,7 +232,7 @@ Proof using All. have {}LT : (size (com G) ≤ 1)%nat by lia. iAaccIntro with "QI". { iDestruct "◯m" as "[◯m \$]". iFrame. iIntros "QI !> !>". iExists _. iFrame. } { iDestruct "◯m" as "[◯m \$]". iFrame. iIntros "QI !> !>". iExists _. iFrame. done. } iIntros (v V' G' enqId deqId enq deq Vdeq M') "(QI & #⊒V' & #QL' & %F)". set (dV := mkGraphEvent deq Vdeq M') in *. ... ... @@ -234,47 +242,47 @@ Proof using All. destruct CASE as (-> & -> & ? & EsG' & _ & ComG' & ?). have HdV : G'.(Es) !! deqId = Some dV. { subst deqId. rewrite EsG'. apply lookup_app_1_eq. } (* WLOG, let e1 be an unmatched enqueue *) wlog: e1 e2 eV1 eV2 v1 v2 NEe12 HeV1 HeV2 Henq1 Henq2 HM1 HM2 / unmatched_enq_2 G e1. { case (decide (unmatched_enq_2 G e1)) => [?|MATCH] X; first by eapply (X e1 e2). eapply (X e2 e1); [done..|]. clear X. unfold unmatched_enq_2 in MATCH |- *. split. { exists v2. apply (f_equal (fmap ge_event)) in HeV2. move: HeV2. rewrite /= Henq2 //. } intros d2 In2 So2. apply MATCH. split. { exists v1. apply (f_equal (fmap ge_event)) in HeV1. move: HeV1. rewrite /= Henq1 //. } intros d1 In1 So1. rewrite -(bsq_cons_so_com _ QC) in LT. have INCL : {[(e1,d1); (e2,d2)]} ⊆ G.(so) by set_solver +So1 So2. move: INCL => /(subseteq_size _ _). rewrite size_union; [|set_solver +NEe12]. rewrite !size_singleton. lia. } intros [_ UNMATCHED]. (* Empty dequeue couldn't have seen an unmatched enqueue. Contradiction. *) refine (_ (bsq_cons_non_empty _ QC' _ _ HdV ltac:(done) e1 _ eV1 _ ltac:(done) _)); cycle 1. { rewrite EsG'. eapply prefix_lookup; [done|by eexists]. } { set_solver +SubM' HM1. } intros (d' & Com_ed' & _). rewrite ComG' -(bsq_cons_so_com _ QC) in Com_ed'. apply (UNMATCHED d'); [|done]. specialize (egcons_so _ EGC _ _ Com_ed') as (_ & dV' & _ & HdV' & _). apply lookup_lt_Some in HdV'. rewrite /to_set. apply elem_of_set_seq. lia. case (decide (unmatched_enq_2 G e1)) => [[_ UNMATCHED1]|MATCHED1]. + (* Empty dequeue couldn't have seen an unmatched enqueue. Contradiction. *) refine (_ (bsq_cons_non_empty _ QC' _ _ HdV ltac:(done) e1 _ eV1 _ ltac:(done) _)); cycle 1. { rewrite EsG'. eapply prefix_lookup; [done|by eexists]. } { set_solver +SubM' HM1. } intros (d' & Com_ed' & _). rewrite ComG' -(bsq_cons_so_com _ QC) in Com_ed'. apply (UNMATCHED1 d'); [|done]. specialize (egcons_so _ EGC _ _ Com_ed') as (_ & dV' & _ & HdV' & _). apply lookup_lt_Some in HdV'. rewrite /to_set. apply elem_of_set_seq. lia. + (* Since e1 is matched, e2 couldn't have been matched. *) have UNMATCHED2 : set_Forall (λ d2 : nat, (e2, d2) ∉ so G) (to_set (Es G)). { intros d2 In2 So2. apply MATCHED1. split. { exists 1. apply (f_equal (fmap ge_event)) in HeV1. move: HeV1. rewrite /= Henq1 //. } intros d1 In1 So1. rewrite -(bsq_cons_so_com _ QC) in LT. have INCL : {[(e1,d1); (e2,d2)]} ⊆ G.(so) by set_solver +So1 So2. move: INCL => /(subseteq_size _ _). rewrite size_union; [|set_solver +NEe12]. rewrite !size_singleton. lia. } refine (_ (bsq_cons_non_empty _ QC' _ _ HdV ltac:(done) e2 _ eV2 _ ltac:(done) _)); cycle 1. { rewrite EsG'. eapply prefix_lookup; [done|by eexists]. } { set_solver +SubM' HM2. } intros (d' & Com_ed' & _). rewrite ComG' -(bsq_cons_so_com _ QC) in Com_ed'. apply (UNMATCHED2 d'); [|done]. specialize (egcons_so _ EGC _ _ Com_ed') as (_ & dV' & _ & HdV' & _). apply lookup_lt_Some in HdV'. rewrite /to_set. apply elem_of_set_seq. lia. - (* successful dequeue *) rewrite /is_enqueue /is_dequeue in CASE. destruct CASE as (?&_&_&_& NoSo & _ & _ & ComG' & _). destruct CASE as (?& -> & -> & ? & NoSo & EsG' & _ & ComG' &_&_&_& eV & HeV & ? &_). iIntros "!>". iSplitL. { iNext. iExists _. iFrame. rewrite ComG' size_union. - rewrite size_singleton (comm plus). iFrame. - rewrite size_singleton (comm plus). iFrame. iPureIntro. rewrite EsG'. intros ??? [?|[-> <-]]%lookup_app_1; [by eapply Hv|done]. - apply disjoint_singleton_l. rewrite -(bsq_cons_so_com _ QC). by apply NoSo. } iIntros "_ Post". by iApply "Post". iIntros "_ Post". iApply "Post". iPureIntro. by apply (Hv _ _ _ HeV). Qed. End spmc_mp.
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!