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