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

/*
 * mem.spin: Promela code to validate memory barriers with OOO memory.
 *
 * 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 Mathieu Desnoyers
 */

/* Promela validation variables. */

/* specific defines "included" here */
/* DEFINES file "included" here */

/* All signal readers have same PID and uses same reader variable */
#ifdef TEST_SIGNAL_ON_WRITE
#define get_pid()	((_pid < 1) -> 0 : 1)
#elif defined(TEST_SIGNAL_ON_READ)
#define get_pid()	((_pid < 2) -> 0 : 1)
#else
#define get_pid()	(_pid)
#endif

#define get_readerid()	(get_pid())

/*
 * Each process have its own data in cache. Caches are randomly updated.
 * smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces
 * both.
 */

typedef per_proc_byte {
	byte val[NR_PROCS];
};

/* Bitfield has a maximum of 8 procs */
typedef per_proc_bit {
	byte bitfield;
};

#define DECLARE_CACHED_VAR(type, x)	\
	type mem_##x;			\
	per_proc_##type cached_##x;	\
	per_proc_bit cache_dirty_##x;

#define INIT_CACHED_VAR(x, v, j)	\
	mem_##x = v;			\
	cache_dirty_##x.bitfield = 0;	\
	j = 0;				\
	do				\
	:: j < NR_PROCS ->		\
		cached_##x.val[j] = v;	\
		j++			\
	:: j >= NR_PROCS -> break	\
	od;

#define IS_CACHE_DIRTY(x, id)	(cache_dirty_##x.bitfield & (1 << id))

#define READ_CACHED_VAR(x)	(cached_##x.val[get_pid()])

#define WRITE_CACHED_VAR(x, v)				\
	atomic {					\
		cached_##x.val[get_pid()] = v;		\
		cache_dirty_##x.bitfield =		\
			cache_dirty_##x.bitfield | (1 << get_pid());	\
	}

#define CACHE_WRITE_TO_MEM(x, id)			\
	if						\
	:: IS_CACHE_DIRTY(x, id) ->			\
		mem_##x = cached_##x.val[id];		\
		cache_dirty_##x.bitfield =		\
			cache_dirty_##x.bitfield & (~(1 << id));	\
	:: else ->					\
		skip					\
	fi;

#define CACHE_READ_FROM_MEM(x, id)	\
	if				\
	:: !IS_CACHE_DIRTY(x, id) ->	\
		cached_##x.val[id] = mem_##x;\
	:: else ->			\
		skip			\
	fi;

/*
 * May update other caches if cache is dirty, or not.
 */
#define RANDOM_CACHE_WRITE_TO_MEM(x, id)\
	if				\
	:: 1 -> CACHE_WRITE_TO_MEM(x, id);	\
	:: 1 -> skip			\
	fi;

#define RANDOM_CACHE_READ_FROM_MEM(x, id)\
	if				\
	:: 1 -> CACHE_READ_FROM_MEM(x, id);	\
	:: 1 -> skip			\
	fi;

/*
 * Remote barriers tests the scheme where a signal (or IPI) is sent to all
 * reader threads to promote their compiler barrier to a smp_mb().
 */
#ifdef REMOTE_BARRIERS

inline smp_rmb_pid(i, j)
{
	atomic {
		CACHE_READ_FROM_MEM(urcu_gp_ctr, i);
		j = 0;
		do
		:: j < NR_READERS ->
			CACHE_READ_FROM_MEM(urcu_active_readers[j], i);
			j++
		:: j >= NR_READERS -> break
		od;
		CACHE_READ_FROM_MEM(generation_ptr, i);
	}
}

inline smp_wmb_pid(i, j)
{
	atomic {
		CACHE_WRITE_TO_MEM(urcu_gp_ctr, i);
		j = 0;
		do
		:: j < NR_READERS ->
			CACHE_WRITE_TO_MEM(urcu_active_readers[j], i);
			j++
		:: j >= NR_READERS -> break
		od;
		CACHE_WRITE_TO_MEM(generation_ptr, i);
	}
}

inline smp_mb_pid(i, j)
{
	atomic {
#ifndef NO_WMB
		smp_wmb_pid(i, j);
#endif
#ifndef NO_RMB
		smp_rmb_pid(i, j);
#endif
#ifdef NO_WMB
#ifdef NO_RMB
		ooo_mem(j);
#endif
#endif
	}
}

/*
 * Readers do a simple barrier(), writers are doing a smp_mb() _and_ sending a
 * signal or IPI to have all readers execute a smp_mb.
 * We are not modeling the whole rendez-vous between readers and writers here,
 * we just let the writer update each reader's caches remotely.
 */
inline smp_mb(i, j)
{
	if
	:: get_pid() >= NR_READERS ->
		smp_mb_pid(get_pid(), j);
		i = 0;
		do
		:: i < NR_READERS ->
			smp_mb_pid(i, j);
			i++;
		:: i >= NR_READERS -> break
		od;
		smp_mb_pid(get_pid(), j);
	:: else -> skip;
	fi;
}

#else

inline smp_rmb(i, j)
{
	atomic {
		CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
		i = 0;
		do
		:: i < NR_READERS ->
			CACHE_READ_FROM_MEM(urcu_active_readers[i], get_pid());
			i++
		:: i >= NR_READERS -> break
		od;
		CACHE_READ_FROM_MEM(generation_ptr, get_pid());
	}
}

