Commit c4c9bf84 authored by Hai Dang's avatar Hai Dang
Browse files

Merge branch 'jaehwang/spsc' into 'graphs_multi'

use simpler ghost in proof_producer_consumer

See merge request !26
parents e41906eb 25aa375d
From gpfsl.algebra Require Import mono_list.
From iris.algebra Require Import excl_auth.
From iris.proofmode Require Import tactics.
From gpfsl.lang Require Import notation.
......@@ -107,7 +107,7 @@ End lemmas.
Section producer_consumer.
Context `{!noprolG Σ,
!inG Σ (graphR qevent),
!inG Σ (mono_listR (leibnizO event_id))}.
!inG Σ (excl_authR (leibnizO (list event_id)))}.
Context (pcN qN : namespace)
(DISJ1: pcN ## histN) (DISJ2: qN ## histN) (DISJ3: pcN ## qN).
......@@ -125,35 +125,33 @@ Notation consume := (consume Q.(dequeue)).
Notation produce_consume_first_half := (produce_consume_first_half Q.(enqueue) Q.(dequeue)).
(* The authoritative list of events that the client has generated. *)
Notation Events γ f es := ( own γ (ML{#f} (es : listO (leibnizO event_id))) : vProp)%I.
Definition QEAuth γ es : vProp := own γ (E (es : leibnizO (list event_id))) .
Definition QEFrag γ es : vProp := own γ (E (es : leibnizO (list event_id))) .
Section ghost.
Lemma Events_alloc : |==> γ, Events γ (1/2) [] Events γ (1/2) [].
Lemma QE_alloc : |==> γ, QEAuth γ [] QEFrag γ [].
Proof.
rewrite /QEAuth /QEFrag.
setoid_rewrite <- embed_sep. setoid_rewrite <- own_op.
rewrite -embed_exist -embed_bupd -own_alloc; first eauto.
rewrite -mono_list_auth_frac_op Qp_half_half.
apply mono_list_auth_valid.
by apply excl_auth_valid.
Qed.
Lemma Events_add γ es e :
Events γ (1/2) es - Events γ (1/2) es ==
Events γ (1/2) (es ++ [e]) Events γ (1/2) (es ++ [e]).
Lemma QE_update {γ es} es' :
QEAuth γ es - QEFrag γ es == QEAuth γ es' QEFrag γ es'.
Proof.
iIntros "E1 E2". iCombine "E1 E2" as "E".
setoid_rewrite <- embed_sep. setoid_rewrite <- own_op.
rewrite -!mono_list_auth_frac_op !Qp_half_half.
iMod (own_update with "E") as "$"; last done.
apply (mono_list_update (es ++ [e])). by exists [e].
apply excl_auth_update.
Qed.
End ghost.
(* [vl]: values that will be produced *)
Definition PCInv q γg γe γd γx vl : vProp := G es ds xs,
Definition PCInv q γg γe γd vl : vProp := G es ds xs,
Q.(QueueInv) γg q G
Events γe (1/2) es (* enqueues ordered by po *)
Events γd (1/2) ds (* dequeues ordered by po *)
Events γx (1/2) xs (* empty deqeueus ordered by po *)
QEAuth γe es (* enqueues ordered by po *)
QEAuth γd ds (* dequeues ordered by po *)
(* Thanks to SPSC, we can easily have an inductive invariant that matches up
enqueue events by the producer and dequeue events by the consumer at every
......@@ -166,7 +164,7 @@ Definition PCInv q γg γe γd γx vl : vProp := ∃ G es ds xs,
EmpDeqs G xs
.
Instance PCInv_objective q γg γe γd γx vl : Objective (PCInv q γg γe γd γx vl) := _.
Instance PCInv_objective q γg γe γd vl : Objective (PCInv q γg γe γd vl) := _.
(** Extract the element i in (arr, vl) *)
......@@ -189,12 +187,12 @@ Qed.
The events es0 in the graph (G0, M0) have produced the elements [0,i) of vl.
The elements [i,n) are to be produced.
The pre-condition here is the loop invariant. *)
Lemma produce_loop_spec γg γe γd γx vl n tid q pa G0 M0 es0 i
Lemma produce_loop_spec γg γe γd vl n tid q pa G0 M0 es0 i
(Hn : length vl = n) (Hi : length es0 = i) (LT : i < n)
(GT : Forall (λ v, 0 < v)%Z vl) :
inv pcN (PCInv q γg γe γd γx vl) -
inv pcN (PCInv q γg γe γd vl) -
{{{ Q.(QueueLocal) qN γg q G0 M0
Events γe (1/2) es0
QEFrag γe es0
pa ↦∗ (to_arr vl)
Produced G0 es0 vl Forall (λ e, e M0) es0 }}}
produce_loop [ #q; #pa; #n] [ #i] @ tid;
......@@ -220,9 +218,9 @@ Proof using All.
awp_apply (enqueue_spec with "⊒V QL"); [done|..].
{ rewrite ->Forall_lookup in GT. by apply (GT i). }
iInv pcN as (????) "[QI >(●e & ●d & ●x & %PERM & %PROD & %CONS & %MATCH & %EMP)]".
iInv pcN as (????) "[QI >(●e & ●d & %PERM & %PROD & %CONS & %MATCH & %EMP)]".
iDestruct (own_valid_2 with "●e ◯e") as %[_ <-%leibniz_equiv]%mono_list_auth_frac_op_valid.
iDestruct (own_valid_2 with "●e ◯e") as %<-%excl_auth_agree_L.
iAaccIntro with "QI".
{ iFrame. iIntros "QI !> !>". iExists _,_,_,_. iFrame. iPureIntro. done. }
......@@ -263,7 +261,7 @@ Proof using All.
intros ? e0 [Ei0|[-> <-]]%lookup_app_1; [|done].
specialize (SEEN_ENQ _ _ Ei0). set_solver +SEEN_ENQ SubMM'. }
iMod (Events_add _ _ enqId with "●e ◯e") as "[●e ◯e]".
iMod (QE_update (es ++ [enqId]) with "●e ◯e") as "[●e ◯e]".
iIntros "!>". iSplitR "◯e PA Post".
{ (* close inv *)
iNext. iExists _,_,_,_. iFrame. iPureIntro. split_and!; [|done|done| |done].
......@@ -288,12 +286,11 @@ Qed.
and written those to ca. The rest of ca is all 0's.
The elements [i,m) are to be consumed.
The pre-condition here is the loop invariant. *)
Lemma consume_loop_spec γg γe γd γx vl n m tid q ca G0 M0 ds0 xs0 i
Lemma consume_loop_spec γg γe γd vl n m tid q ca G0 M0 ds0 i
(Hn : length vl = n) (Hm : m n) (Hi : length ds0 = i) (LT : i < m) :
inv pcN (PCInv q γg γe γd γx vl) -
inv pcN (PCInv q γg γe γd vl) -
{{{ Q.(QueueLocal) qN γg q G0 M0
Events γd (1/2) ds0
Events γx (1/2) xs0
QEFrag γd ds0
ca ↦∗ to_arr ((take i vl) ++ replicate (m - i) 0%Z)
Consumed G0 ds0 vl
}}}
......@@ -302,17 +299,16 @@ Lemma consume_loop_spec γg γe γd γx vl n m tid q ca G0 M0 ds0 xs0 i
Proof using All.
iIntros "#PCInv" (Φ) "!> P Post".
wp_lam.
iLöb as "IH" forall (G0 M0 ds0 xs0 i Hi LT).
iDestruct "P" as "(QL & ◯d & ◯x & CA & %CONS0)".
iLöb as "IH" forall (G0 M0 ds0 i Hi LT).
iDestruct "P" as "(QL & ◯d & CA & %CONS0)".
wp_rec. wp_op. rewrite bool_decide_false; [|lia]. wp_if.
iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]".
awp_apply (dequeue_spec with "⊒V QL"); [solve_ndisj|].
iInv pcN as (????) "[QI >(●e & ●d & ●x & %PERM & %PROD & %CONS & %MATCH & %EMP)]".
iInv pcN as (????) "[QI >(●e & ●d & %PERM & %PROD & %CONS & %MATCH & %EMP)]".
iDestruct (own_valid_2 with "●d ◯d") as %[_ <-%leibniz_equiv]%mono_list_auth_frac_op_valid.
iDestruct (own_valid_2 with "●x ◯x") as %[_ <-%leibniz_equiv]%mono_list_auth_frac_op_valid.
iDestruct (own_valid_2 with "●d ◯d") as %<-%excl_auth_agree_L.
have [NODUPes [NODUPds NODUPxs]] : NoDup es NoDup ds NoDup xs.
{ symmetry in PERM. move: PERM => /ord_nodup.
move=> /NoDup_app [?][_] /NoDup_app [?][_]? //. }
......@@ -330,17 +326,17 @@ Proof using All.
destruct CASE as [CASE|CASE].
{ destruct CASE as (-> & -> & ? & EsG' & ?).
iMod (Events_add _ _ deqId with "●x ◯x") as "[●x ◯x]".
iIntros "!>". iSplitR "◯d ◯x CA Post".
{ iNext. iExists _,_,_,_. iFrame. iPureIntro. split_and!; [|done|done|done|].
iIntros "!>". iSplitR "◯d CA Post".
{ iNext. iExists _,_,_, (xs ++ [deqId]). iFrame.
iPureIntro. split_and!; [|done|done|done|].
- subst deqId. rewrite EsG' app_length /= seq_app /=.
rewrite (assoc app ds) (assoc app es). by f_equiv.
- constructor. intros ?? [Xi0|[-> <-]]%lookup_app_1.
+ destruct EMP'. apply (EMPS _ _ Xi0).
+ eexists. rewrite EsG'. subst deqId. split; [apply lookup_app_1_eq|done]. }
iIntros "_". wp_let. wp_op. wp_if.
iApply ("IH" $! _ _ ds _ i with "[%] [%] [-Post] Post"); [done..|].
iFrame "QL' ◯d ◯x CA". iPureIntro. done. }
iApply ("IH" $! _ _ ds i with "[%] [%] [-Post] Post"); [done..|].
iFrame "QL' ◯d CA". iPureIntro. done. }
rewrite /is_enqueue /is_dequeue in CASE.
destruct CASE as (? & -> & -> & ? & ? & EsG' & SoG' & ComG' & ? & ? & ? & eV & HeV & ? & ?).
......@@ -355,7 +351,7 @@ Proof using All.
iDestruct (graph_master_consistent with "Gm") as %EGC'.
iSpecialize ("QI" with "[$Gm]").
(* find the maching enqueue in [es] ([im]-th) *)
(* find the matching enqueue in [es] ([im]-th) *)
have [im Eim] : im, es !! im = Some enqId.
{ apply lookup_lt_Some in HeV as LTenqId.
move: (lookup_xo _ _ LTenqId) => /(elem_of_list_lookup_2 _ _ _).
......@@ -452,8 +448,8 @@ Proof using All.
- eexists. rewrite EsG'. subst deqId dV i.
split; [apply lookup_app_1_eq|by eauto]. }
iMod (Events_add _ _ deqId with "●d ◯d") as "[●d ◯d]".
iIntros "!>". iSplitR "◯d ◯x CA Post".
iMod (QE_update (ds ++ [deqId]) with "●d ◯d") as "[●d ◯d]".
iIntros "!>". iSplitR "◯d CA Post".
{ (* close inv *)
iNext. iExists _,_,_,_. iFrame. iPureIntro. split_and!; [|done|done| |done].
- subst deqId. rewrite EsG' app_length /= seq_app /=.
......@@ -489,9 +485,9 @@ Proof using All.
case (decide (i + 1 = m)) as [->|NE].
{ wp_rec. wp_op. rewrite bool_decide_true; [|done]. wp_pures.
iApply "Post". rewrite Nat.sub_diag /= app_nil_r. by iFrame "CA". }
iApply ("IH" $! _ _ (ds ++ [deqId]) _ (i + 1) with "[%] [%] [-Post] Post");
iApply ("IH" $! _ _ (ds ++ [deqId]) (i + 1) with "[%] [%] [-Post] Post");
[rewrite app_length Hi //=|lia|].
iFrame (CONS'') "QL' CA ◯d ◯x".
iFrame (CONS'') "QL' CA ◯d".
Qed.
(** The producer is forked and run on a child thread, which the code doesn't
......@@ -507,19 +503,18 @@ Lemma produce_consume_first_half_spec γg vl tid q pa ca n
{{{ RET #; ca ↦∗ (to_arr (take n vl)) }}}.
Proof using All.
iIntros (Φ) "(QI & #QL & PA & CA) Post".
iMod Events_alloc as (γe) "[●e ◯e]".
iMod Events_alloc as (γd) "[●d ◯d]".
iMod Events_alloc as (γx) "[●x ◯x]".
iMod (inv_alloc pcN _ (PCInv q γg γe γd γx vl)%positive with "[QI ●e ●d ●x]") as "#Inv".
iMod QE_alloc as (γe) "[●e ◯e]".
iMod QE_alloc as (γd) "[●d ◯d]".
iMod (inv_alloc pcN _ (PCInv q γg γe γd vl)%positive with "[QI ●e ●d]") as "#Inv".
{ iNext. iExists _, [], [], []. simpl. iFrame. iPureIntro. done. }
wp_lam.
wp_apply (wp_fork with "[PA ◯e]"); first done.
{ iIntros "!>" (?). wp_op. rewrite -Nat2Z.inj_add. wp_lam.
iApply (produce_loop_spec _ _ _ _ vl (n + n) _ _ _ _ _ [] 0
iApply (produce_loop_spec _ _ _ vl (n + n) _ _ _ _ _ [] 0
with "[] [$QL $◯e $PA //] []"); [done|done|lia|done|done|done]. }
iIntros "_". wp_seq. wp_lam.
iApply (consume_loop_spec _ _ _ _ vl (n + n) n _ _ _ _ _ [] [] 0
with "[] [$QL $◯d $◯x CA] [Post]"); [done|lia|done|lia|done| |done].
iApply (consume_loop_spec _ _ _ vl (n + n) n _ _ _ _ _ [] 0
with "[] [$QL $◯d CA] [Post]"); [done|lia|done|lia|done| |done].
rewrite Nat.sub_0_r /= /to_arr fmap_replicate /=. iFrame "CA".
iPureIntro. done.
Qed.
......
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