[userspace-rcu.git] / ticketlock-testwait / lock_progress.spin.input

#define refcount_gt_one (refcount > 1)
/*
 * 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
 */

/* 16 CPUs max (byte has 8 bits, divided in two) */

#ifndef CONFIG_BITS_PER_BYTE
#define BITS_PER_BYTE		8
#else
// test progress failure with shorter byte size. Will fail with 5 proc.
#define BITS_PER_BYTE		CONFIG_BITS_PER_BYTE
#endif

#define HBPB			(BITS_PER_BYTE / 2)	/* 4 */
#define HMASK			((1 << HBPB) - 1)	/* 0x0F */

/* for byte type */
#define LOW_HALF(val)		((val) & HMASK)
#define LOW_HALF_INC		1

#define HIGH_HALF(val)		((val) & (HMASK << HBPB))
#define HIGH_HALF_INC		(1 << HBPB)

byte lock = 0;
byte refcount = 0;

#define need_pause()	(_pid == 2)

/*
 * Test weak fairness by either not pausing or cycling for any number of
 * steps, or forever.
 * Models a slow thread. Should be added between each atomic steps.
 * To test for wait-freedom (no starvation of a specific thread), add do_pause
 * in threads other than the one we are checking for progress (and which
 * contains the progress label).
 * To test for lock-freedom (system-wide progress), add to all threads except
 * one. All threads contain progress labels.
 */
inline do_pause()
{
	if
	:: need_pause() ->
		if
		:: 1 ->
			do
			:: 1 ->
				skip;
			od;
		:: 1 -> skip;
		fi;
	:: else ->
		skip;
	fi;
}

inline spin_lock(lock, ticket)
{
	atomic {
		ticket = HIGH_HALF(lock) >> HBPB;
		lock = lock + HIGH_HALF_INC;	/* overflow expected */
	}

	do
	:: 1 ->
		if
		:: (LOW_HALF(lock) == ticket) ->
			break;
		:: else ->
			skip;
		fi;
	od;
}

inline spin_unlock(lock)
{
	lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC);
}

proctype proc_A()
{
	byte ticket;

	do
	:: 1 ->
progress_A:
		spin_lock(lock, ticket);
		refcount = refcount + 1;
		refcount = refcount - 1;
		spin_unlock(lock);
	od;
}

proctype proc_B()
{
	byte ticket;

	do
	:: 1 ->
		do_pause();
		spin_lock(lock, ticket);
		refcount = refcount + 1;
		do_pause();
		refcount = refcount - 1;
		spin_unlock(lock);
	od;
}

init
{
	run proc_A();
	run proc_B();
	run proc_B();
	run proc_B();
	run proc_B();
}
Commit	Line	Data
5c020b8d MD	1	#define refcount_gt_one (refcount > 1)
	2	/*
	3	* This program is free software; you can redistribute it and/or modify
	4	* it under the terms of the GNU General Public License as published by
	5	* the Free Software Foundation; either version 2 of the License, or
	6	* (at your option) any later version.
	7	*
	8	* This program is distributed in the hope that it will be useful,
	9	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	10	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	11	* GNU General Public License for more details.
	12	*
	13	* You should have received a copy of the GNU General Public License
	14	* along with this program; if not, write to the Free Software
	15	* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
	16	*
	17	* Copyright (c) 2009 Mathieu Desnoyers
	18	*/
	19
	20	/* 16 CPUs max (byte has 8 bits, divided in two) */
	21
	22	#ifndef CONFIG_BITS_PER_BYTE
	23	#define BITS_PER_BYTE 8
	24	#else
	25	// test progress failure with shorter byte size. Will fail with 5 proc.
	26	#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE
	27	#endif
	28
	29	#define HBPB (BITS_PER_BYTE / 2) /* 4 */
	30	#define HMASK ((1 << HBPB) - 1) /* 0x0F */
	31
	32	/* for byte type */
	33	#define LOW_HALF(val) ((val) & HMASK)
	34	#define LOW_HALF_INC 1
	35
	36	#define HIGH_HALF(val) ((val) & (HMASK << HBPB))
	37	#define HIGH_HALF_INC (1 << HBPB)
	38
	39	byte lock = 0;
	40	byte refcount = 0;
	41
	42	#define need_pause() (_pid == 2)
	43
	44	/*
	45	* Test weak fairness by either not pausing or cycling for any number of
	46	* steps, or forever.
	47	* Models a slow thread. Should be added between each atomic steps.
	48	* To test for wait-freedom (no starvation of a specific thread), add do_pause
	49	* in threads other than the one we are checking for progress (and which
	50	* contains the progress label).
	51	* To test for lock-freedom (system-wide progress), add to all threads except
	52	* one. All threads contain progress labels.
	53	*/
	54	inline do_pause()
	55	{
	56	if
	57	:: need_pause() ->
	58	if
	59	:: 1 ->
	60	do
	61	:: 1 ->
	62	skip;
	63	od;
	64	:: 1 -> skip;
65	fi;
66	:: else ->
67	skip;
68	fi;
69	}
70
71	inline spin_lock(lock, ticket)
72	{
73	atomic {
74	ticket = HIGH_HALF(lock) >> HBPB;
75	lock = lock + HIGH_HALF_INC; /* overflow expected */
76	}
77
78	do
79	:: 1 ->
80	if
81	:: (LOW_HALF(lock) == ticket) ->
82	break;
83	:: else ->
84	skip;
85	fi;
86	od;
87	}
88
89	inline spin_unlock(lock)
90	{
91	lock = HIGH_HALF(lock) \| LOW_HALF(lock + LOW_HALF_INC);
92	}
93
94	proctype proc_A()
95	{
96	byte ticket;
97
98	do
99	:: 1 ->
100	progress_A:
101	spin_lock(lock, ticket);
102	refcount = refcount + 1;
103	refcount = refcount - 1;
104	spin_unlock(lock);
105	od;
106	}
107
108	proctype proc_B()
109	{
110	byte ticket;
111
112	do
113	:: 1 ->
114	do_pause();
115	spin_lock(lock, ticket);
116	refcount = refcount + 1;
117	do_pause();
118	refcount = refcount - 1;
119	spin_unlock(lock);
120	od;
121	}
122
123	init
124	{
125	run proc_A();
126	run proc_B();
127	run proc_B();
128	run proc_B();
129	run proc_B();
130	}