inline smp_wmb(i, j)
{
	atomic {
		CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
		i = 0;
		do
		:: i < NR_READERS ->
			CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid());
			i++
		:: i >= NR_READERS -> break
		od;
		CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
	}
}

inline smp_mb(i, j)
{
	atomic {
#ifndef NO_WMB
		smp_wmb(i, j);
#endif
#ifndef NO_RMB
		smp_rmb(i, j);
#endif
#ifdef NO_WMB
#ifdef NO_RMB
		ooo_mem(i);
#endif
#endif
	}
}

#endif

/* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */
DECLARE_CACHED_VAR(byte, urcu_gp_ctr);
/* Note ! currently only two readers */
DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
/* pointer generation */
DECLARE_CACHED_VAR(byte, generation_ptr);

byte last_free_gen = 0;
bit free_done = 0;
byte read_generation[NR_READERS];
bit data_access[NR_READERS];

bit write_lock = 0;

bit init_done = 0;

bit sighand_exec = 0;

inline wait_init_done()
{
	do
	:: init_done == 0 -> skip;
	:: else -> break;
	od;
}

#ifdef TEST_SIGNAL

inline wait_for_sighand_exec()
{
	sighand_exec = 0;
	do
	:: sighand_exec == 0 -> skip;
	:: else -> break;
	od;
}

#ifdef TOO_BIG_STATE_SPACE
inline wait_for_sighand_exec()
{
	sighand_exec = 0;
	do
	:: sighand_exec == 0 -> skip;
	:: else ->
		if
		:: 1 -> break;
		:: 1 -> sighand_exec = 0;
			skip;
		fi;
	od;
}
#endif

#else

inline wait_for_sighand_exec()
{
	skip;
}

#endif

#ifdef TEST_SIGNAL_ON_WRITE
/* Block on signal handler execution */
inline dispatch_sighand_write_exec()
{
	sighand_exec = 1;
	do
	:: sighand_exec == 1 ->
		skip;
	:: else ->
		break;
	od;
}

#else

inline dispatch_sighand_write_exec()
{
	skip;
}

#endif

#ifdef TEST_SIGNAL_ON_READ
/* Block on signal handler execution */
inline dispatch_sighand_read_exec()
{
	sighand_exec = 1;
	do
	:: sighand_exec == 1 ->
		skip;
	:: else ->
		break;
	od;
}

#else

inline dispatch_sighand_read_exec()
{
	skip;
}

#endif


inline ooo_mem(i)
{
	atomic {
		RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
		i = 0;
		do
		:: i < NR_READERS ->
			RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i],
				get_pid());
			i++
		:: i >= NR_READERS -> break
		od;
		RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
		RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
		i = 0;
		do
		:: i < NR_READERS ->
			RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i],
				get_pid());
			i++
		:: i >= NR_READERS -> break
		od;
		RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid());
	}
}

inline wait_for_reader(tmp, tmp2, i, j)
{
	do
	:: 1 ->
		tmp2 = READ_CACHED_VAR(urcu_active_readers[tmp]);
		ooo_mem(i);
		dispatch_sighand_write_exec();
		if
		:: (tmp2 & RCU_GP_CTR_NEST_MASK)
			&& ((tmp2 ^ READ_CACHED_VAR(urcu_gp_ctr))
				& RCU_GP_CTR_BIT) ->
#ifndef GEN_ERROR_WRITER_PROGRESS
			smp_mb(i, j);
#else
			ooo_mem(i);
#endif
			dispatch_sighand_write_exec();
		:: else	->
			break;
		fi;
	od;
}

inline wait_for_quiescent_state(tmp, tmp2, i, j)
{
	tmp = 0;
	do
	:: tmp < NR_READERS ->
		wait_for_reader(tmp, tmp2, i, j);
		if
		:: (NR_READERS > 1) && (tmp < NR_READERS - 1)
			-> ooo_mem(i);
			   dispatch_sighand_write_exec();
		:: else
			-> skip;
		fi;
		tmp++
	:: tmp >= NR_READERS -> break
	od;
}

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

inline urcu_one_read(i, j, nest_i, tmp, tmp2)
{
	nest_i = 0;
	do
	:: nest_i < READER_NEST_LEVEL ->
		ooo_mem(i);
		dispatch_sighand_read_exec();
		tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
		ooo_mem(i);
		dispatch_sighand_read_exec();
		if
		:: (!(tmp & RCU_GP_CTR_NEST_MASK))
			->
			tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
			ooo_mem(i);
			dispatch_sighand_read_exec();
			WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
					 tmp2);
		:: else	->
			WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
					 tmp + 1);
		fi;
		smp_mb(i, j);
		dispatch_sighand_read_exec();
		nest_i++;
	:: nest_i >= READER_NEST_LEVEL -> break;
	od;

	read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
	data_access[get_readerid()] = 1;
	data_access[get_readerid()] = 0;

	nest_i = 0;
	do
	:: nest_i < READER_NEST_LEVEL ->
		smp_mb(i, j);
		dispatch_sighand_read_exec();
		tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
		ooo_mem(i);
		dispatch_sighand_read_exec();
		WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
		nest_i++;
	:: nest_i >= READER_NEST_LEVEL -> break;
	od;
	//ooo_mem(i);
	//dispatch_sighand_read_exec();
	//smp_mc(i);	/* added */
}

