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