From 2937ba8c50d24a3b72aabe4c3e6e827fe37f0c91 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Tue, 9 Oct 2012 00:12:47 -0400 Subject: [PATCH] Revert "spinlock model: Simplify state-space" This reverts commit a9227ee907160443d0e4b1639b274ab9278d92fa. Need to study impact on progress. Signed-off-by: Mathieu Desnoyers --- spinlock/mem.spin | 15 +++++++++++++-- 1 file changed, 13 insertions(+), 2 deletions(-) diff --git a/spinlock/mem.spin b/spinlock/mem.spin index 072d4d2..9e87809 100644 --- a/spinlock/mem.spin +++ b/spinlock/mem.spin @@ -21,7 +21,17 @@ byte refcount = 0; inline spin_lock(lock) { - atomic{ !lock -> lock = 1} + do + :: 1 -> atomic { + if + :: (lock) -> + skip; + :: else -> + lock = 1; + break; + fi; + } + od; } inline spin_unlock(lock) @@ -32,7 +42,8 @@ inline spin_unlock(lock) proctype proc_X() { do - :: spin_lock(lock); + :: 1 -> + spin_lock(lock); refcount = refcount + 1; refcount = refcount - 1; spin_unlock(lock); -- 2.34.1