+++ /dev/null
-#define read_one_is_one (read_one == 1)
-#define read_two_is_one (read_two == 1)
-#define read_two_done (read_two != 2)
+++ /dev/null
-# 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) Mathieu Desnoyers, 2009
-#
-# Authors: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
-
-#CFLAGS=-DSAFETY
-#CFLAGS=-DHASH64 -DREACH
-CFLAGS=-DHASH64
-
-#try pan -i to get the smallest trace.
-
-SPINFILE=mem.spin
-
-default:
- make read_order | tee read_order.log
- make read_order_no_wmb | tee read_order_no_wmb.log
- make read_order_no_rmb | tee read_order_no_rmb.log
- make asserts | tee asserts.log
- make summary
-
-#show trail : spin -v -t -N pan.ltl input.spin
-# after each individual make.
-
-summary:
- @echo
- @echo "Verification summary"
- @grep error *.log
-
-asserts: clean
- cat DEFINES > .input.spin
- cat ${SPINFILE} >> .input.spin
- rm -f .input.spin.trail
- spin -a -X .input.spin
- gcc -w ${CFLAGS} -DSAFETY -o pan pan.c
- ./pan -v -c1 -X -m10000 -w19
- cp .input.spin $@.spin.input
- -cp .input.spin.trail $@.spin.input.trail
-
-read_order: clean read_order_ltl run
- cp .input.spin $@.spin.input
- -cp .input.spin.trail $@.spin.input.trail
-
-read_order_no_rmb: clean read_order_ltl read_order_no_rmb_define run
- cp .input.spin $@.spin.input
- -cp .input.spin.trail $@.spin.input.trail
-
-read_order_no_rmb_define:
- cp read_order_no_rmb.define .input.define
-
-read_order_no_wmb: clean read_order_ltl read_order_no_wmb_define run
- cp .input.spin $@.spin.input
- -cp .input.spin.trail $@.spin.input.trail
-
-read_order_no_wmb_define:
- cp read_order_no_wmb.define .input.define
-
-read_order_ltl:
- touch .input.define
- cat DEFINES > pan.ltl
- cat .input.define >> pan.ltl
- spin -f "!(`cat read_order.ltl | grep -v ^//`)" >> pan.ltl
-
-run: pan
- ./pan -a -v -c1 -X -m10000 -w19
-
-pan: pan.c
- gcc -w ${CFLAGS} -o pan pan.c
-
-pan.c: pan.ltl ${SPINFILE}
- cat DEFINES > .input.spin
- cat .input.define >> .input.spin
- cat ${SPINFILE} >> .input.spin
- rm -f .input.spin.trail
- spin -a -X -N pan.ltl .input.spin
-
-.PHONY: clean default distclean summary
-clean:
- rm -f pan* trail.out .input.spin* *.spin.trail .input.define
-distclean:
- rm -f *.trail *.input *.log
+++ /dev/null
-#!/bin/sh
-#
-# Compiles and runs the urcu.spin Promela model.
-#
-# 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) IBM Corporation, 2009
-# Mathieu Desnoyers, 2009
-#
-# Authors: Paul E. McKenney <paulmck@linux.vnet.ibm.com>
-# Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
-
-# Basic execution, without LTL clauses. See Makefile.
-
-spin -a mem.spin
-cc -DSAFETY -o pan pan.c
-./pan -v -c1 -X -m10000000 -w21
+++ /dev/null
-/*
- * 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. */
-
-/*
- * Produced process data flow. Updated after each instruction to show which
- * variables are ready. Assigned using SSA (static single assignment) (defuse
- * analysis must be done on the program to map "real" variables to single define
- * followed by use). Using one-hot bit encoding per variable to save state
- * space. Used as triggers to execute the instructions having those variables
- * as input.
- */
-
-#define PRODUCE_TOKENS(state, bits) \
- state = (state) | (bits)
-
-/* All bits must be active to consume. All notbits must be inactive. */
-/* Consuming a token does not clear it, it just waits for it. */
-#define CONSUME_TOKENS(state, bits, notbits) \
- ((!((state) & (notbits))) && ((state) & (bits)) == (bits))
-
-#define CLEAR_TOKENS(state, bits) \
- state = (state) & ~(bits)
-
-#define NR_PROCS 2
-
-#define get_pid() (_pid)
-
-/*
- * Each process have its own data in cache. Caches are randomly updated.
- * smp_wmb and smp_rmb forces cache updates (write and read), wmb_mb forces
- * both.
- */
-
-#define DECLARE_CACHED_VAR(type, x, v) \
- type mem_##x = v; \
- type cached_##x[NR_PROCS] = v; \
- bit cache_dirty_##x[NR_PROCS] = 0;
-
-#define IS_CACHE_DIRTY(x, id) (cache_dirty_##x[id])
-
-#define READ_CACHED_VAR(x) \
- (cached_##x[get_pid()])
-
-#define WRITE_CACHED_VAR(x, v) \
- atomic { \
- cached_##x[get_pid()] = v; \
- cache_dirty_##x[get_pid()] = 1; \
- }
-
-#define CACHE_WRITE_TO_MEM(x, id) \
- if \
- :: IS_CACHE_DIRTY(x, id) -> \
- mem_##x = cached_##x[id]; \
- cache_dirty_##x[id] = 0; \
- :: else -> \
- skip \
- fi;
-
-#define CACHE_READ_FROM_MEM(x, id) \
- if \
- :: !IS_CACHE_DIRTY(x, id) -> \
- cached_##x[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;
-
-inline ooo_mem()
-{
- atomic {
- RANDOM_CACHE_WRITE_TO_MEM(alpha, get_pid());
- RANDOM_CACHE_WRITE_TO_MEM(beta, get_pid());
- RANDOM_CACHE_READ_FROM_MEM(alpha, get_pid());
- RANDOM_CACHE_READ_FROM_MEM(beta, get_pid());
- }
-}
-
-/* must consume all prior read tokens */
-inline smp_rmb()
-{
- atomic {
- /* todo : consume all read tokens .. ? */
- CACHE_READ_FROM_MEM(alpha, get_pid());
- CACHE_READ_FROM_MEM(beta, get_pid());
- }
-}
-
-/* must consume all prior write tokens */
-inline smp_wmb()
-{
- atomic {
- CACHE_WRITE_TO_MEM(alpha, get_pid());
- CACHE_WRITE_TO_MEM(beta, get_pid());
- }
-}
-
-/* sync_core() must consume all prior read and write tokens, including rmb/wmb
- * tokens */
-
-/* must consume all prior read and write tokens */
-inline smp_mb()
-{
- atomic {
- smp_wmb();
- /* sync_core() */
- smp_rmb();
- }
-}
-
-/* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */
-DECLARE_CACHED_VAR(byte, alpha, 0);
-DECLARE_CACHED_VAR(byte, beta, 0);
-
-/* value 2 is uninitialized */
-byte read_one = 2;
-byte read_two = 2;
-
-/*
- * Bit encoding, proc_one_produced :
- */
-
-#define P1_PROD_NONE (1 << 0)
-
-#define P1_READ_ONE (1 << 1)
-#define P1_RMB (1 << 2)
-#define P1_READ_TWO (1 << 3)
-
-int proc_one_produced;
-
-active proctype test_proc_one()
-{
- assert(get_pid() < NR_PROCS);
-
- PRODUCE_TOKENS(proc_one_produced, P1_PROD_NONE);
-#ifdef NO_RMB
- PRODUCE_TOKENS(proc_one_produced, P1_RMB);
-#endif
-
- do
- :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE, P1_READ_ONE) ->
- ooo_mem();
- read_one = READ_CACHED_VAR(beta);
- ooo_mem();
- PRODUCE_TOKENS(proc_one_produced, P1_READ_ONE);
- :: CONSUME_TOKENS(proc_one_produced, P1_READ_ONE, P1_RMB) ->
- smp_rmb();
- PRODUCE_TOKENS(proc_one_produced, P1_RMB);
- :: CONSUME_TOKENS(proc_one_produced, P1_RMB, P1_READ_TWO) ->
- ooo_mem();
- read_two = READ_CACHED_VAR(alpha);
- ooo_mem();
- PRODUCE_TOKENS(proc_one_produced, P1_READ_TWO);
- :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE | P1_READ_ONE
- | P1_RMB | P1_READ_TWO, 0) ->
- break;
- od;
-
- //CLEAR_TOKENS(proc_one_produced,
- // P1_PROD_NONE | P1_READ_ONE | P1_RMB | P2_READ_TWO);
-
- // test : [] (read_one == 1 -> read_two == 1)
- assert(read_one != 1 || read_two == 1);
-}
-
-
-/*
- * Bit encoding, proc_two_produced :
- */
-
-#define P2_PROD_NONE (1 << 0)
-
-#define P2_WRITE_ONE (1 << 1)
-#define P2_WMB (1 << 2)
-#define P2_WRITE_TWO (1 << 3)
-
-int proc_two_produced;
-
-active proctype test_proc_two()
-{
- assert(get_pid() < NR_PROCS);
-
- PRODUCE_TOKENS(proc_two_produced, P2_PROD_NONE);
-#ifdef NO_WMB
- PRODUCE_TOKENS(proc_two_produced, P2_WMB);
-#endif
-
- do
- :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE, P2_WRITE_ONE) ->
- ooo_mem();
- WRITE_CACHED_VAR(alpha, 1);
- ooo_mem();
- PRODUCE_TOKENS(proc_two_produced, P2_WRITE_ONE);
- :: CONSUME_TOKENS(proc_two_produced, P2_WRITE_ONE, P2_WMB) ->
- smp_wmb();
- PRODUCE_TOKENS(proc_two_produced, P2_WMB);
- :: CONSUME_TOKENS(proc_two_produced, P2_WMB, P2_WRITE_TWO) ->
- ooo_mem();
- WRITE_CACHED_VAR(beta, 1);
- ooo_mem();
- PRODUCE_TOKENS(proc_two_produced, P2_WRITE_TWO);
- :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE | P2_WRITE_ONE
- | P2_WMB | P2_WRITE_TWO, 0) ->
- break;
- od;
-
- //CLEAR_TOKENS(proc_two_produced,
- // P2_PROD_NONE | P2_WRITE_ONE | P2_WMB | P2_WRITE_TWO);
-}
+++ /dev/null
-[] (read_one_is_one -> (!read_two_done || read_two_is_one))
+++ /dev/null
-#define NO_RMB
+++ /dev/null
-#define NO_WMB
+++ /dev/null
-http://spinroot.com/spin/Man/ltl.html
-http://en.wikipedia.org/wiki/Linear_temporal_logic
-http://www.dcs.gla.ac.uk/~muffy/MRS4-2002/lect11.ppt
-
-http://www.lsv.ens-cachan.fr/~gastin/ltl2ba/index.php
-http://spinroot.com/spin/Man/index.html
-http://spinroot.com/spin/Man/promela.html
-#define read_one_is_zero (read_one == 0)
-#define read_two_is_zero (read_two == 0)
+#define read_one_is_one (read_one == 1)
+#define read_two_is_one (read_two == 1)
+#define read_two_done (read_two != 2)
/* Promela validation variables. */
-#define NR_READERS 1
-#define NR_WRITERS 1
+/*
+ * Produced process control and data flow. Updated after each instruction to
+ * show which variables are ready. Using one-hot bit encoding per variable to
+ * save state space. Used as triggers to execute the instructions having those
+ * variables as input. Leaving bits active to inhibit instruction execution.
+ * Scheme used to make instruction disabling and automatic dependency fall-back
+ * automatic.
+ */
+
+#define CONSUME_TOKENS(state, bits, notbits) \
+ ((!(state & (notbits))) && (state & (bits)) == (bits))
+
+#define PRODUCE_TOKENS(state, bits) \
+ state = state | (bits);
+
+#define CLEAR_TOKENS(state, bits) \
+ state = state & ~(bits)
#define NR_PROCS 2
* both.
*/
-#define DECLARE_CACHED_VAR(type, x, v) \
- type mem_##x = v; \
- type cached_##x[NR_PROCS] = v; \
- bit cache_dirty_##x[NR_PROCS] = 0
+#define DECLARE_CACHED_VAR(type, x, v) \
+ type mem_##x = v; \
+ type cached_##x[NR_PROCS] = v; \
+ bit cache_dirty_##x[NR_PROCS] = 0;
#define IS_CACHE_DIRTY(x, id) (cache_dirty_##x[id])
-#define READ_CACHED_VAR(x) (cached_##x[get_pid()])
+#define READ_CACHED_VAR(x) \
+ (cached_##x[get_pid()])
-#define WRITE_CACHED_VAR(x, v) \
- atomic { \
+#define WRITE_CACHED_VAR(x, v) \
+ atomic { \
cached_##x[get_pid()] = v; \
cache_dirty_##x[get_pid()] = 1; \
}
skip \
fi;
-#define CACHE_READ_FROM_MEM(x, id) \
- if \
- :: !IS_CACHE_DIRTY(x, id) -> \
- cached_##x[id] = mem_##x;\
- :: else -> \
- skip \
+#define CACHE_READ_FROM_MEM(x, id) \
+ if \
+ :: !IS_CACHE_DIRTY(x, id) -> \
+ cached_##x[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 \
+#define RANDOM_CACHE_WRITE_TO_MEM(x, id) \
+ if \
:: 1 -> CACHE_WRITE_TO_MEM(x, id); \
- :: 1 -> skip \
+ :: 1 -> skip \
fi;
#define RANDOM_CACHE_READ_FROM_MEM(x, id)\
- if \
+ if \
:: 1 -> CACHE_READ_FROM_MEM(x, id); \
- :: 1 -> skip \
+ :: 1 -> skip \
fi;
+inline ooo_mem()
+{
+ atomic {
+ RANDOM_CACHE_WRITE_TO_MEM(alpha, get_pid());
+ RANDOM_CACHE_WRITE_TO_MEM(beta, get_pid());
+ RANDOM_CACHE_READ_FROM_MEM(alpha, get_pid());
+ RANDOM_CACHE_READ_FROM_MEM(beta, get_pid());
+ }
+}
+
+/* must consume all prior read tokens */
inline smp_rmb()
{
atomic {
+ /* todo : consume all read tokens .. ? */
CACHE_READ_FROM_MEM(alpha, get_pid());
CACHE_READ_FROM_MEM(beta, get_pid());
}
}
+/* must consume all prior write tokens */
inline smp_wmb()
{
atomic {
}
}
+/* sync_core() must consume all prior read and write tokens, including rmb/wmb
+ * tokens */
+
+/* must consume all prior read and write tokens */
inline smp_mb()
{
atomic {
smp_wmb();
+ /* sync_core() */
smp_rmb();
}
}
DECLARE_CACHED_VAR(byte, alpha, 0);
DECLARE_CACHED_VAR(byte, beta, 0);
-inline ooo_mem()
-{
- atomic {
- RANDOM_CACHE_WRITE_TO_MEM(alpha, get_pid());
- RANDOM_CACHE_WRITE_TO_MEM(beta, get_pid());
- RANDOM_CACHE_READ_FROM_MEM(alpha, get_pid());
- RANDOM_CACHE_READ_FROM_MEM(beta, get_pid());
- }
-}
-
/* value 2 is uninitialized */
byte read_one = 2;
byte read_two = 2;
+/*
+ * Bit encoding, proc_one_produced :
+ */
+
+#define P1_PROD_NONE (1 << 0)
+
+#define P1_READ_ONE (1 << 1)
+#define P1_RMB (1 << 2)
+#define P1_READ_TWO (1 << 3)
+
+/* Only need a single color. */
+byte proc_one_produced;
+
active proctype test_proc_one()
{
assert(get_pid() < NR_PROCS);
- ooo_mem();
- WRITE_CACHED_VAR(alpha, 1);
- ooo_mem();
-#ifndef NO_WMB
- smp_wmb();
- ooo_mem();
-#endif
-#ifndef NO_RMB
- smp_rmb();
- ooo_mem();
+ PRODUCE_TOKENS(proc_one_produced, P1_PROD_NONE);
+#ifdef NO_RMB
+ PRODUCE_TOKENS(proc_one_produced, P1_RMB);
#endif
- read_one = READ_CACHED_VAR(beta);
- ooo_mem();
- // test : [] (read_one == 0 -> read_two != 0)
- // test : [] (read_two == 0 -> read_one != 0)
- assert(!(read_one == 0 && read_two == 0));
+
+ do
+ :: CONSUME_TOKENS(proc_one_produced,
+ P1_PROD_NONE, P1_READ_ONE) ->
+ ooo_mem();
+ read_one = READ_CACHED_VAR(beta);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_one_produced, P1_READ_ONE);
+ :: CONSUME_TOKENS(proc_one_produced,
+ P1_READ_ONE, P1_RMB) ->
+ smp_rmb();
+ PRODUCE_TOKENS(proc_one_produced, P1_RMB);
+ :: CONSUME_TOKENS(proc_one_produced,
+ P1_RMB, P1_READ_TWO) ->
+ ooo_mem();
+ read_two = READ_CACHED_VAR(alpha);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_one_produced, P1_READ_TWO);
+ :: CONSUME_TOKENS(proc_one_produced,
+ P1_PROD_NONE | P1_READ_ONE | P1_RMB
+ | P1_READ_TWO, 0) ->
+ break;
+ od;
+
+ //CLEAR_TOKENS(proc_one_produced,
+ // P1_PROD_NONE | P1_READ_ONE | P1_RMB | P1_READ_TWO);
+
+ // test : [] (read_one == 1 -> read_two == 1)
+ assert(read_one != 1 || read_two == 1);
}
+
+/*
+ * Bit encoding, proc_two_produced :
+ */
+
+#define P2_PROD_NONE (1 << 0)
+
+#define P2_WRITE_ONE (1 << 1)
+#define P2_WMB (1 << 2)
+#define P2_WRITE_TWO (1 << 3)
+
+/* Only need a single color. */
+byte proc_two_produced;
+
active proctype test_proc_two()
{
assert(get_pid() < NR_PROCS);
- ooo_mem();
- WRITE_CACHED_VAR(beta, 1);
- ooo_mem();
-#ifndef NO_WMB
- smp_wmb();
- ooo_mem();
+ PRODUCE_TOKENS(proc_two_produced, P2_PROD_NONE);
+#ifdef NO_WMB
+ PRODUCE_TOKENS(proc_two_produced, P2_WMB);
#endif
-#ifndef NO_RMB
- smp_rmb();
- ooo_mem();
-#endif
- read_two = READ_CACHED_VAR(alpha);
- ooo_mem();
- // test : [] (read_one == 0 -> read_two != 0)
- // test : [] (read_two == 0 -> read_one != 0)
- assert(!(read_one == 0 && read_two == 0));
+
+ do
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_PROD_NONE, P2_WRITE_ONE) ->
+ ooo_mem();
+ WRITE_CACHED_VAR(alpha, 1);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_two_produced, P2_WRITE_ONE);
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_WRITE_ONE, P2_WMB) ->
+ smp_wmb();
+ PRODUCE_TOKENS(proc_two_produced, P2_WMB);
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_WMB, P2_WRITE_TWO) ->
+ ooo_mem();
+ WRITE_CACHED_VAR(beta, 1);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_two_produced, P2_WRITE_TWO);
+ :: CONSUME_TOKENS(proc_two_produced,
+ P2_PROD_NONE | P2_WRITE_ONE
+ | P2_WMB | P2_WRITE_TWO, 0) ->
+ break;
+ od;
+
+ //CLEAR_TOKENS(proc_two_produced,
+ // P2_PROD_NONE | P2_WRITE_ONE | P2_WMB | P2_WRITE_TWO);
}
-[] (read_one_is_zero -> !read_two_is_zero)
+[] (read_one_is_one -> (!read_two_done || read_two_is_one))
make read_order | tee read_order.log
make read_order_no_wmb | tee read_order_no_wmb.log
make read_order_no_rmb | tee read_order_no_rmb.log
+ make read_order_no_sync | tee read_order_no_sync.log
make asserts | tee asserts.log
make summary
cp .input.spin $@.spin.input
-cp .input.spin.trail $@.spin.input.trail
+read_order_no_sync: clean read_order_ltl read_order_no_sync_define run
+ cp .input.spin $@.spin.input
+ -cp .input.spin.trail $@.spin.input.trail
+
+read_order_no_sync_define:
+ cp read_order_no_sync.define .input.define
+
read_order_no_rmb: clean read_order_ltl read_order_no_rmb_define run
cp .input.spin $@.spin.input
-cp .input.spin.trail $@.spin.input.trail
/* Promela validation variables. */
/*
- * Produced process data flow. Updated after each instruction to show which
- * variables are ready. Assigned using SSA (static single assignment) (defuse
- * analysis must be done on the program to map "real" variables to single define
- * followed by use). Using one-hot bit encoding per variable to save state
- * space. Used as triggers to execute the instructions having those variables
- * as input.
+ * Produced process control and data flow. Updated after each instruction to
+ * show which variables are ready. Using one-hot bit encoding per variable to
+ * save state space. Used as triggers to execute the instructions having those
+ * variables as input. Leaving bits active to inhibit instruction execution.
+ * Scheme used to make instruction disabling and automatic dependency fall-back
+ * automatic.
*/
-#define PRODUCE_TOKENS(state, bits) \
- state = (state) | (bits)
+#define CONSUME_TOKENS(state, bits, notbits) \
+ ((!(state & (notbits))) && (state & (bits)) == (bits))
-/* All bits must be active to consume. All notbits must be inactive. */
-/* Consuming a token does not clear it, it just waits for it. */
-#define CONSUME_TOKENS(state, bits, notbits) \
- ((!((state) & (notbits))) && ((state) & (bits)) == (bits))
+#define PRODUCE_TOKENS(state, bits) \
+ state = state | (bits);
-#define CLEAR_TOKENS(state, bits) \
- state = (state) & ~(bits)
+#define CLEAR_TOKENS(state, bits) \
+ state = state & ~(bits)
#define NR_PROCS 2
projects / userspace-rcu.git / commitdiff