active proctype urcu_reader()
{
	byte i, j, nest_i;
	byte tmp, tmp2;

	wait_init_done();

	assert(get_pid() < NR_PROCS);

end_reader:
	do
	:: 1 ->
		/*
		 * We do not test reader's progress here, because we are mainly
		 * interested in writer's progress. The reader never blocks
		 * anyway. We have to test for reader/writer's progress
		 * separately, otherwise we could think the writer is doing
		 * progress when it's blocked by an always progressing reader.
		 */
#ifdef READER_PROGRESS
		/* Only test progress of one random reader. They are all the
		 * same. */
		if
		:: get_readerid() == 0 ->
progress_reader:
			skip;
		fi;
#endif
		urcu_one_read(i, j, nest_i, tmp, tmp2);
	od;
}

#ifdef TEST_SIGNAL
/* signal handler reader */

inline urcu_one_read_sig(i, j, nest_i, tmp, tmp2)
{
	nest_i = 0;
	do
	:: nest_i < READER_NEST_LEVEL ->
		ooo_mem(i);
		tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
		ooo_mem(i);
		if
		:: (!(tmp & RCU_GP_CTR_NEST_MASK))
			->
			tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
			ooo_mem(i);
			WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
					 tmp2);
		:: else	->
			WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
					 tmp + 1);
		fi;
		smp_mb(i, j);
		nest_i++;
	:: nest_i >= READER_NEST_LEVEL -> break;
	od;

	read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
	data_access[get_readerid()] = 1;
	data_access[get_readerid()] = 0;

	nest_i = 0;
	do
	:: nest_i < READER_NEST_LEVEL ->
		smp_mb(i, j);
		tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
		ooo_mem(i);
		WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
		nest_i++;
	:: nest_i >= READER_NEST_LEVEL -> break;
	od;
	//ooo_mem(i);
	//smp_mc(i);	/* added */
}

active proctype urcu_reader_sig()
{
	byte i, j, nest_i;
	byte tmp, tmp2;

	wait_init_done();

	assert(get_pid() < NR_PROCS);

end_reader:
	do
	:: 1 ->
		wait_for_sighand_exec();
		/*
		 * We do not test reader's progress here, because we are mainly
		 * interested in writer's progress. The reader never blocks
		 * anyway. We have to test for reader/writer's progress
		 * separately, otherwise we could think the writer is doing
		 * progress when it's blocked by an always progressing reader.
		 */
#ifdef READER_PROGRESS
		/* Only test progress of one random reader. They are all the
		 * same. */
		if
		:: get_readerid() == 0 ->
progress_reader:
			skip;
		fi;
#endif
		urcu_one_read_sig(i, j, nest_i, tmp, tmp2);
	od;
}

#endif

/* Model the RCU update process. */

active proctype urcu_writer()
{
	byte i, j;
	byte tmp, tmp2;
	byte old_gen;

	wait_init_done();

	assert(get_pid() < NR_PROCS);

	do
	:: (READ_CACHED_VAR(generation_ptr) < 5) ->
#ifdef WRITER_PROGRESS
progress_writer1:
#endif
		ooo_mem(i);
		dispatch_sighand_write_exec();
		atomic {
			old_gen = READ_CACHED_VAR(generation_ptr);
			WRITE_CACHED_VAR(generation_ptr, old_gen + 1);
		}
		ooo_mem(i);
		dispatch_sighand_write_exec();

		do
		:: 1 ->
			atomic {
				if
				:: write_lock == 0 ->
					write_lock = 1;
					break;
				:: else ->
					skip;
				fi;
			}
		od;
		smp_mb(i, j);
		dispatch_sighand_write_exec();
		tmp = READ_CACHED_VAR(urcu_gp_ctr);
		ooo_mem(i);
		dispatch_sighand_write_exec();
		WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
		ooo_mem(i);
		dispatch_sighand_write_exec();
		//smp_mc(i);
		wait_for_quiescent_state(tmp, tmp2, i, j);
		//smp_mc(i);
#ifndef SINGLE_FLIP
		ooo_mem(i);
		dispatch_sighand_write_exec();
		tmp = READ_CACHED_VAR(urcu_gp_ctr);
		ooo_mem(i);
		dispatch_sighand_write_exec();
		WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
		//smp_mc(i);
		ooo_mem(i);
		dispatch_sighand_write_exec();
		wait_for_quiescent_state(tmp, tmp2, i, j);
#endif
		smp_mb(i, j);
		dispatch_sighand_write_exec();
		write_lock = 0;
		/* free-up step, e.g., kfree(). */
		atomic {
			last_free_gen = old_gen;
			free_done = 1;
		}
	:: else -> break;
	od;
	/*
	 * Given the reader loops infinitely, let the writer also busy-loop
	 * with progress here so, with weak fairness, we can test the
	 * writer's progress.
	 */
end_writer:
	do
	:: 1 ->
#ifdef WRITER_PROGRESS
progress_writer2:
#endif
		dispatch_sighand_write_exec();
	od;
}

