projects / urcu.git / blob
? search:
summary | shortlog | log | commit | commitdiff | tree
blame | history | raw | HEAD
Update formal model from local copy
[urcu.git] / formal-model / urcu-controldataflow-alpha-ipi-progress-minimal / urcu_progress_writer_error.spin.input
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)
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 #else
386 DECLARE_CACHED_VAR(byte, rcu_ptr);
387 byte ptr_read_first[NR_READERS];
388 #endif
389
390 bit data_read_first[NR_READERS];
391
392 bit init_done = 0;
393
394 inline wait_init_done()
395 {
396 do
397 :: init_done == 0 -> skip;
398 :: else -> break;
399 od;
400 }
401
402 inline ooo_mem(i)
403 {
404 atomic {
405 RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
406 i = 0;
407 do
408 :: i < NR_READERS ->
409 RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i],
410 get_pid());
411 i++
412 :: i >= NR_READERS -> break
413 od;
414 RANDOM_CACHE_WRITE_TO_MEM(rcu_ptr, get_pid());
415 i = 0;
416 do
417 :: i < SLAB_SIZE ->
418 RANDOM_CACHE_WRITE_TO_MEM(rcu_data[i], get_pid());
419 i++
420 :: i >= SLAB_SIZE -> break
421 od;
422 #ifdef HAVE_OOO_CACHE_READ
423 RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
424 i = 0;
425 do
426 :: i < NR_READERS ->
427 RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i],
428 get_pid());
429 i++
430 :: i >= NR_READERS -> break
431 od;
432 RANDOM_CACHE_READ_FROM_MEM(rcu_ptr, get_pid());
433 i = 0;
434 do
435 :: i < SLAB_SIZE ->
436 RANDOM_CACHE_READ_FROM_MEM(rcu_data[i], get_pid());
437 i++
438 :: i >= SLAB_SIZE -> break
439 od;
440 #else
441 smp_rmb(i);
442 #endif /* HAVE_OOO_CACHE_READ */
443 }
444 }
445
446 /*
447 * Bit encoding, urcu_reader :
448 */
449
450 int _proc_urcu_reader;
451 #define proc_urcu_reader _proc_urcu_reader
452
453 /* Body of PROCEDURE_READ_LOCK */
454 #define READ_PROD_A_READ (1 << 0)
455 #define READ_PROD_B_IF_TRUE (1 << 1)
456 #define READ_PROD_B_IF_FALSE (1 << 2)
457 #define READ_PROD_C_IF_TRUE_READ (1 << 3)
458
459 #define PROCEDURE_READ_LOCK(base, consumetoken, consumetoken2, producetoken) \
460 :: CONSUME_TOKENS(proc_urcu_reader, (consumetoken | consumetoken2), READ_PROD_A_READ << base) -> \
461 ooo_mem(i); \
462 tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \
463 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_A_READ << base); \
464 :: CONSUME_TOKENS(proc_urcu_reader, \
465 READ_PROD_A_READ << base, /* RAW, pre-dominant */ \
466 (READ_PROD_B_IF_TRUE | READ_PROD_B_IF_FALSE) << base) -> \
467 if \
468 :: (!(tmp & RCU_GP_CTR_NEST_MASK)) -> \
469 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_TRUE << base); \
470 :: else -> \
471 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_B_IF_FALSE << base); \
472 fi; \
473 /* IF TRUE */ \
474 :: CONSUME_TOKENS(proc_urcu_reader, consumetoken, /* prefetch */ \
475 READ_PROD_C_IF_TRUE_READ << base) -> \
476 ooo_mem(i); \
477 tmp2 = READ_CACHED_VAR(urcu_gp_ctr); \
478 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_C_IF_TRUE_READ << base); \
479 :: CONSUME_TOKENS(proc_urcu_reader, \
480 (READ_PROD_B_IF_TRUE \
481 | READ_PROD_C_IF_TRUE_READ /* pre-dominant */ \
482 | READ_PROD_A_READ) << base, /* WAR */ \
483 producetoken) -> \
484 ooo_mem(i); \
485 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2); \
486 PRODUCE_TOKENS(proc_urcu_reader, producetoken); \
487 /* IF_MERGE implies \
488 * post-dominance */ \
489 /* ELSE */ \
490 :: CONSUME_TOKENS(proc_urcu_reader, \
491 (READ_PROD_B_IF_FALSE /* pre-dominant */ \
492 | READ_PROD_A_READ) << base, /* WAR */ \
493 producetoken) -> \
494 ooo_mem(i); \
495 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], \
496 tmp + 1); \
497 PRODUCE_TOKENS(proc_urcu_reader, producetoken); \
498 /* IF_MERGE implies \
499 * post-dominance */ \
500 /* ENDIF */ \
501 skip
502
503 /* Body of PROCEDURE_READ_LOCK */
504 #define READ_PROC_READ_UNLOCK (1 << 0)
505
506 #define PROCEDURE_READ_UNLOCK(base, consumetoken, producetoken) \
507 :: CONSUME_TOKENS(proc_urcu_reader, \
508 consumetoken, \
509 READ_PROC_READ_UNLOCK << base) -> \
510 ooo_mem(i); \
511 tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]); \
512 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_UNLOCK << base); \
513 :: CONSUME_TOKENS(proc_urcu_reader, \
514 consumetoken \
515 | (READ_PROC_READ_UNLOCK << base), /* WAR */ \
516 producetoken) -> \
517 ooo_mem(i); \
518 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp - 1); \
519 PRODUCE_TOKENS(proc_urcu_reader, producetoken); \
520 skip
521
522
523 #define READ_PROD_NONE (1 << 0)
524
525 /* PROCEDURE_READ_LOCK base = << 1 : 1 to 5 */
526 #define READ_LOCK_BASE 1
527 #define READ_LOCK_OUT (1 << 5)
528
529 #define READ_PROC_FIRST_MB (1 << 6)
530
531 #define READ_PROC_READ_GEN (1 << 12)
532 #define READ_PROC_ACCESS_GEN (1 << 13)
533
534 #define READ_PROC_SECOND_MB (1 << 16)
535
536 /* PROCEDURE_READ_UNLOCK base = << 17 : 17 to 18 */
537 #define READ_UNLOCK_BASE 17
538 #define READ_UNLOCK_OUT (1 << 18)
539
540 /* Should not include branches */
541 #define READ_PROC_ALL_TOKENS (READ_PROD_NONE \
542 | READ_LOCK_OUT \
543 | READ_PROC_FIRST_MB \
544 | READ_PROC_READ_GEN \
545 | READ_PROC_ACCESS_GEN \
546 | READ_PROC_SECOND_MB \
547 | READ_UNLOCK_OUT)
548
549 /* Must clear all tokens, including branches */
550 #define READ_PROC_ALL_TOKENS_CLEAR ((1 << 30) - 1)
551
552 inline urcu_one_read(i, j, nest_i, tmp, tmp2)
553 {
554 PRODUCE_TOKENS(proc_urcu_reader, READ_PROD_NONE);
555
556 #ifdef NO_MB
557 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB);
558 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB);
559 #endif
560
561 #ifdef REMOTE_BARRIERS
562 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB);
563 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB);
564 #endif
565
566 do
567 :: 1 ->
568
569 #ifdef REMOTE_BARRIERS
570 /*
571 * Signal-based memory barrier will only execute when the
572 * execution order appears in program order.
573 */
574 if
575 :: 1 ->
576 atomic {
577 if
578 :: CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE,
579 READ_LOCK_OUT
580 | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN
581 | READ_UNLOCK_OUT)
582 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE
583 | READ_LOCK_OUT,
584 READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN
585 | READ_UNLOCK_OUT)
586 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE
587 | READ_LOCK_OUT
588 | READ_PROC_READ_GEN, READ_PROC_ACCESS_GEN
589 | READ_UNLOCK_OUT)
590 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE
591 | READ_LOCK_OUT
592 | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN,
593 READ_UNLOCK_OUT)
594 || CONSUME_TOKENS(proc_urcu_reader, READ_PROD_NONE
595 | READ_LOCK_OUT
596 | READ_PROC_READ_GEN | READ_PROC_ACCESS_GEN
597 | READ_UNLOCK_OUT, 0) ->
598 goto non_atomic3;
599 non_atomic3_end:
600 skip;
601 fi;
602 }
603 fi;
604
605 goto non_atomic3_skip;
606 non_atomic3:
607 smp_mb_recv(i, j);
608 goto non_atomic3_end;
609 non_atomic3_skip:
610
611 #endif /* REMOTE_BARRIERS */
612
613 atomic {
614 if
615 PROCEDURE_READ_LOCK(READ_LOCK_BASE, READ_PROD_NONE, 0, READ_LOCK_OUT);
616
617 :: CONSUME_TOKENS(proc_urcu_reader,
618 READ_LOCK_OUT, /* post-dominant */
619 READ_PROC_FIRST_MB) ->
620 smp_mb_reader(i, j);
621 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_FIRST_MB);
622
623 :: CONSUME_TOKENS(proc_urcu_reader,
624 READ_PROC_FIRST_MB, /* mb() orders reads */
625 READ_PROC_READ_GEN) ->
626 ooo_mem(i);
627 ptr_read_first[get_readerid()] = READ_CACHED_VAR(rcu_ptr);
628 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_READ_GEN);
629
630 :: CONSUME_TOKENS(proc_urcu_reader,
631 READ_PROC_FIRST_MB /* mb() orders reads */
632 | READ_PROC_READ_GEN,
633 READ_PROC_ACCESS_GEN) ->
634 /* smp_read_barrier_depends */
635 goto rmb1;
636 rmb1_end:
637 data_read_first[get_readerid()] =
638 READ_CACHED_VAR(rcu_data[ptr_read_first[get_readerid()]]);
639 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_ACCESS_GEN);
640
641
642 :: CONSUME_TOKENS(proc_urcu_reader,
643 READ_PROC_ACCESS_GEN /* mb() orders reads */
644 | READ_PROC_READ_GEN /* mb() orders reads */
645 | READ_PROC_FIRST_MB /* mb() ordered */
646 | READ_LOCK_OUT, /* post-dominant */
647 READ_PROC_SECOND_MB) ->
648 smp_mb_reader(i, j);
649 PRODUCE_TOKENS(proc_urcu_reader, READ_PROC_SECOND_MB);
650
651 PROCEDURE_READ_UNLOCK(READ_UNLOCK_BASE,
652 READ_PROC_SECOND_MB /* mb() orders reads */
653 | READ_PROC_FIRST_MB /* mb() orders reads */
654 | READ_LOCK_OUT, /* RAW */
655 READ_UNLOCK_OUT);
656
657 :: CONSUME_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS, 0) ->
658 CLEAR_TOKENS(proc_urcu_reader, READ_PROC_ALL_TOKENS_CLEAR);
659 break;
660 fi;
661 }
662 od;
663 /*
664 * Dependency between consecutive loops :
665 * RAW dependency on
666 * WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1)
667 * tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
668 * between loops.
669 * _WHEN THE MB()s are in place_, they add full ordering of the
670 * generation pointer read wrt active reader count read, which ensures
671 * execution will not spill across loop execution.
672 * However, in the event mb()s are removed (execution using signal
673 * handler to promote barrier()() -> smp_mb()), nothing prevents one loop
674 * to spill its execution on other loop's execution.
675 */
676 goto end;
677 rmb1:
678 #ifndef NO_RMB
679 smp_rmb(i);
680 #else
681 ooo_mem(i);
682 #endif
683 goto rmb1_end;
684 end:
685 skip;
686 }
687
688
689
690 active proctype urcu_reader()
691 {
692 byte i, j, nest_i;
693 byte tmp, tmp2;
694
695 /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */
696 DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr);
697 /* Note ! currently only one reader */
698 DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
699 /* RCU data */
700 DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]);
701
702 /* RCU pointer */
703 #if (SLAB_SIZE == 2)
704 DECLARE_PROC_CACHED_VAR(bit, rcu_ptr);
705 #else
706 DECLARE_PROC_CACHED_VAR(byte, rcu_ptr);
707 #endif
708
709 atomic {
710 INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1);
711 INIT_PROC_CACHED_VAR(rcu_ptr, 0);
712
713 i = 0;
714 do
715 :: i < NR_READERS ->
716 INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0);
717 i++;
718 :: i >= NR_READERS -> break
719 od;
720 INIT_PROC_CACHED_VAR(rcu_data[0], WINE);
721 i = 1;
722 do
723 :: i < SLAB_SIZE ->
724 INIT_PROC_CACHED_VAR(rcu_data[i], POISON);
725 i++
726 :: i >= SLAB_SIZE -> break
727 od;
728 }
729
730 wait_init_done();
731
732 assert(get_pid() < NR_PROCS);
733
734 end_reader:
735 do
736 :: 1 ->
737 /*
738 * We do not test reader's progress here, because we are mainly
739 * interested in writer's progress. The reader never blocks
740 * anyway. We have to test for reader/writer's progress
741 * separately, otherwise we could think the writer is doing
742 * progress when it's blocked by an always progressing reader.
743 */
744 #ifdef READER_PROGRESS
745 progress_reader:
746 #endif
747 urcu_one_read(i, j, nest_i, tmp, tmp2);
748 od;
749 }
750
751 /* no name clash please */
752 #undef proc_urcu_reader
753
754
755 /* Model the RCU update process. */
756
757 /*
758 * Bit encoding, urcu_writer :
759 * Currently only supports one reader.
760 */
761
762 int _proc_urcu_writer;
763 #define proc_urcu_writer _proc_urcu_writer
764
765 #define WRITE_PROD_NONE (1 << 0)
766
767 #define WRITE_DATA (1 << 1)
768 #define WRITE_PROC_WMB (1 << 2)
769 #define WRITE_XCHG_PTR (1 << 3)
770
771 #define WRITE_PROC_FIRST_MB (1 << 4)
772
773 /* first flip */
774 #define WRITE_PROC_FIRST_READ_GP (1 << 5)
775 #define WRITE_PROC_FIRST_WRITE_GP (1 << 6)
776 #define WRITE_PROC_FIRST_WAIT (1 << 7)
777 #define WRITE_PROC_FIRST_WAIT_LOOP (1 << 8)
778
779 /* second flip */
780 #define WRITE_PROC_SECOND_READ_GP (1 << 9)
781 #define WRITE_PROC_SECOND_WRITE_GP (1 << 10)
782 #define WRITE_PROC_SECOND_WAIT (1 << 11)
783 #define WRITE_PROC_SECOND_WAIT_LOOP (1 << 12)
784
785 #define WRITE_PROC_SECOND_MB (1 << 13)
786
787 #define WRITE_FREE (1 << 14)
788
789 #define WRITE_PROC_ALL_TOKENS (WRITE_PROD_NONE \
790 | WRITE_DATA \
791 | WRITE_PROC_WMB \
792 | WRITE_XCHG_PTR \
793 | WRITE_PROC_FIRST_MB \
794 | WRITE_PROC_FIRST_READ_GP \
795 | WRITE_PROC_FIRST_WRITE_GP \
796 | WRITE_PROC_FIRST_WAIT \
797 | WRITE_PROC_SECOND_READ_GP \
798 | WRITE_PROC_SECOND_WRITE_GP \
799 | WRITE_PROC_SECOND_WAIT \
800 | WRITE_PROC_SECOND_MB \
801 | WRITE_FREE)
802
803 #define WRITE_PROC_ALL_TOKENS_CLEAR ((1 << 15) - 1)
804
805 /*
806 * Mutexes are implied around writer execution. A single writer at a time.
807 */
808 active proctype urcu_writer()
809 {
810 byte i, j;
811 byte tmp, tmp2, tmpa;
812 byte cur_data = 0, old_data, loop_nr = 0;
813 byte cur_gp_val = 0; /*
814 * Keep a local trace of the current parity so
815 * we don't add non-existing dependencies on the global
816 * GP update. Needed to test single flip case.
817 */
818
819 /* Keep in sync manually with smp_rmb, smp_wmb, ooo_mem and init() */
820 DECLARE_PROC_CACHED_VAR(byte, urcu_gp_ctr);
821 /* Note ! currently only one reader */
822 DECLARE_PROC_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
823 /* RCU data */
824 DECLARE_PROC_CACHED_VAR(bit, rcu_data[SLAB_SIZE]);
825
826 /* RCU pointer */
827 #if (SLAB_SIZE == 2)
828 DECLARE_PROC_CACHED_VAR(bit, rcu_ptr);
829 #else
830 DECLARE_PROC_CACHED_VAR(byte, rcu_ptr);
831 #endif
832
833 atomic {
834 INIT_PROC_CACHED_VAR(urcu_gp_ctr, 1);
835 INIT_PROC_CACHED_VAR(rcu_ptr, 0);
836
837 i = 0;
838 do
839 :: i < NR_READERS ->
840 INIT_PROC_CACHED_VAR(urcu_active_readers[i], 0);
841 i++;
842 :: i >= NR_READERS -> break
843 od;
844 INIT_PROC_CACHED_VAR(rcu_data[0], WINE);
845 i = 1;
846 do
847 :: i < SLAB_SIZE ->
848 INIT_PROC_CACHED_VAR(rcu_data[i], POISON);
849 i++
850 :: i >= SLAB_SIZE -> break
851 od;
852 }
853
854
855 wait_init_done();
856
857 assert(get_pid() < NR_PROCS);
858
859 do
860 :: (loop_nr < 3) ->
861 #ifdef WRITER_PROGRESS
862 progress_writer1:
863 #endif
864 loop_nr = loop_nr + 1;
865
866 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROD_NONE);
867
868 #ifdef NO_WMB
869 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB);
870 #endif
871
872 #ifdef NO_MB
873 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB);
874 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
875 #endif
876
877 #ifdef SINGLE_FLIP
878 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
879 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP);
880 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT);
881 /* For single flip, we need to know the current parity */
882 cur_gp_val = cur_gp_val ^ RCU_GP_CTR_BIT;
883 #endif
884
885 do :: 1 ->
886 atomic {
887 if
888
889 :: CONSUME_TOKENS(proc_urcu_writer,
890 WRITE_PROD_NONE,
891 WRITE_DATA) ->
892 ooo_mem(i);
893 cur_data = (cur_data + 1) % SLAB_SIZE;
894 WRITE_CACHED_VAR(rcu_data[cur_data], WINE);
895 PRODUCE_TOKENS(proc_urcu_writer, WRITE_DATA);
896
897
898 :: CONSUME_TOKENS(proc_urcu_writer,
899 WRITE_DATA,
900 WRITE_PROC_WMB) ->
901 smp_wmb(i);
902 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_WMB);
903
904 :: CONSUME_TOKENS(proc_urcu_writer,
905 WRITE_PROC_WMB,
906 WRITE_XCHG_PTR) ->
907 /* rcu_xchg_pointer() */
908 atomic {
909 old_data = READ_CACHED_VAR(rcu_ptr);
910 WRITE_CACHED_VAR(rcu_ptr, cur_data);
911 }
912 PRODUCE_TOKENS(proc_urcu_writer, WRITE_XCHG_PTR);
913
914 :: CONSUME_TOKENS(proc_urcu_writer,
915 WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR,
916 WRITE_PROC_FIRST_MB) ->
917 goto smp_mb_send1;
918 smp_mb_send1_end:
919 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_MB);
920
921 /* first flip */
922 :: CONSUME_TOKENS(proc_urcu_writer,
923 WRITE_PROC_FIRST_MB,
924 WRITE_PROC_FIRST_READ_GP) ->
925 tmpa = READ_CACHED_VAR(urcu_gp_ctr);
926 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_READ_GP);
927 :: CONSUME_TOKENS(proc_urcu_writer,
928 WRITE_PROC_FIRST_MB | WRITE_PROC_WMB
929 | WRITE_PROC_FIRST_READ_GP,
930 WRITE_PROC_FIRST_WRITE_GP) ->
931 ooo_mem(i);
932 WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT);
933 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WRITE_GP);
934
935 :: CONSUME_TOKENS(proc_urcu_writer,
936 //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */
937 WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */
938 WRITE_PROC_FIRST_WAIT | WRITE_PROC_FIRST_WAIT_LOOP) ->
939 ooo_mem(i);
940 //smp_mb(i); /* TEST */
941 /* ONLY WAITING FOR READER 0 */
942 tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
943 #ifndef SINGLE_FLIP
944 /* In normal execution, we are always starting by
945 * waiting for the even parity.
946 */
947 cur_gp_val = RCU_GP_CTR_BIT;
948 #endif
949 if
950 :: (tmp2 & RCU_GP_CTR_NEST_MASK)
951 && ((tmp2 ^ cur_gp_val) & RCU_GP_CTR_BIT) ->
952 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP);
953 :: else ->
954 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT);
955 fi;
956
957 :: CONSUME_TOKENS(proc_urcu_writer,
958 //WRITE_PROC_FIRST_WRITE_GP /* TEST ADDING SYNC CORE */
959 WRITE_PROC_FIRST_WRITE_GP
960 | WRITE_PROC_FIRST_READ_GP
961 | WRITE_PROC_FIRST_WAIT_LOOP
962 | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR
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 /* The memory barrier will invalidate the
969 * second read done as prefetching. Note that all
970 * instructions with side-effects depending on
971 * WRITE_PROC_SECOND_READ_GP should also depend on
972 * completion of this busy-waiting loop. */
973 CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
974 #else
975 ooo_mem(i);
976 #endif
977 /* This instruction loops to WRITE_PROC_FIRST_WAIT */
978 CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_FIRST_WAIT_LOOP | WRITE_PROC_FIRST_WAIT);
979
980 /* second flip */
981 :: CONSUME_TOKENS(proc_urcu_writer,
982 //WRITE_PROC_FIRST_WAIT | //test /* no dependency. Could pre-fetch, no side-effect. */
983 WRITE_PROC_FIRST_WRITE_GP
984 | WRITE_PROC_FIRST_READ_GP
985 | WRITE_PROC_FIRST_MB,
986 WRITE_PROC_SECOND_READ_GP) ->
987 ooo_mem(i);
988 //smp_mb(i); /* TEST */
989 tmpa = READ_CACHED_VAR(urcu_gp_ctr);
990 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_READ_GP);
991 :: CONSUME_TOKENS(proc_urcu_writer,
992 WRITE_PROC_FIRST_WAIT /* dependency on first wait, because this
993 * instruction has globally observable
994 * side-effects.
995 */
996 | WRITE_PROC_FIRST_MB
997 | WRITE_PROC_WMB
998 | WRITE_PROC_FIRST_READ_GP
999 | WRITE_PROC_FIRST_WRITE_GP
1000 | WRITE_PROC_SECOND_READ_GP,
1001 WRITE_PROC_SECOND_WRITE_GP) ->
1002 ooo_mem(i);
1003 WRITE_CACHED_VAR(urcu_gp_ctr, tmpa ^ RCU_GP_CTR_BIT);
1004 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WRITE_GP);
1005
1006 :: CONSUME_TOKENS(proc_urcu_writer,
1007 //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */
1008 WRITE_PROC_FIRST_WAIT
1009 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */
1010 WRITE_PROC_SECOND_WAIT | WRITE_PROC_SECOND_WAIT_LOOP) ->
1011 ooo_mem(i);
1012 //smp_mb(i); /* TEST */
1013 /* ONLY WAITING FOR READER 0 */
1014 tmp2 = READ_CACHED_VAR(urcu_active_readers[0]);
1015 if
1016 :: (tmp2 & RCU_GP_CTR_NEST_MASK)
1017 && ((tmp2 ^ 0) & RCU_GP_CTR_BIT) ->
1018 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP);
1019 :: else ->
1020 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT);
1021 fi;
1022
1023 :: CONSUME_TOKENS(proc_urcu_writer,
1024 //WRITE_PROC_FIRST_WRITE_GP | /* TEST ADDING SYNC CORE */
1025 WRITE_PROC_SECOND_WRITE_GP
1026 | WRITE_PROC_FIRST_WRITE_GP
1027 | WRITE_PROC_SECOND_READ_GP
1028 | WRITE_PROC_FIRST_READ_GP
1029 | WRITE_PROC_SECOND_WAIT_LOOP
1030 | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR
1031 | WRITE_PROC_FIRST_MB, /* can be reordered before/after flips */
1032 0) ->
1033 #ifndef GEN_ERROR_WRITER_PROGRESS
1034 goto smp_mb_send3;
1035 smp_mb_send3_end:
1036 #else
1037 ooo_mem(i);
1038 #endif
1039 /* This instruction loops to WRITE_PROC_SECOND_WAIT */
1040 CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_WAIT_LOOP | WRITE_PROC_SECOND_WAIT);
1041
1042
1043 :: CONSUME_TOKENS(proc_urcu_writer,
1044 WRITE_PROC_FIRST_WAIT
1045 | WRITE_PROC_SECOND_WAIT
1046 | WRITE_PROC_FIRST_READ_GP
1047 | WRITE_PROC_SECOND_READ_GP
1048 | WRITE_PROC_FIRST_WRITE_GP
1049 | WRITE_PROC_SECOND_WRITE_GP
1050 | WRITE_DATA | WRITE_PROC_WMB | WRITE_XCHG_PTR
1051 | WRITE_PROC_FIRST_MB,
1052 WRITE_PROC_SECOND_MB) ->
1053 goto smp_mb_send4;
1054 smp_mb_send4_end:
1055 PRODUCE_TOKENS(proc_urcu_writer, WRITE_PROC_SECOND_MB);
1056
1057 :: CONSUME_TOKENS(proc_urcu_writer,
1058 WRITE_XCHG_PTR
1059 | WRITE_PROC_FIRST_WAIT
1060 | WRITE_PROC_SECOND_WAIT
1061 | WRITE_PROC_WMB /* No dependency on
1062 * WRITE_DATA because we
1063 * write to a
1064 * different location. */
1065 | WRITE_PROC_SECOND_MB
1066 | WRITE_PROC_FIRST_MB,
1067 WRITE_FREE) ->
1068 WRITE_CACHED_VAR(rcu_data[old_data], POISON);
1069 PRODUCE_TOKENS(proc_urcu_writer, WRITE_FREE);
1070
1071 :: CONSUME_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS, 0) ->
1072 CLEAR_TOKENS(proc_urcu_writer, WRITE_PROC_ALL_TOKENS_CLEAR);
1073 break;
1074 fi;
1075 }
1076 od;
1077 /*
1078 * Note : Promela model adds implicit serialization of the
1079 * WRITE_FREE instruction. Normally, it would be permitted to
1080 * spill on the next loop execution. Given the validation we do
1081 * checks for the data entry read to be poisoned, it's ok if
1082 * we do not check "late arriving" memory poisoning.
1083 */
1084 :: else -> break;
1085 od;
1086 /*
1087 * Given the reader loops infinitely, let the writer also busy-loop
1088 * with progress here so, with weak fairness, we can test the
1089 * writer's progress.
1090 */
1091 end_writer:
1092 do
1093 :: 1 ->
1094 #ifdef WRITER_PROGRESS
1095 progress_writer2:
1096 #endif
1097 #ifdef READER_PROGRESS
1098 /*
1099 * Make sure we don't block the reader's progress.
1100 */
1101 smp_mb_send(i, j, 5);
1102 #endif
1103 skip;
1104 od;
1105
1106 /* Non-atomic parts of the loop */
1107 goto end;
1108 smp_mb_send1:
1109 smp_mb_send(i, j, 1);
1110 goto smp_mb_send1_end;
1111 #ifndef GEN_ERROR_WRITER_PROGRESS
1112 smp_mb_send2:
1113 smp_mb_send(i, j, 2);
1114 goto smp_mb_send2_end;
1115 smp_mb_send3:
1116 smp_mb_send(i, j, 3);
1117 goto smp_mb_send3_end;
1118 #endif
1119 smp_mb_send4:
1120 smp_mb_send(i, j, 4);
1121 goto smp_mb_send4_end;
1122 end:
1123 skip;
1124 }
1125
1126 /* no name clash please */
1127 #undef proc_urcu_writer
1128
1129
1130 /* Leave after the readers and writers so the pid count is ok. */
1131 init {
1132 byte i, j;
1133
1134 atomic {
1135 INIT_CACHED_VAR(urcu_gp_ctr, 1);
1136 INIT_CACHED_VAR(rcu_ptr, 0);
1137
1138 i = 0;
1139 do
1140 :: i < NR_READERS ->
1141 INIT_CACHED_VAR(urcu_active_readers[i], 0);
1142 ptr_read_first[i] = 1;
1143 data_read_first[i] = WINE;
1144 i++;
1145 :: i >= NR_READERS -> break
1146 od;
1147 INIT_CACHED_VAR(rcu_data[0], WINE);
1148 i = 1;
1149 do
1150 :: i < SLAB_SIZE ->
1151 INIT_CACHED_VAR(rcu_data[i], POISON);
1152 i++
1153 :: i >= SLAB_SIZE -> break
1154 od;
1155
1156 init_done = 1;
1157 }
1158 }
Userspace RCU (urcu) for Linux
This page took 0.092322 seconds and 4 git commands to generate.