From 710b09b7ba5203ea868240c1746d0ac0fc65f884 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Mon, 23 Feb 2009 02:02:54 -0500 Subject: [PATCH] dual writer fix Make mutex between writers really atomic. Fixes the two flips run. Signed-off-by: Mathieu Desnoyers --- formal-model/urcu/Makefile | 4 ++-- formal-model/urcu/urcu.spin | 19 ++++++++++++------- 2 files changed, 14 insertions(+), 9 deletions(-) diff --git a/formal-model/urcu/Makefile b/formal-model/urcu/Makefile index 7802c7f..7b395cb 100644 --- a/formal-model/urcu/Makefile +++ b/formal-model/urcu/Makefile @@ -44,7 +44,7 @@ asserts: clean rm -f .input.spin.trail spin -a -X .input.spin gcc -w ${CFLAGS} -DSAFETY -o pan pan.c - ./pan -v -c1 -X -m10000 -w19 + ./pan -v -c1 -X -m10000 -w20 cp .input.spin $@.spin.input -cp .input.spin.trail $@.spin.input.trail @@ -87,7 +87,7 @@ urcu_free_ltl: spin -f "!(`cat urcu_free.ltl | grep -v ^//`)" >> pan.ltl run: pan - ./pan -a -v -c1 -X -m10000 -w19 + ./pan -a -v -c1 -X -m10000 -w20 pan: pan.c gcc -w ${CFLAGS} -o pan pan.c diff --git a/formal-model/urcu/urcu.spin b/formal-model/urcu/urcu.spin index 7f94d3b..5ac2f02 100644 --- a/formal-model/urcu/urcu.spin +++ b/formal-model/urcu/urcu.spin @@ -225,11 +225,16 @@ active [NR_WRITERS] proctype urcu_writer() ooo_mem(i); do - :: write_lock == 0 -> - write_lock = 1; - break; - :: else -> - skip; + :: 1 -> + atomic { + if + :: write_lock == 0 -> + write_lock = 1; + break; + :: else -> + skip; + fi; + } od; smp_mb(i); ooo_mem(i); @@ -251,11 +256,11 @@ active [NR_WRITERS] proctype urcu_writer() #endif ooo_mem(i); smp_mb(i); - /* free-up step, e.g., kfree(). */ ooo_mem(i); + write_lock = 0; + /* free-up step, e.g., kfree(). */ atomic { last_free_gen = old_gen; free_done = 1; - write_lock = 0; } } -- 2.34.1