/* Leave after the readers and writers so the pid count is ok. */
init {
	byte i, j;

	atomic {
		INIT_CACHED_VAR(urcu_gp_ctr, 1, j);
		INIT_CACHED_VAR(generation_ptr, 0, j);

		i = 0;
		do
		:: i < NR_READERS ->
			INIT_CACHED_VAR(urcu_active_readers[i], 0, j);
			read_generation[i] = 1;
			data_access[i] = 0;
			i++;
		:: i >= NR_READERS -> break
		od;
		init_done = 1;
	}
}
Commit	Line	Data
60a1db9d MD	1	/*
	2	* mem.spin: Promela code to validate memory barriers with OOO memory.
	3	*
	4	* This program is free software; you can redistribute it and/or modify
	5	* it under the terms of the GNU General Public License as published by
	6	* the Free Software Foundation; either version 2 of the License, or
	7	* (at your option) any later version.
	8	*
	9	* This program is distributed in the hope that it will be useful,
	10	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	11	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	12	* GNU General Public License for more details.
	13	*
	14	* You should have received a copy of the GNU General Public License
	15	* along with this program; if not, write to the Free Software
	16	* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
	17	*
	18	* Copyright (c) 2009 Mathieu Desnoyers
	19	*/
	20
	21	/* Promela validation variables. */
	22
8bc62ca4 MD	23	/* specific defines "included" here */
	24	/* DEFINES file "included" here */
	25
	26	/* All signal readers have same PID and uses same reader variable */
	27	#ifdef TEST_SIGNAL_ON_WRITE
	28	#define get_pid() ((_pid < 1) -> 0 : 1)
	29	#elif defined(TEST_SIGNAL_ON_READ)
	30	#define get_pid() ((_pid < 2) -> 0 : 1)
	31	#else
60a1db9d	32	#define get_pid() (_pid)
8bc62ca4 MD	33	#endif
	34
	35	#define get_readerid() (get_pid())
60a1db9d MD	36
	37	/*
	38	* Each process have its own data in cache. Caches are randomly updated.
a5b558b0	39	* smp_wmb and smp_rmb forces cache updates (write and read), smp_mb forces
60a1db9d MD	40	* both.
	41	*/
	42
8bc62ca4 MD	43	typedef per_proc_byte {
	44	byte val[NR_PROCS];
	45	};
	46
	47	/* Bitfield has a maximum of 8 procs */
	48	typedef per_proc_bit {
	49	byte bitfield;
	50	};
	51
	52	#define DECLARE_CACHED_VAR(type, x) \
	53	type mem_##x; \
	54	per_proc_##type cached_##x; \
	55	per_proc_bit cache_dirty_##x;
	56
	57	#define INIT_CACHED_VAR(x, v, j) \
	58	mem_##x = v; \
	59	cache_dirty_##x.bitfield = 0; \
	60	j = 0; \
	61	do \
	62	:: j < NR_PROCS -> \
	63	cached_##x.val[j] = v; \
	64	j++ \
	65	:: j >= NR_PROCS -> break \
	66	od;
60a1db9d	67
8bc62ca4	68	#define IS_CACHE_DIRTY(x, id) (cache_dirty_##x.bitfield & (1 << id))
60a1db9d	69
8bc62ca4	70	#define READ_CACHED_VAR(x) (cached_##x.val[get_pid()])
60a1db9d	71
8bc62ca4 MD	72	#define WRITE_CACHED_VAR(x, v) \
	73	atomic { \
	74	cached_##x.val[get_pid()] = v; \
	75	cache_dirty_##x.bitfield = \
	76	cache_dirty_##x.bitfield \| (1 << get_pid()); \
60a1db9d MD	77	}
60a1db9d MD	78
8bc62ca4 MD	79	#define CACHE_WRITE_TO_MEM(x, id) \
	80	if \
	81	:: IS_CACHE_DIRTY(x, id) -> \
	82	mem_##x = cached_##x.val[id]; \
	83	cache_dirty_##x.bitfield = \
	84	cache_dirty_##x.bitfield & (~(1 << id)); \
	85	:: else -> \
	86	skip \
60a1db9d MD	87	fi;
	88
	89	#define CACHE_READ_FROM_MEM(x, id) \
	90	if \
	91	:: !IS_CACHE_DIRTY(x, id) -> \
8bc62ca4	92	cached_##x.val[id] = mem_##x;\
60a1db9d MD	93	:: else -> \
	94	skip \
	95	fi;
	96
	97	/*
	98	* May update other caches if cache is dirty, or not.
	99	*/
	100	#define RANDOM_CACHE_WRITE_TO_MEM(x, id)\
	101	if \
	102	:: 1 -> CACHE_WRITE_TO_MEM(x, id); \
	103	:: 1 -> skip \
	104	fi;
	105
	106	#define RANDOM_CACHE_READ_FROM_MEM(x, id)\
	107	if \
	108	:: 1 -> CACHE_READ_FROM_MEM(x, id); \
	109	:: 1 -> skip \
	110	fi;
	111
cc76fd1d MD	112	/*
	113	* Remote barriers tests the scheme where a signal (or IPI) is sent to all
	114	* reader threads to promote their compiler barrier to a smp_mb().
	115	*/
	116	#ifdef REMOTE_BARRIERS
	117
