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

/*
 * futex.spin: Promela code to validate futex wakeup algorithm.
 *
 * Algorithm verified :
 *
 * queue = 0;
 * fut = 0;
 * runvar = 0;
 *
 *                            Waker
 *                            queue = 1;
 *                            if (fut == -1) {
 *                              fut = 0;
 *                            }
 *
 * Waiter
 * while (1) {
 *   progress:
 *   fut = fut - 1;
 *   if (queue == 1) {
 *     fut = 0;
 *   } else {
 *     if (fut == -1) {
 *        while (fut == -1) { }
 *     }
 *   }
 *   queue = 0;
 * }
 *
 * if queue = 1, then !_np
 *
 * 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
 */

int queue = 0;
int fut = 0;

active proctype waker()
{
	queue = 1;

	if
	:: (fut == -1) ->
		fut = 0;
	:: else ->
		skip;
	fi;

	queue = 1;

	if
	:: (fut == -1) ->
		fut = 0;
	:: else ->
		skip;
	fi;

#ifdef INJ_QUEUE_NO_WAKE
	queue = 1;
#endif
}


active proctype waiter()
{
	do
	:: 1 ->
#ifndef INJ_LATE_DEC
		fut = fut - 1;
#endif
		if
		:: (queue == 1) ->
#ifndef INJ_LATE_DEC
			fut = 0;
#endif
			skip;
		:: else ->
#ifdef INJ_LATE_DEC
			fut = fut - 1;
#endif
			if
			:: (fut == -1) ->
				do
				:: 1 ->
					if
					:: (fut == -1) ->
						skip;
					:: else ->
						break;
					fi;
				od;
			:: else ->
				skip;
			fi;
		fi;
progress:
		queue = 0;
	od;
}
Commit	Line	Data
d4de4869 MD	1	/*
	2	* futex.spin: Promela code to validate futex wakeup algorithm.
	3	*
	4	* Algorithm verified :
	5	*
	6	* queue = 0;
	7	* fut = 0;
	8	* runvar = 0;
	9	*
	10	* Waker
	11	* queue = 1;
	12	* if (fut == -1) {
	13	* fut = 0;
	14	* }
	15	*
	16	* Waiter
	17	* while (1) {
	18	* progress:
	19	* fut = fut - 1;
	20	* if (queue == 1) {
	21	* fut = 0;
	22	* } else {
	23	* if (fut == -1) {
	24	* while (fut == -1) { }
	25	* }
	26	* }
	27	* queue = 0;
	28	* }
	29	*
	30	* if queue = 1, then !_np
	31	*
	32	* This program is free software; you can redistribute it and/or modify
	33	* it under the terms of the GNU General Public License as published by
	34	* the Free Software Foundation; either version 2 of the License, or
	35	* (at your option) any later version.
	36	*
	37	* This program is distributed in the hope that it will be useful,
	38	* but WITHOUT ANY WARRANTY; without even the implied warranty of
	39	* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
	40	* GNU General Public License for more details.
	41	*
	42	* You should have received a copy of the GNU General Public License
	43	* along with this program; if not, write to the Free Software
	44	* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA 02111-1307, USA.
	45	*
	46	* Copyright (c) 2009 Mathieu Desnoyers
	47	*/
	48
	49	int queue = 0;
	50	int fut = 0;
	51
	52	active proctype waker()
	53	{
	54	queue = 1;
	55
	56	if
	57	:: (fut == -1) ->
	58	fut = 0;
	59	:: else ->
	60	skip;
	61	fi;
	62
	63	queue = 1;
	64
65	if
66	:: (fut == -1) ->
67	fut = 0;
68	:: else ->
69	skip;
70	fi;
71
72	#ifdef INJ_QUEUE_NO_WAKE
73	queue = 1;
74	#endif
75	}
76
77
78	active proctype waiter()
79	{
80	do
81	:: 1 ->
82	#ifndef INJ_LATE_DEC
83	fut = fut - 1;
84	#endif
85	if
86	:: (queue == 1) ->
87	#ifndef INJ_LATE_DEC
88	fut = 0;
89	#endif
90	skip;
91	:: else ->
92	#ifdef INJ_LATE_DEC
93	fut = fut - 1;
94	#endif
95	if
96	:: (fut == -1) ->
97	do
98	:: 1 ->
99	if
100	:: (fut == -1) ->
d4de4869 MD	101	skip;
	102	:: else ->
	103	break;
	104	fi;
	105	od;
	106	:: else ->
	107	skip;
	108	fi;
	109	fi;
9b35d5dc	110	progress:
d4de4869 MD	111	queue = 0;
	112	od;
	113	}