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

Add producer/consumer code

parent 1c9d9e9b
......@@ -143,6 +143,7 @@ theories/examples/stack/proof_elim_graph_closed.v
theories/examples/queue/spec_per_elem.v
theories/examples/queue/code_ms.v
theories/examples/queue/code_hw.v
theories/examples/queue/code_producer_consumer.v
theories/examples/queue/spec_graph.v
theories/examples/queue/proof_ms_gps.v
theories/examples/queue/proof_ms_graph.v
......
From gpfsl.lang Require Export notation.
From gpfsl.lang Require Import tactics.
Require Import iris.prelude.options.
Section code.
Variables (enqueue dequeue : val).
(** Iterate the array "a" from "i" up to (but not including) "n" and enqueue
the elements in "q" in the array index order. *)
Definition produce_loop : val :=
λ: ["q"; "a"; "n"],
rec: "loop" ["i"] :=
if: "i" = "n"
then #
else
let: "e":= !("a" + "i") in
enqueue ["q"; "e"];;
"loop" ["i" + #1]
.
(** Enqueue the elements of array "a" with size "n" into "q" *)
Definition produce : val :=
λ: ["q"; "a"; "n"], produce_loop ["q"; "a"; "n"; #0].
(** Dequeue elements from "q" into array "a" from index "i" to "n". *)
Definition consume_loop : val :=
λ: ["q"; "a"; "n"],
rec: "loop" ["i"] :=
if: "i" = "n"
then #
else
let: "e" := dequeue ["q"] in
if: #0 < "e"
then
("a" + "i") <- "e";;
"loop" ["i" + #1]
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].
(** 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"
elements to be consumed. *)
Definition produce_consume : val :=
λ: ["q"; "pa"; "ca"; "n"],
Fork
( produce ["q" ; "pa"; "n"] );; (* || *) consume ["q" ; "pa"; "n"]
.
(** Sequential produce-consume. *)
Definition produce_consume_seq : val :=
λ: ["q"; "pa"; "ca"; "n"],
produce ["q" ; "pa"; "n"] ;; consume ["q" ; "pa"; "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