8bc62ca4	118	inline smp_rmb_pid(i, j)
cc76fd1d MD	119	{
	120	atomic {
	121	CACHE_READ_FROM_MEM(urcu_gp_ctr, i);
8bc62ca4 MD	122	j = 0;
	123	do
	124	:: j < NR_READERS ->
	125	CACHE_READ_FROM_MEM(urcu_active_readers[j], i);
	126	j++
	127	:: j >= NR_READERS -> break
	128	od;
cc76fd1d MD	129	CACHE_READ_FROM_MEM(generation_ptr, i);
	130	}
	131	}
	132
8bc62ca4	133	inline smp_wmb_pid(i, j)
cc76fd1d MD	134	{
	135	atomic {
	136	CACHE_WRITE_TO_MEM(urcu_gp_ctr, i);
8bc62ca4 MD	137	j = 0;
	138	do
	139	:: j < NR_READERS ->
	140	CACHE_WRITE_TO_MEM(urcu_active_readers[j], i);
	141	j++
	142	:: j >= NR_READERS -> break
	143	od;
cc76fd1d MD	144	CACHE_WRITE_TO_MEM(generation_ptr, i);
	145	}
	146	}
	147
8bc62ca4	148	inline smp_mb_pid(i, j)
cc76fd1d MD	149	{
	150	atomic {
	151	#ifndef NO_WMB
8bc62ca4	152	smp_wmb_pid(i, j);
cc76fd1d MD	153	#endif
cc76fd1d MD	154	#ifndef NO_RMB
8bc62ca4	155	smp_rmb_pid(i, j);
cc76fd1d	156	#endif
a5b558b0 MD	157	#ifdef NO_WMB
a5b558b0 MD	158	#ifdef NO_RMB
8bc62ca4	159	ooo_mem(j);
a5b558b0 MD	160	#endif
a5b558b0 MD	161	#endif
cc76fd1d MD	162	}
	163	}
	164
	165	/*
	166	* Readers do a simple barrier(), writers are doing a smp_mb() _and_ sending a
	167	* signal or IPI to have all readers execute a smp_mb.
	168	* We are not modeling the whole rendez-vous between readers and writers here,
	169	* we just let the writer update each reader's caches remotely.
	170	*/
8bc62ca4	171	inline smp_mb(i, j)
cc76fd1d MD	172	{
	173	if
	174	:: get_pid() >= NR_READERS ->
8bc62ca4	175	smp_mb_pid(get_pid(), j);
cc76fd1d MD	176	i = 0;
	177	do
	178	:: i < NR_READERS ->
8bc62ca4	179	smp_mb_pid(i, j);
cc76fd1d MD	180	i++;
	181	:: i >= NR_READERS -> break
	182	od;
8bc62ca4	183	smp_mb_pid(get_pid(), j);
cc76fd1d MD	184	:: else -> skip;
	185	fi;
	186	}
	187
	188	#else
	189
8bc62ca4	190	inline smp_rmb(i, j)
60a1db9d MD	191	{
	192	atomic {
	193	CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
8bc62ca4 MD	194	i = 0;
	195	do
	196	:: i < NR_READERS ->
	197	CACHE_READ_FROM_MEM(urcu_active_readers[i], get_pid());
	198	i++
	199	:: i >= NR_READERS -> break
	200	od;
60a1db9d MD	201	CACHE_READ_FROM_MEM(generation_ptr, get_pid());
	202	}
	203	}
	204
8bc62ca4	205	inline smp_wmb(i, j)
60a1db9d MD	206	{
	207	atomic {
	208	CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
8bc62ca4 MD	209	i = 0;
	210	do
	211	:: i < NR_READERS ->
	212	CACHE_WRITE_TO_MEM(urcu_active_readers[i], get_pid());
	213	i++
	214	:: i >= NR_READERS -> break
	215	od;
60a1db9d MD	216	CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
	217	}
	218	}
	219
8bc62ca4	220	inline smp_mb(i, j)
60a1db9d MD	221	{
	222	atomic {
	223	#ifndef NO_WMB
8bc62ca4	224	smp_wmb(i, j);
60a1db9d MD	225	#endif
60a1db9d MD	226	#ifndef NO_RMB
8bc62ca4	227	smp_rmb(i, j);
60a1db9d	228	#endif
a5b558b0 MD	229	#ifdef NO_WMB
	230	#ifdef NO_RMB
	231	ooo_mem(i);
	232	#endif
	233	#endif
60a1db9d MD	234	}
	235	}
	236
cc76fd1d MD	237	#endif
cc76fd1d MD	238
8bc62ca4 MD	239	/* Keep in sync manually with smp_rmb, wmp_wmb, ooo_mem and init() */
	240	DECLARE_CACHED_VAR(byte, urcu_gp_ctr);
	241	/* Note ! currently only two readers */
	242	DECLARE_CACHED_VAR(byte, urcu_active_readers[NR_READERS]);
60a1db9d	243	/* pointer generation */
8bc62ca4	244	DECLARE_CACHED_VAR(byte, generation_ptr);
60a1db9d MD	245
	246	byte last_free_gen = 0;
	247	bit free_done = 0;
