Commit 59d29dd4 authored by Jaehwang Jung's avatar Jaehwang Jung
Browse files

fix code_producer_consumer

parent ce28da7a
......@@ -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,19 @@ 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"]
.
(* Consumer gets the first n elements of 2n elements that the producer sent. *)
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.
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