[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 NR_READERS 1	/* the writer is also a signal reader */
#define NR_WRITERS 1

#define NR_PROCS 1

#define get_pid()	(0)

#elif defined(TEST_SIGNAL_ON_READ)

#define get_pid()	((_pid < 2) -> 0 : 1)

#define NR_READERS 1
#define NR_WRITERS 1

#define NR_PROCS 2

#else

#define get_pid()	(_pid)

#define NR_READERS 1
#define NR_WRITERS 1

#define NR_PROCS 2

#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_writer(i, j)
{
	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);
}

inline smp_mb_reader(i, j)
{
	skip;
}

#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
	}
}

inline smp_mb_writer(i, j)
{
	smp_mb(i, j);
}

inline smp_mb_reader(i, j)
{
	smp_mb(i, j);
}

#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_writer(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. */

#ifndef TEST_SIGNAL_ON_WRITE

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_reader(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_reader(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
progress_reader:
#endif
		urcu_one_read(i, j, nest_i, tmp, tmp2);
	od;
}

#endif //!TEST_SIGNAL_ON_WRITE

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