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