From d149fa02aaafa08c2d02712afd3cbbbc5f8d5f67 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Mon, 8 Oct 2012 17:48:58 -0400 Subject: [PATCH] ticketlock model: state-space simplication Signed-off-by: Mathieu Desnoyers --- ticketlock/mem-progress.spin | 18 +++++------------- ticketlock/mem.spin | 14 +++----------- 2 files changed, 8 insertions(+), 24 deletions(-) diff --git a/ticketlock/mem-progress.spin b/ticketlock/mem-progress.spin index dad43a4..b739541 100644 --- a/ticketlock/mem-progress.spin +++ b/ticketlock/mem-progress.spin @@ -45,15 +45,8 @@ inline spin_lock(lock, ticket) lock = lock + HIGH_HALF_INC; /* overflow expected */ } - do - :: 1 -> - if - :: (LOW_HALF(lock) == ticket) -> - break; - :: else -> - skip; - fi; - od; + /* busy-wait */ + LOW_HALF(lock) == ticket -> 1; } inline spin_unlock(lock) @@ -66,9 +59,9 @@ proctype proc_A() byte ticket; do - :: 1 -> -progress_A: + :: spin_lock(lock, ticket); +progress_A: refcount = refcount + 1; refcount = refcount - 1; spin_unlock(lock); @@ -80,8 +73,7 @@ proctype proc_B() byte ticket; do - :: 1 -> - spin_lock(lock, ticket); + :: spin_lock(lock, ticket); refcount = refcount + 1; refcount = refcount - 1; spin_unlock(lock); diff --git a/ticketlock/mem.spin b/ticketlock/mem.spin index 445ee9a..59acfcf 100644 --- a/ticketlock/mem.spin +++ b/ticketlock/mem.spin @@ -44,15 +44,8 @@ inline spin_lock(lock, ticket) lock = lock + HIGH_HALF_INC; /* overflow expected */ } - do - :: 1 -> - if - :: (LOW_HALF(lock) == ticket) -> - break; - :: else -> - skip; - fi; - od; + /* busy-wait */ + LOW_HALF(lock) == ticket -> 1; } inline spin_unlock(lock) @@ -65,8 +58,7 @@ proctype proc_X() byte ticket; do - :: 1-> - spin_lock(lock, ticket); + :: spin_lock(lock, ticket); refcount = refcount + 1; refcount = refcount - 1; spin_unlock(lock); -- 2.34.1