[urcu.git] / formal-model / urcu.spin

/*
 * urcu.spin: Promela code to validate urcu.  See commit number
 *	3a9e6e9df706b8d39af94d2f027210e2e7d4106e of Mathieu Desnoyer's
 *      git archive at git://lttng.org/userspace-rcu.git
 *
 * This program is free software; you can redistribute it and/or modify
 * it under the terms of the GNU General Public License as published by
 * the Free Software Foundation; either version 2 of the License, or
 * (at your option) any later version.
 *
 * This program is distributed in the hope that it will be useful,
 * but WITHOUT ANY WARRANTY; without even the implied warranty of
 * MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
 * GNU General Public License for more details.
 *
 * You should have received a copy of the GNU General Public License
 * along with this program; if not, write to the Free Software
 * Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
 *
 * Copyright (c) 2009 Paul E. McKenney, IBM Corporation.
 */

/* Promela validation variables. */

bit removed = 0;  /* Has RCU removal happened, e.g., list_del_rcu()? */
bit free = 0;     /* Has RCU reclamation happened, e.g., kfree()? */
bit need_mb = 0;  /* =1 says need reader mb, =0 for reader response. */
byte reader_progress[4];
		  /* Count of read-side statement executions. */
bit reader_done = 0;
		  /* =0 says reader still running, =1 says done. */
bit updater_done = 0;
		  /* =0 says updater still running, =1 says done. */

/* urcu definitions and variables, taken straight from the algorithm. */

#define RCU_GP_CTR_BIT (1 << 7)
#define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1)

byte urcu_gp_ctr = 1;
byte urcu_active_readers = 0;

/* Model the RCU read-side critical section. */

proctype urcu_reader()
{
	bit done = 0;
	bit mbok;
	byte tmp;
	byte tmp_removed;
	byte tmp_free;

	/* Absorb any early requests for memory barriers. */
	do
	:: need_mb == 1 ->
		need_mb = 0;
	:: !updater_done -> skip;
	:: 1 -> break;
	od;

	/*
	 * Each pass through this loop executes one read-side statement
	 * from the following code fragment:
	 *
	 *	rcu_read_lock(); [0a]
	 *	rcu_read_lock(); [0b]
	 *	p = rcu_dereference(global_p); [1]
	 *	x = p->data; [2]
	 *	rcu_read_unlock(); [3b]
	 *	rcu_read_unlock(); [3a]
	 *
	 * Because we are modeling a weak-memory machine, these statements
	 * can be seen in any order, the only restriction being that
	 * rcu_read_unlock() cannot precede the corresponding rcu_read_lock().
	 * The placement of the inner rcu_read_lock() and rcu_read_unlock()
	 * is non-deterministic, the above is but one possible placement.
	 * Intestingly enough, this model validates all possible placements
	 * of the inner rcu_read_lock() and rcu_read_unlock() statements,
	 * with the only constraint being that the rcu_read_lock() must
	 * precede the rcu_read_unlock().
	 *
	 * We also respond to memory-barrier requests, but only if our
	 * execution happens to be ordered.  If the current state is
	 * misordered, we ignore memory-barrier requests.
	 */
	do
	:: 1 ->
		if
		:: reader_progress[0] < 2 -> /* [0a and 0b] */
			tmp = urcu_active_readers;
			if
			:: (tmp & RCU_GP_CTR_NEST_MASK) == 0 ->
				tmp = urcu_gp_ctr;
				do
				:: (reader_progress[1] +
				    reader_progress[2] +
				    reader_progress[3] == 0) && need_mb == 1 ->
					need_mb = 0;
				:: !updater_done -> skip;
				:: 1 -> break;
				od;
				urcu_active_readers = tmp;
			 :: else ->
				urcu_active_readers = tmp + 1;
			fi;
			reader_progress[0] = reader_progress[0] + 1;
		:: reader_progress[1] == 0 -> /* [1] */
			tmp_removed = removed;
			reader_progress[1] = 1;
		:: reader_progress[2] == 0 -> /* [2] */
			tmp_free = free;
			reader_progress[2] = 1;
		:: ((reader_progress[0] > reader_progress[3]) &&
		    (reader_progress[3] < 2)) -> /* [3a and 3b] */
			tmp = urcu_active_readers - 1;
			urcu_active_readers = tmp;
			reader_progress[3] = reader_progress[3] + 1;
		:: else -> break;
		fi;

		/* Process memory-barrier requests, if it is safe to do so. */
		atomic {
			mbok = 0;
			tmp = 0;
			do
			:: tmp < 4 && reader_progress[tmp] == 0 ->
				tmp = tmp + 1;
				break;
			:: tmp < 4 && reader_progress[tmp] != 0 ->
				tmp = tmp + 1;
			:: tmp >= 4 &&
			   reader_progress[0] == reader_progress[3] ->
				done = 1;
				break;
			:: tmp >= 4 &&
			   reader_progress[0] != reader_progress[3] ->
			   	break;
			od;
			do
			:: tmp < 4 && reader_progress[tmp] == 0 ->
				tmp = tmp + 1;
			:: tmp < 4 && reader_progress[tmp] != 0 ->
				break;
			:: tmp >= 4 ->
				mbok = 1;
				break;
			od

		}

		if
		:: mbok == 1 ->
			/* We get here if mb processing is safe. */
			do
			:: need_mb == 1 ->
				need_mb = 0;
			:: !updater_done -> skip;
			:: 1 -> break;
			od;
		:: else -> skip;
		fi;

		/*
		 * Check to see if we have modeled the entire RCU read-side
		 * critical section, and leave if so.
		 */
		if
		:: done == 1 -> break;
		:: else -> skip;
		fi
	od;
	assert((tmp_free == 0) || (tmp_removed == 1));

	/* Reader has completed. */
	reader_done = 1;

	/* Process any late-arriving memory-barrier requests. */
	do
	:: need_mb == 1 ->
		need_mb = 0;
	:: !updater_done -> skip;
	:: 1 -> break;
	od;
}