8bc62ca4 MD	248	byte read_generation[NR_READERS];
8bc62ca4 MD	249	bit data_access[NR_READERS];
60a1db9d	250
2ba2a48d MD	251	bit write_lock = 0;
2ba2a48d MD	252
8bc62ca4 MD	253	bit init_done = 0;
	254
	255	bit sighand_exec = 0;
	256
	257	inline wait_init_done()
	258	{
	259	do
	260	:: init_done == 0 -> skip;
	261	:: else -> break;
	262	od;
	263	}
	264
	265	#ifdef TEST_SIGNAL
	266
86ea30a2 MD	267	inline wait_for_sighand_exec()
	268	{
	269	sighand_exec = 0;
	270	do
	271	:: sighand_exec == 0 -> skip;
	272	:: else -> break;
	273	od;
	274	}
	275
	276	#ifdef TOO_BIG_STATE_SPACE
8bc62ca4 MD	277	inline wait_for_sighand_exec()
	278	{
	279	sighand_exec = 0;
	280	do
	281	:: sighand_exec == 0 -> skip;
	282	:: else ->
	283	if
	284	:: 1 -> break;
	285	:: 1 -> sighand_exec = 0;
	286	skip;
	287	fi;
	288	od;
	289	}
86ea30a2	290	#endif
8bc62ca4 MD	291
	292	#else
	293
	294	inline wait_for_sighand_exec()
	295	{
	296	skip;
	297	}
	298
	299	#endif
	300
	301	#ifdef TEST_SIGNAL_ON_WRITE
	302	/* Block on signal handler execution */
	303	inline dispatch_sighand_write_exec()
	304	{
	305	sighand_exec = 1;
	306	do
	307	:: sighand_exec == 1 ->
	308	skip;
	309	:: else ->
	310	break;
	311	od;
	312	}
	313
	314	#else
	315
	316	inline dispatch_sighand_write_exec()
	317	{
	318	skip;
	319	}
	320
	321	#endif
	322
	323	#ifdef TEST_SIGNAL_ON_READ
	324	/* Block on signal handler execution */
	325	inline dispatch_sighand_read_exec()
	326	{
	327	sighand_exec = 1;
	328	do
	329	:: sighand_exec == 1 ->
	330	skip;
	331	:: else ->
	332	break;
	333	od;
	334	}
	335
	336	#else
	337
	338	inline dispatch_sighand_read_exec()
	339	{
	340	skip;
	341	}
	342
	343	#endif
	344
	345
60a1db9d MD	346	inline ooo_mem(i)
	347	{
	348	atomic {
	349	RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid());
8bc62ca4 MD	350	i = 0;
	351	do
	352	:: i < NR_READERS ->
	353	RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers[i],
	354	get_pid());
	355	i++
	356	:: i >= NR_READERS -> break
	357	od;
60a1db9d MD	358	RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid());
60a1db9d MD	359	RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid());
8bc62ca4 MD	360	i = 0;
	361	do
	362	:: i < NR_READERS ->
	363	RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers[i],
	364	get_pid());
	365	i++
	366	:: i >= NR_READERS -> break
	367	od;
60a1db9d MD	368	RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid());
	369	}
	370	}
	371
8bc62ca4	372	inline wait_for_reader(tmp, tmp2, i, j)
60a1db9d	373	{
60a1db9d	374	do
89674313	375	:: 1 ->
8bc62ca4	376	tmp2 = READ_CACHED_VAR(urcu_active_readers[tmp]);
a570e118	377	ooo_mem(i);
8bc62ca4	378	dispatch_sighand_write_exec();
89674313	379	if
8bc62ca4 MD	380	:: (tmp2 & RCU_GP_CTR_NEST_MASK)
8bc62ca4 MD	381	&& ((tmp2 ^ READ_CACHED_VAR(urcu_gp_ctr))
89674313 MD	382	& RCU_GP_CTR_BIT) ->
89674313 MD	383	#ifndef GEN_ERROR_WRITER_PROGRESS
8bc62ca4	384	smp_mb(i, j);
89674313	385	#else
a5b558b0	386	ooo_mem(i);
89674313	387	#endif
8bc62ca4	388	dispatch_sighand_write_exec();
89674313	389	:: else ->
60a1db9d	390	break;
89674313	391	fi;
60a1db9d MD	392	od;
	393	}
	394
8bc62ca4	395	inline wait_for_quiescent_state(tmp, tmp2, i, j)
60a1db9d	396	{
8bc62ca4	397	tmp = 0;
60a1db9d	398	do
8bc62ca4 MD	399	:: tmp < NR_READERS ->
8bc62ca4 MD	400	wait_for_reader(tmp, tmp2, i, j);
a5b558b0	401	if
8bc62ca4 MD	402	:: (NR_READERS > 1) && (tmp < NR_READERS - 1)
	403	-> ooo_mem(i);
	404	dispatch_sighand_write_exec();
a5b558b0 MD	405	:: else
	406	-> skip;
	407	fi;
8bc62ca4 MD	408	tmp++
8bc62ca4 MD	409	:: tmp >= NR_READERS -> break
60a1db9d MD	410	od;
	411	}
	412
	413	/* Model the RCU read-side critical section. */
	414
