Commit | Line | Data |
---|---|---|
2e33016f MD |
1 | /* |
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. | |
7 | * | |
8 | * Algorithm verified : | |
9 | * | |
10 | * queue = 0; | |
11 | * waiting = 0; | |
12 | * gp_futex = 0; | |
13 | * gp = 1; | |
14 | * | |
15 | * Waker | |
16 | * while (1) { | |
17 | * this.queue = gp; | |
18 | * if (this.waiting == 1) { | |
19 | * this.waiting = 0; | |
20 | * if (gp_futex == -1) { | |
21 | * gp_futex = 0; | |
22 | * futex_wake = 1; | |
23 | * } | |
24 | * } | |
25 | * } | |
26 | * | |
27 | * Waiter | |
28 | * in_registry = 1; | |
29 | * while (1) { | |
30 | * gp_futex = -1; | |
31 | * waiting |= (queue != gp); | |
32 | * in_registry &= (queue != gp); | |
33 | * if (all in_registry == 0) { | |
34 | * progress: | |
35 | * gp_futex = 0; | |
36 | * gp = !gp; | |
37 | * restart; | |
38 | * } else { | |
39 | * futex_wake = (gp_futex == -1 ? 0 : 1); | |
40 | * while (futex_wake == 0) { } | |
41 | * } | |
42 | * queue = 0; | |
43 | * } | |
44 | * | |
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. | |
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 | * | |
63 | * Copyright (c) 2009-2011 Mathieu Desnoyers | |
64 | */ | |
65 | ||
66 | #define get_pid() (_pid) | |
67 | ||
68 | int queue[2] = 0; | |
69 | int waiting[2] = 0; | |
70 | int futex_wake = 0; | |
71 | int gp_futex = 0; | |
72 | int gp = 1; | |
73 | int in_registry[2] = 0; | |
74 | ||
75 | active [2] proctype waker() | |
76 | { | |
77 | assert(get_pid() < 2); | |
78 | ||
79 | do | |
80 | :: 1 -> | |
81 | queue[get_pid()] = gp; | |
82 | ||
83 | if | |
84 | :: (waiting[get_pid()] == 1) -> | |
85 | waiting[get_pid()] = 0; | |
86 | if | |
87 | :: (gp_futex == -1) -> | |
88 | gp_futex = 0; | |
89 | #ifndef INJ_QUEUE_NO_WAKE | |
90 | futex_wake = 1; | |
91 | #endif | |
92 | :: else -> | |
93 | skip; | |
94 | fi; | |
95 | fi; | |
96 | od; | |
97 | } | |
98 | ||
99 | ||
100 | active proctype waiter() | |
101 | { | |
102 | restart: | |
103 | in_registry[0] = 1; | |
104 | in_registry[1] = 1; | |
105 | do | |
106 | :: 1 -> | |
107 | #if (!defined(INJ_LATE_DEC) && !defined(INJ_INVERT_WAITING_VS_GP_FUTEX)) | |
108 | gp_futex = -1; | |
109 | #endif | |
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; | |
122 | ||
123 | if | |
124 | :: (in_registry[0] == 1 && queue[0] == gp) -> | |
125 | in_registry[0] = 0; | |
126 | :: else -> | |
127 | skip; | |
128 | fi; | |
129 | if | |
130 | :: (in_registry[1] == 1 && queue[1] == gp) -> | |
131 | in_registry[1] = 0; | |
132 | :: else -> | |
133 | skip; | |
134 | fi; | |
135 | #ifdef INJ_INVERT_WAITING_VS_GP_FUTEX | |
136 | gp_futex = -1; | |
137 | #endif | |
138 | ||
139 | if | |
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; | |
161 | fi; | |
162 | od; | |
163 | } |