Commit | Line | Data |
---|---|---|
551ac1a3 MD |
1 | /* |
2 | * mem.spin: Promela code to validate memory barriers with OOO memory. | |
3 | * | |
4 | * This program is free software; you can redistribute it and/or modify | |
5 | * it under the terms of the GNU General Public License as published by | |
6 | * the Free Software Foundation; either version 2 of the License, or | |
7 | * (at your option) any later version. | |
8 | * | |
9 | * This program is distributed in the hope that it will be useful, | |
10 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
11 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
12 | * GNU General Public License for more details. | |
13 | * | |
14 | * You should have received a copy of the GNU General Public License | |
15 | * along with this program; if not, write to the Free Software | |
16 | * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. | |
17 | * | |
18 | * Copyright (c) 2009 Mathieu Desnoyers | |
19 | */ | |
20 | ||
21 | /* Promela validation variables. */ | |
22 | ||
23 | /* specific defines "included" here */ | |
24 | /* DEFINES file "included" here */ | |
25 | ||
26 | #define NR_READERS 1 | |
27 | #define NR_WRITERS 1 | |
28 | ||
29 | #define NR_PROCS 2 | |
30 | ||
31 | #define get_pid() (_pid) | |
32 | ||
33 | #define get_readerid() (get_pid()) | |
34 | ||
35 | /* | |
36 | * Produced process control and data flow. Updated after each instruction to | |
37 | * show which variables are ready. Using one-hot bit encoding per variable to | |
38 | * save state space. Used as triggers to execute the instructions having those | |
39 | * variables as input. Leaving bits active to inhibit instruction execution. | |
40 | * Scheme used to make instruction disabling and automatic dependency fall-back | |
41 | * automatic. | |
42 | */ | |
43 | ||
44 | #define CONSUME_TOKENS(state, bits, notbits) \ | |
45 | ((!(state & (notbits))) && (state & (bits)) == (bits)) | |
46 | ||
47 | #define PRODUCE_TOKENS(state, bits) \ | |
48 | state = state | (bits); | |
49 | ||
50 | #define CLEAR_TOKENS(state, bits) \ | |
51 | state = state & ~(bits) | |
52 | ||
53 | /* | |
54 | * Types of dependency : | |
55 | * | |
56 | * Data dependency | |
57 | * | |
58 | * - True dependency, Read-after-Write (RAW) | |
59 | * | |
60 | * This type of dependency happens when a statement depends on the result of a | |
61 | * previous statement. This applies to any statement which needs to read a | |
62 | * variable written by a preceding statement. | |
63 | * | |
64 | * - False dependency, Write-after-Read (WAR) | |
65 | * | |
66 | * Typically, variable renaming can ensure that this dependency goes away. | |
67 | * However, if the statements must read and then write from/to the same variable | |
68 | * in the OOO memory model, renaming may be impossible, and therefore this | |
69 | * causes a WAR dependency. | |
70 | * | |
71 | * - Output dependency, Write-after-Write (WAW) | |
72 | * | |
73 | * Two writes to the same variable in subsequent statements. Variable renaming | |
74 | * can ensure this is not needed, but can be required when writing multiple | |
75 | * times to the same OOO mem model variable. | |
76 | * | |
77 | * Control dependency | |
78 | * | |
79 | * Execution of a given instruction depends on a previous instruction evaluating | |
80 | * in a way that allows its execution. E.g. : branches. | |
81 | * | |
82 | * Useful considerations for joining dependencies after branch | |
83 | * | |
84 | * - Pre-dominance | |
85 | * | |
86 | * "We say box i dominates box j if every path (leading from input to output | |
87 | * through the diagram) which passes through box j must also pass through box | |
88 | * i. Thus box i dominates box j if box j is subordinate to box i in the | |
89 | * program." | |
90 | * | |
91 | * http://www.hipersoft.rice.edu/grads/publications/dom14.pdf | |
92 | * Other classic algorithm to calculate dominance : Lengauer-Tarjan (in gcc) | |
93 | * | |
94 | * - Post-dominance | |
95 | * | |
96 | * Just as pre-dominance, but with arcs of the data flow inverted, and input vs | |
97 | * output exchanged. Therefore, i post-dominating j ensures that every path | |
98 | * passing by j will pass by i before reaching the output. | |
99 | * | |
100 | * Other considerations | |
101 | * | |
102 | * Note about "volatile" keyword dependency : The compiler will order volatile | |
103 | * accesses so they appear in the right order on a given CPU. They can be | |
104 | * reordered by the CPU instruction scheduling. This therefore cannot be | |
105 | * considered as a depencency. | |
106 | * | |
107 | * References : | |
108 | * | |
109 | * Cooper, Keith D.; & Torczon, Linda. (2005). Engineering a Compiler. Morgan | |
110 | * Kaufmann. ISBN 1-55860-698-X. | |
111 | * Kennedy, Ken; & Allen, Randy. (2001). Optimizing Compilers for Modern | |
112 | * Architectures: A Dependence-based Approach. Morgan Kaufmann. ISBN | |
113 | * 1-55860-286-0. | |
114 | * Muchnick, Steven S. (1997). Advanced Compiler Design and Implementation. | |
115 | * Morgan Kaufmann. ISBN 1-55860-320-4. | |
116 | */ | |
117 | ||
118 | /* | |
119 | * Note about loops and nested calls | |
120 | * | |
121 | * To keep this model simple, loops expressed in the framework will behave as if | |
122 | * there was a core synchronizing instruction between loops. To see the effect | |
123 | * of loop unrolling, manually unrolling loops is required. Note that if loops | |
124 | * end or start with a core synchronizing instruction, the model is appropriate. | |
125 | * Nested calls are not supported. | |
126 | */ | |
127 | ||
128 | /* | |
129 | * Each process have its own data in cache. Caches are randomly updated. | |
130 | * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces | |
131 | * both. | |
132 | */ | |
133 | ||
134 | typedef per_proc_byte { | |
135 | byte val[NR_PROCS]; | |
136 | }; | |
137 | ||
138 | /* Bitfield has a maximum of 8 procs */ | |
139 | typedef per_proc_bit { | |
140 | byte bitfield; | |
141 | }; | |
142 | ||
143 | #define DECLARE_CACHED_VAR(type, x) \ | |
144 | type mem_##x; \ | |
145 | per_proc_##type cached_##x; \ | |
146 | per_proc_bit cache_dirty_##x; | |
147 | ||
148 | #define INIT_CACHED_VAR(x, v, j) \ | |
149 | mem_##x = v; \ | |
150 | cache_dirty_##x.bitfield = 0; \ | |
151 | j = 0; \ | |
152 | do \ | |
153 | :: j < NR_PROCS -> \ | |
154 | cached_##x.val[j] = v; \ | |
155 | j++ \ | |
156 | :: j >= NR_PROCS -> break \ | |
157 | od; | |
158 | ||
159 | #define IS_CACHE_DIRTY(x, id) (cache_dirty_##x.bitfield & (1 << id)) | |
160 | ||
161 | #define READ_CACHED_VAR(x) (cached_##x.val[get_pid()]) | |
162 | ||
163 | #define WRITE_CACHED_VAR(x, v) \ | |
164 | atomic { \ | |
165 | cached_##x.val[get_pid()] = v; \ | |
166 | cache_dirty_##x.bitfield = \ | |
167 | cache_dirty_##x.bitfield | (1 << get_pid()); \ | |
168 | } | |
169 | ||
170 | #define CACHE_WRITE_TO_MEM(x, id) \ | |
171 | if \ | |
172 | :: IS_CACHE_DIRTY(x, id) -> \ | |
173 | mem_##x = cached_##x.val[id]; \ | |
174 | cache_dirty_##x.bitfield = \ | |
175 | cache_dirty_##x.bitfield & (~(1 << id)); \ | |
176 | :: else -> \ | |
177 | skip \ | |
178 | fi; | |
179 | ||
180 | #define CACHE_READ_FROM_MEM(x, id) \ | |
181 | if \ | |
182 | :: !IS_CACHE_DIRTY(x, id) -> \ | |
183 | cached_##x.val[id] = mem_##x;\ | |
184 | :: else -> \ | |
185 | skip \ | |
186 | fi; | |
187 | ||
188 | /* | |
189 | * May update other caches if cache is dirty, or not. | |
190 | */ | |
191 | #define RANDOM_CACHE_WRITE_TO_MEM(x, id)\ | |
192 | if \ | |
193 | :: 1 -> CACHE_WRITE_TO_MEM(x, id); \ | |
194 | :: 1 -> skip \ | |
195 | fi; | |
196 | ||
197 | #define RANDOM_CACHE_READ_FROM_MEM(x, id)\ | |
198 | if \ | |
199 | :: 1 -> CACHE_READ_FROM_MEM(x, id); \ | |
200 | :: 1 -> skip \ | |
201 | fi; | |
202 | ||
203 | /* Must consume all prior read tokens. All subsequent reads depend on it. */ | |
204 | inline smp_rmb(i, j) | |
205 | { | |
206 | atomic { | |
207 | CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); | |
208 | i = 0; | |
209 | do | |
210 | :: i < NR_READERS -> | |
211 | CACHE_READ_FROM_MEM(urcu_active_readers[i], get_pid()); | |
212 | i++ | |
213 | :: i >= NR_READERS -> break | |
214 | od; | |
215 | CACHE_READ_FROM_MEM(generation_ptr, get_pid()); | |
216 | } | |
217 | } | |
218 | ||
219 | /* Must consume all prior write tokens. All subsequent writes depend on it. */ | |
220 | inline smp_wmb(i, j) | |
221 | { | |
222 | atomic { | |
223 | CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); | |
224 | i = 0; | |
225 | do | |
226 | :: i < NR_READERS -> | |
227 | CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid()); | |
228 | i++ | |
229 | :: i >= NR_READERS -> break | |
230 | od; | |
231 | CACHE_WRITE_TO_MEM(generation_ptr, get_pid()); | |
232 | } | |
233 | } | |
234 | ||
235 | /* Synchronization point. Must consume all prior read and write tokens. All | |
236 | * subsequent reads and writes depend on it. */ | |
237 | inline smp_mb(i, j) | |
238 | { | |
239 | atomic { | |
240 | smp_wmb(i, j); | |
241 | smp_rmb(i, j); | |
242 | } | |
243 | } | |
244 | ||
245 | ||
246 | #ifdef REMOTE_BARRIERS | |
247 | ||
248 | bit reader_barrier[NR_READERS]; | |
249 | ||
250 | /* | |
251 | * We cannot leave the barriers dependencies in place in REMOTE_BARRIERS mode | |
252 | * because they would add unexisting core synchronization and would therefore | |
253 | * create an incomplete model. | |
254 | * Therefore, we model the read-side memory barriers by completely disabling the | |
255 | * memory barriers and their dependencies from the read-side. One at a time | |
256 | * (different verification runs), we make a different instruction listen for | |
257 | * signals. | |
258 | */ | |
259 | ||
260 | #define smp_mb_reader(i, j) | |
261 | ||
262 | /* | |
263 | * Service 0, 1 or many barrier requests. | |
264 | */ | |
265 | inline smp_mb_recv(i, j) | |
266 | { | |
267 | do | |
268 | :: (reader_barrier[get_readerid()] == 1) -> | |
269 | smp_mb(i, j); | |
270 | reader_barrier[get_readerid()] = 0; | |
271 | :: 1 -> skip; | |
272 | :: 1 -> break; | |
273 | od; | |
274 | } | |
275 | ||
276 | inline smp_mb_send(i, j) | |
277 | { | |
278 | smp_mb(i, j); | |
279 | i = 0; | |
280 | do | |
281 | :: i < NR_READERS -> | |
282 | reader_barrier[i] = 1; | |
283 | do | |
284 | :: (reader_barrier[i] == 1) -> skip; | |
285 | :: (reader_barrier[i] == 0) -> break; | |
286 | od; | |
287 | i++; | |
288 | :: i >= NR_READERS -> | |
289 | break | |
290 | od; | |
291 | smp_mb(i, j); | |
292 | } | |
293 | ||
294 | #else | |
295 | ||
296 | #define smp_mb_send smp_mb | |
297 | #define smp_mb_reader smp_mb | |
298 | #define smp_mb_recv(i, j) | |
299 | ||
300 | #endif | |
301 | ||
302 | /* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */ | |
303 | DECLARE_CACHED_VAR(byte, urcu_gp_ctr); | |
304 | /* Note ! currently only two readers */ | |
305 | DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]); | |
306 | /* pointer generation */ | |
307 | DECLARE_CACHED_VAR(byte, generation_ptr); | |
308 | ||
309 | byte last_free_gen = 0; | |
310 | bit free_done = 0; | |
311 | byte read_generation[NR_READERS]; | |
312 | bit data_access[NR_READERS]; | |
313 | ||
314 | bit write_lock = 0; | |
315 | ||
316 | bit init_done = 0; | |
317 | ||
318 | bit sighand_exec = 0; | |
319 | ||
320 | inline wait_init_done() | |
321 | { | |
322 | do | |
323 | :: init_done == 0 -> skip; | |
324 | :: else -> break; | |
325 | od; | |
326 | } | |
327 | ||
328 | inline ooo_mem(i) | |
329 | { | |
330 | atomic { | |
331 | RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); | |
332 | i = 0; | |
333 | do | |
334 | :: i < NR_READERS -> | |
335 | RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i], | |
336 | get_pid()); | |
337 | i++ | |
338 | :: i >= NR_READERS -> break | |
339 | od; | |
340 | RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid()); | |
341 | RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); | |
342 | i = 0; | |
343 | do | |
344 | :: i < NR_READERS -> | |
345 | RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i], | |
346 | get_pid()); | |
347 | i++ | |
348 | :: i >= NR_READERS -> break | |
349 | od; | |
350 | RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid()); | |
351 | } | |
352 | } | |
353 | ||
354 | /* | |
355 | * Bit encoding, urcu_reader : | |
356 | */ | |
357 | ||
358 | int _proc_urcu_reader; | |
359 | #define proc_urcu_reader _proc_urcu_reader | |
360 | ||
361 | /* Body of PROCEDURE_READ_LOCK */ | |
362 | #define READ_PROD_A_READ (1 << 0) | |
363 | #define READ_PROD_B_IF_TRUE (1 << 1) | |
364 | #define READ_PROD_B_IF_FALSE (1 << 2) | |
365 | #define READ_PROD_C_IF_TRUE_READ (1 << 3) | |
366 | ||
367 | #define PROCEDURE_READ_LOCK(base, consumetoken, producetoken) \ | |
368 | :: CONSUME_TOKENS(proc_urcu_reader, consumetoken, READ_PROD_A_READ << base) -> \ | |
369 | ooo_mem(i); \ | |
370 | tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \ | |
371 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_A_READ << base); \ | |
372 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
373 | READ_PROD_A_READ << base, /* RAW, pre-dominant */ \ | |
374 | (READ_PROD_B_IF_TRUE | READ_PROD_B_IF_FALSE) << base) -> \ | |
375 | if \ | |
376 | :: (!(tmp & RCU_GP_CTR_NEST_MASK)) -> \ | |
377 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base); \ | |
378 | :: else -> \ | |
379 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_FALSE << base); \ | |
380 | fi; \ | |
381 | /* IF TRUE */ \ | |
382 | :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base, \ | |
383 | READ_PROD_C_IF_TRUE_READ << base) -> \ | |
384 | ooo_mem(i); \ | |
385 | tmp2 = READ_CACHED_VAR(urcu_gp_ctr); \ | |
386 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_C_IF_TRUE_READ << base); \ | |
387 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
388 | (READ_PROD_C_IF_TRUE_READ /* pre-dominant */ \ | |
389 | | READ_PROD_A_READ) << base, /* WAR */ \ | |
390 | producetoken) -> \ | |
391 | ooo_mem(i); \ | |
392 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2); \ | |
393 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ | |
394 | /* IF_MERGE implies \ | |
395 | * post-dominance */ \ | |
396 | /* ELSE */ \ | |
397 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
398 | (READ_PROD_B_IF_FALSE /* pre-dominant */ \ | |
399 | | READ_PROD_A_READ) << base, /* WAR */ \ | |
400 | producetoken) -> \ | |
401 | ooo_mem(i); \ | |
402 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], \ | |
403 | tmp + 1); \ | |
404 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ | |
405 | /* IF_MERGE implies \ | |
406 | * post-dominance */ \ | |
407 | /* ENDIF */ \ | |
408 | skip | |
409 | ||
410 | /* Body of PROCEDURE_READ_LOCK */ | |
411 | #define READ_PROC_READ_UNLOCK (1 << 0) | |
412 | ||
413 | #define PROCEDURE_READ_UNLOCK(base, consumetoken, producetoken) \ | |
414 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
415 | consumetoken, \ | |
416 | READ_PROC_READ_UNLOCK << base) -> \ | |
417 | ooo_mem(i); \ | |
418 | tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \ | |
419 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_UNLOCK << base); \ | |
420 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
421 | consumetoken \ | |
422 | | (READ_PROC_READ_UNLOCK << base), /* WAR */ \ | |
423 | producetoken) -> \ | |
424 | ooo_mem(i); \ | |
425 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1); \ | |
426 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ | |
427 | skip | |
428 | ||
429 | ||
430 | #define READ_PROD_NONE (1 << 0) | |
431 | ||
432 | /* PROCEDURE_READ_LOCK base = << 1 : 1 to 5 */ | |
433 | #define READ_LOCK_BASE 1 | |
434 | #define READ_LOCK_OUT (1 << 5) | |
435 | ||
436 | #define READ_PROC_FIRST_MB (1 << 6) | |
437 | ||
438 | /* PROCEDURE_READ_LOCK (NESTED) base : << 7 : 7 to 11 */ | |
439 | #define READ_LOCK_NESTED_BASE 7 | |
440 | #define READ_LOCK_NESTED_OUT (1 << 11) | |
441 | ||
442 | #define READ_PROC_READ_GEN (1 << 12) | |
443 | ||
444 | /* PROCEDURE_READ_UNLOCK (NESTED) base = << 13 : 13 to 14 */ | |
445 | #define READ_UNLOCK_NESTED_BASE 13 | |
446 | #define READ_UNLOCK_NESTED_OUT (1 << 14) | |
447 | ||
448 | #define READ_PROC_SECOND_MB (1 << 15) | |
449 | ||
450 | /* PROCEDURE_READ_UNLOCK base = << 16 : 16 to 17 */ | |
451 | #define READ_UNLOCK_BASE 16 | |
452 | #define READ_UNLOCK_OUT (1 << 17) | |
453 | ||
454 | /* PROCEDURE_READ_LOCK_UNROLL base = << 18 : 18 to 22 */ | |
455 | #define READ_LOCK_UNROLL_BASE 18 | |
456 | #define READ_LOCK_OUT_UNROLL (1 << 22) | |
457 | ||
458 | #define READ_PROC_THIRD_MB (1 << 23) | |
459 | ||
460 | #define READ_PROC_READ_GEN_UNROLL (1 << 24) | |
461 | ||
462 | #define READ_PROC_FOURTH_MB (1 << 25) | |
463 | ||
464 | /* PROCEDURE_READ_UNLOCK_UNROLL base = << 26 : 26 to 27 */ | |
465 | #define READ_UNLOCK_UNROLL_BASE 26 | |
466 | #define READ_UNLOCK_OUT_UNROLL (1 << 27) | |
467 | ||
468 | ||
469 | /* Should not include branches */ | |
470 | #define READ_PROC_ALL_TOKENS (READ_PROD_NONE \ | |
471 | | READ_LOCK_OUT \ | |
472 | | READ_PROC_FIRST_MB \ | |
473 | | READ_LOCK_NESTED_OUT \ | |
474 | | READ_PROC_READ_GEN \ | |
475 | | READ_UNLOCK_NESTED_OUT \ | |
476 | | READ_PROC_SECOND_MB \ | |
477 | | READ_UNLOCK_OUT \ | |
478 | | READ_LOCK_OUT_UNROLL \ | |
479 | | READ_PROC_THIRD_MB \ | |
480 | | READ_PROC_READ_GEN_UNROLL \ | |
481 | | READ_PROC_FOURTH_MB \ | |
482 | | READ_UNLOCK_OUT_UNROLL) | |
483 | ||
484 | /* Must clear all tokens, including branches */ | |
485 | #define READ_PROC_ALL_TOKENS_CLEAR ((1 << 28) - 1) | |
486 | ||
487 | inline urcu_one_read(i, j, nest_i, tmp, tmp2) | |
488 | { | |
489 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_NONE); | |
490 | ||
491 | #ifdef NO_MB | |
492 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); | |
493 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); | |
494 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB); | |
495 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB); | |
496 | #endif | |
497 | ||
498 | #ifdef REMOTE_BARRIERS | |
499 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); | |
500 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); | |
501 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB); | |
502 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB); | |
503 | #endif | |
504 | ||
505 | do | |
506 | :: 1 -> | |
507 | ||
508 | #ifdef REMOTE_BARRIERS | |
509 | /* | |
510 | * Signal-based memory barrier will only execute when the | |
511 | * execution order appears in program order. | |
512 | */ | |
513 | if | |
514 | :: 1 -> | |
515 | atomic { | |
516 | if | |
517 | :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE, | |
518 | READ_LOCK_OUT | READ_LOCK_NESTED_OUT | |
519 | | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT | |
520 | | READ_UNLOCK_OUT | |
521 | | READ_LOCK_OUT_UNROLL | |
522 | | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
523 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT, | |
524 | READ_LOCK_NESTED_OUT | |
525 | | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT | |
526 | | READ_UNLOCK_OUT | |
527 | | READ_LOCK_OUT_UNROLL | |
528 | | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
529 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | READ_LOCK_NESTED_OUT, | |
530 | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT | |
531 | | READ_UNLOCK_OUT | |
532 | | READ_LOCK_OUT_UNROLL | |
533 | | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
534 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
535 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN, | |
536 | READ_UNLOCK_NESTED_OUT | |
537 | | READ_UNLOCK_OUT | |
538 | | READ_LOCK_OUT_UNROLL | |
539 | | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
540 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
541 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT, | |
542 | READ_UNLOCK_OUT | |
543 | | READ_LOCK_OUT_UNROLL | |
544 | | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
545 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
546 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT | |
547 | | READ_UNLOCK_OUT, | |
548 | READ_LOCK_OUT_UNROLL | |
549 | | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
550 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
551 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT | |
552 | | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL, | |
553 | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
554 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
555 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT | |
556 | | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL | |
557 | | READ_PROC_READ_GEN_UNROLL, | |
558 | READ_UNLOCK_OUT_UNROLL) | |
559 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
560 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_UNLOCK_NESTED_OUT | |
561 | | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL | |
562 | | READ_PROC_READ_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL, | |
563 | 0) -> | |
564 | goto non_atomic3; | |
565 | non_atomic3_end: | |
566 | skip; | |
567 | fi; | |
568 | } | |
569 | :: 1 -> skip; | |
570 | fi; | |
571 | ||
572 | goto non_atomic3_skip; | |
573 | non_atomic3: | |
574 | smp_mb_recv(i, j); | |
575 | goto non_atomic3_end; | |
576 | non_atomic3_skip: | |
577 | ||
578 | #endif /* REMOTE_BARRIERS */ | |
579 | ||
580 | atomic { | |
581 | if | |
582 | PROCEDURE_READ_LOCK(READ_LOCK_BASE, READ_PROD_NONE, READ_LOCK_OUT); | |
583 | ||
584 | :: CONSUME_TOKENS(proc_urcu_reader, | |
585 | READ_LOCK_OUT, /* post-dominant */ | |
586 | READ_PROC_FIRST_MB) -> | |
587 | smp_mb_reader(i, j); | |
588 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); | |
589 | ||
590 | PROCEDURE_READ_LOCK(READ_LOCK_NESTED_BASE, READ_PROC_FIRST_MB | READ_LOCK_OUT, | |
591 | READ_LOCK_NESTED_OUT); | |
592 | ||
593 | :: CONSUME_TOKENS(proc_urcu_reader, | |
594 | READ_PROC_FIRST_MB, /* mb() orders reads */ | |
595 | READ_PROC_READ_GEN) -> | |
596 | ooo_mem(i); | |
597 | read_generation[get_readerid()] = | |
598 | READ_CACHED_VAR(generation_ptr); | |
599 | goto non_atomic; | |
600 | non_atomic_end: | |
601 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN); | |
602 | ||
603 | /* Note : we remove the nested memory barrier from the read unlock | |
604 | * model, given it is not usually needed. The implementation has the barrier | |
605 | * because the performance impact added by a branch in the common case does not | |
606 | * justify it. | |
607 | */ | |
608 | ||
609 | PROCEDURE_READ_UNLOCK(READ_UNLOCK_NESTED_BASE, | |
610 | READ_PROC_FIRST_MB | |
611 | | READ_LOCK_OUT | |
612 | | READ_LOCK_NESTED_OUT, | |
613 | READ_UNLOCK_NESTED_OUT); | |
614 | ||
615 | ||
616 | :: CONSUME_TOKENS(proc_urcu_reader, | |
617 | READ_PROC_READ_GEN /* mb() orders reads */ | |
618 | | READ_PROC_FIRST_MB /* mb() ordered */ | |
619 | | READ_LOCK_OUT /* post-dominant */ | |
620 | | READ_LOCK_NESTED_OUT /* post-dominant */ | |
621 | | READ_UNLOCK_NESTED_OUT, | |
622 | READ_PROC_SECOND_MB) -> | |
623 | smp_mb_reader(i, j); | |
624 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); | |
625 | ||
626 | PROCEDURE_READ_UNLOCK(READ_UNLOCK_BASE, | |
627 | READ_PROC_SECOND_MB /* mb() orders reads */ | |
628 | | READ_PROC_FIRST_MB /* mb() orders reads */ | |
629 | | READ_LOCK_NESTED_OUT /* RAW */ | |
630 | | READ_LOCK_OUT /* RAW */ | |
631 | | READ_UNLOCK_NESTED_OUT, /* RAW */ | |
632 | READ_UNLOCK_OUT); | |
633 | ||
634 | /* Unrolling loop : second consecutive lock */ | |
635 | /* reading urcu_active_readers, which have been written by | |
636 | * READ_UNLOCK_OUT : RAW */ | |
637 | PROCEDURE_READ_LOCK(READ_LOCK_UNROLL_BASE, | |
638 | READ_UNLOCK_OUT /* RAW */ | |
639 | | READ_PROC_SECOND_MB /* mb() orders reads */ | |
640 | | READ_PROC_FIRST_MB /* mb() orders reads */ | |
641 | | READ_LOCK_NESTED_OUT /* RAW */ | |
642 | | READ_LOCK_OUT /* RAW */ | |
643 | | READ_UNLOCK_NESTED_OUT, /* RAW */ | |
644 | READ_LOCK_OUT_UNROLL); | |
645 | ||
646 | ||
647 | :: CONSUME_TOKENS(proc_urcu_reader, | |
648 | READ_PROC_FIRST_MB /* mb() ordered */ | |
649 | | READ_PROC_SECOND_MB /* mb() ordered */ | |
650 | | READ_LOCK_OUT_UNROLL /* post-dominant */ | |
651 | | READ_LOCK_NESTED_OUT | |
652 | | READ_LOCK_OUT | |
653 | | READ_UNLOCK_NESTED_OUT | |
654 | | READ_UNLOCK_OUT, | |
655 | READ_PROC_THIRD_MB) -> | |
656 | smp_mb_reader(i, j); | |
657 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB); | |
658 | ||
659 | :: CONSUME_TOKENS(proc_urcu_reader, | |
660 | READ_PROC_FIRST_MB /* mb() orders reads */ | |
661 | | READ_PROC_SECOND_MB /* mb() orders reads */ | |
662 | | READ_PROC_THIRD_MB, /* mb() orders reads */ | |
663 | READ_PROC_READ_GEN_UNROLL) -> | |
664 | ooo_mem(i); | |
665 | read_generation[get_readerid()] = | |
666 | READ_CACHED_VAR(generation_ptr); | |
667 | goto non_atomic2; | |
668 | non_atomic2_end: | |
669 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL); | |
670 | ||
671 | :: CONSUME_TOKENS(proc_urcu_reader, | |
672 | READ_PROC_READ_GEN_UNROLL /* mb() orders reads */ | |
673 | | READ_PROC_FIRST_MB /* mb() ordered */ | |
674 | | READ_PROC_SECOND_MB /* mb() ordered */ | |
675 | | READ_PROC_THIRD_MB /* mb() ordered */ | |
676 | | READ_LOCK_OUT_UNROLL /* post-dominant */ | |
677 | | READ_LOCK_NESTED_OUT | |
678 | | READ_LOCK_OUT | |
679 | | READ_UNLOCK_NESTED_OUT | |
680 | | READ_UNLOCK_OUT, | |
681 | READ_PROC_FOURTH_MB) -> | |
682 | smp_mb_reader(i, j); | |
683 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB); | |
684 | ||
685 | PROCEDURE_READ_UNLOCK(READ_UNLOCK_UNROLL_BASE, | |
686 | READ_PROC_FOURTH_MB /* mb() orders reads */ | |
687 | | READ_PROC_THIRD_MB /* mb() orders reads */ | |
688 | | READ_LOCK_OUT_UNROLL /* RAW */ | |
689 | | READ_PROC_SECOND_MB /* mb() orders reads */ | |
690 | | READ_PROC_FIRST_MB /* mb() orders reads */ | |
691 | | READ_LOCK_NESTED_OUT /* RAW */ | |
692 | | READ_LOCK_OUT /* RAW */ | |
693 | | READ_UNLOCK_NESTED_OUT, /* RAW */ | |
694 | READ_UNLOCK_OUT_UNROLL); | |
695 | :: CONSUME_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS, 0) -> | |
696 | CLEAR_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS_CLEAR); | |
697 | break; | |
698 | fi; | |
699 | } | |
700 | od; | |
701 | /* | |
702 | * Dependency between consecutive loops : | |
703 | * RAW dependency on | |
704 | * WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1) | |
705 | * tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); | |
706 | * between loops. | |
707 | * _WHEN THE MB()s are in place_, they add full ordering of the | |
708 | * generation pointer read wrt active reader count read, which ensures | |
709 | * execution will not spill across loop execution. | |
710 | * However, in the event mb()s are removed (execution using signal | |
711 | * handler to promote barrier()() -> smp_mb()), nothing prevents one loop | |
712 | * to spill its execution on other loop's execution. | |
713 | */ | |
714 | goto end; | |
715 | non_atomic: | |
716 | data_access[get_readerid()] = 1; | |
717 | data_access[get_readerid()] = 0; | |
718 | goto non_atomic_end; | |
719 | non_atomic2: | |
720 | data_access[get_readerid()] = 1; | |
721 | data_access[get_readerid()] = 0; | |
722 | goto non_atomic2_end; | |
723 | end: | |
724 | skip; | |
725 | } | |
726 | ||
727 | ||
728 | ||
729 | active proctype urcu_reader() | |
730 | { | |
731 | byte i, j, nest_i; | |
732 | byte tmp, tmp2; | |
733 | ||
734 | wait_init_done(); | |
735 | ||
736 | assert(get_pid() < NR_PROCS); | |
737 | ||
738 | end_reader: | |
739 | do | |
740 | :: 1 -> | |
741 | /* | |
742 | * We do not test reader's progress here, because we are mainly | |
743 | * interested in writer's progress. The reader never blocks | |
744 | * anyway. We have to test for reader/writer's progress | |
745 | * separately, otherwise we could think the writer is doing | |
746 | * progress when it's blocked by an always progressing reader. | |
747 | */ | |
748 | #ifdef READER_PROGRESS | |
749 | progress_reader: | |
750 | #endif | |
751 | urcu_one_read(i, j, nest_i, tmp, tmp2); | |
752 | od; | |
753 | } | |
754 | ||
755 | /* no name clash please */ | |
756 | #undef proc_urcu_reader | |
757 | ||
758 | ||
759 | /* Model the RCU update process. */ | |
760 | ||
761 | /* | |
762 | * Bit encoding, urcu_writer : | |
763 | * Currently only supports one reader. | |
764 | */ | |
765 | ||
766 | int _proc_urcu_writer; | |
767 | #define proc_urcu_writer _proc_urcu_writer | |
768 | ||
769 | #define WRITE_PROD_NONE (1 << 0) | |
770 | ||
771 | #define WRITE_PROC_FIRST_MB (1 << 1) | |
772 | ||
773 | /* first flip */ | |
774 | #define WRITE_PROC_FIRST_READ_GP (1 << 2) | |
775 | #define WRITE_PROC_FIRST_WRITE_GP (1 << 3) | |
776 | #define WRITE_PROC_FIRST_WAIT (1 << 4) | |
777 | #define WRITE_PROC_FIRST_WAIT_LOOP (1 << 5) | |
778 | ||
779 | /* second flip */ | |
780 | #define WRITE_PROC_SECOND_READ_GP (1 << 6) | |
781 | #define WRITE_PROC_SECOND_WRITE_GP (1 << 7) | |
782 | #define WRITE_PROC_SECOND_WAIT (1 << 8) | |
783 | #define WRITE_PROC_SECOND_WAIT_LOOP (1 << 9) | |
784 | ||
785 | #define WRITE_PROC_SECOND_MB (1 << 10) | |
786 | ||
787 | #define WRITE_PROC_ALL_TOKENS (WRITE_PROD_NONE \ | |
788 | | WRITE_PROC_FIRST_MB \ | |
789 | | WRITE_PROC_FIRST_READ_GP \ | |
790 | | WRITE_PROC_FIRST_WRITE_GP \ | |
791 | | WRITE_PROC_FIRST_WAIT \ | |
792 | | WRITE_PROC_SECOND_READ_GP \ | |
793 | | WRITE_PROC_SECOND_WRITE_GP \ | |
794 | | WRITE_PROC_SECOND_WAIT \ | |
795 | | WRITE_PROC_SECOND_MB) | |
796 | ||
797 | #define WRITE_PROC_ALL_TOKENS_CLEAR ((1 << 11) - 1) | |
798 | ||
799 | active proctype urcu_writer() | |
800 | { | |
801 | byte i, j; | |
802 | byte tmp, tmp2, tmpa; | |
803 | byte old_gen; | |
804 | ||
805 | wait_init_done(); | |
806 | ||
807 | assert(get_pid() < NR_PROCS); | |
808 | ||
809 | do | |
810 | :: (READ_CACHED_VAR(generation_ptr) < 5) -> | |
811 | #ifdef WRITER_PROGRESS | |
812 | progress_writer1: | |
813 | #endif | |
814 | ooo_mem(i); | |
815 | atomic { | |
816 | old_gen = READ_CACHED_VAR(generation_ptr); | |
817 | WRITE_CACHED_VAR(generation_ptr, old_gen + 1); | |
818 | } | |
819 | ooo_mem(i); | |
820 | ||
821 | do | |
822 | :: 1 -> | |
823 | atomic { | |
824 | if | |
825 | :: write_lock == 0 -> | |
826 | write_lock = 1; | |
827 | break; | |
828 | :: else -> | |
829 | skip; | |
830 | fi; | |
831 | } | |
832 | od; | |
833 | ||
834 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROD_NONE); | |
835 | ||
836 | #ifdef NO_MB | |
837 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB); | |
838 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB); | |
839 | #endif | |
840 | ||
841 | #ifdef SINGLE_FLIP | |
842 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); | |
843 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP); | |
844 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT); | |
845 | #endif | |
846 | ||
847 | do | |
848 | :: CONSUME_TOKENS(proc_urcu_writer, | |
849 | WRITE_PROD_NONE, | |
850 | WRITE_PROC_FIRST_MB) -> | |
851 | smp_mb_send(i, j); | |
852 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB); | |
853 | ||
854 | /* first flip */ | |
855 | :: CONSUME_TOKENS(proc_urcu_writer, | |
856 | WRITE_PROC_FIRST_MB, | |
857 | WRITE_PROC_FIRST_READ_GP) -> | |
858 | tmpa = READ_CACHED_VAR(urcu_gp_ctr); | |
859 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_READ_GP); | |
860 | :: CONSUME_TOKENS(proc_urcu_writer, | |
861 | WRITE_PROC_FIRST_MB | WRITE_PROC_FIRST_READ_GP, | |
862 | WRITE_PROC_FIRST_WRITE_GP) -> | |
863 | ooo_mem(i); | |
864 | WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT); | |
865 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WRITE_GP); | |
866 | ||
867 | :: CONSUME_TOKENS(proc_urcu_writer, | |
868 | //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */ | |
869 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
870 | WRITE_PROC_FIRST_WAIT | WRITE_PROC_FIRST_WAIT_LOOP) -> | |
871 | ooo_mem(i); | |
872 | /* ONLY WAITING FOR READER 0 */ | |
873 | tmp2 = READ_CACHED_VAR(urcu_active_readers[0]); | |
874 | if | |
875 | :: (tmp2 & RCU_GP_CTR_NEST_MASK) | |
876 | && ((tmp2 ^ RCU_GP_CTR_BIT) & RCU_GP_CTR_BIT) -> | |
877 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP); | |
878 | :: else -> | |
879 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT); | |
880 | fi; | |
881 | ||
882 | :: CONSUME_TOKENS(proc_urcu_writer, | |
883 | //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */ | |
884 | WRITE_PROC_FIRST_WRITE_GP | |
885 | | WRITE_PROC_FIRST_READ_GP | |
886 | | WRITE_PROC_FIRST_WAIT_LOOP | |
887 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
888 | 0) -> | |
889 | #ifndef GEN_ERROR_WRITER_PROGRESS | |
890 | smp_mb_send(i, j); | |
891 | #else | |
892 | ooo_mem(i); | |
893 | #endif | |
894 | /* This instruction loops to WRITE_PROC_FIRST_WAIT */ | |
895 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP | WRITE_PROC_FIRST_WAIT); | |
896 | ||
897 | /* second flip */ | |
898 | :: CONSUME_TOKENS(proc_urcu_writer, | |
899 | WRITE_PROC_FIRST_WAIT /* Control dependency : need to branch out of | |
900 | * the loop to execute the next flip (CHECK) */ | |
901 | | WRITE_PROC_FIRST_WRITE_GP | |
902 | | WRITE_PROC_FIRST_READ_GP | |
903 | | WRITE_PROC_FIRST_MB, | |
904 | WRITE_PROC_SECOND_READ_GP) -> | |
905 | //smp_mb_send(i, j); //TEST | |
906 | ooo_mem(i); | |
907 | tmpa = READ_CACHED_VAR(urcu_gp_ctr); | |
908 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); | |
909 | :: CONSUME_TOKENS(proc_urcu_writer, | |
910 | WRITE_PROC_FIRST_MB | |
911 | | WRITE_PROC_FIRST_READ_GP | |
912 | | WRITE_PROC_FIRST_WRITE_GP | |
913 | | WRITE_PROC_SECOND_READ_GP, | |
914 | WRITE_PROC_SECOND_WRITE_GP) -> | |
915 | ooo_mem(i); | |
916 | WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT); | |
917 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP); | |
918 | ||
919 | :: CONSUME_TOKENS(proc_urcu_writer, | |
920 | //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */ | |
921 | WRITE_PROC_FIRST_WAIT | |
922 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
923 | WRITE_PROC_SECOND_WAIT | WRITE_PROC_SECOND_WAIT_LOOP) -> | |
924 | ooo_mem(i); | |
925 | /* ONLY WAITING FOR READER 0 */ | |
926 | tmp2 = READ_CACHED_VAR(urcu_active_readers[0]); | |
927 | if | |
928 | :: (tmp2 & RCU_GP_CTR_NEST_MASK) | |
929 | && ((tmp2 ^ 0) & RCU_GP_CTR_BIT) -> | |
930 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP); | |
931 | :: else -> | |
932 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT); | |
933 | fi; | |
934 | ||
935 | :: CONSUME_TOKENS(proc_urcu_writer, | |
936 | //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */ | |
937 | WRITE_PROC_SECOND_WRITE_GP | |
938 | | WRITE_PROC_FIRST_WRITE_GP | |
939 | | WRITE_PROC_SECOND_READ_GP | |
940 | | WRITE_PROC_FIRST_READ_GP | |
941 | | WRITE_PROC_SECOND_WAIT_LOOP | |
942 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
943 | 0) -> | |
944 | #ifndef GEN_ERROR_WRITER_PROGRESS | |
945 | smp_mb_send(i, j); | |
946 | #else | |
947 | ooo_mem(i); | |
948 | #endif | |
949 | /* This instruction loops to WRITE_PROC_SECOND_WAIT */ | |
950 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP | WRITE_PROC_SECOND_WAIT); | |
951 | ||
952 | ||
953 | :: CONSUME_TOKENS(proc_urcu_writer, | |
954 | WRITE_PROC_FIRST_WAIT | |
955 | | WRITE_PROC_SECOND_WAIT | |
956 | | WRITE_PROC_FIRST_READ_GP | |
957 | | WRITE_PROC_SECOND_READ_GP | |
958 | | WRITE_PROC_FIRST_WRITE_GP | |
959 | | WRITE_PROC_SECOND_WRITE_GP | |
960 | | WRITE_PROC_FIRST_MB, | |
961 | WRITE_PROC_SECOND_MB) -> | |
962 | smp_mb_send(i, j); | |
963 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB); | |
964 | ||
965 | :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) -> | |
966 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR); | |
967 | break; | |
968 | od; | |
969 | ||
970 | write_lock = 0; | |
971 | /* free-up step, e.g., kfree(). */ | |
972 | atomic { | |
973 | last_free_gen = old_gen; | |
974 | free_done = 1; | |
975 | } | |
976 | :: else -> break; | |
977 | od; | |
978 | /* | |
979 | * Given the reader loops infinitely, let the writer also busy-loop | |
980 | * with progress here so, with weak fairness, we can test the | |
981 | * writer's progress. | |
982 | */ | |
983 | end_writer: | |
984 | do | |
985 | :: 1 -> | |
986 | #ifdef WRITER_PROGRESS | |
987 | progress_writer2: | |
988 | #endif | |
989 | skip; | |
990 | od; | |
991 | } | |
992 | ||
993 | /* no name clash please */ | |
994 | #undef proc_urcu_writer | |
995 | ||
996 | ||
997 | /* Leave after the readers and writers so the pid count is ok. */ | |
998 | init { | |
999 | byte i, j; | |
1000 | ||
1001 | atomic { | |
1002 | INIT_CACHED_VAR(urcu_gp_ctr, 1, j); | |
1003 | INIT_CACHED_VAR(generation_ptr, 0, j); | |
1004 | ||
1005 | i = 0; | |
1006 | do | |
1007 | :: i < NR_READERS -> | |
1008 | INIT_CACHED_VAR(urcu_active_readers[i], 0, j); | |
1009 | read_generation[i] = 1; | |
1010 | data_access[i] = 0; | |
1011 | i++; | |
1012 | :: i >= NR_READERS -> break | |
1013 | od; | |
1014 | init_done = 1; | |
1015 | } | |
1016 | } |