8bc62ca4	415	inline urcu_one_read(i, j, nest_i, tmp, tmp2)
6ae334b0	416	{
	417	nest_i = 0;
	418	do
	419	:: nest_i < READER_NEST_LEVEL ->
	420	ooo_mem(i);
8bc62ca4 MD	421	dispatch_sighand_read_exec();
8bc62ca4 MD	422	tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
6ae334b0	423	ooo_mem(i);
8bc62ca4	424	dispatch_sighand_read_exec();
6ae334b0	425	if
	426	:: (!(tmp & RCU_GP_CTR_NEST_MASK))
	427	->
	428	tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
	429	ooo_mem(i);
8bc62ca4 MD	430	dispatch_sighand_read_exec();
	431	WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
	432	tmp2);
6ae334b0	433	:: else ->
8bc62ca4	434	WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
6ae334b0	435	tmp + 1);
6ae334b0	436	fi;
8bc62ca4 MD	437	smp_mb(i, j);
8bc62ca4 MD	438	dispatch_sighand_read_exec();
6ae334b0	439	nest_i++;
	440	:: nest_i >= READER_NEST_LEVEL -> break;
	441	od;
	442
8bc62ca4 MD	443	read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
	444	data_access[get_readerid()] = 1;
	445	data_access[get_readerid()] = 0;
6ae334b0	446
	447	nest_i = 0;
	448	do
	449	:: nest_i < READER_NEST_LEVEL ->
8bc62ca4 MD	450	smp_mb(i, j);
	451	dispatch_sighand_read_exec();
	452	tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
6ae334b0	453	ooo_mem(i);
8bc62ca4 MD	454	dispatch_sighand_read_exec();
8bc62ca4 MD	455	WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
6ae334b0	456	nest_i++;
	457	:: nest_i >= READER_NEST_LEVEL -> break;
	458	od;
8bc62ca4 MD	459	//ooo_mem(i);
8bc62ca4 MD	460	//dispatch_sighand_read_exec();
6ae334b0	461	//smp_mc(i); /* added */
	462	}
	463
8bc62ca4	464	active proctype urcu_reader()
60a1db9d	465	{
8bc62ca4	466	byte i, j, nest_i;
60a1db9d MD	467	byte tmp, tmp2;
60a1db9d MD	468
8bc62ca4 MD	469	wait_init_done();
8bc62ca4 MD	470
60a1db9d MD	471	assert(get_pid() < NR_PROCS);
60a1db9d MD	472
89674313 MD	473	end_reader:
	474	do
	475	:: 1 ->
	476	/*
	477	* We do not test reader's progress here, because we are mainly
	478	* interested in writer's progress. The reader never blocks
	479	* anyway. We have to test for reader/writer's progress
	480	* separately, otherwise we could think the writer is doing
	481	* progress when it's blocked by an always progressing reader.
	482	*/
	483	#ifdef READER_PROGRESS
8bc62ca4 MD	484	/* Only test progress of one random reader. They are all the
	485	* same. */
	486	if
	487	:: get_readerid() == 0 ->
89674313	488	progress_reader:
8bc62ca4 MD	489	skip;
8bc62ca4 MD	490	fi;
89674313	491	#endif
8bc62ca4 MD	492	urcu_one_read(i, j, nest_i, tmp, tmp2);
	493	od;
	494	}
	495
	496	#ifdef TEST_SIGNAL
	497	/* signal handler reader */
	498
	499	inline urcu_one_read_sig(i, j, nest_i, tmp, tmp2)
	500	{
	501	nest_i = 0;
	502	do
	503	:: nest_i < READER_NEST_LEVEL ->
	504	ooo_mem(i);
	505	tmp = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
	506	ooo_mem(i);
	507	if
	508	:: (!(tmp & RCU_GP_CTR_NEST_MASK))
	509	->
	510	tmp2 = READ_CACHED_VAR(urcu_gp_ctr);
	511	ooo_mem(i);
	512	WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
	513	tmp2);
	514	:: else ->
	515	WRITE_CACHED_VAR(urcu_active_readers[get_readerid()],
	516	tmp + 1);
	517	fi;
	518	smp_mb(i, j);
	519	nest_i++;
	520	:: nest_i >= READER_NEST_LEVEL -> break;
	521	od;
	522
	523	read_generation[get_readerid()] = READ_CACHED_VAR(generation_ptr);
	524	data_access[get_readerid()] = 1;
	525	data_access[get_readerid()] = 0;
	526
	527	nest_i = 0;
	528	do
	529	:: nest_i < READER_NEST_LEVEL ->
	530	smp_mb(i, j);
	531	tmp2 = READ_CACHED_VAR(urcu_active_readers[get_readerid()]);
	532	ooo_mem(i);
	533	WRITE_CACHED_VAR(urcu_active_readers[get_readerid()], tmp2 - 1);
	534	nest_i++;
	535	:: nest_i >= READER_NEST_LEVEL -> break;
