0b55f123 |
1 | //#define NUMPROCS 5 |
2 | #define NUMPROCS 4 |
3 | #define BUFSIZE 4 |
4 | #define NR_SUBBUFS 2 |
5 | #define SUBBUF_SIZE (BUFSIZE / NR_SUBBUFS) |
6 | |
7 | byte write_off = 0; |
8 | byte read_off = 0; |
9 | byte events_lost = 0; |
10 | byte deliver = 0; // Number of subbuffers delivered |
11 | byte refcount = 0; |
12 | |
13 | byte commit_count[NR_SUBBUFS]; |
14 | |
15 | byte buffer_use_count[BUFSIZE]; |
16 | |
17 | proctype switcher() |
18 | { |
19 | int prev_off, new_off, tmp_commit; |
20 | int size; |
21 | |
22 | cmpxchg_loop: |
23 | atomic { |
24 | prev_off = write_off; |
25 | size = SUBBUF_SIZE - (prev_off % SUBBUF_SIZE); |
26 | new_off = prev_off + size; |
27 | if |
28 | :: new_off - read_off > BUFSIZE -> |
29 | goto not_needed; |
30 | :: else -> skip |
31 | fi; |
32 | } |
33 | atomic { |
34 | if |
35 | :: prev_off != write_off -> goto cmpxchg_loop |
36 | :: else -> write_off = new_off; |
37 | fi; |
38 | } |
39 | |
40 | atomic { |
41 | tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; |
42 | commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; |
43 | if |
44 | :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++ |
45 | :: else -> skip |
46 | fi; |
47 | } |
48 | not_needed: |
49 | skip; |
50 | } |
51 | |
52 | proctype tracer(byte size) |
53 | { |
54 | int prev_off, new_off, tmp_commit; |
55 | int i; |
56 | int j; |
57 | |
58 | cmpxchg_loop: |
59 | atomic { |
60 | prev_off = write_off; |
61 | new_off = prev_off + size; |
62 | } |
63 | atomic { |
64 | if |
65 | :: new_off - read_off > BUFSIZE -> goto lost |
66 | :: else -> skip |
67 | fi; |
68 | } |
69 | atomic { |
70 | if |
71 | :: prev_off != write_off -> goto cmpxchg_loop |
72 | :: else -> write_off = new_off; |
73 | fi; |
74 | i = 0; |
75 | do |
76 | :: i < size -> |
77 | buffer_use_count[(prev_off + i) % BUFSIZE] |
78 | = buffer_use_count[(prev_off + i) % BUFSIZE] + 1; |
79 | i++ |
80 | :: i >= size -> break |
81 | od; |
82 | } |
83 | do |
84 | :: j < BUFSIZE -> |
85 | assert(buffer_use_count[j] < 2); |
86 | j++ |
87 | :: j >= BUFSIZE -> break |
88 | od; |
89 | |
90 | |
91 | |
92 | // writing to buffer... |
93 | |
94 | atomic { |
95 | i = 0; |
96 | do |
97 | :: i < size -> |
98 | buffer_use_count[(prev_off + i) % BUFSIZE] |
99 | = buffer_use_count[(prev_off + i) % BUFSIZE] - 1; |
100 | i++ |
101 | :: i >= size -> break |
102 | od; |
103 | tmp_commit = commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] + size; |
104 | commit_count[(prev_off % BUFSIZE) / SUBBUF_SIZE] = tmp_commit; |
105 | if |
106 | :: tmp_commit % SUBBUF_SIZE == 0 -> deliver++ |
107 | :: else -> skip |
108 | fi; |
109 | } |
110 | goto end; |
111 | lost: |
112 | events_lost++; |
113 | end: |
114 | refcount = refcount - 1; |
115 | } |
116 | |
117 | proctype reader() |
118 | { |
119 | int i; |
120 | int j; |
121 | //atomic { |
122 | // do |
123 | // :: (deliver == (NUMPROCS - events_lost) / SUBBUF_SIZE) -> break; |
124 | // od; |
125 | //} |
126 | do |
127 | :: (write_off / SUBBUF_SIZE) - (read_off / SUBBUF_SIZE) > 0 && commit_count[(read_off % BUFSIZE) / SUBBUF_SIZE] % SUBBUF_SIZE == 0 -> |
128 | atomic { |
129 | i = 0; |
130 | do |
131 | :: i < SUBBUF_SIZE -> |
132 | buffer_use_count[(read_off + i) % BUFSIZE] |
133 | = buffer_use_count[(read_off + i) % BUFSIZE] + 1; |
134 | i++ |
135 | :: i >= SUBBUF_SIZE -> break |
136 | od; |
137 | } |
138 | j = 0; |
139 | do |
140 | :: j < BUFSIZE -> |
141 | assert(buffer_use_count[j] < 2); |
142 | j++ |
143 | :: j >= BUFSIZE -> break |
144 | od; |
145 | |
146 | // reading from buffer... |
147 | |
148 | atomic { |
149 | i = 0; |
150 | do |
151 | :: i < SUBBUF_SIZE -> |
152 | buffer_use_count[(read_off + i) % BUFSIZE] |
153 | = buffer_use_count[(read_off + i) % BUFSIZE] - 1; |
154 | i++ |
155 | :: i >= SUBBUF_SIZE -> break |
156 | od; |
157 | read_off = read_off + SUBBUF_SIZE; |
158 | } |
159 | :: read_off >= (NUMPROCS - events_lost) -> break; |
160 | od; |
161 | } |
162 | |
163 | proctype cleaner() |
164 | { |
165 | atomic { |
166 | do |
167 | :: refcount == 0 -> |
168 | run switcher(); |
169 | break; |
170 | od; |
171 | } |
172 | } |
173 | |
174 | init { |
175 | int i = 0; |
176 | int j = 0; |
177 | int sum = 0; |
178 | int commit_sum = 0; |
179 | |
180 | atomic { |
181 | i = 0; |
182 | do |
183 | :: i < NR_SUBBUFS -> |
184 | commit_count[i] = 0; |
185 | i++ |
186 | :: i >= NR_SUBBUFS -> break |
187 | od; |
188 | i = 0; |
189 | do |
190 | :: i < BUFSIZE -> |
191 | buffer_use_count[i] = 0; |
192 | i++ |
193 | :: i >= BUFSIZE -> break |
194 | od; |
195 | run reader(); |
196 | run cleaner(); |
197 | i = 0; |
198 | do |
199 | :: i < NUMPROCS -> |
200 | refcount = refcount + 1; |
201 | run tracer(1); |
202 | i++ |
203 | :: i >= NUMPROCS -> break |
204 | od; |
205 | run switcher(); |
206 | } |
207 | atomic { |
208 | assert(write_off - read_off >= 0); |
209 | j = 0; |
210 | commit_sum = 0; |
211 | do |
212 | :: j < NR_SUBBUFS -> |
213 | commit_sum = commit_sum + commit_count[j]; |
214 | j++ |
215 | :: j >= NR_SUBBUFS -> break |
216 | od; |
217 | assert(commit_sum <= write_off); |
218 | j = 0; |
219 | do |
220 | :: j < BUFSIZE -> |
221 | assert(buffer_use_count[j] < 2); |
222 | j++ |
223 | :: j >= BUFSIZE -> break |
224 | od; |
225 | |
226 | //assert(events_lost == 0); |
227 | } |
228 | } |