2 * urcu_mbmin.spin: Promela code to validate urcu. See commit number
3 * 3a9e6e9df706b8d39af94d2f027210e2e7d4106e of Mathieu Desnoyer's
4 * git archive at git://lttng.org/userspace-rcu.git, but with
5 * memory barriers removed.
7 * This validates a single reader against a single updater. The
8 * updater is assumed to have smp_mb() barriers between each pair
9 * of operations, and this model validates that a signal-mediated
10 * broadcast barrier is required only at the beginning and end of
11 * the synchronize_rcu().
13 * Note that the second half of a prior synchronize_rcu() is modelled
14 * as well as the current synchronize_rcu().
16 * This program is free software; you can redistribute it and/or modify
17 * it under the terms of the GNU General Public License as published by
18 * the Free Software Foundation; either version 2 of the License, or
19 * (at your option) any later version.
21 * This program is distributed in the hope that it will be useful,
22 * but WITHOUT ANY WARRANTY; without even the implied warranty of
23 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
24 * GNU General Public License for more details.
26 * You should have received a copy of the GNU General Public License
27 * along with this program; if not, write to the Free Software
28 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
30 * Copyright (c) 2009 Paul E. McKenney, IBM Corporation.
33 /* Promela validation variables. */
35 bit removed = 0; /* Has RCU removal happened, e.g., list_del_rcu()? */
36 bit free = 0; /* Has RCU reclamation happened, e.g., kfree()? */
37 bit need_mb = 0; /* =1 says need reader mb, =0 for reader response. */
38 byte reader_progress[4]; /* Count of read-side statement executions. */
39 bit reader_done = 0; /* =0 says reader still running, =1 says done. */
40 bit updater_done = 0; /* =0 says updater still running, =1 says done. */
42 /* Broadcast memory barriers to enable, prior synchronize_rcu() instance. */
44 /* #define MB_A */ /* Not required for correctness. */
45 /* #define MB_B */ /* Not required for correctness. */
46 /* #define MB_C */ /* Not required for correctness. */
48 /* Broadcast memory barriers to enable, current synchronize_rcu() instance. */
50 #define MB_D /* First broadcast barrier in synchronize_rcu(). */
51 /* #define MB_E */ /* Not required for correctness. */
52 /* #define MB_F */ /* Not required for correctness. */
53 #define MB_G /* Last broadcast barrier in synchronize_rcu(). */
55 /* urcu definitions and variables, taken straight from the algorithm. */
57 #define RCU_GP_CTR_BIT (1 << 7)
58 #define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1)
61 byte urcu_active_readers = 0;
63 /* Model the RCU read-side critical section. */
65 proctype urcu_reader()
73 /* Absorb any early requests for memory barriers. */
81 * Each pass through this loop executes one read-side statement
82 * from the following code fragment:
84 * rcu_read_lock(); [0a]
85 * rcu_read_lock(); [0b]
86 * p = rcu_dereference(global_p); [1]
88 * rcu_read_unlock(); [3b]
89 * rcu_read_unlock(); [3a]
91 * Because we are modeling a weak-memory machine, these statements
92 * can be seen in any order, the only restriction being that
93 * rcu_read_unlock() cannot precede the corresponding rcu_read_lock().
94 * The placement of the inner rcu_read_lock() and rcu_read_unlock()
95 * is non-deterministic, the above is but one possible placement.
96 * Intestingly enough, this model validates all possible placements
97 * of the inner rcu_read_lock() and rcu_read_unlock() statements,
98 * with the only constraint being that the rcu_read_lock() must
99 * precede the rcu_read_unlock().
101 * We also respond to memory-barrier requests, but only if our
102 * execution happens to be ordered. If the current state is
103 * misordered, we ignore memory-barrier requests.
108 :: reader_progress[0] < 2 -> /* [0a and 0b] */
109 tmp = urcu_active_readers;
111 :: (tmp & RCU_GP_CTR_NEST_MASK) == 0 ->
114 :: (reader_progress[1] +
116 reader_progress[3] == 0) && need_mb == 1 ->
118 :: need_mb == 0 && !updater_done -> skip;
121 urcu_active_readers = tmp;
123 urcu_active_readers = tmp + 1;
125 reader_progress[0] = reader_progress[0] + 1;
126 :: reader_progress[1] == 0 -> /* [1] */
127 tmp_removed = removed;
128 reader_progress[1] = 1;
129 :: reader_progress[2] == 0 -> /* [2] */
131 reader_progress[2] = 1;
132 :: ((reader_progress[0] > reader_progress[3]) &&
133 (reader_progress[3] < 2)) -> /* [3a and 3b] */
134 tmp = urcu_active_readers - 1;
135 urcu_active_readers = tmp;
136 reader_progress[3] = reader_progress[3] + 1;
140 /* Process memory-barrier requests, if it is safe to do so. */
145 :: tmp < 4 && reader_progress[tmp] == 0 ->
148 :: tmp < 4 && reader_progress[tmp] != 0 ->
151 reader_progress[0] == reader_progress[3] ->
155 reader_progress[0] != reader_progress[3] ->
159 :: tmp < 4 && reader_progress[tmp] == 0 ->
161 :: tmp < 4 && reader_progress[tmp] != 0 ->
172 /* We get here if mb processing is safe. */
182 * Check to see if we have modeled the entire RCU read-side
183 * critical section, and leave if so.
186 :: done == 1 -> break;
190 assert((tmp_free == 0) || (tmp_removed == 1));
192 /* Reader has completed. */
196 * Process any late-arriving memory-barrier requests, and
197 * in addition create a progress cycle.
211 /* Model the RCU update process. */
213 proctype urcu_updater()
218 * ----------------------------------------------------------------
219 * prior synchronize_rcu().
222 /* prior synchronize_rcu(), second counter flip. */
224 need_mb = 1; /* mb() A (analogous to omitted barrier between E and F) */
226 :: need_mb == 1 && !reader_done -> skip;
227 :: need_mb == 0 || reader_done -> break;
229 #endif /* #ifdef MB_A */
230 urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
232 need_mb = 1; /* mb() B (analogous to F) */
234 :: need_mb == 1 && !reader_done -> skip;
235 :: need_mb == 0 || reader_done -> break;
237 #endif /* #ifdef MB_B */
241 :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
242 (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
243 (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
249 need_mb = 1; /* mb() C absolutely required by analogy with G */
251 :: need_mb == 1 && !reader_done -> skip;
252 :: need_mb == 0 || reader_done -> break;
254 #endif /* #ifdef MB_C */
256 /* Removal statement, e.g., list_del_rcu(). */
260 * prior synchronize_rcu().
261 * ----------------------------------------------------------------
265 * ----------------------------------------------------------------
266 * current synchronize_rcu().
269 /* current synchronize_rcu(), first counter flip. */
271 need_mb = 1; /* mb() D suggested */
273 :: need_mb == 1 && !reader_done -> skip;
274 :: need_mb == 0 || reader_done -> break;
276 #endif /* #ifdef MB_D */
277 urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
279 need_mb = 1; /* mb() E required if D not present */
281 :: need_mb == 1 && !reader_done -> skip;
282 :: need_mb == 0 || reader_done -> break;
284 #endif /* #ifdef MB_E */
286 /* current synchronize_rcu(), first-flip check plus second flip. */
292 :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
293 (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
294 (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
299 urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
302 urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
306 :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
307 (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
308 (tmp & ~RCU_GP_CTR_NEST_MASK) ->
315 /* current synchronize_rcu(), second counter flip check. */
317 need_mb = 1; /* mb() F not required */
319 :: need_mb == 1 && !reader_done -> skip;
320 :: need_mb == 0 || reader_done -> break;
322 #endif /* #ifdef MB_F */
326 :: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
327 (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
328 (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
334 need_mb = 1; /* mb() G absolutely required */
336 :: need_mb == 1 && !reader_done -> skip;
337 :: need_mb == 0 || reader_done -> break;
339 #endif /* #ifdef MB_G */
342 * current synchronize_rcu().
343 * ----------------------------------------------------------------
346 /* free-up step, e.g., kfree(). */
349 /* We are done, so kill all the infinite loops in the reader. */
352 /* Create a progress cycle. Correctness requires we get here. */
362 * Initialize the array, spawn a reader and an updater. Because readers
363 * are independent of each other, only one reader is needed.
368 reader_progress[0] = 0;
369 reader_progress[1] = 0;
370 reader_progress[2] = 0;
371 reader_progress[3] = 0;