From 29f38067765e2d60bbf9bebcf6b7d3084b8bdec0 Mon Sep 17 00:00:00 2001 From: Mathieu Desnoyers Date: Sat, 26 Sep 2009 08:19:26 -0400 Subject: [PATCH] Add multiple reader queues to futex model Signed-off-by: Mathieu Desnoyers --- formal-model/futex-wakeup/DEFINES | 2 +- formal-model/futex-wakeup/futex.spin | 25 ++++++++++++++++++------- 2 files changed, 19 insertions(+), 8 deletions(-) diff --git a/formal-model/futex-wakeup/DEFINES b/formal-model/futex-wakeup/DEFINES index 7c9a54f..e328b55 100644 --- a/formal-model/futex-wakeup/DEFINES +++ b/formal-model/futex-wakeup/DEFINES @@ -1 +1 @@ -#define queue_has_entry (queue == 1) +#define queue_has_entry (queue[0] == 1 || queue[1] == 1) diff --git a/formal-model/futex-wakeup/futex.spin b/formal-model/futex-wakeup/futex.spin index 1cb6442..5459a53 100644 --- a/formal-model/futex-wakeup/futex.spin +++ b/formal-model/futex-wakeup/futex.spin @@ -46,12 +46,16 @@ * Copyright (c) 2009 Mathieu Desnoyers */ -int queue = 0; +#define get_pid() (_pid) + +int queue[2] = 0; int fut = 0; -active proctype waker() +active [2] proctype waker() { - queue = 1; + assert(get_pid() < 2); + + queue[get_pid()] = 1; if :: (fut == -1) -> @@ -60,7 +64,7 @@ active proctype waker() skip; fi; - queue = 1; + queue[get_pid()] = 1; if :: (fut == -1) -> @@ -70,7 +74,7 @@ active proctype waker() fi; #ifdef INJ_QUEUE_NO_WAKE - queue = 1; + queue[get_pid()] = 1; #endif } @@ -83,7 +87,7 @@ active proctype waiter() fut = fut - 1; #endif if - :: (queue == 1) -> + :: (queue[0] == 1 || queue[1] == 1) -> #ifndef INJ_LATE_DEC fut = 0; #endif @@ -108,6 +112,13 @@ active proctype waiter() fi; fi; progress: - queue = 0; + if + :: queue[0] == 1 -> + queue[0] = 0; + fi; + if + :: queue[1] == 1 -> + queue[1] = 0; + fi; od; } -- 2.34.1