From 656c7dc16c88b6683727087013c702687dfd022b Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Sat, 26 Sep 2009 02:53:44 -0400 Subject: [PATCH] Add multicoreverif paper ticketlock and spinlock models Signed-off-by: Mathieu Desnoyers --- formal-model/spinlock/DEFINES | 1 + formal-model/spinlock/Makefile | 103 ++++++++++++++++ formal-model/spinlock/lock_progress.ltl | 1 + formal-model/spinlock/mem-progress.spin | 69 +++++++++++ formal-model/spinlock/mem.sh | 29 +++++ formal-model/spinlock/mem.spin | 57 +++++++++ formal-model/spinlock/refcount.ltl | 1 + formal-model/spinlock/references.txt | 7 ++ formal-model/ticketlock/DEFINES | 1 + formal-model/ticketlock/Makefile | 112 ++++++++++++++++++ .../ticketlock/config_4_bits_per_byte.define | 1 + formal-model/ticketlock/lock_progress.ltl | 1 + formal-model/ticketlock/mem-progress.spin | 98 +++++++++++++++ formal-model/ticketlock/mem.sh | 29 +++++ formal-model/ticketlock/mem.spin | 83 +++++++++++++ formal-model/ticketlock/refcount.ltl | 1 + formal-model/ticketlock/references.txt | 7 ++ 17 files changed, 601 insertions(+) create mode 100644 formal-model/spinlock/DEFINES create mode 100644 formal-model/spinlock/Makefile create mode 100644 formal-model/spinlock/lock_progress.ltl create mode 100644 formal-model/spinlock/mem-progress.spin create mode 100644 formal-model/spinlock/mem.sh create mode 100644 formal-model/spinlock/mem.spin create mode 100644 formal-model/spinlock/refcount.ltl create mode 100644 formal-model/spinlock/references.txt create mode 100644 formal-model/ticketlock/DEFINES create mode 100644 formal-model/ticketlock/Makefile create mode 100644 formal-model/ticketlock/config_4_bits_per_byte.define create mode 100644 formal-model/ticketlock/lock_progress.ltl create mode 100644 formal-model/ticketlock/mem-progress.spin create mode 100644 formal-model/ticketlock/mem.sh create mode 100644 formal-model/ticketlock/mem.spin create mode 100644 formal-model/ticketlock/refcount.ltl create mode 100644 formal-model/ticketlock/references.txt diff --git a/formal-model/spinlock/DEFINES b/formal-model/spinlock/DEFINES new file mode 100644 index 0000000..4eb5315 --- /dev/null +++ b/formal-model/spinlock/DEFINES @@ -0,0 +1 @@ +#define refcount_gt_one (refcount > 1) diff --git a/formal-model/spinlock/Makefile b/formal-model/spinlock/Makefile new file mode 100644 index 0000000..a153e7a --- /dev/null +++ b/formal-model/spinlock/Makefile @@ -0,0 +1,103 @@ +# 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 +SPINFILE_FAIR=mem-progress.spin + +default: + make refcount | tee refcount.log + make lock_progress | tee lock_progress.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 + +refcount: clean refcount_ltl run + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +refcount_ltl: + touch .input.define + cat DEFINES > pan.ltl + cat .input.define >> pan.ltl + spin -f "!(`cat refcount.ltl | grep -v ^//`)" >> pan.ltl + +lock_progress: clean lock_progress_ltl run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +lock_progress_ltl: + touch .input.define + cat .input.define > pan.ltl + cat DEFINES >> pan.ltl + spin -f "!(`cat lock_progress.ltl | grep -v ^//`)" >> pan.ltl + +run: pan + ./pan -a -v -c1 -X -m10000 -w19 + +run_weak_fair: pan_fair + ./pan_fair -a -f -v -c1 -X -m10000000 -w20 + +pan_fair: pan_fair.c + gcc -w ${CFLAGS} -o pan_fair pan_fair.c + +pan: pan.c + gcc -w ${CFLAGS} -o pan pan.c + +pan_fair.c: pan.ltl ${SPINFILE_FAIR} + cat DEFINES > .input.spin + cat .input.define >> .input.spin + cat ${SPINFILE_FAIR} >> .input.spin + rm -f .input.spin.trail + spin -a -X -N pan.ltl .input.spin + mv pan.c pan_fair.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/spinlock/lock_progress.ltl b/formal-model/spinlock/lock_progress.ltl new file mode 100644 index 0000000..8718641 --- /dev/null +++ b/formal-model/spinlock/lock_progress.ltl @@ -0,0 +1 @@ +([] <> !np_) diff --git a/formal-model/spinlock/mem-progress.spin b/formal-model/spinlock/mem-progress.spin new file mode 100644 index 0000000..7930d04 --- /dev/null +++ b/formal-model/spinlock/mem-progress.spin @@ -0,0 +1,69 @@ +/* + * 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 + */ + +byte lock = 0; +byte refcount = 0; + +inline spin_lock(lock) +{ + do + :: 1 -> atomic { + if + :: (lock) -> + skip; + :: else -> + lock = 1; + break; + fi; + } + od; +} + +inline spin_unlock(lock) +{ + lock = 0; +} + +proctype proc_A() +{ + do + :: 1-> +progress_A: + spin_lock(lock); + refcount = refcount + 1; + refcount = refcount - 1; + spin_unlock(lock); + od; +} + +proctype proc_B() +{ + do + :: 1-> + spin_lock(lock); + refcount = refcount + 1; + refcount = refcount - 1; + spin_unlock(lock); + od; +} + +init +{ + run proc_A(); + run proc_B(); +} diff --git a/formal-model/spinlock/mem.sh b/formal-model/spinlock/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/formal-model/spinlock/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/spinlock/mem.spin b/formal-model/spinlock/mem.spin new file mode 100644 index 0000000..9e87809 --- /dev/null +++ b/formal-model/spinlock/mem.spin @@ -0,0 +1,57 @@ +/* + * 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 + */ + +byte lock = 0; +byte refcount = 0; + +inline spin_lock(lock) +{ + do + :: 1 -> atomic { + if + :: (lock) -> + skip; + :: else -> + lock = 1; + break; + fi; + } + od; +} + +inline spin_unlock(lock) +{ + lock = 0; +} + +proctype proc_X() +{ + do + :: 1 -> + spin_lock(lock); + refcount = refcount + 1; + refcount = refcount - 1; + spin_unlock(lock); + od; +} + +init +{ + run proc_X(); + run proc_X(); +} diff --git a/formal-model/spinlock/refcount.ltl b/formal-model/spinlock/refcount.ltl new file mode 100644 index 0000000..48f971f --- /dev/null +++ b/formal-model/spinlock/refcount.ltl @@ -0,0 +1 @@ +[] (!(refcount_gt_one)) diff --git a/formal-model/spinlock/references.txt b/formal-model/spinlock/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/spinlock/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/ticketlock/DEFINES b/formal-model/ticketlock/DEFINES new file mode 100644 index 0000000..4eb5315 --- /dev/null +++ b/formal-model/ticketlock/DEFINES @@ -0,0 +1 @@ +#define refcount_gt_one (refcount > 1) diff --git a/formal-model/ticketlock/Makefile b/formal-model/ticketlock/Makefile new file mode 100644 index 0000000..c41afd3 --- /dev/null +++ b/formal-model/ticketlock/Makefile @@ -0,0 +1,112 @@ +# 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 +SPINFILE_FAIR=mem-progress.spin + +default: + make refcount | tee refcount.log + make refcount_4_bits_per_byte | tee refcount_4_bits_per_byte.log + make lock_progress | tee lock_progress.log + make lock_progress_4_bits_per_byte | tee lock_progress_4_bits_per_byte.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 -m10000000 -w19 + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +refcount: clean refcount_ltl run + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +refcount_ltl: + touch .input.define + cat DEFINES > pan.ltl + cat .input.define >> pan.ltl + spin -f "!(`cat refcount.ltl | grep -v ^//`)" >> pan.ltl + +refcount_4_bits_per_byte: clean refcount_ltl config_4_bits_per_byte_define run + +lock_progress: clean lock_progress_ltl run_weak_fair + cp .input.spin $@.spin.input + -cp .input.spin.trail $@.spin.input.trail + +lock_progress_ltl: + touch .input.define + cat .input.define > pan.ltl + cat DEFINES >> pan.ltl + spin -f "!(`cat lock_progress.ltl | grep -v ^//`)" >> pan.ltl + +lock_progress_4_bits_per_byte: clean lock_progress_ltl config_4_bits_per_byte_define run + +config_4_bits_per_byte_define: + cp config_4_bits_per_byte.define .input.define + +run: pan + ./pan -a -v -c1 -X -m1000000 -w19 + +run_weak_fair: pan_fair + ./pan_fair -a -f -v -c1 -X -m1000000 -w20 + +pan_fair: pan_fair.c + gcc -w ${CFLAGS} -DNFAIR=4 -o pan_fair pan_fair.c + +pan: pan.c + gcc -w ${CFLAGS} -o pan pan.c + +pan_fair.c: pan.ltl ${SPINFILE_FAIR} + cat DEFINES > .input.spin + cat .input.define >> .input.spin + cat ${SPINFILE_FAIR} >> .input.spin + rm -f .input.spin.trail + spin -a -X -N pan.ltl .input.spin + mv pan.c pan_fair.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/ticketlock/config_4_bits_per_byte.define b/formal-model/ticketlock/config_4_bits_per_byte.define new file mode 100644 index 0000000..e1d13ca --- /dev/null +++ b/formal-model/ticketlock/config_4_bits_per_byte.define @@ -0,0 +1 @@ +#define CONFIG_BITS_PER_BYTE 4 diff --git a/formal-model/ticketlock/lock_progress.ltl b/formal-model/ticketlock/lock_progress.ltl new file mode 100644 index 0000000..8718641 --- /dev/null +++ b/formal-model/ticketlock/lock_progress.ltl @@ -0,0 +1 @@ +([] <> !np_) diff --git a/formal-model/ticketlock/mem-progress.spin b/formal-model/ticketlock/mem-progress.spin new file mode 100644 index 0000000..dad43a4 --- /dev/null +++ b/formal-model/ticketlock/mem-progress.spin @@ -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) 2009 Mathieu Desnoyers + */ + +/* 16 CPUs max (byte has 8 bits, divided in two) */ + +#ifndef CONFIG_BITS_PER_BYTE +#define BITS_PER_BYTE 8 +#else +// test progress failure with shorter byte size. Will fail with 5 proc. +#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE +#endif + +#define HBPB (BITS_PER_BYTE / 2) /* 4 */ +#define HMASK ((1 << HBPB) - 1) /* 0x0F */ + +/* for byte type */ +#define LOW_HALF(val) ((val) & HMASK) +#define LOW_HALF_INC 1 + +#define HIGH_HALF(val) ((val) & (HMASK << HBPB)) +#define HIGH_HALF_INC (1 << HBPB) + +byte lock = 0; +byte refcount = 0; + +inline spin_lock(lock, ticket) +{ + atomic { + ticket = HIGH_HALF(lock) >> HBPB; + lock = lock + HIGH_HALF_INC; /* overflow expected */ + } + + do + :: 1 -> + if + :: (LOW_HALF(lock) == ticket) -> + break; + :: else -> + skip; + fi; + od; +} + +inline spin_unlock(lock) +{ + lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC); +} + +proctype proc_A() +{ + byte ticket; + + do + :: 1 -> +progress_A: + spin_lock(lock, ticket); + refcount = refcount + 1; + refcount = refcount - 1; + spin_unlock(lock); + od; +} + +proctype proc_B() +{ + byte ticket; + + do + :: 1 -> + spin_lock(lock, ticket); + refcount = refcount + 1; + refcount = refcount - 1; + spin_unlock(lock); + od; +} + +init +{ + run proc_A(); + run proc_B(); + run proc_B(); + run proc_B(); + run proc_B(); +} diff --git a/formal-model/ticketlock/mem.sh b/formal-model/ticketlock/mem.sh new file mode 100644 index 0000000..56e8123 --- /dev/null +++ b/formal-model/ticketlock/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/ticketlock/mem.spin b/formal-model/ticketlock/mem.spin new file mode 100644 index 0000000..445ee9a --- /dev/null +++ b/formal-model/ticketlock/mem.spin @@ -0,0 +1,83 @@ +/* + * 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 + */ + +/* 16 CPUs max (byte has 8 bits, divided in two) */ + +#ifndef CONFIG_BITS_PER_BYTE +#define BITS_PER_BYTE 8 +#else +#define BITS_PER_BYTE CONFIG_BITS_PER_BYTE +#endif + +#define HBPB (BITS_PER_BYTE / 2) /* 4 */ +#define HMASK ((1 << HBPB) - 1) /* 0x0F */ + +/* for byte type */ +#define LOW_HALF(val) ((val) & HMASK) +#define LOW_HALF_INC 1 + +#define HIGH_HALF(val) ((val) & (HMASK << HBPB)) +#define HIGH_HALF_INC (1 << HBPB) + +byte lock = 0; +byte refcount = 0; + +inline spin_lock(lock, ticket) +{ + atomic { + ticket = HIGH_HALF(lock) >> HBPB; + lock = lock + HIGH_HALF_INC; /* overflow expected */ + } + + do + :: 1 -> + if + :: (LOW_HALF(lock) == ticket) -> + break; + :: else -> + skip; + fi; + od; +} + +inline spin_unlock(lock) +{ + lock = HIGH_HALF(lock) | LOW_HALF(lock + LOW_HALF_INC); +} + +proctype proc_X() +{ + byte ticket; + + do + :: 1-> + spin_lock(lock, ticket); + refcount = refcount + 1; + refcount = refcount - 1; + spin_unlock(lock); + od; +} + +init +{ + run proc_X(); + run proc_X(); + run proc_X(); + run proc_X(); + run proc_X(); +} diff --git a/formal-model/ticketlock/refcount.ltl b/formal-model/ticketlock/refcount.ltl new file mode 100644 index 0000000..48f971f --- /dev/null +++ b/formal-model/ticketlock/refcount.ltl @@ -0,0 +1 @@ +[] (!(refcount_gt_one)) diff --git a/formal-model/ticketlock/references.txt b/formal-model/ticketlock/references.txt new file mode 100644 index 0000000..ca6798f --- /dev/null +++ b/formal-model/ticketlock/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