From bac061a165dc6a98ca31ae170c556aa8c89bb45e Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Mon, 27 Apr 2009 16:19:17 -0400 Subject: [PATCH] Add ooo mem instruction scheduling Signed-off-by: Mathieu Desnoyers --- formal-model/ooomem-deps/DEFINES | 2 + formal-model/ooomem-deps/Makefile | 82 ++++++++ formal-model/ooomem-deps/mem.sh | 29 +++ formal-model/ooomem-deps/mem.spin | 192 ++++++++++++++++++ formal-model/ooomem-deps/read_order.ltl | 1 + .../ooomem-deps/read_order_sync_core.define | 1 + formal-model/ooomem-deps/references.txt | 7 + 7 files changed, 314 insertions(+) create mode 100644 formal-model/ooomem-deps/DEFINES create mode 100644 formal-model/ooomem-deps/Makefile create mode 100644 formal-model/ooomem-deps/mem.sh create mode 100644 formal-model/ooomem-deps/mem.spin create mode 100644 formal-model/ooomem-deps/read_order.ltl create mode 100644 formal-model/ooomem-deps/read_order_sync_core.define create mode 100644 formal-model/ooomem-deps/references.txt diff --git a/formal-model/ooomem-deps/DEFINES b/formal-model/ooomem-deps/DEFINES new file mode 100644 index 0000000..e74150d --- /dev/null +++ b/formal-model/ooomem-deps/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-deps/Makefile b/formal-model/ooomem-deps/Makefile new file mode 100644 index 0000000..e63a073 --- /dev/null +++ b/formal-model/ooomem-deps/Makefile @@ -0,0 +1,82 @@ +# 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 + +SPINFILE=mem.spin + +default: + make read_order | tee read_order.log + make read_order_sync_core | tee read_order_sync_core.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_sync_core: clean read_order_ltl read_order_sync_core_define run + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +read_order_sync_core_define: + cp read_order_sync_core.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-deps/mem.sh b/formal-model/ooomem-deps/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/formal-model/ooomem-deps/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-deps/mem.spin b/formal-model/ooomem-deps/mem.spin new file mode 100644 index 0000000..ca68cb7 --- /dev/null +++ b/formal-model/ooomem-deps/mem.spin @@ -0,0 +1,192 @@ +/* + * 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. */ + +#define NR_READERS 1 +#define NR_WRITERS 1 + +#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 smp_rmb() +{ + atomic { + CACHE_READ_FROM_MEM(alpha, get_pid()); + CACHE_READ_FROM_MEM(beta, get_pid()); + } +} + +inline smp_wmb() +{ + atomic { + CACHE_WRITE_TO_MEM(alpha, get_pid()); + CACHE_WRITE_TO_MEM(beta, get_pid()); + } +} + +inline smp_mb() +{ + atomic { + smp_wmb(); + smp_rmb(); + } +} + +/* + * Instruction scheduling support. Declares instruction data flow dependency. + * INSTRUCTION_SCHED_BEGIN/INSTRUCTION_SCHED_END can be nested. + */ +#define INSTRUCTION_SCHED_BEGIN(i) \ + if \ + :: 1 -> \ + ooo_mem(i) + +/* No data flow dependency between two consecutive instructions */ +#define INSTRUCTION_SCHED_NODEP_NEXT(i) \ + :: 1 -> \ + ooo_mem(i) + +/* Has dependency between two consecutive instructions */ +#define INSTRUCTION_SCHED_DEP_NEXT(i) \ + ooo_mem(i) + +#define INSTRUCTION_SCHED_END(i) \ + 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()); + } +} + +/* 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); + + INSTRUCTION_SCHED_BEGIN(); + WRITE_CACHED_VAR(alpha, 1); + INSTRUCTION_SCHED_DEP_NEXT(); + smp_wmb(); +#ifndef USE_SYNC_CORE + INSTRUCTION_SCHED_NODEP_NEXT(); +#else + // if we use a sync_core(); (equivalent to smp_mb()) + INSTRUCTION_SCHED_DEP_NEXT(); +#endif + smp_rmb(); + INSTRUCTION_SCHED_DEP_NEXT(); + read_one = READ_CACHED_VAR(beta); + INSTRUCTION_SCHED_END(); + + // 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); + + INSTRUCTION_SCHED_BEGIN(); + WRITE_CACHED_VAR(beta, 1); + INSTRUCTION_SCHED_DEP_NEXT(); + smp_wmb(); +#ifndef USE_SYNC_CORE + INSTRUCTION_SCHED_NODEP_NEXT(); +#else + // if we use a sync_core(); (equivalent to smp_mb()) + // INSTRUCTION_SCHED_DEP_NEXT(); +#endif + smp_rmb(); + INSTRUCTION_SCHED_DEP_NEXT(); + read_two = READ_CACHED_VAR(alpha); + INSTRUCTION_SCHED_END(); + + // 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-deps/read_order.ltl b/formal-model/ooomem-deps/read_order.ltl new file mode 100644 index 0000000..f4dbf03 --- /dev/null +++ b/formal-model/ooomem-deps/read_order.ltl @@ -0,0 +1 @@ +[] (read_one_is_zero -> !read_two_is_zero) diff --git a/formal-model/ooomem-deps/read_order_sync_core.define b/formal-model/ooomem-deps/read_order_sync_core.define new file mode 100644 index 0000000..eb80fc9 --- /dev/null +++ b/formal-model/ooomem-deps/read_order_sync_core.define @@ -0,0 +1 @@ +#define USE_SYNC_CORE diff --git a/formal-model/ooomem-deps/references.txt b/formal-model/ooomem-deps/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/ooomem-deps/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