projects / userspace-rcu.git / blob
? search:


2aac6eb6a25eb3fd786a3da4ff1e2ab95e229f24
[userspace-rcu.git] /
1 #define WRITER_PROGRESS
2 #define GEN_ERROR_WRITER_PROGRESS
3
4 #define read_free_race (read_generation[0] == last_free_gen)
5 #define read_free (free_done && data_access[0])
6
7 //#define TEST_SIGNAL
8 //#define TEST_SIGNAL_ON_READ
9 //#define TEST_SIGNAL_ON_WRITE
10
11 #define RCU_GP_CTR_BIT (1 << 7)
12 #define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1)
13
14 #ifndef READER_NEST_LEVEL
15 //#define READER_NEST_LEVEL 1
16 #define READER_NEST_LEVEL 2
17 #endif
18
19 #define REMOTE_BARRIERS
20 /*
21 * mem.spin: Promela code to validate memory barriers with OOO memory.
22 *
23 * This program is free software; you can redistribute it and/or modify
24 * it under the terms of the GNU General Public License as published by
25 * the Free Software Foundation; either version 2 of the License, or
26 * (at your option) any later version.
27 *
28 * This program is distributed in the hope that it will be useful,
29 * but WITHOUT ANY WARRANTY; without even the implied warranty of
30 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
31 * GNU General Public License for more details.
32 *
33 * You should have received a copy of the GNU General Public License
34 * along with this program; if not, write to the Free Software
35 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
36 *
37 * Copyright (c) 2009 Mathieu Desnoyers
38 */
39
40 /* Promela validation variables. */
41
42 /* specific defines "included" here */
43 /* DEFINES file "included" here */
44
45 /* All signal readers have same PID and uses same reader variable */
46 #ifdef TEST_SIGNAL_ON_WRITE
47
48 #define NR_READERS 1 /* the writer is also a signal reader */
49 #define NR_WRITERS 1
50
51 #define NR_PROCS 1
52
53 #define get_pid() (0)
54
55 #elif defined(TEST_SIGNAL_ON_READ)
56
57 #define get_pid() ((_pid < 2) -> 0 : 1)
58
59 #define NR_READERS 1
60 #define NR_WRITERS 1
61
62 #define NR_PROCS 2
63
64 #else
65
66 #define get_pid() (_pid)
67
68 #define NR_READERS 1
69 #define NR_WRITERS 1
70
71 #define NR_PROCS 2
72
73 #endif
74
75 #define get_readerid() (get_pid())
76
77 /*
78 * Each process have its own data in cache. Caches are randomly updated.
79 * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces
80 * both.
81 */
82
83 typedef per_proc_byte {
84 byte val[NR_PROCS];
85 };
86
87 /* Bitfield has a maximum of 8 procs */
88 typedef per_proc_bit {
89 byte bitfield;
90 };
91
92 #define DECLARE_CACHED_VAR(type, x) \
93 type mem_##x; \
94 per_proc_##type cached_##x; \
95 per_proc_bit cache_dirty_##x;
96
97 #define INIT_CACHED_VAR(x, v, j) \
98 mem_##x = v; \
99 cache_dirty_##x.bitfield = 0; \
100 j = 0; \
101 do \
102 :: j < NR_PROCS -> \
103 cached_##x.val[j] = v; \
104 j++ \
105 :: j >= NR_PROCS -> break \
106 od;
107
108 #define IS_CACHE_DIRTY(x, id) (cache_dirty_##x.bitfield & (1 << id))
109
110 #define READ_CACHED_VAR(x) (cached_##x.val[get_pid()])
111
112 #define WRITE_CACHED_VAR(x, v) \
113 atomic { \
114 cached_##x.val[get_pid()] = v; \
115 cache_dirty_##x.bitfield = \
116 cache_dirty_##x.bitfield | (1 << get_pid()); \
117 }
118
119 #define CACHE_WRITE_TO_MEM(x, id) \
120 if \
121 :: IS_CACHE_DIRTY(x, id) -> \
122 mem_##x = cached_##x.val[id]; \
123 cache_dirty_##x.bitfield = \
124 cache_dirty_##x.bitfield & (~(1 << id)); \
125 :: else -> \
126 skip \
127 fi;
128
129 #define CACHE_READ_FROM_MEM(x, id) \
130 if \
131 :: !IS_CACHE_DIRTY(x, id) -> \
132 cached_##x.val[id] = mem_##x;\
133 :: else -> \
134 skip \
135 fi;
136
137 /*
138 * May update other caches if cache is dirty, or not.
139 */
140 #define RANDOM_CACHE_WRITE_TO_MEM(x, id)\
141 if \
142 :: 1 -> CACHE_WRITE_TO_MEM(x, id); \
143 :: 1 -> skip \
144 fi;
145
146 #define RANDOM_CACHE_READ_FROM_MEM(x, id)\
147 if \
148 :: 1 -> CACHE_READ_FROM_MEM(x, id); \
149 :: 1 -> skip \
150 fi;
151
152 /*
153 * Remote barriers tests the scheme where a signal (or IPI) is sent to all
154 * reader threads to promote their compiler barrier to a smp_mb().
155 */
156 #ifdef REMOTE_BARRIERS
157
158 inline smp_rmb_pid(i, j)
159 {
160 atomic {
161 CACHE_READ_FROM_MEM(urcu_gp_ctr, i);
162 j = 0;
163 do
164 :: j < NR_READERS ->
165 CACHE_READ_FROM_MEM(urcu_active_readers[j], i);
166 j++
167 :: j >= NR_READERS -> break
168 od;
169 CACHE_READ_FROM_MEM(generation_ptr, i);
170 }
171 }
172
173 inline smp_wmb_pid(i, j)
174 {
175 atomic {
176 CACHE_WRITE_TO_MEM(urcu_gp_ctr, i);
177 j = 0;
178 do
179 :: j < NR_READERS ->
180 CACHE_WRITE_TO_MEM(urcu_active_readers[j], i);
181 j++
182 :: j >= NR_READERS -> break
183 od;
184 CACHE_WRITE_TO_MEM(generation_ptr, i);
185 }
186 }
187
188 inline smp_mb_pid(i, j)
189 {
190 atomic {
191 #ifndef NO_WMB
192 smp_wmb_pid(i, j);
193 #endif
194 #ifndef NO_RMB
195 smp_rmb_pid(i, j);
196 #endif
197 #ifdef NO_WMB
198 #ifdef NO_RMB
199 ooo_mem(j);
200 #endif
201 #endif
202 }
203 }
204
205 /*
206 * Readers do a simple barrier(), writers are doing a smp_mb() _and_ sending a
207 * signal or IPI to have all readers execute a smp_mb.
208 * We are not modeling the whole rendez-vous between readers and writers here,
209 * we just let the writer update each reader's caches remotely.
210 */
211 inline smp_mb_writer(i, j)
212 {
213 smp_mb_pid(get_pid(), j);
214 i = 0;
215 do
216 :: i < NR_READERS ->
217 smp_mb_pid(i, j);
218 i++;
219 :: i >= NR_READERS -> break
220 od;
221 smp_mb_pid(get_pid(), j);
222 }
223
224 inline smp_mb_reader(i, j)
225 {
226 skip;
227 }
228
229 #else
230
231 inline smp_rmb(i, j)
232 {
233 atomic {
234 CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
235 i = 0;
236 do
237 :: i < NR_READERS ->
238 CACHE_READ_FROM_MEM(urcu_active_readers[i], get_pid());
239 i++
240 :: i >= NR_READERS -> break
241 od;
242 CACHE_READ_FROM_MEM(generation_ptr, get_pid());
243 }
244 }
245
246 inline smp_wmb(i, j)
247 {
248 atomic {
249 CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
250 i = 0;
251 do
252 :: i < NR_READERS ->
253 CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid());
254 i++
255 :: i >= NR_READERS -> break
256 od;
257 CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
258 }
259 }
260
261 inline smp_mb(i, j)
262 {
263 atomic {
264 #ifndef NO_WMB
265 smp_wmb(i, j);
266 #endif
267 #ifndef NO_RMB
268 smp_rmb(i, j);
269 #endif
270 #ifdef NO_WMB
271 #ifdef NO_RMB
272 ooo_mem(i);
273 #endif
274 #endif
275 }
276 }
277
278 inline smp_mb_writer(i, j)
279 {
280 smp_mb(i, j);
281 }
282
283 inline smp_mb_reader(i, j)
284 {
285 smp_mb(i, j);
286 }
287
288 #endif
289
290 /* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */
291 DECLARE_CACHED_VAR(byte, urcu_gp_ctr);
292 /* Note ! currently only two readers */
293 DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
294 /* pointer generation */
295 DECLARE_CACHED_VAR(byte, generation_ptr);
296
297 byte last_free_gen = 0;
298 bit free_done = 0;
299 byte read_generation[NR_READERS];
300 bit data_access[NR_READERS];
301
302 bit write_lock = 0;
303
304 bit init_done = 0;
305
306 bit sighand_exec = 0;
307
308 inline wait_init_done()
309 {
310 do
311 :: init_done == 0 -> skip;
312 :: else -> break;
313 od;
314 }
315
316 #ifdef TEST_SIGNAL
317
318 inline wait_for_sighand_exec()
319 {
320 sighand_exec = 0;
321 do
322 :: sighand_exec == 0 -> skip;
323 :: else -> break;
324 od;
325 }
326
327 #ifdef TOO_BIG_STATE_SPACE
328 inline wait_for_sighand_exec()
329 {
330 sighand_exec = 0;
331 do
332 :: sighand_exec == 0 -> skip;
333 :: else ->
334 if
335 :: 1 -> break;
336 :: 1 -> sighand_exec = 0;
337 skip;
338 fi;
339 od;
340 }
341 #endif
342
343 #else
344
345 inline wait_for_sighand_exec()
346 {
347 skip;
348 }
349
350 #endif
351
352 #ifdef TEST_SIGNAL_ON_WRITE
353 /* Block on signal handler execution */
354 inline dispatch_sighand_write_exec()
355 {
356 sighand_exec = 1;
357 do
358 :: sighand_exec == 1 ->
359 skip;
360 :: else ->
361 break;
362 od;
363 }
364
365 #else
366
367 inline dispatch_sighand_write_exec()
368 {
369 skip;
370 }
371
372 #endif
373
374 #ifdef TEST_SIGNAL_ON_READ
375 /* Block on signal handler execution */
376 inline dispatch_sighand_read_exec()
377 {
378 sighand_exec = 1;
379 do
380 :: sighand_exec == 1 ->
381 skip;
382 :: else ->
383 break;
384 od;
385 }
386
387 #else
388
389 inline dispatch_sighand_read_exec()
390 {
391 skip;
392 }
393
394 #endif
395
396
397 inline ooo_mem(i)
398 {
399 atomic {
400 RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
401 i = 0;
402 do
403 :: i < NR_READERS ->
404 RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i],
405 get_pid());
406 i++
407 :: i >= NR_READERS -> break
408 od;
409 RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
410 RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
411 i = 0;
412 do
413 :: i < NR_READERS ->
414 RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i],
415 get_pid());
416 i++
417 :: i >= NR_READERS -> break
418 od;
419 RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid());
420 }
421 }
422
423 inline wait_for_reader(tmp, tmp2, i, j)
424 {
425 do
426 :: 1 ->
427 tmp2 = READ_CACHED_VAR(urcu_active_readers[tmp]);
428 ooo_mem(i);
429 dispatch_sighand_write_exec();
430 if
431 :: (tmp2 & RCU_GP_CTR_NEST_MASK)
432 && ((tmp2 ^ READ_CACHED_VAR(urcu_gp_ctr))
433 & RCU_GP_CTR_BIT) ->
434 #ifndef GEN_ERROR_WRITER_PROGRESS
435 smp_mb_writer(i, j);
436 #else
437 ooo_mem(i);
438 #endif
439 dispatch_sighand_write_exec();
440 :: else ->
441 break;
442 fi;
443 od;
444 }
445
446 inline wait_for_quiescent_state(tmp, tmp2, i, j)
447 {
448 tmp = 0;
449 do
450 :: tmp < NR_READERS ->
451 wait_for_reader(tmp, tmp2, i, j);
452 if
453 :: (NR_READERS > 1) && (tmp < NR_READERS - 1)
454 -> ooo_mem(i);
455 dispatch_sighand_write_exec();
456 :: else
457 -> skip;
458 fi;
459 tmp++
460 :: tmp >= NR_READERS -> break
461 od;
462 }
463
464 /* Model the RCU read-side critical section. */
465
466 #ifndef TEST_SIGNAL_ON_WRITE
467
468 inline urcu_one_read(i, j, nest_i, tmp, tmp2)
469 {
470 nest_i = 0;
471 do
472 :: nest_i < READER_NEST_LEVEL ->
473 ooo_mem(i);
474 dispatch_sighand_read_exec();
475 tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
476 ooo_mem(i);
477 dispatch_sighand_read_exec();
478 if
479 :: (!(tmp & RCU_GP_CTR_NEST_MASK))
480 ->
481 tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
482 ooo_mem(i);
483 dispatch_sighand_read_exec();
484 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
485 tmp2);
486 :: else ->
487 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
488 tmp + 1);
489 fi;
490 smp_mb_reader(i, j);
491 dispatch_sighand_read_exec();
492 nest_i++;
493 :: nest_i >= READER_NEST_LEVEL -> break;
494 od;
495
496 read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
497 data_access[get_readerid()] = 1;
498 data_access[get_readerid()] = 0;
499
500 nest_i = 0;
501 do
502 :: nest_i < READER_NEST_LEVEL ->
503 smp_mb_reader(i, j);
504 dispatch_sighand_read_exec();
505 tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
506 ooo_mem(i);
507 dispatch_sighand_read_exec();
508 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
509 nest_i++;
510 :: nest_i >= READER_NEST_LEVEL -> break;
511 od;
512 //ooo_mem(i);
513 //dispatch_sighand_read_exec();
514 //smp_mc(i); /* added */
515 }
516
517 active proctype urcu_reader()
518 {
519 byte i, j, nest_i;
520 byte tmp, tmp2;
521
522 wait_init_done();
523
524 assert(get_pid() < NR_PROCS);
525
526 end_reader:
527 do
528 :: 1 ->
529 /*
530 * We do not test reader's progress here, because we are mainly
531 * interested in writer's progress. The reader never blocks
532 * anyway. We have to test for reader/writer's progress
533 * separately, otherwise we could think the writer is doing
534 * progress when it's blocked by an always progressing reader.
535 */
536 #ifdef READER_PROGRESS
537 progress_reader:
538 #endif
539 urcu_one_read(i, j, nest_i, tmp, tmp2);
540 od;
541 }
542
543 #endif //!TEST_SIGNAL_ON_WRITE
544
545 #ifdef TEST_SIGNAL
546 /* signal handler reader */
547
548 inline urcu_one_read_sig(i, j, nest_i, tmp, tmp2)
549 {
550 nest_i = 0;
551 do
552 :: nest_i < READER_NEST_LEVEL ->
553 ooo_mem(i);
554 tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
555 ooo_mem(i);
556 if
557 :: (!(tmp & RCU_GP_CTR_NEST_MASK))
558 ->
559 tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
560 ooo_mem(i);
561 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
562 tmp2);
563 :: else ->
564 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
565 tmp + 1);
566 fi;
567 smp_mb_reader(i, j);
568 nest_i++;
569 :: nest_i >= READER_NEST_LEVEL -> break;
570 od;
571
572 read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
573 data_access[get_readerid()] = 1;
574 data_access[get_readerid()] = 0;
575
576 nest_i = 0;
577 do
578 :: nest_i < READER_NEST_LEVEL ->
579 smp_mb_reader(i, j);
580 tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
581 ooo_mem(i);
582 WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
583 nest_i++;
584 :: nest_i >= READER_NEST_LEVEL -> break;
585 od;
586 //ooo_mem(i);
587 //smp_mc(i); /* added */
588 }
589
590 active proctype urcu_reader_sig()
591 {
592 byte i, j, nest_i;
593 byte tmp, tmp2;
594
595 wait_init_done();
596
597 assert(get_pid() < NR_PROCS);
598
599 end_reader:
600 do
601 :: 1 ->
602 wait_for_sighand_exec();
603 /*
604 * We do not test reader's progress here, because we are mainly
605 * interested in writer's progress. The reader never blocks
606 * anyway. We have to test for reader/writer's progress
607 * separately, otherwise we could think the writer is doing
608 * progress when it's blocked by an always progressing reader.
609 */
610 #ifdef READER_PROGRESS
611 progress_reader:
612 #endif
613 urcu_one_read_sig(i, j, nest_i, tmp, tmp2);
614 od;
615 }
616
617 #endif
618
619 /* Model the RCU update process. */
620
621 active proctype urcu_writer()
622 {
623 byte i, j;
624 byte tmp, tmp2;
625 byte old_gen;
626
627 wait_init_done();
628
629 assert(get_pid() < NR_PROCS);
630
631 do
632 :: (READ_CACHED_VAR(generation_ptr) < 5) ->
633 #ifdef WRITER_PROGRESS
634 progress_writer1:
635 #endif
636 ooo_mem(i);
637 dispatch_sighand_write_exec();
638 atomic {
639 old_gen = READ_CACHED_VAR(generation_ptr);
640 WRITE_CACHED_VAR(generation_ptr, old_gen + 1);
641 }
642 ooo_mem(i);
643 dispatch_sighand_write_exec();
644
645 do
646 :: 1 ->
647 atomic {
648 if
649 :: write_lock == 0 ->
650 write_lock = 1;
651 break;
652 :: else ->
653 skip;
654 fi;
655 }
656 od;
657 smp_mb_writer(i, j);
658 dispatch_sighand_write_exec();
659 tmp = READ_CACHED_VAR(urcu_gp_ctr);
660 ooo_mem(i);
661 dispatch_sighand_write_exec();
662 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
663 ooo_mem(i);
664 dispatch_sighand_write_exec();
665 //smp_mc(i);
666 wait_for_quiescent_state(tmp, tmp2, i, j);
667 //smp_mc(i);
668 #ifndef SINGLE_FLIP
669 ooo_mem(i);
670 dispatch_sighand_write_exec();
671 tmp = READ_CACHED_VAR(urcu_gp_ctr);
672 ooo_mem(i);
673 dispatch_sighand_write_exec();
674 WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
675 //smp_mc(i);
676 ooo_mem(i);
677 dispatch_sighand_write_exec();
678 wait_for_quiescent_state(tmp, tmp2, i, j);
679 #endif
680 smp_mb_writer(i, j);
681 dispatch_sighand_write_exec();
682 write_lock = 0;
683 /* free-up step, e.g., kfree(). */
684 atomic {
685 last_free_gen = old_gen;
686 free_done = 1;
687 }
688 :: else -> break;
689 od;
690 /*
691 * Given the reader loops infinitely, let the writer also busy-loop
692 * with progress here so, with weak fairness, we can test the
693 * writer's progress.
694 */
695 end_writer:
696 do
697 :: 1 ->
698 #ifdef WRITER_PROGRESS
699 progress_writer2:
700 #endif
701 dispatch_sighand_write_exec();
702 od;
703 }
704
705 /* Leave after the readers and writers so the pid count is ok. */
706 init {
707 byte i, j;
708
709 atomic {
710 INIT_CACHED_VAR(urcu_gp_ctr, 1, j);
711 INIT_CACHED_VAR(generation_ptr, 0, j);
712
713 i = 0;
714 do
715 :: i < NR_READERS ->
716 INIT_CACHED_VAR(urcu_active_readers[i], 0, j);
717 read_generation[i] = 1;
718 data_access[i] = 0;
719 i++;
720 :: i >= NR_READERS -> break
721 od;
722 init_done = 1;
723 }
724 }
Userspace RCU (urcu) for Linux
This page took 0.041997 seconds and 3 git commands to generate.