/* Model the RCU update process. */

proctype urcu_updater()
{
	/* prior synchronize_rcu(), second counter flip. */
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;
	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;
	do
	:: 1 ->
		if
		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
		   (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
			skip;
		:: else -> break;
		fi;
	od;
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;

	/* Removal statement, e.g., list_del_rcu(). */
	removed = 1;

	/* current synchronize_rcu(), first counter flip. */
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;
	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;
	do
	:: 1 ->
		if
		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
		   (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
			skip;
		:: else -> break;
		fi;
	od;
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;

	/* current synchronize_rcu(), second counter flip. */
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;
	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;
	do
	:: 1 ->
		if
		:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
		   (urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
		   (urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
			skip;
		:: else -> break;
		fi;
	od;
	need_mb = 1;
	do
	:: need_mb == 1 -> skip;
	:: need_mb == 0 -> break;
	od;

	/* free-up step, e.g., kfree(). */
	free = 1;

	/*
	 * Signal updater done, ending any otherwise-infinite loops
	 * in the reading process.
	 */
	updater_done = 1;
}

/*
 * Initialize the array, spawn a reader and an updater.  Because readers
 * are independent of each other, only one reader is needed.
 */

init {
	atomic {
		reader_progress[0] = 0;
		reader_progress[1] = 0;
		reader_progress[2] = 0;
		reader_progress[3] = 0;
		run urcu_reader();
		run urcu_updater();
	}
}
Commit	Line	Data
5464000f MD	1	/*
	2	* urcu.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
	5	*
	6	* This program is free software; you can redistribute it and/or modify
	7	* it under the terms of the GNU General Public License as published by
	8	* the Free Software Foundation; either version 2 of the License, or
	9	* (at your option) any later version.
	10	*
	11	* This program is distributed in the hope that it will be useful,
	12	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	13	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	14	* GNU General Public License for more details.
	15	*
	16	* You should have received a copy of the GNU General Public License
	17	* along with this program; if not, write to the Free Software
	18	* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
	19	*
	20	* Copyright (c) 2009 Paul E. McKenney, IBM Corporation.
	21	*/
	22
	23	/* Promela validation variables. */
	24
	25	bit removed = 0; /* Has RCU removal happened, e.g., list_del_rcu()? */
	26	bit free = 0; /* Has RCU reclamation happened, e.g., kfree()? */
	27	bit need_mb = 0; /* =1 says need reader mb, =0 for reader response. */
	28	byte reader_progress[4];
	29	/* Count of read-side statement executions. */
545a4f13 PM	30	bit reader_done = 0;
	31	/* =0 says reader still running, =1 says done. */
	32	bit updater_done = 0;
	33	/* =0 says updater still running, =1 says done. */
5464000f MD	34
	35	/* urcu definitions and variables, taken straight from the algorithm. */
	36
	37	#define RCU_GP_CTR_BIT (1 << 7)
	38	#define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1)
	39
	40	byte urcu_gp_ctr = 1;
	41	byte urcu_active_readers = 0;
	42
	43	/* Model the RCU read-side critical section. */
	44
	45	proctype urcu_reader()
	46	{
	47	bit done = 0;
	48	bit mbok;
	49	byte tmp;
	50	byte tmp_removed;
	51	byte tmp_free;
	52
	53	/* Absorb any early requests for memory barriers. */
	54	do
	55	:: need_mb == 1 ->
	56	need_mb = 0;
545a4f13	57	:: !updater_done -> skip;
5464000f MD	58	:: 1 -> break;
	59	od;
	60
	61	/*
	62	* Each pass through this loop executes one read-side statement
	63	* from the following code fragment:
	64	*
	65	* rcu_read_lock(); [0a]
	66	* rcu_read_lock(); [0b]
	67	* p = rcu_dereference(global_p); [1]
	68	* x = p->data; [2]
	69	* rcu_read_unlock(); [3b]
	70	* rcu_read_unlock(); [3a]
	71	*
	72	* Because we are modeling a weak-memory machine, these statements
	73	* can be seen in any order, the only restriction being that
	74	* rcu_read_unlock() cannot precede the corresponding rcu_read_lock().
	75	* The placement of the inner rcu_read_lock() and rcu_read_unlock()
	76	* is non-deterministic, the above is but one possible placement.
	77	* Intestingly enough, this model validates all possible placements
	78	* of the inner rcu_read_lock() and rcu_read_unlock() statements,
	79	* with the only constraint being that the rcu_read_lock() must
	80	* precede the rcu_read_unlock().
	81	*
	82	* We also respond to memory-barrier requests, but only if our
	83	* execution happens to be ordered. If the current state is
	84	* misordered, we ignore memory-barrier requests.
	85	*/
	86	do
	87	:: 1 ->
	88	if
	89	:: reader_progress[0] < 2 -> /* [0a and 0b] */
	90	tmp = urcu_active_readers;
	91	if
	92	:: (tmp & RCU_GP_CTR_NEST_MASK) == 0 ->
	93	tmp = urcu_gp_ctr;
	94	do
	95	:: (reader_progress[1] +
	96	reader_progress[2] +
	97	reader_progress[3] == 0) && need_mb == 1 ->
	98	need_mb = 0;
545a4f13	99	:: !updater_done -> skip;
5464000f MD	100	:: 1 -> break;
	101	od;
	102	urcu_active_readers = tmp;
	103	:: else ->
	104	urcu_active_readers = tmp + 1;
	105	fi;
	106	reader_progress[0] = reader_progress[0] + 1;
	107	:: reader_progress[1] == 0 -> /* [1] */
	108	tmp_removed = removed;
	109	reader_progress[1] = 1;
	110	:: reader_progress[2] == 0 -> /* [2] */
	111	tmp_free = free;
	112	reader_progress[2] = 1;
	113	:: ((reader_progress[0] > reader_progress[3]) &&
	114	(reader_progress[3] < 2)) -> /* [3a and 3b] */
	115	tmp = urcu_active_readers - 1;
	116	urcu_active_readers = tmp;
	117	reader_progress[3] = reader_progress[3] + 1;
	118	:: else -> break;
	119	fi;
	120
	121	/* Process memory-barrier requests, if it is safe to do so. */
	122	atomic {
	123	mbok = 0;
	124	tmp = 0;
	125	do
	126	:: tmp < 4 && reader_progress[tmp] == 0 ->
	127	tmp = tmp + 1;
	128	break;
	129	:: tmp < 4 && reader_progress[tmp] != 0 ->
	130	tmp = tmp + 1;
f321bf38 PM	131	:: tmp >= 4 &&
f321bf38 PM	132	reader_progress[0] == reader_progress[3] ->
5464000f MD	133	done = 1;
5464000f MD	134	break;
f321bf38 PM	135	:: tmp >= 4 &&
	136	reader_progress[0] != reader_progress[3] ->
	137	break;
5464000f MD	138	od;
	139	do
	140	:: tmp < 4 && reader_progress[tmp] == 0 ->
	141	tmp = tmp + 1;
	142	:: tmp < 4 && reader_progress[tmp] != 0 ->
	143	break;
	144	:: tmp >= 4 ->
	145	mbok = 1;
	146	break;
	147	od
	148
	149	}
	150
	151	if
	152	:: mbok == 1 ->
	153	/* We get here if mb processing is safe. */
	154	do
	155	:: need_mb == 1 ->
	156	need_mb = 0;
545a4f13	157	:: !updater_done -> skip;
5464000f MD	158	:: 1 -> break;
	159	od;
	160	:: else -> skip;
	161	fi;
	162
	163	/*
	164	* Check to see if we have modeled the entire RCU read-side
	165	* critical section, and leave if so.
	166	*/
	167	if
	168	:: done == 1 -> break;
	169	:: else -> skip;
	170	fi
	171	od;
	172	assert((tmp_free == 0) \|\| (tmp_removed == 1));
	173
545a4f13 PM	174	/* Reader has completed. */
	175	reader_done = 1;
	176
5464000f MD	177	/* Process any late-arriving memory-barrier requests. */
	178	do
	179	:: need_mb == 1 ->
	180	need_mb = 0;
545a4f13	181	:: !updater_done -> skip;
5464000f MD	182	:: 1 -> break;
	183	od;
	184	}
	185
	186	/* Model the RCU update process. */
	187
	188	proctype urcu_updater()
	189	{
9d950311 PM	190	/* prior synchronize_rcu(), second counter flip. */
	191	need_mb = 1;
	192	do
	193	:: need_mb == 1 -> skip;
	194	:: need_mb == 0 -> break;
	195	od;
	196	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
	197	need_mb = 1;
	198	do
	199	:: need_mb == 1 -> skip;
	200	:: need_mb == 0 -> break;
	201	od;
	202	do
	203	:: 1 ->
	204	if
	205	:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
	206	(urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
	207	(urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
	208	skip;
	209	:: else -> break;
	210	fi;
	211	od;
	212	need_mb = 1;
	213	do
	214	:: need_mb == 1 -> skip;
	215	:: need_mb == 0 -> break;
	216	od;
	217
5464000f MD	218	/* Removal statement, e.g., list_del_rcu(). */
	219	removed = 1;
	220
9d950311	221	/* current synchronize_rcu(), first counter flip. */
5464000f MD	222	need_mb = 1;
	223	do
	224	:: need_mb == 1 -> skip;
	225	:: need_mb == 0 -> break;
	226	od;
	227	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
	228	need_mb = 1;
	229	do
	230	:: need_mb == 1 -> skip;
	231	:: need_mb == 0 -> break;
	232	od;
	233	do
	234	:: 1 ->
5464000f MD	235	if
	236	:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
	237	(urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
	238	(urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
	239	skip;
	240	:: else -> break;
9d950311	241	fi;
5464000f MD	242	od;
	243	need_mb = 1;
	244	do
	245	:: need_mb == 1 -> skip;
	246	:: need_mb == 0 -> break;
	247	od;
	248
9d950311	249	/* current synchronize_rcu(), second counter flip. */
5464000f MD	250	need_mb = 1;
	251	do
	252	:: need_mb == 1 -> skip;
	253	:: need_mb == 0 -> break;
	254	od;
	255	urcu_gp_ctr = urcu_gp_ctr + RCU_GP_CTR_BIT;
	256	need_mb = 1;
	257	do
	258	:: need_mb == 1 -> skip;
	259	:: need_mb == 0 -> break;
	260	od;
	261	do
	262	:: 1 ->
5464000f MD	263	if
	264	:: (urcu_active_readers & RCU_GP_CTR_NEST_MASK) != 0 &&
	265	(urcu_active_readers & ~RCU_GP_CTR_NEST_MASK) !=
	266	(urcu_gp_ctr & ~RCU_GP_CTR_NEST_MASK) ->
	267	skip;
	268	:: else -> break;
	269	fi;
	270	od;
	271	need_mb = 1;
	272	do
	273	:: need_mb == 1 -> skip;
	274	:: need_mb == 0 -> break;
	275	od;
	276
	277	/* free-up step, e.g., kfree(). */
	278	free = 1;
545a4f13 PM	279
	280	/*
	281	* Signal updater done, ending any otherwise-infinite loops
	282	* in the reading process.
	283	*/
	284	updater_done = 1;
5464000f MD	285	}
	286
	287	/*
	288	* Initialize the array, spawn a reader and an updater. Because readers
	289	* are independent of each other, only one reader is needed.
	290	*/
	291
	292	init {
	293	atomic {
	294	reader_progress[0] = 0;
	295	reader_progress[1] = 0;
	296	reader_progress[2] = 0;
	297	reader_progress[3] = 0;
	298	run urcu_reader();
	299	run urcu_updater();
	300	}
	301	}