-
Notifications
You must be signed in to change notification settings - Fork 0
/
code_slot_bag_oloc.v
141 lines (121 loc) · 3.93 KB
/
code_slot_bag_oloc.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
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
From smr.lang Require Import tactics notation.
From iris.prelude Require Import options.
(** Sequential bag using linked list *)
Notation seqNodeSize := 2%nat (only parsing).
Notation seqNodeNext := 0 (only parsing).
Notation seqNodeValue := 1 (only parsing).
Notation seqSize := 1%nat (only parsing).
Notation seqHead := 0 (only parsing).
Definition seq_bag_new : val :=
λ: <>,
let: "seq" := AllocN #seqSize #0 in
"seq" +ₗ #seqHead <- #NULL;;
"seq".
Definition seq_bag_add : val :=
λ: "seq" "ptr",
let: "head" := !("seq" +ₗ #seqHead) in
let: "seqNode" := AllocN #seqNodeSize #0 in
"seqNode" +ₗ #seqNodeNext <- "head";;
"seqNode" +ₗ #seqNodeValue <- "ptr";;
"seq" +ₗ #seqHead <- "seqNode".
Definition seq_bag_contains_loop : val :=
rec: "loop" "head" "ptr" :=
if: "head" = #NULL
then #false
else
if: !("head" +ₗ #seqNodeValue) = "ptr"
then #true
else "loop" !("head" +ₗ #seqNodeNext) "ptr".
Definition seq_bag_contains : val :=
λ: "seq" "ptr",
let: "head" := !("seq" +ₗ #seqHead) in
seq_bag_contains_loop "head" "ptr".
Definition seq_bag_contains_other_loop : val :=
rec: "loop" "head" "val" :=
if: "head" = #NULL
then #false
else
if: !("head" +ₗ #seqNodeValue) ≠ "val"
then #true
else "loop" !("head" +ₗ #seqNodeNext) "val".
Definition seq_bag_contains_other : val :=
λ: "seq" "val",
let: "head" := !("seq" +ₗ #seqHead) in
seq_bag_contains_other_loop "head" "val".
(** Slot *)
Notation slotSize := 3%nat (only parsing).
Notation slotNext := 0 (only parsing).
Notation slotActive := 1 (only parsing).
Notation slotValue := 2 (only parsing).
Definition slot_new : val :=
λ: <>,
let: "slot" := AllocN #slotSize #0 in
"slot" +ₗ #slotNext <- #NULL;;
"slot" +ₗ #slotActive <- #true;;
"slot" +ₗ #slotValue <- #NULL;;
"slot".
Definition slot_set : val :=
λ: "slot" "ptr",
"slot" +ₗ #slotValue <- "ptr".
Definition slot_unset : val :=
λ: "slot",
"slot" +ₗ #slotValue <- #NULL.
Definition slot_drop : val :=
λ: "slot",
"slot" +ₗ #slotActive <- #false.
(** SlotBag *)
Notation slotBagSize := 1 (only parsing).
Notation slotBagHead := 0 (only parsing).
Definition slot_bag_new : val :=
λ: <>,
let: "slotBag" := AllocN #slotBagSize #0 in
"slotBag" +ₗ #slotBagHead <- #NULL;;
"slotBag".
Definition slot_try_acquire_inactive_slot_loop : val :=
rec: "loop" "slot" :=
if: "slot" = #NULL
then #NULL
else
let: "next" := !("slot" +ₗ #slotNext) in
if: CAS ("slot" +ₗ #slotActive) #false #true
then "slot"
else "loop" "next".
Definition slot_bag_try_acquire_inactive_slot : val :=
λ: "slotBag",
let: "head" := !("slotBag" +ₗ #slotBagHead) in
slot_try_acquire_inactive_slot_loop "head".
Definition slot_bag_push_slot_loop : val :=
rec: "loop" "slotBag" "new" :=
let: "head" := !("slotBag" +ₗ #slotBagHead) in
"new" +ₗ #slotNext <- "head";;
if: CAS ("slotBag" +ₗ #slotBagHead) "head" "new" then
#()
else
"loop" "slotBag" "new".
Definition slot_bag_acquire_slot : val :=
λ: "slotBag",
let: "slot" := slot_bag_try_acquire_inactive_slot "slotBag" in
if: "slot" ≠ #NULL
then "slot"
else
let: "new" := slot_new #() in
slot_bag_push_slot_loop "slotBag" "new";;
"new".
Definition slot_bag_snapshot_loop : val :=
rec: "loop" "snapshot" "slot" :=
if: "slot" = #NULL then
#()
else
let: "active" := !("slot" +ₗ #slotActive) in
( if: "active" then
let: "value" := !("slot" +ₗ #slotValue) in
seq_bag_add "snapshot" "value"
else #() ) ;;
let: "next" := !("slot" +ₗ #slotNext) in
"loop" "snapshot" "next".
Definition slot_bag_snapshot : val :=
λ: "slotBag",
let: "snapshot" := seq_bag_new #() in
let: "head" := !("slotBag" +ₗ #slotBagHead) in
slot_bag_snapshot_loop "snapshot" "head";;
"snapshot".