From 03c9e0f3f9c72b36b9da30ad4b6ecb055fb6adff Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Fri, 8 May 2009 14:14:30 -0400 Subject: [PATCH] Add instruction scheduling model using SSA model 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 --- .../ooomem-double-update-minimal/DEFINES | 3 + .../ooomem-double-update-minimal/Makefile | 93 ++++++ .../ooomem-double-update-minimal/mem.sh | 29 ++ .../ooomem-double-update-minimal/mem.spin | 236 ++++++++++++++++ .../read_order.ltl | 1 + .../read_order_no_rmb.define | 1 + .../read_order_no_wmb.define | 1 + .../references.txt | 7 + formal-model/ooomem-two-writes/DEFINES | 2 + formal-model/ooomem-two-writes/Makefile | 93 ++++++ formal-model/ooomem-two-writes/mem.sh | 29 ++ formal-model/ooomem-two-writes/mem.spin | 267 ++++++++++++++++++ formal-model/ooomem-two-writes/read_order.ltl | 1 + .../ooomem-two-writes/read_order.ltl.bkp | 1 + .../read_order_no_rmb.define | 1 + .../read_order_no_wmb.define | 1 + formal-model/ooomem-two-writes/references.txt | 7 + 17 files changed, 773 insertions(+) create mode 100644 formal-model/ooomem-double-update-minimal/DEFINES create mode 100644 formal-model/ooomem-double-update-minimal/Makefile create mode 100644 formal-model/ooomem-double-update-minimal/mem.sh create mode 100644 formal-model/ooomem-double-update-minimal/mem.spin create mode 100644 formal-model/ooomem-double-update-minimal/read_order.ltl create mode 100644 formal-model/ooomem-double-update-minimal/read_order_no_rmb.define create mode 100644 formal-model/ooomem-double-update-minimal/read_order_no_wmb.define create mode 100644 formal-model/ooomem-double-update-minimal/references.txt create mode 100644 formal-model/ooomem-two-writes/DEFINES create mode 100644 formal-model/ooomem-two-writes/Makefile create mode 100644 formal-model/ooomem-two-writes/mem.sh create mode 100644 formal-model/ooomem-two-writes/mem.spin create mode 100644 formal-model/ooomem-two-writes/read_order.ltl create mode 100644 formal-model/ooomem-two-writes/read_order.ltl.bkp create mode 100644 formal-model/ooomem-two-writes/read_order_no_rmb.define create mode 100644 formal-model/ooomem-two-writes/read_order_no_wmb.define create mode 100644 formal-model/ooomem-two-writes/references.txt diff --git a/formal-model/ooomem-double-update-minimal/DEFINES b/formal-model/ooomem-double-update-minimal/DEFINES new file mode 100644 index 0000000..7cf7b24 --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/DEFINES @@ -0,0 +1,3 @@ +#define read_one_is_one (read_one == 1) +#define read_two_is_one (read_two == 1) +#define read_two_done (read_two != 2) diff --git a/formal-model/ooomem-double-update-minimal/Makefile b/formal-model/ooomem-double-update-minimal/Makefile new file mode 100644 index 0000000..37422b5 --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/Makefile @@ -0,0 +1,93 @@ +# 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 + +#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 diff --git a/formal-model/ooomem-double-update-minimal/mem.sh b/formal-model/ooomem-double-update-minimal/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/mem.sh @@ -0,0 +1,29 @@ +#!/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 +# Mathieu Desnoyers + +# Basic execution, without LTL clauses. See Makefile. + +spin -a mem.spin +cc -DSAFETY -o pan pan.c +./pan -v -c1 -X -m10000000 -w21 diff --git a/formal-model/ooomem-double-update-minimal/mem.spin b/formal-model/ooomem-double-update-minimal/mem.spin new file mode 100644 index 0000000..9fc540a --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/mem.spin @@ -0,0 +1,236 @@ +/* + * 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); +} diff --git a/formal-model/ooomem-double-update-minimal/read_order.ltl b/formal-model/ooomem-double-update-minimal/read_order.ltl new file mode 100644 index 0000000..dec26f2 --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/read_order.ltl @@ -0,0 +1 @@ +[] (read_one_is_one -> (!read_two_done || read_two_is_one)) diff --git a/formal-model/ooomem-double-update-minimal/read_order_no_rmb.define b/formal-model/ooomem-double-update-minimal/read_order_no_rmb.define new file mode 100644 index 0000000..73e61a4 --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/read_order_no_rmb.define @@ -0,0 +1 @@ +#define NO_RMB diff --git a/formal-model/ooomem-double-update-minimal/read_order_no_wmb.define b/formal-model/ooomem-double-update-minimal/read_order_no_wmb.define new file mode 100644 index 0000000..710f29d --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/read_order_no_wmb.define @@ -0,0 +1 @@ +#define NO_WMB diff --git a/formal-model/ooomem-double-update-minimal/references.txt b/formal-model/ooomem-double-update-minimal/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/ooomem-double-update-minimal/references.txt @@ -0,0 +1,7 @@ +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 diff --git a/formal-model/ooomem-two-writes/DEFINES b/formal-model/ooomem-two-writes/DEFINES new file mode 100644 index 0000000..e74150d --- /dev/null +++ b/formal-model/ooomem-two-writes/DEFINES @@ -0,0 +1,2 @@ +#define read_one_is_zero (read_one == 0) +#define read_two_is_zero (read_two == 0) diff --git a/formal-model/ooomem-two-writes/Makefile b/formal-model/ooomem-two-writes/Makefile new file mode 100644 index 0000000..37422b5 --- /dev/null +++ b/formal-model/ooomem-two-writes/Makefile @@ -0,0 +1,93 @@ +# 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 + +#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 diff --git a/formal-model/ooomem-two-writes/mem.sh b/formal-model/ooomem-two-writes/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/formal-model/ooomem-two-writes/mem.sh @@ -0,0 +1,29 @@ +#!/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 +# Mathieu Desnoyers + +# Basic execution, without LTL clauses. See Makefile. + +spin -a mem.spin +cc -DSAFETY -o pan pan.c +./pan -v -c1 -X -m10000000 -w21 diff --git a/formal-model/ooomem-two-writes/mem.spin b/formal-model/ooomem-two-writes/mem.spin new file mode 100644 index 0000000..4892c5e --- /dev/null +++ b/formal-model/ooomem-two-writes/mem.spin @@ -0,0 +1,267 @@ +/* + * 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)); +} diff --git a/formal-model/ooomem-two-writes/read_order.ltl b/formal-model/ooomem-two-writes/read_order.ltl new file mode 100644 index 0000000..f4dbf03 --- /dev/null +++ b/formal-model/ooomem-two-writes/read_order.ltl @@ -0,0 +1 @@ +[] (read_one_is_zero -> !read_two_is_zero) diff --git a/formal-model/ooomem-two-writes/read_order.ltl.bkp b/formal-model/ooomem-two-writes/read_order.ltl.bkp new file mode 100644 index 0000000..f4dbf03 --- /dev/null +++ b/formal-model/ooomem-two-writes/read_order.ltl.bkp @@ -0,0 +1 @@ +[] (read_one_is_zero -> !read_two_is_zero) diff --git a/formal-model/ooomem-two-writes/read_order_no_rmb.define b/formal-model/ooomem-two-writes/read_order_no_rmb.define new file mode 100644 index 0000000..73e61a4 --- /dev/null +++ b/formal-model/ooomem-two-writes/read_order_no_rmb.define @@ -0,0 +1 @@ +#define NO_RMB diff --git a/formal-model/ooomem-two-writes/read_order_no_wmb.define b/formal-model/ooomem-two-writes/read_order_no_wmb.define new file mode 100644 index 0000000..710f29d --- /dev/null +++ b/formal-model/ooomem-two-writes/read_order_no_wmb.define @@ -0,0 +1 @@ +#define NO_WMB diff --git a/formal-model/ooomem-two-writes/references.txt b/formal-model/ooomem-two-writes/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/ooomem-two-writes/references.txt @@ -0,0 +1,7 @@ +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 -- 2.34.1