Commit 1c49c2a3 authored by Hai Dang's avatar Hai Dang
Browse files

Add comments and reshuffle

parent 523962be
......@@ -52,7 +52,8 @@ Definition produce_consume : val :=
( produce ["q" ; "pa"; "n"] );; (* || *) consume ["q" ; "ca"; "n"]
.
(* Consumer gets the first n elements of 2n elements that the producer sent. *)
(* The consumer tries to consume half (n) elements of the 2n elements that the
producer produces. In case of SPSC, the consumer gets the first half. *)
Definition produce_consume_first_half : val :=
λ: ["q"; "pa"; "ca"; "n"],
Fork
......
......@@ -9,57 +9,21 @@ From gpfsl.examples Require Import set_helper.
Require Import iris.prelude.options.
Definition pcN := nroot .@ "pc".
Definition qN := nroot .@ "q".
(** Verifying clients that uses a queue in the SPSC (single-producer, single-
consumer) fashion, using the graph-based LAT spec for queue. *)
Local Notation graph := (graph qevent).
Implicit Types (G : graph).
Section producer_consumer.
Context `{noprolG Σ, inG Σ (graphR qevent), inG Σ (mono_listR (leibnizO event_id))}.
Local Notation iProp := (iProp Σ).
Local Notation vProp := (vProp Σ).
Local Open Scope nat_scope.
Implicit Types
(q pa ca : loc) (vl : list Z)
(es ds xs : list event_id).
(* [queue_FIFO] is sufficient for single-producer/single-consumer. *)
Hypothesis Q : weak_queue_spec Σ.
Local Existing Instances QueueInv_Objective QueueLocal_Persistent.
Notation produce_loop := (produce_loop Q.(enqueue)).
Notation produce := (produce Q.(enqueue)).
Notation consume_loop := (consume_loop Q.(dequeue)).
Notation consume := (consume Q.(dequeue)).
Notation produce_consume_first_half := (produce_consume_first_half Q.(enqueue) Q.(dequeue)).
Notation Events γ f es := ( own γ (ML{#f} (es : listO (leibnizO event_id))) : vProp)%I.
Section ghost.
Lemma Events_alloc : |==> γ, Events γ (1/2) [] Events γ (1/2) [].
Proof.
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.
Qed.
Lemma Events_add γ es e :
Events γ (1/2) es - Events γ (1/2) es ==
Events γ (1/2) (es ++ [e]) Events γ (1/2) (es ++ [e]).
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].
Qed.
End ghost.
(** This is the strong inverse of [graph_xo_eco]: if e1 is before e2 in the list
order, the e1 happens-before e2. *)
Definition sequential G es :=
i1 i2 e1 e2 eV2
(EID1 : es !! i1 = Some e1) (EID2 : es !! i2 = Some e2)
......@@ -67,11 +31,12 @@ Definition sequential G es :=
(SEQ : i1 < i2),
e1 eV2.(ge_lview).
(* [ds] matches with the prefix of [es]. *)
(** The dequeue list [ds] matches with the prefix of the enqueue list [es]. *)
Definition matches G es ds :=
i d (DV : ds !! i = Some d),
e, es !! i = Some e (e, d) G.(com).
(** The enqueue list (of events) [es] produces the value list [vl] *)
Inductive Produced G es vl : Prop :=
| Produced_intro
(ENQS :
......@@ -81,6 +46,7 @@ Inductive Produced G es vl : Prop :=
(ENQ_SEQ : sequential G es)
.
(** The dequeue list (of events) [ds] consumes the value list [vl] *)
Inductive Consumed G ds vl : Prop :=
| Consumed_intro
(DEQS :
......@@ -89,6 +55,7 @@ Inductive Consumed G ds vl : Prop :=
v, dV.(ge_event) = Deq v vl !! i = Some v)
.
(** The list [xs] is of empty dequeues *)
Inductive EmpDeqs G xs : Prop :=
| EmpDeqs_intro
(EMPS :
......@@ -98,40 +65,9 @@ Inductive EmpDeqs G xs : Prop :=
Local Hint Constructors Produced Consumed EmpDeqs : core.
(* [vl]: values that will be produced *)
Definition PCInv q γg γe γd γx 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 *)
seq 0 (length G.(Es)) es ++ ds ++ xs
Produced G es vl
Consumed G ds vl
matches G es ds
EmpDeqs G xs
.
Instance PCInv_objective q γg γe γd γx vl : Objective (PCInv q γg γe γd γx vl) := _.
Definition to_arr (vl : list Z) := LitV LitInt <$> vl.
Section lemmas.
Lemma array_access (arr : loc) vl (i : nat) v (VAL : vl !! i = Some v):
arr ↦∗ to_arr vl
(arr ↦∗ (LitV LitInt <$> take i vl)
(arr >> i) #v
(arr >> i >> 1) ↦∗ (LitV LitInt <$> (drop (S i) vl))).
Proof.
rewrite -{1}(take_drop_middle _ _ _ VAL).
rewrite /to_arr fmap_app fmap_cons /=.
rewrite ->own_loc_na_vec_app, own_loc_na_vec_cons.
rewrite fmap_take take_length.
apply lookup_lt_Some in VAL as LT.
have {}LT : (i < length (to_arr vl))%nat by rewrite fmap_length.
rewrite (_ : i `min` (length (to_arr vl)) = i)%nat; [done|lia].
Qed.
Lemma Produced_mono G G' es vl (SubGG' : G G') :
Produced G es vl Produced G' es vl.
Proof.
......@@ -168,6 +104,91 @@ Proof.
Qed.
End lemmas.
Section producer_consumer.
Context `{!noprolG Σ,
!inG Σ (graphR qevent),
!inG Σ (mono_listR (leibnizO event_id))}.
Context (pcN qN : namespace)
(DISJ1: pcN ## histN) (DISJ2: qN ## histN) (DISJ3: pcN ## qN).
(* [queue_FIFO] is sufficient for single-producer/single-consumer. *)
Hypothesis Q : weak_queue_spec Σ.
Local Existing Instances QueueInv_Objective QueueLocal_Persistent.
Local Notation iProp := (iProp Σ).
Local Notation vProp := (vProp Σ).
Notation produce_loop := (produce_loop Q.(enqueue)).
Notation produce := (produce Q.(enqueue)).
Notation consume_loop := (consume_loop Q.(dequeue)).
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.
Section ghost.
Lemma Events_alloc : |==> γ, Events γ (1/2) [] Events γ (1/2) [].
Proof.
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.
Qed.
Lemma Events_add γ es e :
Events γ (1/2) es - Events γ (1/2) es ==
Events γ (1/2) (es ++ [e]) Events γ (1/2) (es ++ [e]).
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].
Qed.
End ghost.
(* [vl]: values that will be produced *)
Definition PCInv q γg γe γd γx 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 *)
(* 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
(dequeue) step, instead of having to look into the whole history and prove
that only one certain permutation is possible. *)
seq 0 (length G.(Es)) es ++ ds ++ xs
Produced G es vl
Consumed G ds vl
matches G es ds
EmpDeqs G xs
.
Instance PCInv_objective q γg γe γd γx vl : Objective (PCInv q γg γe γd γx vl) := _.
(** Extract the element i in (arr, vl) *)
Lemma array_access (arr : loc) vl (i : nat) v (VAL : vl !! i = Some v):
arr ↦∗ to_arr vl
(arr ↦∗ (LitV LitInt <$> take i vl)
(arr >> i) #v
(arr >> i >> 1) ↦∗ (LitV LitInt <$> (drop (S i) vl))).
Proof.
rewrite -{1}(take_drop_middle _ _ _ VAL).
rewrite /to_arr fmap_app fmap_cons /=.
rewrite ->own_loc_na_vec_app, own_loc_na_vec_cons.
rewrite fmap_take take_length.
apply lookup_lt_Some in VAL as LT.
have {}LT : (i < length (to_arr vl))%nat by rewrite fmap_length.
rewrite (_ : i `min` (length (to_arr vl)) = i)%nat; [done|lia].
Qed.
(** Specs for a partially produced array, in single-producer mode:
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
(Hn : length vl = n) (Hi : length es0 = i) (LT : i < n)
(GT : Forall (λ v, 0 < v)%Z vl) :
......@@ -178,7 +199,7 @@ Lemma produce_loop_spec γg γe γd γx vl n tid q pa G0 M0 es0 i
Produced G0 es0 vl Forall (λ e, e M0) es0 }}}
produce_loop [ #q; #pa; #n] [ #i] @ tid;
{{{ RET #; True }}}.
Proof.
Proof using All.
iIntros "#PCInv" (Φ) "!> P Post".
wp_lam.
iLöb as "IH" forall (G0 M0 es0 i Hi LT).
......@@ -196,8 +217,7 @@ Proof.
wp_let.
iDestruct (monPred_in_intro True%I with "[//]") as (V) "[#⊒V _]".
awp_apply (enqueue_spec with "⊒V QL").
{ solve_ndisj. }
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)]".
......@@ -263,6 +283,11 @@ Proof.
iFrame "QL' PA ◯e". iPureIntro. done.
Qed.
(** Specs for a partially consumed array, in single-consumer mode:
The events es0 in the graph (G0, M0) have consumed the elements [0,i) of vl,
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
(Hn : length vl = n) (Hm : m n) (Hi : length ds0 = i) (LT : i < m) :
inv pcN (PCInv q γg γe γd γx vl) -
......@@ -274,7 +299,7 @@ Lemma consume_loop_spec γg γe γd γx vl n m tid q ca G0 M0 ds0 xs0 i
}}}
consume_loop [ #q; #ca; #m] [ #i] @ tid;
{{{ RET #; ca ↦∗ (to_arr (take m vl)) }}}.
Proof.
Proof using All.
iIntros "#PCInv" (Φ) "!> P Post".
wp_lam.
iLöb as "IH" forall (G0 M0 ds0 xs0 i Hi LT).
......@@ -469,6 +494,10 @@ Proof.
iFrame (CONS'') "QL' CA ◯d ◯x".
Qed.
(** The producer is forked and run on a child thread, which the code doesn't
join with later, so in the post-condition we only have the consumer array [ca]
left. To also recollect the producer array [pa], we'd need to wait and join
with the producer thread. *)
Lemma produce_consume_first_half_spec γg vl tid q pa ca n
(Hn : length vl = n + n) (NZ : n > 0) (GT : Forall (λ v, 0 < v)%Z vl) :
{{{ Q.(QueueInv) γg q Q.(QueueLocal) qN γg q
......
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