Commit | Line | Data |
---|---|---|
d4de4869 MD |
1 | /* |
2 | * futex.spin: Promela code to validate futex wakeup algorithm. | |
3 | * | |
4 | * Algorithm verified : | |
5 | * | |
6 | * queue = 0; | |
2a8044f3 PB |
7 | * waiting = 0; |
8 | * gp_futex = 0; | |
9 | * gp = 1; | |
d4de4869 | 10 | * |
2a8044f3 PB |
11 | * Waker |
12 | * while (1) { | |
13 | * this.queue = gp; | |
14 | * if (gp_futex == -1) { | |
15 | * gp_futex = 0; | |
16 | * futex_wake = 1; | |
d4de4869 | 17 | * } |
2a8044f3 | 18 | * } |
d4de4869 MD |
19 | * |
20 | * Waiter | |
2a8044f3 | 21 | * in_registry = 1; |
d4de4869 | 22 | * while (1) { |
2a8044f3 PB |
23 | * gp_futex = -1; |
24 | * in_registry &= (queue != gp); | |
25 | * if (all in_registry == 0) { | |
26 | * progress: | |
27 | * gp_futex = 0; | |
28 | * gp = !gp; | |
29 | * restart; | |
d4de4869 | 30 | * } else { |
2a8044f3 PB |
31 | * futex_wake = (gp_futex == -1 ? 0 : 1); |
32 | * while (futex_wake == 0) { } | |
d4de4869 MD |
33 | * } |
34 | * queue = 0; | |
35 | * } | |
36 | * | |
2a8044f3 PB |
37 | * By testing progress, i.e. [] <> !np_, we check that an infinite sequence |
38 | * of update_counter_and_wait (and consequently of synchronize_rcu) will | |
39 | * not block. | |
d4de4869 MD |
40 | * |
41 | * This program is free software; you can redistribute it and/or modify | |
42 | * it under the terms of the GNU General Public License as published by | |
43 | * the Free Software Foundation; either version 2 of the License, or | |
44 | * (at your option) any later version. | |
45 | * | |
46 | * This program is distributed in the hope that it will be useful, | |
47 | * but WITHOUT ANY WARRANTY; without even the implied warranty of | |
48 | * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the | |
49 | * GNU General Public License for more details. | |
50 | * | |
51 | * You should have received a copy of the GNU General Public License | |
52 | * along with this program; if not, write to the Free Software | |
53 | * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA. | |
54 | * | |
55 | * Copyright (c) 2009 Mathieu Desnoyers | |
56 | */ | |
57 | ||
29f38067 MD |
58 | #define get_pid() (_pid) |
59 | ||
60 | int queue[2] = 0; | |
2a8044f3 PB |
61 | int futex_wake = 0; |
62 | int gp_futex = 0; | |
63 | int gp = 1; | |
64 | int in_registry[2] = 0; | |
d4de4869 | 65 | |
29f38067 | 66 | active [2] proctype waker() |
d4de4869 | 67 | { |
29f38067 MD |
68 | assert(get_pid() < 2); |
69 | ||
2a8044f3 PB |
70 | do |
71 | :: 1 -> | |
72 | queue[get_pid()] = gp; | |
73 | ||
74 | if | |
75 | :: (gp_futex == -1) -> | |
76 | gp_futex = 0; | |
77 | #ifndef INJ_QUEUE_NO_WAKE | |
78 | futex_wake = 1; | |
d4de4869 | 79 | #endif |
2a8044f3 PB |
80 | :: else -> |
81 | skip; | |
82 | fi; | |
83 | od; | |
d4de4869 MD |
84 | } |
85 | ||
86 | ||
87 | active proctype waiter() | |
88 | { | |
2a8044f3 PB |
89 | restart: |
90 | in_registry[0] = 1; | |
91 | in_registry[1] = 1; | |
d4de4869 MD |
92 | do |
93 | :: 1 -> | |
94 | #ifndef INJ_LATE_DEC | |
2a8044f3 | 95 | gp_futex = -1; |
d4de4869 | 96 | #endif |
2a8044f3 | 97 | |
d4de4869 | 98 | if |
2a8044f3 PB |
99 | :: (in_registry[0] == 1 && queue[0] == gp) -> |
100 | in_registry[0] = 0; | |
d4de4869 | 101 | :: else -> |
2a8044f3 | 102 | skip; |
d4de4869 | 103 | fi; |
29f38067 | 104 | if |
2a8044f3 PB |
105 | :: (in_registry[1] == 1 && queue[1] == gp) -> |
106 | in_registry[1] = 0; | |
107 | :: else -> | |
108 | skip; | |
29f38067 MD |
109 | fi; |
110 | if | |
2a8044f3 PB |
111 | :: (in_registry[0] == 0 && in_registry[1] == 0) -> |
112 | progress: | |
113 | #ifndef INJ_LATE_DEC | |
114 | gp_futex = 0; | |
115 | #endif | |
116 | gp = !gp; | |
117 | goto restart; | |
118 | :: else -> | |
119 | #ifdef INJ_LATE_DEC | |
120 | gp_futex = -1; | |
121 | #endif | |
122 | futex_wake = gp_futex + 1; | |
123 | do | |
124 | :: 1 -> | |
125 | if | |
126 | :: (futex_wake == 0) -> | |
127 | skip; | |
128 | :: else -> | |
129 | break; | |
130 | fi; | |
131 | od; | |
29f38067 | 132 | fi; |
d4de4869 MD |
133 | od; |
134 | } |