89674313	536	od;
8bc62ca4 MD	537	//ooo_mem(i);
8bc62ca4 MD	538	//smp_mc(i); /* added */
60a1db9d MD	539	}
60a1db9d MD	540
8bc62ca4 MD	541	active proctype urcu_reader_sig()
	542	{
	543	byte i, j, nest_i;
	544	byte tmp, tmp2;
	545
	546	wait_init_done();
	547
	548	assert(get_pid() < NR_PROCS);
	549
	550	end_reader:
	551	do
	552	:: 1 ->
	553	wait_for_sighand_exec();
	554	/*
	555	* We do not test reader's progress here, because we are mainly
	556	* interested in writer's progress. The reader never blocks
	557	* anyway. We have to test for reader/writer's progress
	558	* separately, otherwise we could think the writer is doing
	559	* progress when it's blocked by an always progressing reader.
	560	*/
	561	#ifdef READER_PROGRESS
	562	/* Only test progress of one random reader. They are all the
	563	* same. */
	564	if
	565	:: get_readerid() == 0 ->
	566	progress_reader:
	567	skip;
	568	fi;
	569	#endif
	570	urcu_one_read_sig(i, j, nest_i, tmp, tmp2);
	571	od;
	572	}
	573
	574	#endif
	575
60a1db9d MD	576	/* Model the RCU update process. */
60a1db9d MD	577
8bc62ca4	578	active proctype urcu_writer()
60a1db9d MD	579	{
60a1db9d MD	580	byte i, j;
8bc62ca4	581	byte tmp, tmp2;
60a1db9d MD	582	byte old_gen;
60a1db9d MD	583
8bc62ca4 MD	584	wait_init_done();
8bc62ca4 MD	585
60a1db9d MD	586	assert(get_pid() < NR_PROCS);
60a1db9d MD	587
2ba2a48d	588	do
89674313 MD	589	:: (READ_CACHED_VAR(generation_ptr) < 5) ->
	590	#ifdef WRITER_PROGRESS
	591	progress_writer1:
	592	#endif
	593	ooo_mem(i);
8bc62ca4	594	dispatch_sighand_write_exec();
710b09b7	595	atomic {
89674313 MD	596	old_gen = READ_CACHED_VAR(generation_ptr);
89674313 MD	597	WRITE_CACHED_VAR(generation_ptr, old_gen + 1);
710b09b7	598	}
89674313	599	ooo_mem(i);
8bc62ca4	600	dispatch_sighand_write_exec();
89674313 MD	601
	602	do
	603	:: 1 ->
	604	atomic {
	605	if
	606	:: write_lock == 0 ->
	607	write_lock = 1;
	608	break;
	609	:: else ->
	610	skip;
	611	fi;
	612	}
	613	od;
8bc62ca4 MD	614	smp_mb(i, j);
8bc62ca4 MD	615	dispatch_sighand_write_exec();
89674313 MD	616	tmp = READ_CACHED_VAR(urcu_gp_ctr);
89674313 MD	617	ooo_mem(i);
8bc62ca4	618	dispatch_sighand_write_exec();
89674313 MD	619	WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
89674313 MD	620	ooo_mem(i);
8bc62ca4	621	dispatch_sighand_write_exec();
89674313	622	//smp_mc(i);
8bc62ca4	623	wait_for_quiescent_state(tmp, tmp2, i, j);
89674313	624	//smp_mc(i);
d4e437ba	625	#ifndef SINGLE_FLIP
89674313	626	ooo_mem(i);
8bc62ca4	627	dispatch_sighand_write_exec();
89674313 MD	628	tmp = READ_CACHED_VAR(urcu_gp_ctr);
89674313 MD	629	ooo_mem(i);
8bc62ca4	630	dispatch_sighand_write_exec();
89674313 MD	631	WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT);
	632	//smp_mc(i);
	633	ooo_mem(i);
8bc62ca4 MD	634	dispatch_sighand_write_exec();
8bc62ca4 MD	635	wait_for_quiescent_state(tmp, tmp2, i, j);
d4e437ba	636	#endif
8bc62ca4 MD	637	smp_mb(i, j);
8bc62ca4 MD	638	dispatch_sighand_write_exec();
89674313 MD	639	write_lock = 0;
	640	/* free-up step, e.g., kfree(). */
	641	atomic {
	642	last_free_gen = old_gen;
	643	free_done = 1;
	644	}
	645	:: else -> break;
2ba2a48d	646	od;
89674313 MD	647	/*
	648	* Given the reader loops infinitely, let the writer also busy-loop
	649	* with progress here so, with weak fairness, we can test the
	650	* writer's progress.
	651	*/
	652	end_writer:
	653	do
	654	:: 1 ->
	655	#ifdef WRITER_PROGRESS
	656	progress_writer2:
2ba2a48d	657	#endif
8bc62ca4	658	dispatch_sighand_write_exec();
89674313	659	od;
60a1db9d	660	}
8bc62ca4 MD	661
	662	/* Leave after the readers and writers so the pid count is ok. */
	663	init {
	664	byte i, j;
	665
	666	atomic {
	667	INIT_CACHED_VAR(urcu_gp_ctr, 1, j);
	668	INIT_CACHED_VAR(generation_ptr, 0, j);
	669
	670	i = 0;
	671	do
	672	:: i < NR_READERS ->
	673	INIT_CACHED_VAR(urcu_active_readers[i], 0, j);
	674	read_generation[i] = 1;
	675	data_access[i] = 0;
	676	i++;
	677	:: i >= NR_READERS -> break
	678	od;
	679	init_done = 1;
	680	}
	681	}