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