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
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
|
(* ****** ****** *)
//
// Fourslot algorithm for fully asynchrous read/write by Simpson
//
(* ****** ****** *)
//
// Author: Hongwei Xi
// Authoremail: gmhwxiATgmailDOTcom
// Start time: May, 2013
//
(* ****** ****** *)
//
#include "share/atspre_staload.hats"
//
(* ****** ****** *)
abst@ype bit = int
extern
castfn bit2int (i: bit): natLt(2)
extern
castfn int2bit (i: natLt(2)): bit
extern
fun{} not_bit (i: bit): bit
overload not with not_bit
implement{}
not_bit (i) = int2bit (1 - bit2int (i))
(* ****** ****** *)
absvtype data_vtype (a:t@ype) = ptr
vtypedef data (a:t0p) = data_vtype (a)
extern
fun{a:t0p}
data_make_elt (x: a): data (a)
extern
fun{} data_free {a:t0p} (A: data (a)): void
extern
fun{a:t0p}
data_read (A: !data (a), i: bit, j: bit): a
extern
fun{a:t0p}
data_write (A: !data (a), i: bit, j: bit, x: a): void
local
assume
data_vtype (a:t0p) = arrayptr (a, 4)
in (* in of [local] *)
implement{a}
data_make_elt (x) = arrayptr_make_elt<a> (i2sz(4), x)
implement{}
data_free (A) = arrayptr_free (A)
implement{a}
data_read (A, i, j) = A[2 * bit2int (i) + bit2int (j)]
implement{a}
data_write (A, i, j, x) = A[2 * bit2int (i) + bit2int (j)] := x
end // end of [local]
(* ****** ****** *)
absvtype slot_vtype = ptr
vtypedef slot = slot_vtype
extern
fun{} slot_make (): slot
extern
fun{} slot_free (S: slot): void
extern
fun{} slot_get (S: !slot, i: bit): bit
extern
fun{} slot_set (S: !slot, i: bit, j: bit): void
local
assume
slot_vtype = arrayptr (bit, 2)
in (* in of [local] *)
implement{}
slot_make () =
arrayptr_make_elt<bit> (i2sz(2), int2bit(0))
// end of [slot_make]
implement{}
slot_free (S) = arrayptr_free (S)
implement{}
slot_get (S, i) = S[bit2int(i)]
implement{}
slot_set (S, i, j) = S[bit2int(i)] := j
end // end of [local]
(* ****** ****** *)
staload UN = "prelude/SATS/unsafe.sats"
(* ****** ****** *)
//
extern fun{} latest_get (): bit
extern fun{} latest_set (i: bit): void
extern fun{} reading_get (): bit
extern fun{} reading_set (i: bit): void
//
(* ****** ****** *)
fun{a:t0p}
fourslot_read
(
A: !data (a), S: !slot
) : a = let
val pair = latest_get ()
val () = reading_set (pair)
val index = slot_get (S, pair)
in
data_read (A, pair, index)
end // end of [fourslot_read]
(* ****** ****** *)
fun{a:t0p}
fourslot_write
(
A: !data (a), S: !slot, x: a
) : void = let
val pair = not (reading_get ())
val index = not (slot_get (S, pair))
val () = data_write (A, pair, index, x)
val () = slot_set (S, pair, index)
val () = latest_set (pair)
in
// nothing
end // end of [fourslot_write]
(* ****** ****** *)
implement
main0 () =
{
//
local
var latest: int = 0
in
implement{}
latest_get () = $UN.ptr1_get<bit> (addr@(latest))
implement{}
latest_set (i) = $UN.ptr1_set<bit> (addr@(latest), i)
end // end of [local]
//
local
var reading: int = 0
in
implement{}
reading_get () = $UN.ptr1_get<bit> (addr@(reading))
implement{}
reading_set (i) = $UN.ptr1_set<bit> (addr@(reading), i)
end // end of [local]
//
typedef T = int
//
val out = stdout_ref
//
val A = data_make_elt<T> (0)
//
val S = slot_make ()
//
val x0 = fourslot_read<T> (A, S)
val () = fprintln! (out, "x0 = ", x0)
val () = assertloc (x0 = 0)
//
val () = fourslot_write<T> (A, S, 1)
val () = fourslot_write<T> (A, S, ~1)
//
val x1 = fourslot_read<T> (A, S)
val () = fprintln! (out, "x1 = ", x1)
val () = assertloc (x1 = ~1)
//
val () = slot_free (S)
//
val () = data_free (A)
//
} // end of [main0]
(* ****** ****** *)
(* end of [fourslot.dats] *)
|
