-
Notifications
You must be signed in to change notification settings - Fork 1
/
code_producer_consumer.v
68 lines (59 loc) · 2.01 KB
/
code_producer_consumer.v
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
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%nat]
.
(** Enqueue the elements of array "a" with size "n" into "q" *)
Definition produce : val :=
λ: ["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 :=
λ: ["q"; "a"; "n"],
rec: "loop" ["i"] :=
if: "i" = "n"
then #☠
else
let: "e" := dequeue ["q"] in
if: #0%nat < "e"
then
("a" +ₗ "i") <- "e";;
"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%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"
elements to be consumed. *)
Definition produce_consume : val :=
λ: ["q"; "pa"; "ca"; "n"],
Fork
( 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" ; "ca"; "n"]
.
End code.