As promised, here is a new model :-) So far the results are very good.
Basically, I model the dependencies between the instructions using a SSA
assignment. It behaves a bit like a Petri network, passing tokens
between the "instructions". When instructions have multiple dependencies
as input, they wait for all their input tokens to be ready before they
execute. It assumes we have an infinite number of registers available to
hold the variables, given this is an "abstract" architecture.
Signed-off-by: Mathieu Desnoyers <mathieu.desnoyers@polymtl.ca>
--- /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)
+
+/*
+ * 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;
+
+#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;
+
+#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;
+
+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);
+}
+
+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
--- /dev/null
+#define read_one_is_zero (read_one == 0)
+#define read_two_is_zero (read_two == 0)
--- /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)
+
+/*
+ * Bit encoding, proc_one_produced :
+ */
+
+#define P1_PROD_NONE (1 << 0)
+
+#define P1_WRITE (1 << 1)
+#define P1_WMB (1 << 2)
+#define P1_SYNC_CORE (1 << 3)
+#define P1_RMB (1 << 4)
+#define P1_READ (1 << 5)
+
+int proc_one_produced;
+
+#define P2_PROD_NONE (1 << 0)
+
+#define P2_WRITE (1 << 1)
+#define P2_WMB (1 << 2)
+#define P2_SYNC_CORE (1 << 3)
+#define P2_RMB (1 << 4)
+#define P2_READ (1 << 5)
+
+int proc_two_produced;
+
+#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;
+
+active proctype test_proc_one()
+{
+ assert(get_pid() < NR_PROCS);
+
+ PRODUCE_TOKENS(proc_one_produced, P1_PROD_NONE);
+
+#ifdef NO_WMB
+ PRODUCE_TOKENS(proc_one_produced, P1_WMB);
+#endif
+#ifdef NO_RMB
+ PRODUCE_TOKENS(proc_one_produced, P1_RMB);
+#endif
+
+ do
+ :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE, P1_WRITE) ->
+ ooo_mem();
+ WRITE_CACHED_VAR(alpha, 1);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_one_produced, P1_WRITE);
+ :: CONSUME_TOKENS(proc_one_produced, P1_WRITE, P1_WMB) ->
+ smp_wmb();
+ PRODUCE_TOKENS(proc_one_produced, P1_WMB);
+ :: CONSUME_TOKENS(proc_one_produced, P1_WRITE | P1_WMB, P1_SYNC_CORE) ->
+ /* sync_core(); */
+ PRODUCE_TOKENS(proc_one_produced, P1_SYNC_CORE);
+ :: CONSUME_TOKENS(proc_one_produced, P1_SYNC_CORE, P1_RMB) ->
+ smp_rmb();
+ PRODUCE_TOKENS(proc_one_produced, P1_RMB);
+ :: CONSUME_TOKENS(proc_one_produced, P1_RMB | P1_SYNC_CORE, P1_READ) ->
+ ooo_mem();
+ read_one = READ_CACHED_VAR(beta);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_one_produced, P1_READ);
+ :: CONSUME_TOKENS(proc_one_produced, P1_PROD_NONE | P1_WRITE
+ | P1_WMB | P1_SYNC_CORE | P1_RMB | P1_READ, 0) ->
+ break;
+ od;
+
+ //CLEAR_TOKENS(proc_one_produced,
+ // P1_PROD_NONE | P1_WRITE | P1_WMB | P1_SYNC_CORE | P1_RMB |
+ // P2_READ);
+
+ // test : [] (read_one == 0 -> read_two != 0)
+ // test : [] (read_two == 0 -> read_one != 0)
+ assert(!(read_one == 0 && read_two == 0));
+}
+
+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
+#ifdef NO_RMB
+ PRODUCE_TOKENS(proc_two_produced, P2_RMB);
+#endif
+
+ do
+ :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE, P2_WRITE) ->
+ ooo_mem();
+ WRITE_CACHED_VAR(beta, 1);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_two_produced, P2_WRITE);
+ :: CONSUME_TOKENS(proc_two_produced, P2_WRITE, P2_WMB) ->
+ smp_wmb();
+ PRODUCE_TOKENS(proc_two_produced, P2_WMB);
+ :: CONSUME_TOKENS(proc_two_produced, P2_WRITE | P2_WMB, P2_SYNC_CORE) ->
+ /* sync_core(); */
+ PRODUCE_TOKENS(proc_two_produced, P2_SYNC_CORE);
+ :: CONSUME_TOKENS(proc_two_produced, P2_SYNC_CORE, P2_RMB) ->
+ smp_rmb();
+ PRODUCE_TOKENS(proc_two_produced, P2_RMB);
+ :: CONSUME_TOKENS(proc_two_produced, P2_SYNC_CORE | P2_RMB, P2_READ) ->
+ ooo_mem();
+ read_two = READ_CACHED_VAR(alpha);
+ ooo_mem();
+ PRODUCE_TOKENS(proc_two_produced, P2_READ);
+ :: CONSUME_TOKENS(proc_two_produced, P2_PROD_NONE | P2_WRITE
+ | P2_WMB | P2_SYNC_CORE | P2_RMB | P2_READ, 0) ->
+ break;
+ od;
+
+ //CLEAR_TOKENS(proc_two_produced,
+ // P2_PROD_NONE | P2_WRITE | P2_WMB | P2_SYNC_CORE | P2_RMB |
+ // P2_READ);
+
+ // test : [] (read_one == 0 -> read_two != 0)
+ // test : [] (read_two == 0 -> read_one != 0)
+ assert(!(read_one == 0 && read_two == 0));
+}
--- /dev/null
+[] (read_one_is_zero -> !read_two_is_zero)
--- /dev/null
+[] (read_one_is_zero -> !read_two_is_zero)
--- /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
projects / userspace-rcu.git / commitdiff
