projects / urcu.git / blob
? search:


44bbe523e153abfe52c39ee3eac957a4b7f22f46
[urcu.git] / formal-model / urcu-controldataflow / urcu.spin
1 /*
2 * mem.spin: Promela code to validate memory barriers with OOO memory
3 * and out-of-order instruction scheduling.
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;
216 CACHE_READ_FROM_MEM(generation_ptr, get_pid());
217 }
218 }
219
220 /* Must consume all prior write tokens. All subsequent writes depend on it. */
221 inline smp_wmb(i, j)
222 {
223 atomic {
224 CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
225 i = 0;
226 do
227 :: i < NR_READERS ->
228 CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid());
229 i++
230 :: i >= NR_READERS -> break
231 od;
232 CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
233 }
234 }
235
236 /* Synchronization point. Must consume all prior read and write tokens. All
237 * subsequent reads and writes depend on it. */
238 inline smp_mb(i, j)
239 {
240 atomic {
241 smp_wmb(i, j);
242 smp_rmb(i, j);
243 }
244 }
245
246 #ifdef REMOTE_BARRIERS
247
248 bit reader_barrier[NR_READERS];
249
250 /*
251 * We cannot leave the barriers dependencies in place in REMOTE_BARRIERS mode
252 * because they would add unexisting core synchronization and would therefore
253 * create an incomplete model.
254 * Therefore, we model the read-side memory barriers by completely disabling the
255 * memory barriers and their dependencies from the read-side. One at a time
256 * (different verification runs), we make a different instruction listen for
257 * signals.
258 */
259
260 #define smp_mb_reader(i, j)
261
262 /*
263 * Service 0, 1 or many barrier requests.
264 */
265 inline smp_mb_recv(i, j)
266 {
267 do
268 :: (reader_barrier[get_readerid()] == 1) ->
269 smp_mb(i, j);
270 reader_barrier[get_readerid()] = 0;
271 :: 1 ->
272 /*
273 * Busy-looping waiting for other barrier requests are not considered as
274 * non-progress.
275 */
276 #ifdef READER_PROGRESS
277 progress_reader2:
278 #endif
279 skip;
280 :: 1 -> break;
281 od;
282 }
283
284 #ifdef WRITER_PROGRESS
285 #define PROGRESS_LABEL(progressid) progress_writer_progid_##progressid:
286 #else
287 #define PROGRESS_LABEL(progressid)
288 #endif
289
290 #define smp_mb_send(i, j, progressid) \
291 { \
292 smp_mb(i, j); \
293 i = 0; \
294 do \
295 :: i < NR_READERS -> \
296 reader_barrier[i] = 1; \
297 do \
298 :: (reader_barrier[i] == 1) -> \
299 /* \
300 * Busy-looping waiting for reader barrier handling is of little\
301 * interest, given the reader has the ability to totally ignore \
302 * barrier requests. \
303 */ \
304 PROGRESS_LABEL(progressid) \
305 skip; \
306 :: (reader_barrier[i] == 0) -> break; \
307 od; \
308 i++; \
309 :: i >= NR_READERS -> \
310 break \
311 od; \
312 smp_mb(i, j); \
313 }
314
315 #else
316
317 #define smp_mb_send(i, j, progressid) smp_mb(i, j)
318 #define smp_mb_reader smp_mb
319 #define smp_mb_recv(i, j)
320
321 #endif
322
323 /* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */
324 DECLARE_CACHED_VAR(byte, urcu_gp_ctr);
325 /* Note ! currently only two readers */
326 DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
327 /* pointer generation */
328 DECLARE_CACHED_VAR(byte, generation_ptr);
329
330 byte last_free_gen = 0;
331 bit free_done = 0;
332 byte read_generation[NR_READERS];
333 bit data_access[NR_READERS];
334
335 bit write_lock = 0;
336
337 bit init_done = 0;
338
339 bit sighand_exec = 0;
340
341 inline wait_init_done()
342 {
343 do
344 :: init_done == 0 -> skip;
345 :: else -> break;
346 od;
347 }
348
349 inline ooo_mem(i)
350 {
351 atomic {
352 RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
353 i = 0;
354 do
355 :: i < NR_READERS ->
356 RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i],
357 get_pid());
358 i++
359 :: i >= NR_READERS -> break
360 od;
361 RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
362 RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
363 i = 0;
364 do
365 :: i < NR_READERS ->
366 RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i],
367 get_pid());
368 i++
369 :: i >= NR_READERS -> break
370 od;
371 RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid());
372 }
373 }
374
375 /*
376 * Bit encoding, urcu_reader :
377 */
378
379 int _proc_urcu_reader;
380 #define proc_urcu_reader _proc_urcu_reader
381
382 /* Body of PROCEDURE_READ_LOCK */
383 #define READ_PROD_A_READ (1 << 0)
384 #define READ_PROD_B_IF_TRUE (1 << 1)
385 #define READ_PROD_B_IF_FALSE (1 << 2)
386 #define READ_PROD_C_IF_TRUE_READ (1 << 3)
387
388 #define PROCEDURE_READ_LOCK(base, consumetoken, producetoken) \
389 :: CONSUME_TOKENS(proc_urcu_reader, consumetoken, READ_PROD_A_READ << base) -> \
390 ooo_mem(i); \
391 tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \
392 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_A_READ << base); \
393 :: CONSUME_TOKENS(proc_urcu_reader, \
394 READ_PROD_A_READ << base, /* RAW, pre-dominant */ \
395 (READ_PROD_B_IF_TRUE | READ_PROD_B_IF_FALSE) << base) -> \
396 if \
397 :: (!(tmp & RCU_GP_CTR_NEST_MASK)) -> \
398 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base); \
399 :: else -> \
400 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_FALSE << base); \
401 fi; \
402 /* IF TRUE */ \
403 :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base, \
404 READ_PROD_C_IF_TRUE_READ << base) -> \
405 ooo_mem(i); \
406 tmp2 = READ_CACHED_VAR(urcu_gp_ctr); \
407 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_C_IF_TRUE_READ << base); \
408 :: CONSUME_TOKENS(proc_urcu_reader, \
409 (READ_PROD_C_IF_TRUE_READ /* pre-dominant */ \
410 | READ_PROD_A_READ) << base, /* WAR */ \
411 producetoken) -> \
412 ooo_mem(i); \
413 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2); \
414 PRODUCE_TOKENS(proc_urcu_reader, producetoken); \
415 /* IF_MERGE implies \
416 * post-dominance */ \
417 /* ELSE */ \
418 :: CONSUME_TOKENS(proc_urcu_reader, \
419 (READ_PROD_B_IF_FALSE /* pre-dominant */ \
420 | READ_PROD_A_READ) << base, /* WAR */ \
421 producetoken) -> \
422 ooo_mem(i); \
423 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], \
424 tmp + 1); \
425 PRODUCE_TOKENS(proc_urcu_reader, producetoken); \
426 /* IF_MERGE implies \
427 * post-dominance */ \
428 /* ENDIF */ \
429 skip
430
431 /* Body of PROCEDURE_READ_LOCK */
432 #define READ_PROC_READ_UNLOCK (1 << 0)
433
434 #define PROCEDURE_READ_UNLOCK(base, consumetoken, producetoken) \
435 :: CONSUME_TOKENS(proc_urcu_reader, \
436 consumetoken, \
437 READ_PROC_READ_UNLOCK << base) -> \
438 ooo_mem(i); \
439 tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \
440 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_UNLOCK << base); \
441 :: CONSUME_TOKENS(proc_urcu_reader, \
442 consumetoken \
443 | (READ_PROC_READ_UNLOCK << base), /* WAR */ \
444 producetoken) -> \
445 ooo_mem(i); \
446 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1); \
447 PRODUCE_TOKENS(proc_urcu_reader, producetoken); \
448 skip
449
450
451 #define READ_PROD_NONE (1 << 0)
452
453 /* PROCEDURE_READ_LOCK base = << 1 : 1 to 5 */
454 #define READ_LOCK_BASE 1
455 #define READ_LOCK_OUT (1 << 5)
456
457 #define READ_PROC_FIRST_MB (1 << 6)
458
459 /* PROCEDURE_READ_LOCK (NESTED) base : << 7 : 7 to 11 */
460 #define READ_LOCK_NESTED_BASE 7
461 #define READ_LOCK_NESTED_OUT (1 << 11)
462
463 #define READ_PROC_READ_GEN (1 << 12)
464 #define READ_PROC_ACCESS_GEN (1 << 13)
465
466 /* PROCEDURE_READ_UNLOCK (NESTED) base = << 14 : 14 to 15 */
467 #define READ_UNLOCK_NESTED_BASE 14
468 #define READ_UNLOCK_NESTED_OUT (1 << 15)
469
470 #define READ_PROC_SECOND_MB (1 << 16)
471
472 /* PROCEDURE_READ_UNLOCK base = << 17 : 17 to 18 */
473 #define READ_UNLOCK_BASE 17
474 #define READ_UNLOCK_OUT (1 << 18)
475
476 /* PROCEDURE_READ_LOCK_UNROLL base = << 19 : 19 to 23 */
477 #define READ_LOCK_UNROLL_BASE 19
478 #define READ_LOCK_OUT_UNROLL (1 << 23)
479
480 #define READ_PROC_THIRD_MB (1 << 24)
481
482 #define READ_PROC_READ_GEN_UNROLL (1 << 25)
483 #define READ_PROC_ACCESS_GEN_UNROLL (1 << 26)
484
485 #define READ_PROC_FOURTH_MB (1 << 27)
486
487 /* PROCEDURE_READ_UNLOCK_UNROLL base = << 28 : 28 to 29 */
488 #define READ_UNLOCK_UNROLL_BASE 28
489 #define READ_UNLOCK_OUT_UNROLL (1 << 29)
490
491
492 /* Should not include branches */
493 #define READ_PROC_ALL_TOKENS (READ_PROD_NONE \
494 | READ_LOCK_OUT \
495 | READ_PROC_FIRST_MB \
496 | READ_LOCK_NESTED_OUT \
497 | READ_PROC_READ_GEN \
498 | READ_PROC_ACCESS_GEN \
499 | READ_UNLOCK_NESTED_OUT \
500 | READ_PROC_SECOND_MB \
501 | READ_UNLOCK_OUT \
502 | READ_LOCK_OUT_UNROLL \
503 | READ_PROC_THIRD_MB \
504 | READ_PROC_READ_GEN_UNROLL \
505 | READ_PROC_ACCESS_GEN_UNROLL \
506 | READ_PROC_FOURTH_MB \
507 | READ_UNLOCK_OUT_UNROLL)
508
509 /* Must clear all tokens, including branches */
510 #define READ_PROC_ALL_TOKENS_CLEAR ((1 << 30) - 1)
511
512 inline urcu_one_read(i, j, nest_i, tmp, tmp2)
513 {
514 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_NONE);
515
516 #ifdef NO_MB
517 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB);
518 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB);
519 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB);
520 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB);
521 #endif
522
523 #ifdef REMOTE_BARRIERS
524 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB);
525 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB);
526 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB);
527 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB);
528 #endif
529
530 do
531 :: 1 ->
532
533 #ifdef REMOTE_BARRIERS
534 /*
535 * Signal-based memory barrier will only execute when the
536 * execution order appears in program order.
537 */
538 if
539 :: 1 ->
540 atomic {
541 if
542 :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE,
543 READ_LOCK_OUT | READ_LOCK_NESTED_OUT
544 | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
545 | READ_UNLOCK_OUT
546 | READ_LOCK_OUT_UNROLL
547 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
548 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT,
549 READ_LOCK_NESTED_OUT
550 | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
551 | READ_UNLOCK_OUT
552 | READ_LOCK_OUT_UNROLL
553 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
554 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT | READ_LOCK_NESTED_OUT,
555 READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
556 | READ_UNLOCK_OUT
557 | READ_LOCK_OUT_UNROLL
558 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
559 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
560 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN,
561 READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
562 | READ_UNLOCK_OUT
563 | READ_LOCK_OUT_UNROLL
564 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
565 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
566 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN,
567 READ_UNLOCK_NESTED_OUT
568 | READ_UNLOCK_OUT
569 | READ_LOCK_OUT_UNROLL
570 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
571 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
572 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
573 | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT,
574 READ_UNLOCK_OUT
575 | READ_LOCK_OUT_UNROLL
576 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
577 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
578 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
579 | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
580 | READ_UNLOCK_OUT,
581 READ_LOCK_OUT_UNROLL
582 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
583 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
584 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
585 | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
586 | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL,
587 READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
588 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
589 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
590 | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
591 | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL
592 | READ_PROC_READ_GEN_UNROLL,
593 READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL)
594 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
595 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN
596 | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
597 | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL
598 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL,
599 READ_UNLOCK_OUT_UNROLL)
600 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE | READ_LOCK_OUT
601 | READ_LOCK_NESTED_OUT | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN | READ_UNLOCK_NESTED_OUT
602 | READ_UNLOCK_OUT | READ_LOCK_OUT_UNROLL
603 | READ_PROC_READ_GEN_UNROLL | READ_PROC_ACCESS_GEN_UNROLL | READ_UNLOCK_OUT_UNROLL,
604 0) ->
605 goto non_atomic3;
606 non_atomic3_end:
607 skip;
608 fi;
609 }
610 :: 1 -> skip;
611 fi;
612
613 goto non_atomic3_skip;
614 non_atomic3:
615 smp_mb_recv(i, j);
616 goto non_atomic3_end;
617 non_atomic3_skip:
618
619 #endif /* REMOTE_BARRIERS */
620
621 atomic {
622 if
623 PROCEDURE_READ_LOCK(READ_LOCK_BASE, READ_PROD_NONE, READ_LOCK_OUT);
624
625 :: CONSUME_TOKENS(proc_urcu_reader,
626 READ_LOCK_OUT, /* post-dominant */
627 READ_PROC_FIRST_MB) ->
628 smp_mb_reader(i, j);
629 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB);
630
631 PROCEDURE_READ_LOCK(READ_LOCK_NESTED_BASE, READ_PROC_FIRST_MB | READ_LOCK_OUT,
632 READ_LOCK_NESTED_OUT);
633
634 :: CONSUME_TOKENS(proc_urcu_reader,
635 READ_PROC_FIRST_MB, /* mb() orders reads */
636 READ_PROC_READ_GEN) ->
637 ooo_mem(i);
638 read_generation[get_readerid()] =
639 READ_CACHED_VAR(generation_ptr);
640 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN);
641
642 :: CONSUME_TOKENS(proc_urcu_reader,
643 READ_PROC_FIRST_MB /* mb() orders reads */
644 | READ_PROC_READ_GEN,
645 READ_PROC_ACCESS_GEN) ->
646 ooo_mem(i);
647 goto non_atomic;
648 non_atomic_end:
649 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN);
650
651
652 /* Note : we remove the nested memory barrier from the read unlock
653 * model, given it is not usually needed. The implementation has the barrier
654 * because the performance impact added by a branch in the common case does not
655 * justify it.
656 */
657
658 PROCEDURE_READ_UNLOCK(READ_UNLOCK_NESTED_BASE,
659 READ_PROC_FIRST_MB
660 | READ_LOCK_OUT
661 | READ_LOCK_NESTED_OUT,
662 READ_UNLOCK_NESTED_OUT);
663
664
665 :: CONSUME_TOKENS(proc_urcu_reader,
666 READ_PROC_ACCESS_GEN /* mb() orders reads */
667 | READ_PROC_READ_GEN /* mb() orders reads */
668 | READ_PROC_FIRST_MB /* mb() ordered */
669 | READ_LOCK_OUT /* post-dominant */
670 | READ_LOCK_NESTED_OUT /* post-dominant */
671 | READ_UNLOCK_NESTED_OUT,
672 READ_PROC_SECOND_MB) ->
673 smp_mb_reader(i, j);
674 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB);
675
676 PROCEDURE_READ_UNLOCK(READ_UNLOCK_BASE,
677 READ_PROC_SECOND_MB /* mb() orders reads */
678 | READ_PROC_FIRST_MB /* mb() orders reads */
679 | READ_LOCK_NESTED_OUT /* RAW */
680 | READ_LOCK_OUT /* RAW */
681 | READ_UNLOCK_NESTED_OUT, /* RAW */
682 READ_UNLOCK_OUT);
683
684 /* Unrolling loop : second consecutive lock */
685 /* reading urcu_active_readers, which have been written by
686 * READ_UNLOCK_OUT : RAW */
687 PROCEDURE_READ_LOCK(READ_LOCK_UNROLL_BASE,
688 READ_UNLOCK_OUT /* RAW */
689 | READ_PROC_SECOND_MB /* mb() orders reads */
690 | READ_PROC_FIRST_MB /* mb() orders reads */
691 | READ_LOCK_NESTED_OUT /* RAW */
692 | READ_LOCK_OUT /* RAW */
693 | READ_UNLOCK_NESTED_OUT, /* RAW */
694 READ_LOCK_OUT_UNROLL);
695
696
697 :: CONSUME_TOKENS(proc_urcu_reader,
698 READ_PROC_FIRST_MB /* mb() ordered */
699 | READ_PROC_SECOND_MB /* mb() ordered */
700 | READ_LOCK_OUT_UNROLL /* post-dominant */
701 | READ_LOCK_NESTED_OUT
702 | READ_LOCK_OUT
703 | READ_UNLOCK_NESTED_OUT
704 | READ_UNLOCK_OUT,
705 READ_PROC_THIRD_MB) ->
706 smp_mb_reader(i, j);
707 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_THIRD_MB);
708
709 :: CONSUME_TOKENS(proc_urcu_reader,
710 READ_PROC_FIRST_MB /* mb() orders reads */
711 | READ_PROC_SECOND_MB /* mb() orders reads */
712 | READ_PROC_THIRD_MB, /* mb() orders reads */
713 READ_PROC_READ_GEN_UNROLL) ->
714 ooo_mem(i);
715 read_generation[get_readerid()] =
716 READ_CACHED_VAR(generation_ptr);
717 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN_UNROLL);
718
719 :: CONSUME_TOKENS(proc_urcu_reader,
720 READ_PROC_READ_GEN_UNROLL
721 | READ_PROC_FIRST_MB /* mb() orders reads */
722 | READ_PROC_SECOND_MB /* mb() orders reads */
723 | READ_PROC_THIRD_MB, /* mb() orders reads */
724 READ_PROC_ACCESS_GEN_UNROLL) ->
725 ooo_mem(i);
726 goto non_atomic2;
727 non_atomic2_end:
728 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN_UNROLL);
729
730 :: CONSUME_TOKENS(proc_urcu_reader,
731 READ_PROC_READ_GEN_UNROLL /* mb() orders reads */
732 | READ_PROC_ACCESS_GEN_UNROLL /* mb() orders reads */
733 | READ_PROC_FIRST_MB /* mb() ordered */
734 | READ_PROC_SECOND_MB /* mb() ordered */
735 | READ_PROC_THIRD_MB /* mb() ordered */
736 | READ_LOCK_OUT_UNROLL /* post-dominant */
737 | READ_LOCK_NESTED_OUT
738 | READ_LOCK_OUT
739 | READ_UNLOCK_NESTED_OUT
740 | READ_UNLOCK_OUT,
741 READ_PROC_FOURTH_MB) ->
742 smp_mb_reader(i, j);
743 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FOURTH_MB);
744
745 PROCEDURE_READ_UNLOCK(READ_UNLOCK_UNROLL_BASE,
746 READ_PROC_FOURTH_MB /* mb() orders reads */
747 | READ_PROC_THIRD_MB /* mb() orders reads */
748 | READ_LOCK_OUT_UNROLL /* RAW */
749 | READ_PROC_SECOND_MB /* mb() orders reads */
750 | READ_PROC_FIRST_MB /* mb() orders reads */
751 | READ_LOCK_NESTED_OUT /* RAW */
752 | READ_LOCK_OUT /* RAW */
753 | READ_UNLOCK_NESTED_OUT, /* RAW */
754 READ_UNLOCK_OUT_UNROLL);
755 :: CONSUME_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS, 0) ->
756 CLEAR_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS_CLEAR);
757 break;
758 fi;
759 }
760 od;
761 /*
762 * Dependency between consecutive loops :
763 * RAW dependency on
764 * WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1)
765 * tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
766 * between loops.
767 * _WHEN THE MB()s are in place_, they add full ordering of the
768 * generation pointer read wrt active reader count read, which ensures
769 * execution will not spill across loop execution.
770 * However, in the event mb()s are removed (execution using signal
771 * handler to promote barrier()() -> smp_mb()), nothing prevents one loop
772 * to spill its execution on other loop's execution.
773 */
774 goto end;
775 non_atomic:
776 data_access[get_readerid()] = 1;
777 data_access[get_readerid()] = 0;
778 goto non_atomic_end;
779 non_atomic2:
780 data_access[get_readerid()] = 1;
781 data_access[get_readerid()] = 0;
782 goto non_atomic2_end;
783 end:
784 skip;
785 }
786
787
788
789 active proctype urcu_reader()
790 {
791 byte i, j, nest_i;
792 byte tmp, tmp2;
793
794 wait_init_done();
795
796 assert(get_pid() < NR_PROCS);
797
798 end_reader:
799 do
800 :: 1 ->
801 /*
802 * We do not test reader's progress here, because we are mainly
803 * interested in writer's progress. The reader never blocks
804 * anyway. We have to test for reader/writer's progress
805 * separately, otherwise we could think the writer is doing
806 * progress when it's blocked by an always progressing reader.
807 */
808 #ifdef READER_PROGRESS
809 progress_reader:
810 #endif
811 urcu_one_read(i, j, nest_i, tmp, tmp2);
812 od;
813 }
814
815 /* no name clash please */
816 #undef proc_urcu_reader
817
818
819 /* Model the RCU update process. */
820
821 /*
822 * Bit encoding, urcu_writer :
823 * Currently only supports one reader.
824 */
825
826 int _proc_urcu_writer;
827 #define proc_urcu_writer _proc_urcu_writer
828
829 #define WRITE_PROD_NONE (1 << 0)
830
831 #define WRITE_PROC_FIRST_MB (1 << 1)
832
833 /* first flip */
834 #define WRITE_PROC_FIRST_READ_GP (1 << 2)
835 #define WRITE_PROC_FIRST_WRITE_GP (1 << 3)
836 #define WRITE_PROC_FIRST_WAIT (1 << 4)
837 #define WRITE_PROC_FIRST_WAIT_LOOP (1 << 5)
838
839 /* second flip */
840 #define WRITE_PROC_SECOND_READ_GP (1 << 6)
841 #define WRITE_PROC_SECOND_WRITE_GP (1 << 7)
842 #define WRITE_PROC_SECOND_WAIT (1 << 8)
843 #define WRITE_PROC_SECOND_WAIT_LOOP (1 << 9)
844
845 #define WRITE_PROC_SECOND_MB (1 << 10)
846
847 #define WRITE_PROC_ALL_TOKENS (WRITE_PROD_NONE \
848 | WRITE_PROC_FIRST_MB \
849 | WRITE_PROC_FIRST_READ_GP \
850 | WRITE_PROC_FIRST_WRITE_GP \
851 | WRITE_PROC_FIRST_WAIT \
852 | WRITE_PROC_SECOND_READ_GP \
853 | WRITE_PROC_SECOND_WRITE_GP \
854 | WRITE_PROC_SECOND_WAIT \
855 | WRITE_PROC_SECOND_MB)
856
857 #define WRITE_PROC_ALL_TOKENS_CLEAR ((1 << 11) - 1)
858
859 active proctype urcu_writer()
860 {
861 byte i, j;
862 byte tmp, tmp2, tmpa;
863 byte old_gen;
864 byte cur_gp_val = 0; /*
865 * Keep a local trace of the current parity so
866 * we don't add non-existing dependencies on the global
867 * GP update. Needed to test single flip case.
868 */
869
870 wait_init_done();
871
872 assert(get_pid() < NR_PROCS);
873
874 do
875 :: (READ_CACHED_VAR(generation_ptr) < 5) ->
876 #ifdef WRITER_PROGRESS
877 progress_writer1:
878 #endif
879 ooo_mem(i);
880 atomic {
881 old_gen = READ_CACHED_VAR(generation_ptr);
882 WRITE_CACHED_VAR(generation_ptr, old_gen + 1);
883 }
884 ooo_mem(i);
885
886 do
887 :: 1 ->
888 atomic {
889 if
890 :: write_lock == 0 ->
891 write_lock = 1;
892 break;
893 :: else ->
894 skip;
895 fi;
896 }
897 od;
898
899 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROD_NONE);
900
901 #ifdef NO_MB
902 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB);
903 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
904 #endif
905
906 #ifdef SINGLE_FLIP
907 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
908 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP);
909 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT);
910 /* For single flip, we need to know the current parity */
911 cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT;
912 #endif
913
914 do :: 1 ->
915 atomic {
916 if
917 :: CONSUME_TOKENS(proc_urcu_writer,
918 WRITE_PROD_NONE,
919 WRITE_PROC_FIRST_MB) ->
920 goto smp_mb_send1;
921 smp_mb_send1_end:
922 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB);
923
924 /* first flip */
925 :: CONSUME_TOKENS(proc_urcu_writer,
926 WRITE_PROC_FIRST_MB,
927 WRITE_PROC_FIRST_READ_GP) ->
928 tmpa = READ_CACHED_VAR(urcu_gp_ctr);
929 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_READ_GP);
930 :: CONSUME_TOKENS(proc_urcu_writer,
931 WRITE_PROC_FIRST_MB | WRITE_PROC_FIRST_READ_GP,
932 WRITE_PROC_FIRST_WRITE_GP) ->
933 ooo_mem(i);
934 WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT);
935 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WRITE_GP);
936
937 :: CONSUME_TOKENS(proc_urcu_writer,
938 //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */
939 WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */
940 WRITE_PROC_FIRST_WAIT | WRITE_PROC_FIRST_WAIT_LOOP) ->
941 ooo_mem(i);
942 /* ONLY WAITING FOR READER 0 */
943 tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
944 #ifndef SINGLE_FLIP
945 /* In normal execution, we are always starting by
946 * waiting for the even parity.
947 */
948 cur_gp_val = RCU_GP_CTR_BIT;
949 #endif
950 if
951 :: (tmp2 & RCU_GP_CTR_NEST_MASK)
952 && ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) ->
953 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP);
954 :: else ->
955 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT);
956 fi;
957
958 :: CONSUME_TOKENS(proc_urcu_writer,
959 //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */
960 WRITE_PROC_FIRST_WRITE_GP
961 | WRITE_PROC_FIRST_READ_GP
962 | WRITE_PROC_FIRST_WAIT_LOOP
963 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */
964 0) ->
965 #ifndef GEN_ERROR_WRITER_PROGRESS
966 goto smp_mb_send2;
967 smp_mb_send2_end:
968 #else
969 ooo_mem(i);
970 #endif
971 /* This instruction loops to WRITE_PROC_FIRST_WAIT */
972 CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP | WRITE_PROC_FIRST_WAIT);
973
974 /* second flip */
975 :: CONSUME_TOKENS(proc_urcu_writer,
976 WRITE_PROC_FIRST_WAIT /* Control dependency : need to branch out of
977 * the loop to execute the next flip (CHECK) */
978 | WRITE_PROC_FIRST_WRITE_GP
979 | WRITE_PROC_FIRST_READ_GP
980 | WRITE_PROC_FIRST_MB,
981 WRITE_PROC_SECOND_READ_GP) ->
982 ooo_mem(i);
983 tmpa = READ_CACHED_VAR(urcu_gp_ctr);
984 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
985 :: CONSUME_TOKENS(proc_urcu_writer,
986 WRITE_PROC_FIRST_MB
987 | WRITE_PROC_FIRST_READ_GP
988 | WRITE_PROC_FIRST_WRITE_GP
989 | WRITE_PROC_SECOND_READ_GP,
990 WRITE_PROC_SECOND_WRITE_GP) ->
991 ooo_mem(i);
992 WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT);
993 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP);
994
995 :: CONSUME_TOKENS(proc_urcu_writer,
996 //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */
997 WRITE_PROC_FIRST_WAIT
998 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */
999 WRITE_PROC_SECOND_WAIT | WRITE_PROC_SECOND_WAIT_LOOP) ->
1000 ooo_mem(i);
1001 /* ONLY WAITING FOR READER 0 */
1002 tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
1003 if
1004 :: (tmp2 & RCU_GP_CTR_NEST_MASK)
1005 && ((tmp2 ^ 0) & RCU_GP_CTR_BIT) ->
1006 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP);
1007 :: else ->
1008 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT);
1009 fi;
1010
1011 :: CONSUME_TOKENS(proc_urcu_writer,
1012 //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */
1013 WRITE_PROC_SECOND_WRITE_GP
1014 | WRITE_PROC_FIRST_WRITE_GP
1015 | WRITE_PROC_SECOND_READ_GP
1016 | WRITE_PROC_FIRST_READ_GP
1017 | WRITE_PROC_SECOND_WAIT_LOOP
1018 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */
1019 0) ->
1020 #ifndef GEN_ERROR_WRITER_PROGRESS
1021 goto smp_mb_send3;
1022 smp_mb_send3_end:
1023 #else
1024 ooo_mem(i);
1025 #endif
1026 /* This instruction loops to WRITE_PROC_SECOND_WAIT */
1027 CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP | WRITE_PROC_SECOND_WAIT);
1028
1029
1030 :: CONSUME_TOKENS(proc_urcu_writer,
1031 WRITE_PROC_FIRST_WAIT
1032 | WRITE_PROC_SECOND_WAIT
1033 | WRITE_PROC_FIRST_READ_GP
1034 | WRITE_PROC_SECOND_READ_GP
1035 | WRITE_PROC_FIRST_WRITE_GP
1036 | WRITE_PROC_SECOND_WRITE_GP
1037 | WRITE_PROC_FIRST_MB,
1038 WRITE_PROC_SECOND_MB) ->
1039 goto smp_mb_send4;
1040 smp_mb_send4_end:
1041 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
1042
1043 :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) ->
1044 CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR);
1045 break;
1046 fi;
1047 }
1048 od;
1049
1050 write_lock = 0;
1051 /* free-up step, e.g., kfree(). */
1052 atomic {
1053 last_free_gen = old_gen;
1054 free_done = 1;
1055 }
1056 :: else -> break;
1057 od;
1058 /*
1059 * Given the reader loops infinitely, let the writer also busy-loop
1060 * with progress here so, with weak fairness, we can test the
1061 * writer's progress.
1062 */
1063 end_writer:
1064 do
1065 :: 1 ->
1066 #ifdef WRITER_PROGRESS
1067 progress_writer2:
1068 #endif
1069 skip;
1070 od;
1071
1072 /* Non-atomic parts of the loop */
1073 goto end;
1074 smp_mb_send1:
1075 smp_mb_send(i, j, 1);
1076 goto smp_mb_send1_end;
1077 #ifndef GEN_ERROR_WRITER_PROGRESS
1078 smp_mb_send2:
1079 smp_mb_send(i, j, 2);
1080 goto smp_mb_send2_end;
1081 smp_mb_send3:
1082 smp_mb_send(i, j, 3);
1083 goto smp_mb_send3_end;
1084 #endif
1085 smp_mb_send4:
1086 smp_mb_send(i, j, 4);
1087 goto smp_mb_send4_end;
1088 end:
1089 skip;
1090 }
1091
1092 /* no name clash please */
1093 #undef proc_urcu_writer
1094
1095
1096 /* Leave after the readers and writers so the pid count is ok. */
1097 init {
1098 byte i, j;
1099
1100 atomic {
1101 INIT_CACHED_VAR(urcu_gp_ctr, 1, j);
1102 INIT_CACHED_VAR(generation_ptr, 0, j);
1103
1104 i = 0;
1105 do
1106 :: i < NR_READERS ->
1107 INIT_CACHED_VAR(urcu_active_readers[i], 0, j);
1108 read_generation[i] = 1;
1109 data_access[i] = 0;
1110 i++;
1111 :: i >= NR_READERS -> break
1112 od;
1113 init_done = 1;
1114 }
1115 }
Userspace RCU (urcu) for Linux
This page took 0.053731 seconds and 3 git commands to generate.