Commit | Line | Data |
---|---|---|
b6b17880 MD |
1 | #define WRITER_PROGRESS |
2 | #define GEN_ERROR_WRITER_PROGRESS | |
3 | ||
4 | // Poison value for freed memory | |
5 | #define POISON 1 | |
6 | // Memory with correct data | |
7 | #define WINE 0 | |
8 | #define SLAB_SIZE 2 | |
9 | ||
10 | #define read_poison (data_read_first[0] == POISON || data_read_second[0] == POISON) | |
11 | ||
12 | #define RCU_GP_CTR_BIT (1 << 7) | |
13 | #define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1) | |
14 | ||
15 | //disabled | |
16 | #define REMOTE_BARRIERS | |
17 | ||
18 | //#define ARCH_ALPHA | |
19 | #define ARCH_INTEL | |
20 | //#define ARCH_POWERPC | |
21 | /* | |
22 | * mem.spin: Promela code to validate memory barriers with OOO memory | |
23 | * and out-of-order instruction scheduling. | |
24 | * | |
25 | * This program is free software; you can redistribute it and/or modify | |
26 | * it under the terms of the GNU General Public License as published by | |
27 | * the Free Software Foundation; either version 2 of the License, or | |
28 | * (at your option) any later version. | |
29 | * | |
30 | * This program is distributed in the hope that it will be useful, | |
31 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
32 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
33 | * GNU General Public License for more details. | |
34 | * | |
35 | * You should have received a copy of the GNU General Public License | |
36 | * along with this program; if not, write to the Free Software | |
37 | * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. | |
38 | * | |
39 | * Copyright (c) 2009 Mathieu Desnoyers | |
40 | */ | |
41 | ||
42 | /* Promela validation variables. */ | |
43 | ||
44 | /* specific defines "included" here */ | |
45 | /* DEFINES file "included" here */ | |
46 | ||
47 | #define NR_READERS 1 | |
48 | #define NR_WRITERS 1 | |
49 | ||
50 | #define NR_PROCS 2 | |
51 | ||
52 | #define get_pid() (_pid) | |
53 | ||
54 | #define get_readerid() (get_pid()) | |
55 | ||
56 | /* | |
57 | * Produced process control and data flow. Updated after each instruction to | |
58 | * show which variables are ready. Using one-hot bit encoding per variable to | |
59 | * save state space. Used as triggers to execute the instructions having those | |
60 | * variables as input. Leaving bits active to inhibit instruction execution. | |
61 | * Scheme used to make instruction disabling and automatic dependency fall-back | |
62 | * automatic. | |
63 | */ | |
64 | ||
65 | #define CONSUME_TOKENS(state, bits, notbits) \ | |
66 | ((!(state & (notbits))) && (state & (bits)) == (bits)) | |
67 | ||
68 | #define PRODUCE_TOKENS(state, bits) \ | |
69 | state = state | (bits); | |
70 | ||
71 | #define CLEAR_TOKENS(state, bits) \ | |
72 | state = state & ~(bits) | |
73 | ||
74 | /* | |
75 | * Types of dependency : | |
76 | * | |
77 | * Data dependency | |
78 | * | |
79 | * - True dependency, Read-after-Write (RAW) | |
80 | * | |
81 | * This type of dependency happens when a statement depends on the result of a | |
82 | * previous statement. This applies to any statement which needs to read a | |
83 | * variable written by a preceding statement. | |
84 | * | |
85 | * - False dependency, Write-after-Read (WAR) | |
86 | * | |
87 | * Typically, variable renaming can ensure that this dependency goes away. | |
88 | * However, if the statements must read and then write from/to the same variable | |
89 | * in the OOO memory model, renaming may be impossible, and therefore this | |
90 | * causes a WAR dependency. | |
91 | * | |
92 | * - Output dependency, Write-after-Write (WAW) | |
93 | * | |
94 | * Two writes to the same variable in subsequent statements. Variable renaming | |
95 | * can ensure this is not needed, but can be required when writing multiple | |
96 | * times to the same OOO mem model variable. | |
97 | * | |
98 | * Control dependency | |
99 | * | |
100 | * Execution of a given instruction depends on a previous instruction evaluating | |
101 | * in a way that allows its execution. E.g. : branches. | |
102 | * | |
103 | * Useful considerations for joining dependencies after branch | |
104 | * | |
105 | * - Pre-dominance | |
106 | * | |
107 | * "We say box i dominates box j if every path (leading from input to output | |
108 | * through the diagram) which passes through box j must also pass through box | |
109 | * i. Thus box i dominates box j if box j is subordinate to box i in the | |
110 | * program." | |
111 | * | |
112 | * http://www.hipersoft.rice.edu/grads/publications/dom14.pdf | |
113 | * Other classic algorithm to calculate dominance : Lengauer-Tarjan (in gcc) | |
114 | * | |
115 | * - Post-dominance | |
116 | * | |
117 | * Just as pre-dominance, but with arcs of the data flow inverted, and input vs | |
118 | * output exchanged. Therefore, i post-dominating j ensures that every path | |
119 | * passing by j will pass by i before reaching the output. | |
120 | * | |
121 | * Prefetch and speculative execution | |
122 | * | |
123 | * If an instruction depends on the result of a previous branch, but it does not | |
124 | * have side-effects, it can be executed before the branch result is known. | |
125 | * however, it must be restarted if a core-synchronizing instruction is issued. | |
126 | * Note that instructions which depend on the speculative instruction result | |
127 | * but that have side-effects must depend on the branch completion in addition | |
128 | * to the speculatively executed instruction. | |
129 | * | |
130 | * Other considerations | |
131 | * | |
132 | * Note about "volatile" keyword dependency : The compiler will order volatile | |
133 | * accesses so they appear in the right order on a given CPU. They can be | |
134 | * reordered by the CPU instruction scheduling. This therefore cannot be | |
135 | * considered as a depencency. | |
136 | * | |
137 | * References : | |
138 | * | |
139 | * Cooper, Keith D.; & Torczon, Linda. (2005). Engineering a Compiler. Morgan | |
140 | * Kaufmann. ISBN 1-55860-698-X. | |
141 | * Kennedy, Ken; & Allen, Randy. (2001). Optimizing Compilers for Modern | |
142 | * Architectures: A Dependence-based Approach. Morgan Kaufmann. ISBN | |
143 | * 1-55860-286-0. | |
144 | * Muchnick, Steven S. (1997). Advanced Compiler Design and Implementation. | |
145 | * Morgan Kaufmann. ISBN 1-55860-320-4. | |
146 | */ | |
147 | ||
148 | /* | |
149 | * Note about loops and nested calls | |
150 | * | |
151 | * To keep this model simple, loops expressed in the framework will behave as if | |
152 | * there was a core synchronizing instruction between loops. To see the effect | |
153 | * of loop unrolling, manually unrolling loops is required. Note that if loops | |
154 | * end or start with a core synchronizing instruction, the model is appropriate. | |
155 | * Nested calls are not supported. | |
156 | */ | |
157 | ||
158 | /* | |
159 | * Only Alpha has out-of-order cache bank loads. Other architectures (intel, | |
160 | * powerpc, arm) ensure that dependent reads won't be reordered. c.f. | |
161 | * http://www.linuxjournal.com/article/8212) | |
162 | */ | |
163 | #ifdef ARCH_ALPHA | |
164 | #define HAVE_OOO_CACHE_READ | |
165 | #endif | |
166 | ||
167 | /* | |
168 | * Each process have its own data in cache. Caches are randomly updated. | |
169 | * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces | |
170 | * both. | |
171 | */ | |
172 | ||
173 | typedef per_proc_byte { | |
174 | byte val[NR_PROCS]; | |
175 | }; | |
176 | ||
177 | typedef per_proc_bit { | |
178 | bit val[NR_PROCS]; | |
179 | }; | |
180 | ||
181 | /* Bitfield has a maximum of 8 procs */ | |
182 | typedef per_proc_bitfield { | |
183 | byte bitfield; | |
184 | }; | |
185 | ||
186 | #define DECLARE_CACHED_VAR(type, x) \ | |
187 | type mem_##x; | |
188 | ||
189 | #define DECLARE_PROC_CACHED_VAR(type, x)\ | |
190 | type cached_##x; \ | |
191 | bit cache_dirty_##x; | |
192 | ||
193 | #define INIT_CACHED_VAR(x, v) \ | |
194 | mem_##x = v; | |
195 | ||
196 | #define INIT_PROC_CACHED_VAR(x, v) \ | |
197 | cache_dirty_##x = 0; \ | |
198 | cached_##x = v; | |
199 | ||
200 | #define IS_CACHE_DIRTY(x, id) (cache_dirty_##x) | |
201 | ||
202 | #define READ_CACHED_VAR(x) (cached_##x) | |
203 | ||
204 | #define WRITE_CACHED_VAR(x, v) \ | |
205 | atomic { \ | |
206 | cached_##x = v; \ | |
207 | cache_dirty_##x = 1; \ | |
208 | } | |
209 | ||
210 | #define CACHE_WRITE_TO_MEM(x, id) \ | |
211 | if \ | |
212 | :: IS_CACHE_DIRTY(x, id) -> \ | |
213 | mem_##x = cached_##x; \ | |
214 | cache_dirty_##x = 0; \ | |
215 | :: else -> \ | |
216 | skip \ | |
217 | fi; | |
218 | ||
219 | #define CACHE_READ_FROM_MEM(x, id) \ | |
220 | if \ | |
221 | :: !IS_CACHE_DIRTY(x, id) -> \ | |
222 | cached_##x = mem_##x; \ | |
223 | :: else -> \ | |
224 | skip \ | |
225 | fi; | |
226 | ||
227 | /* | |
228 | * May update other caches if cache is dirty, or not. | |
229 | */ | |
230 | #define RANDOM_CACHE_WRITE_TO_MEM(x, id)\ | |
231 | if \ | |
232 | :: 1 -> CACHE_WRITE_TO_MEM(x, id); \ | |
233 | :: 1 -> skip \ | |
234 | fi; | |
235 | ||
236 | #define RANDOM_CACHE_READ_FROM_MEM(x, id)\ | |
237 | if \ | |
238 | :: 1 -> CACHE_READ_FROM_MEM(x, id); \ | |
239 | :: 1 -> skip \ | |
240 | fi; | |
241 | ||
242 | /* Must consume all prior read tokens. All subsequent reads depend on it. */ | |
243 | inline smp_rmb(i) | |
244 | { | |
245 | atomic { | |
246 | CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); | |
247 | i = 0; | |
248 | do | |
249 | :: i < NR_READERS -> | |
250 | CACHE_READ_FROM_MEM(urcu_active_readers[i], get_pid()); | |
251 | i++ | |
252 | :: i >= NR_READERS -> break | |
253 | od; | |
254 | CACHE_READ_FROM_MEM(rcu_ptr, get_pid()); | |
255 | i = 0; | |
256 | do | |
257 | :: i < SLAB_SIZE -> | |
258 | CACHE_READ_FROM_MEM(rcu_data[i], get_pid()); | |
259 | i++ | |
260 | :: i >= SLAB_SIZE -> break | |
261 | od; | |
262 | } | |
263 | } | |
264 | ||
265 | /* Must consume all prior write tokens. All subsequent writes depend on it. */ | |
266 | inline smp_wmb(i) | |
267 | { | |
268 | atomic { | |
269 | CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); | |
270 | i = 0; | |
271 | do | |
272 | :: i < NR_READERS -> | |
273 | CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid()); | |
274 | i++ | |
275 | :: i >= NR_READERS -> break | |
276 | od; | |
277 | CACHE_WRITE_TO_MEM(rcu_ptr, get_pid()); | |
278 | i = 0; | |
279 | do | |
280 | :: i < SLAB_SIZE -> | |
281 | CACHE_WRITE_TO_MEM(rcu_data[i], get_pid()); | |
282 | i++ | |
283 | :: i >= SLAB_SIZE -> break | |
284 | od; | |
285 | } | |
286 | } | |
287 | ||
288 | /* Synchronization point. Must consume all prior read and write tokens. All | |
289 | * subsequent reads and writes depend on it. */ | |
290 | inline smp_mb(i) | |
291 | { | |
292 | atomic { | |
293 | smp_wmb(i); | |
294 | smp_rmb(i); | |
295 | } | |
296 | } | |
297 | ||
298 | #ifdef REMOTE_BARRIERS | |
299 | ||
300 | bit reader_barrier[NR_READERS]; | |
301 | ||
302 | /* | |
303 | * We cannot leave the barriers dependencies in place in REMOTE_BARRIERS mode | |
304 | * because they would add unexisting core synchronization and would therefore | |
305 | * create an incomplete model. | |
306 | * Therefore, we model the read-side memory barriers by completely disabling the | |
307 | * memory barriers and their dependencies from the read-side. One at a time | |
308 | * (different verification runs), we make a different instruction listen for | |
309 | * signals. | |
310 | */ | |
311 | ||
312 | #define smp_mb_reader(i, j) | |
313 | ||
314 | /* | |
315 | * Service 0, 1 or many barrier requests. | |
316 | */ | |
317 | inline smp_mb_recv(i, j) | |
318 | { | |
319 | do | |
320 | :: (reader_barrier[get_readerid()] == 1) -> | |
321 | /* | |
322 | * We choose to ignore cycles caused by writer busy-looping, | |
323 | * waiting for the reader, sending barrier requests, and the | |
324 | * reader always services them without continuing execution. | |
325 | */ | |
326 | progress_ignoring_mb1: | |
327 | smp_mb(i); | |
328 | reader_barrier[get_readerid()] = 0; | |
329 | :: 1 -> | |
330 | /* | |
331 | * We choose to ignore writer's non-progress caused by the | |
332 | * reader ignoring the writer's mb() requests. | |
333 | */ | |
334 | progress_ignoring_mb2: | |
335 | break; | |
336 | od; | |
337 | } | |
338 | ||
339 | #define PROGRESS_LABEL(progressid) progress_writer_progid_##progressid: | |
340 | ||
341 | #define smp_mb_send(i, j, progressid) \ | |
342 | { \ | |
343 | smp_mb(i); \ | |
344 | i = 0; \ | |
345 | do \ | |
346 | :: i < NR_READERS -> \ | |
347 | reader_barrier[i] = 1; \ | |
348 | /* \ | |
349 | * Busy-looping waiting for reader barrier handling is of little\ | |
350 | * interest, given the reader has the ability to totally ignore \ | |
351 | * barrier requests. \ | |
352 | */ \ | |
353 | do \ | |
354 | :: (reader_barrier[i] == 1) -> \ | |
355 | PROGRESS_LABEL(progressid) \ | |
356 | skip; \ | |
357 | :: (reader_barrier[i] == 0) -> break; \ | |
358 | od; \ | |
359 | i++; \ | |
360 | :: i >= NR_READERS -> \ | |
361 | break \ | |
362 | od; \ | |
363 | smp_mb(i); \ | |
364 | } | |
365 | ||
366 | #else | |
367 | ||
368 | #define smp_mb_send(i, j, progressid) smp_mb(i) | |
369 | #define smp_mb_reader(i, j) smp_mb(i) | |
370 | #define smp_mb_recv(i, j) | |
371 | ||
372 | #endif | |
373 | ||
374 | /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */ | |
375 | DECLARE_CACHED_VAR(byte, urcu_gp_ctr); | |
376 | /* Note ! currently only one reader */ | |
377 | DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]); | |
378 | /* RCU data */ | |
379 | DECLARE_CACHED_VAR(bit, rcu_data[SLAB_SIZE]); | |
380 | ||
381 | /* RCU pointer */ | |
382 | #if (SLAB_SIZE == 2) | |
383 | DECLARE_CACHED_VAR(bit, rcu_ptr); | |
384 | bit ptr_read_first[NR_READERS]; | |
385 | bit ptr_read_second[NR_READERS]; | |
386 | #else | |
387 | DECLARE_CACHED_VAR(byte, rcu_ptr); | |
388 | byte ptr_read_first[NR_READERS]; | |
389 | byte ptr_read_second[NR_READERS]; | |
390 | #endif | |
391 | ||
392 | bit data_read_first[NR_READERS]; | |
393 | bit data_read_second[NR_READERS]; | |
394 | ||
395 | bit init_done = 0; | |
396 | ||
397 | inline wait_init_done() | |
398 | { | |
399 | do | |
400 | :: init_done == 0 -> skip; | |
401 | :: else -> break; | |
402 | od; | |
403 | } | |
404 | ||
405 | inline ooo_mem(i) | |
406 | { | |
407 | atomic { | |
408 | RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); | |
409 | i = 0; | |
410 | do | |
411 | :: i < NR_READERS -> | |
412 | RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i], | |
413 | get_pid()); | |
414 | i++ | |
415 | :: i >= NR_READERS -> break | |
416 | od; | |
417 | RANDOM_CACHE_WRITE_TO_MEM(rcu_ptr, get_pid()); | |
418 | i = 0; | |
419 | do | |
420 | :: i < SLAB_SIZE -> | |
421 | RANDOM_CACHE_WRITE_TO_MEM(rcu_data[i], get_pid()); | |
422 | i++ | |
423 | :: i >= SLAB_SIZE -> break | |
424 | od; | |
425 | #ifdef HAVE_OOO_CACHE_READ | |
426 | RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); | |
427 | i = 0; | |
428 | do | |
429 | :: i < NR_READERS -> | |
430 | RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i], | |
431 | get_pid()); | |
432 | i++ | |
433 | :: i >= NR_READERS -> break | |
434 | od; | |
435 | RANDOM_CACHE_READ_FROM_MEM(rcu_ptr, get_pid()); | |
436 | i = 0; | |
437 | do | |
438 | :: i < SLAB_SIZE -> | |
439 | RANDOM_CACHE_READ_FROM_MEM(rcu_data[i], get_pid()); | |
440 | i++ | |
441 | :: i >= SLAB_SIZE -> break | |
442 | od; | |
443 | #else | |
444 | smp_rmb(i); | |
445 | #endif /* HAVE_OOO_CACHE_READ */ | |
446 | } | |
447 | } | |
448 | ||
449 | /* | |
450 | * Bit encoding, urcu_reader : | |
451 | */ | |
452 | ||
453 | int _proc_urcu_reader; | |
454 | #define proc_urcu_reader _proc_urcu_reader | |
455 | ||
456 | /* Body of PROCEDURE_READ_LOCK */ | |
457 | #define READ_PROD_A_READ (1 << 0) | |
458 | #define READ_PROD_B_IF_TRUE (1 << 1) | |
459 | #define READ_PROD_B_IF_FALSE (1 << 2) | |
460 | #define READ_PROD_C_IF_TRUE_READ (1 << 3) | |
461 | ||
462 | #define PROCEDURE_READ_LOCK(base, consumetoken, consumetoken2, producetoken) \ | |
463 | :: CONSUME_TOKENS(proc_urcu_reader, (consumetoken | consumetoken2), READ_PROD_A_READ << base) -> \ | |
464 | ooo_mem(i); \ | |
465 | tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \ | |
466 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_A_READ << base); \ | |
467 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
468 | READ_PROD_A_READ << base, /* RAW, pre-dominant */ \ | |
469 | (READ_PROD_B_IF_TRUE | READ_PROD_B_IF_FALSE) << base) -> \ | |
470 | if \ | |
471 | :: (!(tmp & RCU_GP_CTR_NEST_MASK)) -> \ | |
472 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base); \ | |
473 | :: else -> \ | |
474 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_FALSE << base); \ | |
475 | fi; \ | |
476 | /* IF TRUE */ \ | |
477 | :: CONSUME_TOKENS(proc_urcu_reader, consumetoken, /* prefetch */ \ | |
478 | READ_PROD_C_IF_TRUE_READ << base) -> \ | |
479 | ooo_mem(i); \ | |
480 | tmp2 = READ_CACHED_VAR(urcu_gp_ctr); \ | |
481 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_C_IF_TRUE_READ << base); \ | |
482 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
483 | (READ_PROD_B_IF_TRUE \ | |
484 | | READ_PROD_C_IF_TRUE_READ /* pre-dominant */ \ | |
485 | | READ_PROD_A_READ) << base, /* WAR */ \ | |
486 | producetoken) -> \ | |
487 | ooo_mem(i); \ | |
488 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2); \ | |
489 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ | |
490 | /* IF_MERGE implies \ | |
491 | * post-dominance */ \ | |
492 | /* ELSE */ \ | |
493 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
494 | (READ_PROD_B_IF_FALSE /* pre-dominant */ \ | |
495 | | READ_PROD_A_READ) << base, /* WAR */ \ | |
496 | producetoken) -> \ | |
497 | ooo_mem(i); \ | |
498 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], \ | |
499 | tmp + 1); \ | |
500 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ | |
501 | /* IF_MERGE implies \ | |
502 | * post-dominance */ \ | |
503 | /* ENDIF */ \ | |
504 | skip | |
505 | ||
506 | /* Body of PROCEDURE_READ_LOCK */ | |
507 | #define READ_PROC_READ_UNLOCK (1 << 0) | |
508 | ||
509 | #define PROCEDURE_READ_UNLOCK(base, consumetoken, producetoken) \ | |
510 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
511 | consumetoken, \ | |
512 | READ_PROC_READ_UNLOCK << base) -> \ | |
513 | ooo_mem(i); \ | |
514 | tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \ | |
515 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_UNLOCK << base); \ | |
516 | :: CONSUME_TOKENS(proc_urcu_reader, \ | |
517 | consumetoken \ | |
518 | | (READ_PROC_READ_UNLOCK << base), /* WAR */ \ | |
519 | producetoken) -> \ | |
520 | ooo_mem(i); \ | |
521 | WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp - 1); \ | |
522 | PRODUCE_TOKENS(proc_urcu_reader, producetoken); \ | |
523 | skip | |
524 | ||
525 | ||
526 | #define READ_PROD_NONE (1 << 0) | |
527 | ||
528 | /* PROCEDURE_READ_LOCK base = << 1 : 1 to 5 */ | |
529 | #define READ_LOCK_BASE 1 | |
530 | #define READ_LOCK_OUT (1 << 5) | |
531 | ||
532 | #define READ_PROC_FIRST_MB (1 << 6) | |
533 | ||
534 | /* PROCEDURE_READ_LOCK (NESTED) base : << 7 : 7 to 11 */ | |
535 | #define READ_LOCK_NESTED_BASE 7 | |
536 | #define READ_LOCK_NESTED_OUT (1 << 11) | |
537 | ||
538 | #define READ_PROC_READ_GEN (1 << 12) | |
539 | #define READ_PROC_ACCESS_GEN (1 << 13) | |
540 | ||
541 | /* PROCEDURE_READ_UNLOCK (NESTED) base = << 14 : 14 to 15 */ | |
542 | #define READ_UNLOCK_NESTED_BASE 14 | |
543 | #define READ_UNLOCK_NESTED_OUT (1 << 15) | |
544 | ||
545 | #define READ_PROC_SECOND_MB (1 << 16) | |
546 | ||
547 | /* PROCEDURE_READ_UNLOCK base = << 17 : 17 to 18 */ | |
548 | #define READ_UNLOCK_BASE 17 | |
549 | #define READ_UNLOCK_OUT (1 << 18) | |
550 | ||
551 | /* PROCEDURE_READ_LOCK_UNROLL base = << 19 : 19 to 23 */ | |
552 | #define READ_LOCK_UNROLL_BASE 19 | |
553 | #define READ_LOCK_OUT_UNROLL (1 << 23) | |
554 | ||
555 | #define READ_PROC_THIRD_MB (1 << 24) | |
556 | ||
557 | #define READ_PROC_READ_GEN_UNROLL (1 << 25) | |
558 | #define READ_PROC_ACCESS_GEN_UNROLL (1 << 26) | |
559 | ||
560 | #define READ_PROC_FOURTH_MB (1 << 27) | |
561 | ||
562 | /* PROCEDURE_READ_UNLOCK_UNROLL base = << 28 : 28 to 29 */ | |
563 | #define READ_UNLOCK_UNROLL_BASE 28 | |
564 | #define READ_UNLOCK_OUT_UNROLL (1 << 29) | |
565 | ||
566 | ||
567 | /* Should not include branches */ | |
568 | #define READ_PROC_ALL_TOKENS (READ_PROD_NONE \ | |
569 | | READ_LOCK_OUT \ | |
570 | | READ_PROC_FIRST_MB \ | |
571 | | READ_LOCK_NESTED_OUT \ | |
572 | | READ_PROC_READ_GEN \ | |
573 | | READ_PROC_ACCESS_GEN \ | |
574 | | READ_UNLOCK_NESTED_OUT \ | |
575 | | READ_PROC_SECOND_MB \ | |
576 | | READ_UNLOCK_OUT \ | |
577 | | READ_LOCK_OUT_UNROLL \ | |
578 | | READ_PROC_THIRD_MB \ | |
579 | | READ_PROC_READ_GEN_UNROLL \ | |
580 | | READ_PROC_ACCESS_GEN_UNROLL \ | |
581 | | READ_PROC_FOURTH_MB \ | |
582 | | READ_UNLOCK_OUT_UNROLL) | |
583 | ||
584 | /* Must clear all tokens, including branches */ | |
585 | #define READ_PROC_ALL_TOKENS_CLEAR ((1 << 30) - 1) | |
586 | ||
587 | inline urcu_one_read(i, j, nest_i, tmp, tmp2) | |
588 | { | |
589 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_NONE); | |
590 | ||
591 | #ifdef NO_MB | |
592 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); | |
593 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); | |
594 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB); | |
595 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB); | |
596 | #endif | |
597 | ||
598 | #ifdef REMOTE_BARRIERS | |
599 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); | |
600 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); | |
601 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB); | |
602 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB); | |
603 | #endif | |
604 | ||
605 | do | |
606 | :: 1 -> | |
607 | ||
608 | #ifdef REMOTE_BARRIERS | |
609 | /* | |
610 | * Signal-based memory barrier will only execute when the | |
611 | * execution order appears in program order. | |
612 | */ | |
613 | if | |
614 | :: 1 -> | |
615 | atomic { | |
616 | if | |
617 | :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE, | |
618 | READ_LOCK_OUT | READ_LOCK_NESTED_OUT | |
619 | | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
620 | | READ_UNLOCK_OUT | |
621 | | READ_LOCK_OUT_UNROLL | |
622 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
623 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT, | |
624 | READ_LOCK_NESTED_OUT | |
625 | | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
626 | | READ_UNLOCK_OUT | |
627 | | READ_LOCK_OUT_UNROLL | |
628 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
629 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | READ_LOCK_NESTED_OUT, | |
630 | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
631 | | READ_UNLOCK_OUT | |
632 | | READ_LOCK_OUT_UNROLL | |
633 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
634 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
635 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN, | |
636 | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
637 | | READ_UNLOCK_OUT | |
638 | | READ_LOCK_OUT_UNROLL | |
639 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
640 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
641 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN, | |
642 | READ_UNLOCK_NESTED_OUT | |
643 | | READ_UNLOCK_OUT | |
644 | | READ_LOCK_OUT_UNROLL | |
645 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
646 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
647 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | |
648 | | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT, | |
649 | READ_UNLOCK_OUT | |
650 | | READ_LOCK_OUT_UNROLL | |
651 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
652 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
653 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | |
654 | | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
655 | | READ_UNLOCK_OUT, | |
656 | READ_LOCK_OUT_UNROLL | |
657 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
658 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
659 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | |
660 | | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
661 | | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL, | |
662 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
663 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
664 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | |
665 | | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
666 | | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL | |
667 | | READ_PROC_READ_GEN_UNROLL, | |
668 | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL) | |
669 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
670 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | |
671 | | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
672 | | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL | |
673 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL, | |
674 | READ_UNLOCK_OUT_UNROLL) | |
675 | || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | |
676 | | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT | |
677 | | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL | |
678 | | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL, | |
679 | 0) -> | |
680 | goto non_atomic3; | |
681 | non_atomic3_end: | |
682 | skip; | |
683 | fi; | |
684 | } | |
685 | fi; | |
686 | ||
687 | goto non_atomic3_skip; | |
688 | non_atomic3: | |
689 | smp_mb_recv(i, j); | |
690 | goto non_atomic3_end; | |
691 | non_atomic3_skip: | |
692 | ||
693 | #endif /* REMOTE_BARRIERS */ | |
694 | ||
695 | atomic { | |
696 | if | |
697 | PROCEDURE_READ_LOCK(READ_LOCK_BASE, READ_PROD_NONE, 0, READ_LOCK_OUT); | |
698 | ||
699 | :: CONSUME_TOKENS(proc_urcu_reader, | |
700 | READ_LOCK_OUT, /* post-dominant */ | |
701 | READ_PROC_FIRST_MB) -> | |
702 | smp_mb_reader(i, j); | |
703 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB); | |
704 | ||
705 | PROCEDURE_READ_LOCK(READ_LOCK_NESTED_BASE, READ_PROC_FIRST_MB, READ_LOCK_OUT, | |
706 | READ_LOCK_NESTED_OUT); | |
707 | ||
708 | :: CONSUME_TOKENS(proc_urcu_reader, | |
709 | READ_PROC_FIRST_MB, /* mb() orders reads */ | |
710 | READ_PROC_READ_GEN) -> | |
711 | ooo_mem(i); | |
712 | ptr_read_first[get_readerid()] = READ_CACHED_VAR(rcu_ptr); | |
713 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN); | |
714 | ||
715 | :: CONSUME_TOKENS(proc_urcu_reader, | |
716 | READ_PROC_FIRST_MB /* mb() orders reads */ | |
717 | | READ_PROC_READ_GEN, | |
718 | READ_PROC_ACCESS_GEN) -> | |
719 | /* smp_read_barrier_depends */ | |
720 | goto rmb1; | |
721 | rmb1_end: | |
722 | data_read_first[get_readerid()] = | |
723 | READ_CACHED_VAR(rcu_data[ptr_read_first[get_readerid()]]); | |
724 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN); | |
725 | ||
726 | ||
727 | /* Note : we remove the nested memory barrier from the read unlock | |
728 | * model, given it is not usually needed. The implementation has the barrier | |
729 | * because the performance impact added by a branch in the common case does not | |
730 | * justify it. | |
731 | */ | |
732 | ||
733 | PROCEDURE_READ_UNLOCK(READ_UNLOCK_NESTED_BASE, | |
734 | READ_PROC_FIRST_MB | |
735 | | READ_LOCK_OUT | |
736 | | READ_LOCK_NESTED_OUT, | |
737 | READ_UNLOCK_NESTED_OUT); | |
738 | ||
739 | ||
740 | :: CONSUME_TOKENS(proc_urcu_reader, | |
741 | READ_PROC_ACCESS_GEN /* mb() orders reads */ | |
742 | | READ_PROC_READ_GEN /* mb() orders reads */ | |
743 | | READ_PROC_FIRST_MB /* mb() ordered */ | |
744 | | READ_LOCK_OUT /* post-dominant */ | |
745 | | READ_LOCK_NESTED_OUT /* post-dominant */ | |
746 | | READ_UNLOCK_NESTED_OUT, | |
747 | READ_PROC_SECOND_MB) -> | |
748 | smp_mb_reader(i, j); | |
749 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB); | |
750 | ||
751 | PROCEDURE_READ_UNLOCK(READ_UNLOCK_BASE, | |
752 | READ_PROC_SECOND_MB /* mb() orders reads */ | |
753 | | READ_PROC_FIRST_MB /* mb() orders reads */ | |
754 | | READ_LOCK_NESTED_OUT /* RAW */ | |
755 | | READ_LOCK_OUT /* RAW */ | |
756 | | READ_UNLOCK_NESTED_OUT, /* RAW */ | |
757 | READ_UNLOCK_OUT); | |
758 | ||
759 | /* Unrolling loop : second consecutive lock */ | |
760 | /* reading urcu_active_readers, which have been written by | |
761 | * READ_UNLOCK_OUT : RAW */ | |
762 | PROCEDURE_READ_LOCK(READ_LOCK_UNROLL_BASE, | |
763 | READ_PROC_SECOND_MB /* mb() orders reads */ | |
764 | | READ_PROC_FIRST_MB, /* mb() orders reads */ | |
765 | READ_LOCK_NESTED_OUT /* RAW */ | |
766 | | READ_LOCK_OUT /* RAW */ | |
767 | | READ_UNLOCK_NESTED_OUT /* RAW */ | |
768 | | READ_UNLOCK_OUT, /* RAW */ | |
769 | READ_LOCK_OUT_UNROLL); | |
770 | ||
771 | ||
772 | :: CONSUME_TOKENS(proc_urcu_reader, | |
773 | READ_PROC_FIRST_MB /* mb() ordered */ | |
774 | | READ_PROC_SECOND_MB /* mb() ordered */ | |
775 | | READ_LOCK_OUT_UNROLL /* post-dominant */ | |
776 | | READ_LOCK_NESTED_OUT | |
777 | | READ_LOCK_OUT | |
778 | | READ_UNLOCK_NESTED_OUT | |
779 | | READ_UNLOCK_OUT, | |
780 | READ_PROC_THIRD_MB) -> | |
781 | smp_mb_reader(i, j); | |
782 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB); | |
783 | ||
784 | :: CONSUME_TOKENS(proc_urcu_reader, | |
785 | READ_PROC_FIRST_MB /* mb() orders reads */ | |
786 | | READ_PROC_SECOND_MB /* mb() orders reads */ | |
787 | | READ_PROC_THIRD_MB, /* mb() orders reads */ | |
788 | READ_PROC_READ_GEN_UNROLL) -> | |
789 | ooo_mem(i); | |
790 | ptr_read_second[get_readerid()] = READ_CACHED_VAR(rcu_ptr); | |
791 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL); | |
792 | ||
793 | :: CONSUME_TOKENS(proc_urcu_reader, | |
794 | READ_PROC_READ_GEN_UNROLL | |
795 | | READ_PROC_FIRST_MB /* mb() orders reads */ | |
796 | | READ_PROC_SECOND_MB /* mb() orders reads */ | |
797 | | READ_PROC_THIRD_MB, /* mb() orders reads */ | |
798 | READ_PROC_ACCESS_GEN_UNROLL) -> | |
799 | /* smp_read_barrier_depends */ | |
800 | goto rmb2; | |
801 | rmb2_end: | |
802 | data_read_second[get_readerid()] = | |
803 | READ_CACHED_VAR(rcu_data[ptr_read_second[get_readerid()]]); | |
804 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN_UNROLL); | |
805 | ||
806 | :: CONSUME_TOKENS(proc_urcu_reader, | |
807 | READ_PROC_READ_GEN_UNROLL /* mb() orders reads */ | |
808 | | READ_PROC_ACCESS_GEN_UNROLL /* mb() orders reads */ | |
809 | | READ_PROC_FIRST_MB /* mb() ordered */ | |
810 | | READ_PROC_SECOND_MB /* mb() ordered */ | |
811 | | READ_PROC_THIRD_MB /* mb() ordered */ | |
812 | | READ_LOCK_OUT_UNROLL /* post-dominant */ | |
813 | | READ_LOCK_NESTED_OUT | |
814 | | READ_LOCK_OUT | |
815 | | READ_UNLOCK_NESTED_OUT | |
816 | | READ_UNLOCK_OUT, | |
817 | READ_PROC_FOURTH_MB) -> | |
818 | smp_mb_reader(i, j); | |
819 | PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB); | |
820 | ||
821 | PROCEDURE_READ_UNLOCK(READ_UNLOCK_UNROLL_BASE, | |
822 | READ_PROC_FOURTH_MB /* mb() orders reads */ | |
823 | | READ_PROC_THIRD_MB /* mb() orders reads */ | |
824 | | READ_LOCK_OUT_UNROLL /* RAW */ | |
825 | | READ_PROC_SECOND_MB /* mb() orders reads */ | |
826 | | READ_PROC_FIRST_MB /* mb() orders reads */ | |
827 | | READ_LOCK_NESTED_OUT /* RAW */ | |
828 | | READ_LOCK_OUT /* RAW */ | |
829 | | READ_UNLOCK_NESTED_OUT, /* RAW */ | |
830 | READ_UNLOCK_OUT_UNROLL); | |
831 | :: CONSUME_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS, 0) -> | |
832 | CLEAR_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS_CLEAR); | |
833 | break; | |
834 | fi; | |
835 | } | |
836 | od; | |
837 | /* | |
838 | * Dependency between consecutive loops : | |
839 | * RAW dependency on | |
840 | * WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1) | |
841 | * tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); | |
842 | * between loops. | |
843 | * _WHEN THE MB()s are in place_, they add full ordering of the | |
844 | * generation pointer read wrt active reader count read, which ensures | |
845 | * execution will not spill across loop execution. | |
846 | * However, in the event mb()s are removed (execution using signal | |
847 | * handler to promote barrier()() -> smp_mb()), nothing prevents one loop | |
848 | * to spill its execution on other loop's execution. | |
849 | */ | |
850 | goto end; | |
851 | rmb1: | |
852 | #ifndef NO_RMB | |
853 | smp_rmb(i); | |
854 | #else | |
855 | ooo_mem(i); | |
856 | #endif | |
857 | goto rmb1_end; | |
858 | rmb2: | |
859 | #ifndef NO_RMB | |
860 | smp_rmb(i); | |
861 | #else | |
862 | ooo_mem(i); | |
863 | #endif | |
864 | goto rmb2_end; | |
865 | end: | |
866 | skip; | |
867 | } | |
868 | ||
869 | ||
870 | ||
871 | active proctype urcu_reader() | |
872 | { | |
873 | byte i, j, nest_i; | |
874 | byte tmp, tmp2; | |
875 | ||
876 | /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */ | |
877 | DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr); | |
878 | /* Note ! currently only one reader */ | |
879 | DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]); | |
880 | /* RCU data */ | |
881 | DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]); | |
882 | ||
883 | /* RCU pointer */ | |
884 | #if (SLAB_SIZE == 2) | |
885 | DECLARE_PROC_CACHED_VAR(bit, rcu_ptr); | |
886 | #else | |
887 | DECLARE_PROC_CACHED_VAR(byte, rcu_ptr); | |
888 | #endif | |
889 | ||
890 | atomic { | |
891 | INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1); | |
892 | INIT_PROC_CACHED_VAR(rcu_ptr, 0); | |
893 | ||
894 | i = 0; | |
895 | do | |
896 | :: i < NR_READERS -> | |
897 | INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0); | |
898 | i++; | |
899 | :: i >= NR_READERS -> break | |
900 | od; | |
901 | INIT_PROC_CACHED_VAR(rcu_data[0], WINE); | |
902 | i = 1; | |
903 | do | |
904 | :: i < SLAB_SIZE -> | |
905 | INIT_PROC_CACHED_VAR(rcu_data[i], POISON); | |
906 | i++ | |
907 | :: i >= SLAB_SIZE -> break | |
908 | od; | |
909 | } | |
910 | ||
911 | wait_init_done(); | |
912 | ||
913 | assert(get_pid() < NR_PROCS); | |
914 | ||
915 | end_reader: | |
916 | do | |
917 | :: 1 -> | |
918 | /* | |
919 | * We do not test reader's progress here, because we are mainly | |
920 | * interested in writer's progress. The reader never blocks | |
921 | * anyway. We have to test for reader/writer's progress | |
922 | * separately, otherwise we could think the writer is doing | |
923 | * progress when it's blocked by an always progressing reader. | |
924 | */ | |
925 | #ifdef READER_PROGRESS | |
926 | progress_reader: | |
927 | #endif | |
928 | urcu_one_read(i, j, nest_i, tmp, tmp2); | |
929 | od; | |
930 | } | |
931 | ||
932 | /* no name clash please */ | |
933 | #undef proc_urcu_reader | |
934 | ||
935 | ||
936 | /* Model the RCU update process. */ | |
937 | ||
938 | /* | |
939 | * Bit encoding, urcu_writer : | |
940 | * Currently only supports one reader. | |
941 | */ | |
942 | ||
943 | int _proc_urcu_writer; | |
944 | #define proc_urcu_writer _proc_urcu_writer | |
945 | ||
946 | #define WRITE_PROD_NONE (1 << 0) | |
947 | ||
948 | #define WRITE_DATA (1 << 1) | |
949 | #define WRITE_PROC_WMB (1 << 2) | |
950 | #define WRITE_XCHG_PTR (1 << 3) | |
951 | ||
952 | #define WRITE_PROC_FIRST_MB (1 << 4) | |
953 | ||
954 | /* first flip */ | |
955 | #define WRITE_PROC_FIRST_READ_GP (1 << 5) | |
956 | #define WRITE_PROC_FIRST_WRITE_GP (1 << 6) | |
957 | #define WRITE_PROC_FIRST_WAIT (1 << 7) | |
958 | #define WRITE_PROC_FIRST_WAIT_LOOP (1 << 8) | |
959 | ||
960 | /* second flip */ | |
961 | #define WRITE_PROC_SECOND_READ_GP (1 << 9) | |
962 | #define WRITE_PROC_SECOND_WRITE_GP (1 << 10) | |
963 | #define WRITE_PROC_SECOND_WAIT (1 << 11) | |
964 | #define WRITE_PROC_SECOND_WAIT_LOOP (1 << 12) | |
965 | ||
966 | #define WRITE_PROC_SECOND_MB (1 << 13) | |
967 | ||
968 | #define WRITE_FREE (1 << 14) | |
969 | ||
970 | #define WRITE_PROC_ALL_TOKENS (WRITE_PROD_NONE \ | |
971 | | WRITE_DATA \ | |
972 | | WRITE_PROC_WMB \ | |
973 | | WRITE_XCHG_PTR \ | |
974 | | WRITE_PROC_FIRST_MB \ | |
975 | | WRITE_PROC_FIRST_READ_GP \ | |
976 | | WRITE_PROC_FIRST_WRITE_GP \ | |
977 | | WRITE_PROC_FIRST_WAIT \ | |
978 | | WRITE_PROC_SECOND_READ_GP \ | |
979 | | WRITE_PROC_SECOND_WRITE_GP \ | |
980 | | WRITE_PROC_SECOND_WAIT \ | |
981 | | WRITE_PROC_SECOND_MB \ | |
982 | | WRITE_FREE) | |
983 | ||
984 | #define WRITE_PROC_ALL_TOKENS_CLEAR ((1 << 15) - 1) | |
985 | ||
986 | /* | |
987 | * Mutexes are implied around writer execution. A single writer at a time. | |
988 | */ | |
989 | active proctype urcu_writer() | |
990 | { | |
991 | byte i, j; | |
992 | byte tmp, tmp2, tmpa; | |
993 | byte cur_data = 0, old_data, loop_nr = 0; | |
994 | byte cur_gp_val = 0; /* | |
995 | * Keep a local trace of the current parity so | |
996 | * we don't add non-existing dependencies on the global | |
997 | * GP update. Needed to test single flip case. | |
998 | */ | |
999 | ||
1000 | /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */ | |
1001 | DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr); | |
1002 | /* Note ! currently only one reader */ | |
1003 | DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]); | |
1004 | /* RCU data */ | |
1005 | DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]); | |
1006 | ||
1007 | /* RCU pointer */ | |
1008 | #if (SLAB_SIZE == 2) | |
1009 | DECLARE_PROC_CACHED_VAR(bit, rcu_ptr); | |
1010 | #else | |
1011 | DECLARE_PROC_CACHED_VAR(byte, rcu_ptr); | |
1012 | #endif | |
1013 | ||
1014 | atomic { | |
1015 | INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1); | |
1016 | INIT_PROC_CACHED_VAR(rcu_ptr, 0); | |
1017 | ||
1018 | i = 0; | |
1019 | do | |
1020 | :: i < NR_READERS -> | |
1021 | INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0); | |
1022 | i++; | |
1023 | :: i >= NR_READERS -> break | |
1024 | od; | |
1025 | INIT_PROC_CACHED_VAR(rcu_data[0], WINE); | |
1026 | i = 1; | |
1027 | do | |
1028 | :: i < SLAB_SIZE -> | |
1029 | INIT_PROC_CACHED_VAR(rcu_data[i], POISON); | |
1030 | i++ | |
1031 | :: i >= SLAB_SIZE -> break | |
1032 | od; | |
1033 | } | |
1034 | ||
1035 | ||
1036 | wait_init_done(); | |
1037 | ||
1038 | assert(get_pid() < NR_PROCS); | |
1039 | ||
1040 | do | |
1041 | :: (loop_nr < 3) -> | |
1042 | #ifdef WRITER_PROGRESS | |
1043 | progress_writer1: | |
1044 | #endif | |
1045 | loop_nr = loop_nr + 1; | |
1046 | ||
1047 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROD_NONE); | |
1048 | ||
1049 | #ifdef NO_WMB | |
1050 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB); | |
1051 | #endif | |
1052 | ||
1053 | #ifdef NO_MB | |
1054 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB); | |
1055 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB); | |
1056 | #endif | |
1057 | ||
1058 | #ifdef SINGLE_FLIP | |
1059 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); | |
1060 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP); | |
1061 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT); | |
1062 | /* For single flip, we need to know the current parity */ | |
1063 | cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT; | |
1064 | #endif | |
1065 | ||
1066 | do :: 1 -> | |
1067 | atomic { | |
1068 | if | |
1069 | ||
1070 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1071 | WRITE_PROD_NONE, | |
1072 | WRITE_DATA) -> | |
1073 | ooo_mem(i); | |
1074 | cur_data = (cur_data + 1) % SLAB_SIZE; | |
1075 | WRITE_CACHED_VAR(rcu_data[cur_data], WINE); | |
1076 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_DATA); | |
1077 | ||
1078 | ||
1079 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1080 | WRITE_DATA, | |
1081 | WRITE_PROC_WMB) -> | |
1082 | smp_wmb(i); | |
1083 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB); | |
1084 | ||
1085 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1086 | WRITE_PROC_WMB, | |
1087 | WRITE_XCHG_PTR) -> | |
1088 | /* rcu_xchg_pointer() */ | |
1089 | atomic { | |
1090 | old_data = READ_CACHED_VAR(rcu_ptr); | |
1091 | WRITE_CACHED_VAR(rcu_ptr, cur_data); | |
1092 | } | |
1093 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_XCHG_PTR); | |
1094 | ||
1095 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1096 | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR, | |
1097 | WRITE_PROC_FIRST_MB) -> | |
1098 | goto smp_mb_send1; | |
1099 | smp_mb_send1_end: | |
1100 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB); | |
1101 | ||
1102 | /* first flip */ | |
1103 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1104 | WRITE_PROC_FIRST_MB, | |
1105 | WRITE_PROC_FIRST_READ_GP) -> | |
1106 | tmpa = READ_CACHED_VAR(urcu_gp_ctr); | |
1107 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_READ_GP); | |
1108 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1109 | WRITE_PROC_FIRST_MB | WRITE_PROC_WMB | |
1110 | | WRITE_PROC_FIRST_READ_GP, | |
1111 | WRITE_PROC_FIRST_WRITE_GP) -> | |
1112 | ooo_mem(i); | |
1113 | WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT); | |
1114 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WRITE_GP); | |
1115 | ||
1116 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1117 | //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */ | |
1118 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
1119 | WRITE_PROC_FIRST_WAIT | WRITE_PROC_FIRST_WAIT_LOOP) -> | |
1120 | ooo_mem(i); | |
1121 | //smp_mb(i); /* TEST */ | |
1122 | /* ONLY WAITING FOR READER 0 */ | |
1123 | tmp2 = READ_CACHED_VAR(urcu_active_readers[0]); | |
1124 | #ifndef SINGLE_FLIP | |
1125 | /* In normal execution, we are always starting by | |
1126 | * waiting for the even parity. | |
1127 | */ | |
1128 | cur_gp_val = RCU_GP_CTR_BIT; | |
1129 | #endif | |
1130 | if | |
1131 | :: (tmp2 & RCU_GP_CTR_NEST_MASK) | |
1132 | && ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) -> | |
1133 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP); | |
1134 | :: else -> | |
1135 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT); | |
1136 | fi; | |
1137 | ||
1138 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1139 | //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */ | |
1140 | WRITE_PROC_FIRST_WRITE_GP | |
1141 | | WRITE_PROC_FIRST_READ_GP | |
1142 | | WRITE_PROC_FIRST_WAIT_LOOP | |
1143 | | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR | |
1144 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
1145 | 0) -> | |
1146 | #ifndef GEN_ERROR_WRITER_PROGRESS | |
1147 | goto smp_mb_send2; | |
1148 | smp_mb_send2_end: | |
1149 | /* The memory barrier will invalidate the | |
1150 | * second read done as prefetching. Note that all | |
1151 | * instructions with side-effects depending on | |
1152 | * WRITE_PROC_SECOND_READ_GP should also depend on | |
1153 | * completion of this busy-waiting loop. */ | |
1154 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); | |
1155 | #else | |
1156 | ooo_mem(i); | |
1157 | #endif | |
1158 | /* This instruction loops to WRITE_PROC_FIRST_WAIT */ | |
1159 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP | WRITE_PROC_FIRST_WAIT); | |
1160 | ||
1161 | /* second flip */ | |
1162 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1163 | //WRITE_PROC_FIRST_WAIT | //test /* no dependency. Could pre-fetch, no side-effect. */ | |
1164 | WRITE_PROC_FIRST_WRITE_GP | |
1165 | | WRITE_PROC_FIRST_READ_GP | |
1166 | | WRITE_PROC_FIRST_MB, | |
1167 | WRITE_PROC_SECOND_READ_GP) -> | |
1168 | ooo_mem(i); | |
1169 | //smp_mb(i); /* TEST */ | |
1170 | tmpa = READ_CACHED_VAR(urcu_gp_ctr); | |
1171 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP); | |
1172 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1173 | WRITE_PROC_FIRST_WAIT /* dependency on first wait, because this | |
1174 | * instruction has globally observable | |
1175 | * side-effects. | |
1176 | */ | |
1177 | | WRITE_PROC_FIRST_MB | |
1178 | | WRITE_PROC_WMB | |
1179 | | WRITE_PROC_FIRST_READ_GP | |
1180 | | WRITE_PROC_FIRST_WRITE_GP | |
1181 | | WRITE_PROC_SECOND_READ_GP, | |
1182 | WRITE_PROC_SECOND_WRITE_GP) -> | |
1183 | ooo_mem(i); | |
1184 | WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT); | |
1185 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP); | |
1186 | ||
1187 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1188 | //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */ | |
1189 | WRITE_PROC_FIRST_WAIT | |
1190 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
1191 | WRITE_PROC_SECOND_WAIT | WRITE_PROC_SECOND_WAIT_LOOP) -> | |
1192 | ooo_mem(i); | |
1193 | //smp_mb(i); /* TEST */ | |
1194 | /* ONLY WAITING FOR READER 0 */ | |
1195 | tmp2 = READ_CACHED_VAR(urcu_active_readers[0]); | |
1196 | if | |
1197 | :: (tmp2 & RCU_GP_CTR_NEST_MASK) | |
1198 | && ((tmp2 ^ 0) & RCU_GP_CTR_BIT) -> | |
1199 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP); | |
1200 | :: else -> | |
1201 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT); | |
1202 | fi; | |
1203 | ||
1204 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1205 | //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */ | |
1206 | WRITE_PROC_SECOND_WRITE_GP | |
1207 | | WRITE_PROC_FIRST_WRITE_GP | |
1208 | | WRITE_PROC_SECOND_READ_GP | |
1209 | | WRITE_PROC_FIRST_READ_GP | |
1210 | | WRITE_PROC_SECOND_WAIT_LOOP | |
1211 | | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR | |
1212 | | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */ | |
1213 | 0) -> | |
1214 | #ifndef GEN_ERROR_WRITER_PROGRESS | |
1215 | goto smp_mb_send3; | |
1216 | smp_mb_send3_end: | |
1217 | #else | |
1218 | ooo_mem(i); | |
1219 | #endif | |
1220 | /* This instruction loops to WRITE_PROC_SECOND_WAIT */ | |
1221 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP | WRITE_PROC_SECOND_WAIT); | |
1222 | ||
1223 | ||
1224 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1225 | WRITE_PROC_FIRST_WAIT | |
1226 | | WRITE_PROC_SECOND_WAIT | |
1227 | | WRITE_PROC_FIRST_READ_GP | |
1228 | | WRITE_PROC_SECOND_READ_GP | |
1229 | | WRITE_PROC_FIRST_WRITE_GP | |
1230 | | WRITE_PROC_SECOND_WRITE_GP | |
1231 | | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR | |
1232 | | WRITE_PROC_FIRST_MB, | |
1233 | WRITE_PROC_SECOND_MB) -> | |
1234 | goto smp_mb_send4; | |
1235 | smp_mb_send4_end: | |
1236 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB); | |
1237 | ||
1238 | :: CONSUME_TOKENS(proc_urcu_writer, | |
1239 | WRITE_XCHG_PTR | |
1240 | | WRITE_PROC_FIRST_WAIT | |
1241 | | WRITE_PROC_SECOND_WAIT | |
1242 | | WRITE_PROC_WMB /* No dependency on | |
1243 | * WRITE_DATA because we | |
1244 | * write to a | |
1245 | * different location. */ | |
1246 | | WRITE_PROC_SECOND_MB | |
1247 | | WRITE_PROC_FIRST_MB, | |
1248 | WRITE_FREE) -> | |
1249 | WRITE_CACHED_VAR(rcu_data[old_data], POISON); | |
1250 | PRODUCE_TOKENS(proc_urcu_writer, WRITE_FREE); | |
1251 | ||
1252 | :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) -> | |
1253 | CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR); | |
1254 | break; | |
1255 | fi; | |
1256 | } | |
1257 | od; | |
1258 | /* | |
1259 | * Note : Promela model adds implicit serialization of the | |
1260 | * WRITE_FREE instruction. Normally, it would be permitted to | |
1261 | * spill on the next loop execution. Given the validation we do | |
1262 | * checks for the data entry read to be poisoned, it's ok if | |
1263 | * we do not check "late arriving" memory poisoning. | |
1264 | */ | |
1265 | :: else -> break; | |
1266 | od; | |
1267 | /* | |
1268 | * Given the reader loops infinitely, let the writer also busy-loop | |
1269 | * with progress here so, with weak fairness, we can test the | |
1270 | * writer's progress. | |
1271 | */ | |
1272 | end_writer: | |
1273 | do | |
1274 | :: 1 -> | |
1275 | #ifdef WRITER_PROGRESS | |
1276 | progress_writer2: | |
1277 | #endif | |
1278 | #ifdef READER_PROGRESS | |
1279 | /* | |
1280 | * Make sure we don't block the reader's progress. | |
1281 | */ | |
1282 | smp_mb_send(i, j, 5); | |
1283 | #endif | |
1284 | skip; | |
1285 | od; | |
1286 | ||
1287 | /* Non-atomic parts of the loop */ | |
1288 | goto end; | |
1289 | smp_mb_send1: | |
1290 | smp_mb_send(i, j, 1); | |
1291 | goto smp_mb_send1_end; | |
1292 | #ifndef GEN_ERROR_WRITER_PROGRESS | |
1293 | smp_mb_send2: | |
1294 | smp_mb_send(i, j, 2); | |
1295 | goto smp_mb_send2_end; | |
1296 | smp_mb_send3: | |
1297 | smp_mb_send(i, j, 3); | |
1298 | goto smp_mb_send3_end; | |
1299 | #endif | |
1300 | smp_mb_send4: | |
1301 | smp_mb_send(i, j, 4); | |
1302 | goto smp_mb_send4_end; | |
1303 | end: | |
1304 | skip; | |
1305 | } | |
1306 | ||
1307 | /* no name clash please */ | |
1308 | #undef proc_urcu_writer | |
1309 | ||
1310 | ||
1311 | /* Leave after the readers and writers so the pid count is ok. */ | |
1312 | init { | |
1313 | byte i, j; | |
1314 | ||
1315 | atomic { | |
1316 | INIT_CACHED_VAR(urcu_gp_ctr, 1); | |
1317 | INIT_CACHED_VAR(rcu_ptr, 0); | |
1318 | ||
1319 | i = 0; | |
1320 | do | |
1321 | :: i < NR_READERS -> | |
1322 | INIT_CACHED_VAR(urcu_active_readers[i], 0); | |
1323 | ptr_read_first[i] = 1; | |
1324 | ptr_read_second[i] = 1; | |
1325 | data_read_first[i] = WINE; | |
1326 | data_read_second[i] = WINE; | |
1327 | i++; | |
1328 | :: i >= NR_READERS -> break | |
1329 | od; | |
1330 | INIT_CACHED_VAR(rcu_data[0], WINE); | |
1331 | i = 1; | |
1332 | do | |
1333 | :: i < SLAB_SIZE -> | |
1334 | INIT_CACHED_VAR(rcu_data[i], POISON); | |
1335 | i++ | |
1336 | :: i >= SLAB_SIZE -> break | |
1337 | od; | |
1338 | ||
1339 | init_done = 1; | |
1340 | } | |
1341 | } |