From 821586101518e2cfa82b1c33f9e78d75f43c6dc6 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Mon, 6 Apr 2009 16:30:04 -0400 Subject: [PATCH] Check double write read order Check the following scenario : > > P.S.: Regarding very weak memory-ordering models, I recall that in our > > earlier discussions we considered this scenario: > > CPU 0 CPU 1 > > ----- ----- > > x = 1; y = 1; > > mb(); mb(); > > read y read x > > with the question being whether it was possible for both reads to > > obtain the value 0. With sufficiently weak ordering it is possible, > > but it turned out that there are places in the Linux kernel (I don't > > remember where) that essentially assume this cannot happen. Have you > > gotten far enough in your outline of the semi-formal model to address > > this sort of question? --- formal-model/ooomem-double-update/DEFINES | 2 + formal-model/ooomem-double-update/Makefile | 92 ++++++++++ formal-model/ooomem-double-update/mem.sh | 29 +++ formal-model/ooomem-double-update/mem.spin | 167 ++++++++++++++++++ .../ooomem-double-update/read_order.ltl | 1 + .../read_order_no_rmb.define | 1 + .../read_order_no_wmb.define | 1 + .../ooomem-double-update/references.txt | 7 + 8 files changed, 300 insertions(+) create mode 100644 formal-model/ooomem-double-update/DEFINES create mode 100644 formal-model/ooomem-double-update/Makefile create mode 100644 formal-model/ooomem-double-update/mem.sh create mode 100644 formal-model/ooomem-double-update/mem.spin create mode 100644 formal-model/ooomem-double-update/read_order.ltl create mode 100644 formal-model/ooomem-double-update/read_order_no_rmb.define create mode 100644 formal-model/ooomem-double-update/read_order_no_wmb.define create mode 100644 formal-model/ooomem-double-update/references.txt diff --git a/formal-model/ooomem-double-update/DEFINES b/formal-model/ooomem-double-update/DEFINES new file mode 100644 index 0000000..e74150d --- /dev/null +++ b/formal-model/ooomem-double-update/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-double-update/Makefile b/formal-model/ooomem-double-update/Makefile new file mode 100644 index 0000000..09107bc --- /dev/null +++ b/formal-model/ooomem-double-update/Makefile @@ -0,0 +1,92 @@ +# 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 + +#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 -i -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 -i -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/mem.sh b/formal-model/ooomem-double-update/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/formal-model/ooomem-double-update/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/mem.spin b/formal-model/ooomem-double-update/mem.spin new file mode 100644 index 0000000..4c5d6fd --- /dev/null +++ b/formal-model/ooomem-double-update/mem.spin @@ -0,0 +1,167 @@ +/* + * 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(); + } +} + +/* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */ +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; + +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(); +#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)); +} + +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(); +#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)); +} diff --git a/formal-model/ooomem-double-update/read_order.ltl b/formal-model/ooomem-double-update/read_order.ltl new file mode 100644 index 0000000..f4dbf03 --- /dev/null +++ b/formal-model/ooomem-double-update/read_order.ltl @@ -0,0 +1 @@ +[] (read_one_is_zero -> !read_two_is_zero) diff --git a/formal-model/ooomem-double-update/read_order_no_rmb.define b/formal-model/ooomem-double-update/read_order_no_rmb.define new file mode 100644 index 0000000..73e61a4 --- /dev/null +++ b/formal-model/ooomem-double-update/read_order_no_rmb.define @@ -0,0 +1 @@ +#define NO_RMB diff --git a/formal-model/ooomem-double-update/read_order_no_wmb.define b/formal-model/ooomem-double-update/read_order_no_wmb.define new file mode 100644 index 0000000..710f29d --- /dev/null +++ b/formal-model/ooomem-double-update/read_order_no_wmb.define @@ -0,0 +1 @@ +#define NO_WMB diff --git a/formal-model/ooomem-double-update/references.txt b/formal-model/ooomem-double-update/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/ooomem-double-update/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