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

Merge branch 'jaehwang/spsc' into 'graphs_multi'

prove spsc example with queue graph spec

See merge request !25
parents ce28da7a 1c49c2a3
......@@ -164,6 +164,7 @@ theories/examples/queue/proof_mp_graph.v
theories/examples/queue/proof_ms_abs_graph.v
theories/examples/queue/proof_ms_closed.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_producer_consumer.v
## Chase-Lev Double-ended Queue
theories/examples/chase_lev/code.v
## Exchanger
......
......@@ -84,16 +84,6 @@ Proof.
eexists. eapply prefix_lookup; [done|by eexists].
Qed.
Lemma lookup_xo : (n e : nat) (LT : (e < n)%nat), (seq 0 n) !! e = Some e.
Proof. intros. by rewrite lookup_seq_lt. Qed.
Lemma xo_events E : Forall (λ e, is_Some (E !! e)) (seq 0 (length E)).
Proof.
rewrite Forall_lookup => i e H. have H' := H. apply lookup_lt_is_Some_2.
rewrite lookup_xo in H; simplify_eq;
apply lookup_lt_Some in H'; by rewrite seq_length in H'.
Qed.
Lemma hb_xo_add E eV
(WF : history_wf E)
(HB_XO : hb_ord E (seq 0 (length E))) :
......@@ -118,19 +108,6 @@ Proof.
eapply (HB_XO e1 e2 e1 e2 eV2); [by rewrite lookup_xo..|done|done].
Qed.
Lemma ord_nodup N ord (PERM : ord seq 0 N) : NoDup ord.
Proof. rewrite (NoDup_Permutation_proper _ _ PERM). apply NoDup_seq. Qed.
Lemma ord_idx_event E ord i e
(PERM : ord seq 0 (length E))
(Ee : ord !! i = Some e) :
eV, E !! e = Some eV.
Proof.
apply Permutation_inj in PERM as [LEN (f & _ & PERM)].
rewrite ->PERM,lookup_seq in Ee. des. subst. simpl.
by apply lookup_lt_is_Some_2.
Qed.
Lemma sublist_lookup {A} (ls1 ls2 : list A) i1 x
(SUB : ls1 `sublist_of` ls2)
(LOOKUP : ls1 !! i1 = Some x) :
......
......@@ -631,3 +631,32 @@ Proof.
apply IHi in H. by rewrite H.
Qed.
End alter.
Section xo.
Context {A : Type}.
Implicit Types (l : list A) (ord : list nat).
Lemma lookup_xo : (n e : nat) (LT : (e < n)%nat), (seq 0 n) !! e = Some e.
Proof. intros. by rewrite lookup_seq_lt. Qed.
Lemma xo_events l : Forall (λ e, is_Some (l !! e)) (seq 0 (length l)).
Proof.
rewrite Forall_lookup => i e H. have H' := H. apply lookup_lt_is_Some_2.
rewrite lookup_xo in H; simplify_eq;
apply lookup_lt_Some in H'; by rewrite seq_length in H'.
Qed.
Lemma ord_nodup N ord (PERM : ord seq 0 N) : NoDup ord.
Proof. rewrite (NoDup_Permutation_proper _ _ PERM). apply NoDup_seq. Qed.
Lemma ord_idx_event l ord i e
(PERM : ord seq 0 (length l))
(Ee : ord !! i = Some e) :
is_Some (l !! e).
Proof.
apply Permutation_inj in PERM as [LEN (f & _ & PERM)].
rewrite ->PERM,lookup_seq in Ee. destruct Ee as [-> ?]. simpl.
by apply lookup_lt_is_Some_2.
Qed.
End xo.
......@@ -16,12 +16,12 @@ Definition produce_loop : val :=
else
let: "e":= !("a" + "i") in
enqueue ["q"; "e"];;
"loop" ["i" + #1]
"loop" ["i" + #1%nat]
.
(** Enqueue the elements of array "a" with size "n" into "q" *)
Definition produce : val :=
λ: ["q"; "a"; "n"], produce_loop ["q"; "a"; "n"; #0].
λ: ["q"; "a"; "n"], produce_loop ["q"; "a"; "n"] [ #0%nat].
(** Dequeue elements from "q" into array "a" from index "i" to "n". *)
Definition consume_loop : val :=
......@@ -31,17 +31,17 @@ Definition consume_loop : val :=
then #
else
let: "e" := dequeue ["q"] in
if: #0 < "e"
if: #0%nat < "e"
then
("a" + "i") <- "e";;
"loop" ["i" + #1]
"loop" ["i" + #1%nat]
else
"loop" ["i"]
.
(** Dequeue "n" elements from "q" and put them in "a" using the dequeue order. *)
Definition consume : val :=
λ: ["q"; "a"; "n"], consume_loop ["q"; "a"; "n"; #0].
λ: ["q"; "a"; "n"], consume_loop ["q"; "a"; "n"] [ #0%nat].
(** Concurrently produce in one thread and consume in the other.
We don't need to join because the consumer thread does wait for enough "n"
......@@ -49,12 +49,20 @@ Definition consume : val :=
Definition produce_consume : val :=
λ: ["q"; "pa"; "ca"; "n"],
Fork
( produce ["q" ; "pa"; "n"] );; (* || *) consume ["q" ; "pa"; "n"]
( produce ["q" ; "pa"; "n"] );; (* || *) consume ["q" ; "ca"; "n"]
.
(* 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
( produce ["q" ; "pa"; "n" + "n"] );; (* || *) consume ["q" ; "ca"; "n"]
.
(** Sequential produce-consume. *)
Definition produce_consume_seq : val :=
λ: ["q"; "pa"; "ca"; "n"],
produce ["q" ; "pa"; "n"] ;; consume ["q" ; "pa"; "n"]
produce ["q" ; "pa"; "n"] ;; consume ["q" ; "ca"; "n"]
.
End code.
This diff is collapsed.
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