From 60a1db9d10aaca98e79a5126f168a37d00151845 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Mon, 23 Feb 2009 00:53:37 -0500 Subject: [PATCH] Add ooomem and urcu checks Create a more simple model for ooo memory accesses and basic urcu checks. Signed-off-by: Mathieu Desnoyers --- formal-model/ooomem/DEFINES | 2 + formal-model/ooomem/Makefile | 90 +++++++ formal-model/ooomem/mem.sh | 29 +++ formal-model/ooomem/mem.spin | 161 ++++++++++++ formal-model/ooomem/read_order.ltl | 1 + formal-model/ooomem/read_order_no_rmb.define | 1 + formal-model/ooomem/read_order_no_wmb.define | 1 + formal-model/ooomem/references.txt | 7 + formal-model/urcu/DEFINES | 5 + formal-model/urcu/Makefile | 98 ++++++++ formal-model/urcu/references.txt | 7 + formal-model/urcu/urcu.sh | 29 +++ formal-model/urcu/urcu.spin | 249 +++++++++++++++++++ formal-model/urcu/urcu_free.ltl | 1 + formal-model/urcu/urcu_free_no_mb.define | 2 + formal-model/urcu/urcu_free_no_rmb.define | 1 + formal-model/urcu/urcu_free_no_wmb.define | 1 + 17 files changed, 685 insertions(+) create mode 100644 formal-model/ooomem/DEFINES create mode 100644 formal-model/ooomem/Makefile create mode 100644 formal-model/ooomem/mem.sh create mode 100644 formal-model/ooomem/mem.spin create mode 100644 formal-model/ooomem/read_order.ltl create mode 100644 formal-model/ooomem/read_order_no_rmb.define create mode 100644 formal-model/ooomem/read_order_no_wmb.define create mode 100644 formal-model/ooomem/references.txt create mode 100644 formal-model/urcu/DEFINES create mode 100644 formal-model/urcu/Makefile create mode 100644 formal-model/urcu/references.txt create mode 100644 formal-model/urcu/urcu.sh create mode 100644 formal-model/urcu/urcu.spin create mode 100644 formal-model/urcu/urcu_free.ltl create mode 100644 formal-model/urcu/urcu_free_no_mb.define create mode 100644 formal-model/urcu/urcu_free_no_rmb.define create mode 100644 formal-model/urcu/urcu_free_no_wmb.define diff --git a/formal-model/ooomem/DEFINES b/formal-model/ooomem/DEFINES new file mode 100644 index 0000000..04aa898 --- /dev/null +++ b/formal-model/ooomem/DEFINES @@ -0,0 +1,2 @@ +#define first_read_updated (first_read[0] == 6) +#define second_read_updated (second_read[0] == 4) diff --git a/formal-model/ooomem/Makefile b/formal-model/ooomem/Makefile new file mode 100644 index 0000000..e0aed43 --- /dev/null +++ b/formal-model/ooomem/Makefile @@ -0,0 +1,90 @@ +# 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_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/mem.sh b/formal-model/ooomem/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/formal-model/ooomem/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/mem.spin b/formal-model/ooomem/mem.spin new file mode 100644 index 0000000..a7f2d7d --- /dev/null +++ b/formal-model/ooomem/mem.spin @@ -0,0 +1,161 @@ +/* + * 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()); + } +} + +#define get_readerid() (get_pid()) + +byte first_read[NR_READERS]; +byte second_read[NR_READERS]; + +active [NR_READERS] proctype test_reader() +{ + assert(get_pid() < NR_PROCS); + + ooo_mem(); + first_read[get_readerid()] = READ_CACHED_VAR(beta); + ooo_mem(); +#ifndef NO_RMB + smp_rmb(); + ooo_mem(); +#endif + second_read[get_readerid()] = READ_CACHED_VAR(alpha); + ooo_mem(); + // test : [] (first_read == 6 -> <> second_read == 4) + assert(first_read[get_readerid()] != 6 + || second_read[get_readerid()] == 4); +} + +#define get_writerid() (get_readerid() + NR_READERS) + +active [NR_WRITERS] proctype test_writer() +{ + byte i; + + assert(get_pid() < NR_PROCS); + + ooo_mem(); + WRITE_CACHED_VAR(alpha, 4); + ooo_mem(); +#ifndef NO_WMB + smp_wmb(); + ooo_mem(); +#endif + WRITE_CACHED_VAR(beta, 6); + ooo_mem(); +} diff --git a/formal-model/ooomem/read_order.ltl b/formal-model/ooomem/read_order.ltl new file mode 100644 index 0000000..b1cdfb7 --- /dev/null +++ b/formal-model/ooomem/read_order.ltl @@ -0,0 +1 @@ +[] (first_read_updated -> <> second_read_updated) diff --git a/formal-model/ooomem/read_order_no_rmb.define b/formal-model/ooomem/read_order_no_rmb.define new file mode 100644 index 0000000..73e61a4 --- /dev/null +++ b/formal-model/ooomem/read_order_no_rmb.define @@ -0,0 +1 @@ +#define NO_RMB diff --git a/formal-model/ooomem/read_order_no_wmb.define b/formal-model/ooomem/read_order_no_wmb.define new file mode 100644 index 0000000..710f29d --- /dev/null +++ b/formal-model/ooomem/read_order_no_wmb.define @@ -0,0 +1 @@ +#define NO_WMB diff --git a/formal-model/ooomem/references.txt b/formal-model/ooomem/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/ooomem/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/urcu/DEFINES b/formal-model/urcu/DEFINES new file mode 100644 index 0000000..855dbd5 --- /dev/null +++ b/formal-model/urcu/DEFINES @@ -0,0 +1,5 @@ +#define RCU_GP_CTR_BIT (1 << 7) +#define RCU_GP_CTR_NEST_MASK (RCU_GP_CTR_BIT - 1) + +#define read_free_race (read_generation == last_free_gen) +#define read_free (free_done && data_access) diff --git a/formal-model/urcu/Makefile b/formal-model/urcu/Makefile new file mode 100644 index 0000000..0dc8b2c --- /dev/null +++ b/formal-model/urcu/Makefile @@ -0,0 +1,98 @@ +# 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=urcu.spin + +default: + make urcu_free | tee urcu_free.log + make urcu_free_no_rmb | tee urcu_free_no_rmb.log + make urcu_free_no_wmb | tee urcu_free_no_wmb.log + make urcu_free_no_mb | tee urcu_free_no_mb.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 + +urcu_free: clean urcu_free_ltl run + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +urcu_free_no_rmb: clean urcu_free_ltl urcu_free_no_rmb_define run + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +urcu_free_no_rmb_define: + cp urcu_free_no_rmb.define .input.define + +urcu_free_no_wmb: clean urcu_free_ltl urcu_free_no_wmb_define run + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +urcu_free_no_wmb_define: + cp urcu_free_no_wmb.define .input.define + +urcu_free_no_mb: clean urcu_free_ltl urcu_free_no_mb_define run + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +urcu_free_no_mb_define: + cp urcu_free_no_mb.define .input.define + +urcu_free_ltl: + touch .input.define + cat DEFINES > pan.ltl + cat .input.define >> pan.ltl + spin -f "!(`cat urcu_free.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/urcu/references.txt b/formal-model/urcu/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/urcu/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/urcu/urcu.sh b/formal-model/urcu/urcu.sh new file mode 100644 index 0000000..65ff517 --- /dev/null +++ b/formal-model/urcu/urcu.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 urcu.spin +cc -DSAFETY -o pan pan.c +./pan -v -c1 -X -m10000000 -w21 diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin new file mode 100644 index 0000000..cc84e51 --- /dev/null +++ b/formal-model/urcu/urcu.spin @@ -0,0 +1,249 @@ +/* + * 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(i) +{ + atomic { + CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); + CACHE_READ_FROM_MEM(urcu_active_readers_one, get_pid()); + CACHE_READ_FROM_MEM(generation_ptr, get_pid()); + } +} + +inline smp_wmb(i) +{ + atomic { + CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); + CACHE_WRITE_TO_MEM(urcu_active_readers_one, get_pid()); + CACHE_WRITE_TO_MEM(generation_ptr, get_pid()); + } +} + +inline smp_mb(i) +{ + atomic { +#ifndef NO_WMB + smp_wmb(i); +#endif +#ifndef NO_RMB + smp_rmb(i); +#endif + skip; + } +} + +/* Keep in sync manually with smp_rmb, wmp_wmb and ooo_mem */ +DECLARE_CACHED_VAR(byte, urcu_gp_ctr, 1); +/* Note ! currently only one reader */ +DECLARE_CACHED_VAR(byte, urcu_active_readers_one, 0); +/* pointer generation */ +DECLARE_CACHED_VAR(byte, generation_ptr, 0); + +byte last_free_gen = 0; +bit free_done = 0; +byte read_generation = 1; +bit data_access = 0; + +inline ooo_mem(i) +{ + atomic { + RANDOM_CACHE_WRITE_TO_MEM(urcu_gp_ctr, get_pid()); + RANDOM_CACHE_WRITE_TO_MEM(urcu_active_readers_one, + get_pid()); + RANDOM_CACHE_WRITE_TO_MEM(generation_ptr, get_pid()); + RANDOM_CACHE_READ_FROM_MEM(urcu_gp_ctr, get_pid()); + RANDOM_CACHE_READ_FROM_MEM(urcu_active_readers_one, + get_pid()); + RANDOM_CACHE_READ_FROM_MEM(generation_ptr, get_pid()); + } +} + +#define get_readerid() (get_pid()) +#define get_writerid() (get_readerid() + NR_READERS) + +inline wait_for_reader(tmp, id, i) +{ + tmp = READ_CACHED_VAR(urcu_active_readers_one); + ooo_mem(i); + do + :: (tmp & RCU_GP_CTR_NEST_MASK) && ((tmp ^ READ_CACHED_VAR(urcu_gp_ctr)) + & RCU_GP_CTR_BIT) + -> + ooo_mem(i); + skip; + :: else -> + break; + od; +} + +inline wait_for_quiescent_state(tmp, i, j) +{ + i = 0; + do + :: i < NR_READERS -> + wait_for_reader(tmp, i, j); + i++ + :: i >= NR_READERS -> break + od; +} + +/* Model the RCU read-side critical section. */ + +active [NR_READERS] proctype urcu_reader() +{ + byte i; + byte tmp, tmp2; + + assert(get_pid() < NR_PROCS); + + ooo_mem(i); + tmp = READ_CACHED_VAR(urcu_active_readers_one); + ooo_mem(i); + if + :: (!(tmp & RCU_GP_CTR_NEST_MASK)) + -> + tmp2 = READ_CACHED_VAR(urcu_gp_ctr); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_active_readers_one, tmp2); + :: else -> + WRITE_CACHED_VAR(urcu_active_readers_one, tmp + 1); + fi; + ooo_mem(i); + smp_mb(i); + read_generation = READ_CACHED_VAR(generation_ptr); + ooo_mem(i); + data_access = 1; + ooo_mem(i); + data_access = 0; + ooo_mem(i); + smp_mb(i); + ooo_mem(i); + tmp2 = READ_CACHED_VAR(urcu_active_readers_one); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_active_readers_one, tmp2 - 1); + ooo_mem(i); + //smp_mc(i); /* added */ +} + + +/* Model the RCU update process. */ + +active [NR_WRITERS] proctype urcu_writer() +{ + byte i, j; + byte tmp; + byte old_gen; + + assert(get_pid() < NR_PROCS); + + ooo_mem(i); + atomic { + old_gen = READ_CACHED_VAR(generation_ptr); + WRITE_CACHED_VAR(generation_ptr, old_gen + 1); + } + ooo_mem(i); + + smp_mb(i); + ooo_mem(i); + tmp = READ_CACHED_VAR(urcu_gp_ctr); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT); + ooo_mem(i); + //smp_mc(i); + wait_for_quiescent_state(tmp, i, j); + //smp_mc(i); + ooo_mem(i); + tmp = READ_CACHED_VAR(urcu_gp_ctr); + ooo_mem(i); + WRITE_CACHED_VAR(urcu_gp_ctr, tmp ^ RCU_GP_CTR_BIT); + //smp_mc(i); + ooo_mem(i); + wait_for_quiescent_state(tmp, i, j); + ooo_mem(i); + smp_mb(i); + /* free-up step, e.g., kfree(). */ + ooo_mem(i); + atomic { + last_free_gen = old_gen; + free_done = 1; + } +} diff --git a/formal-model/urcu/urcu_free.ltl b/formal-model/urcu/urcu_free.ltl new file mode 100644 index 0000000..1954414 --- /dev/null +++ b/formal-model/urcu/urcu_free.ltl @@ -0,0 +1 @@ +[] (read_free -> !read_free_race) diff --git a/formal-model/urcu/urcu_free_no_mb.define b/formal-model/urcu/urcu_free_no_mb.define new file mode 100644 index 0000000..136ef67 --- /dev/null +++ b/formal-model/urcu/urcu_free_no_mb.define @@ -0,0 +1,2 @@ +#define NO_RMB +#define NO_WMB diff --git a/formal-model/urcu/urcu_free_no_rmb.define b/formal-model/urcu/urcu_free_no_rmb.define new file mode 100644 index 0000000..73e61a4 --- /dev/null +++ b/formal-model/urcu/urcu_free_no_rmb.define @@ -0,0 +1 @@ +#define NO_RMB diff --git a/formal-model/urcu/urcu_free_no_wmb.define b/formal-model/urcu/urcu_free_no_wmb.define new file mode 100644 index 0000000..710f29d --- /dev/null +++ b/formal-model/urcu/urcu_free_no_wmb.define @@ -0,0 +1 @@ +#define NO_WMB -- 2.34.1