Import QEMU upstream snapshot d2e570c
Upstream: https://gitlab.com/qemu-project/qemu.git Upstream-Commit: d2e570cc0f97b936902a5b1b86b73c0f5998b475
This commit is contained in:
@@ -0,0 +1,93 @@
|
||||
/*
|
||||
* This model describes the interaction between ctx->notify_me
|
||||
* and aio_notify().
|
||||
*
|
||||
* Author: Paolo Bonzini <[email protected]>
|
||||
*
|
||||
* This file is in the public domain. If you really want a license,
|
||||
* the WTFPL will do.
|
||||
*
|
||||
* To simulate it:
|
||||
* spin -p docs/aio_notify.promela
|
||||
*
|
||||
* To verify it:
|
||||
* spin -a docs/aio_notify.promela
|
||||
* gcc -O2 pan.c
|
||||
* ./a.out -a
|
||||
*
|
||||
* To verify it (with a bug planted in the model):
|
||||
* spin -a -DBUG docs/aio_notify.promela
|
||||
* gcc -O2 pan.c
|
||||
* ./a.out -a
|
||||
*/
|
||||
|
||||
#define MAX 4
|
||||
#define LAST (1 << (MAX - 1))
|
||||
#define FINAL ((LAST << 1) - 1)
|
||||
|
||||
bool notify_me;
|
||||
bool event;
|
||||
|
||||
int req;
|
||||
int done;
|
||||
|
||||
active proctype waiter()
|
||||
{
|
||||
int fetch;
|
||||
|
||||
do
|
||||
:: true -> {
|
||||
notify_me++;
|
||||
|
||||
if
|
||||
#ifndef BUG
|
||||
:: (req > 0) -> skip;
|
||||
#endif
|
||||
:: else ->
|
||||
// Wait for a nudge from the other side
|
||||
do
|
||||
:: event == 1 -> { event = 0; break; }
|
||||
od;
|
||||
fi;
|
||||
|
||||
notify_me--;
|
||||
|
||||
atomic { fetch = req; req = 0; }
|
||||
done = done | fetch;
|
||||
}
|
||||
od
|
||||
}
|
||||
|
||||
active proctype notifier()
|
||||
{
|
||||
int next = 1;
|
||||
|
||||
do
|
||||
:: next <= LAST -> {
|
||||
// generate a request
|
||||
req = req | next;
|
||||
next = next << 1;
|
||||
|
||||
// aio_notify
|
||||
if
|
||||
:: notify_me == 1 -> event = 1;
|
||||
:: else -> printf("Skipped event_notifier_set\n"); skip;
|
||||
fi;
|
||||
|
||||
// Test both synchronous and asynchronous delivery
|
||||
if
|
||||
:: 1 -> do
|
||||
:: req == 0 -> break;
|
||||
od;
|
||||
:: 1 -> skip;
|
||||
fi;
|
||||
}
|
||||
od;
|
||||
}
|
||||
|
||||
never { /* [] done < FINAL */
|
||||
accept_init:
|
||||
do
|
||||
:: done < FINAL -> skip;
|
||||
od;
|
||||
}
|
||||
@@ -0,0 +1,152 @@
|
||||
/*
|
||||
* This model describes the interaction between ctx->notified
|
||||
* and ctx->notifier.
|
||||
*
|
||||
* Author: Paolo Bonzini <[email protected]>
|
||||
*
|
||||
* This file is in the public domain. If you really want a license,
|
||||
* the WTFPL will do.
|
||||
*
|
||||
* To verify the buggy version:
|
||||
* spin -a -DBUG1 docs/aio_notify_bug.promela
|
||||
* gcc -O2 pan.c
|
||||
* ./a.out -a -f
|
||||
* (or -DBUG2)
|
||||
*
|
||||
* To verify the fixed version:
|
||||
* spin -a docs/aio_notify_bug.promela
|
||||
* gcc -O2 pan.c
|
||||
* ./a.out -a -f
|
||||
*
|
||||
* Add -DCHECK_REQ to test an alternative invariant and the
|
||||
* "notify_me" optimization.
|
||||
*/
|
||||
|
||||
int notify_me;
|
||||
bool notified;
|
||||
bool event;
|
||||
bool req;
|
||||
bool notifier_done;
|
||||
|
||||
#ifdef CHECK_REQ
|
||||
#define USE_NOTIFY_ME 1
|
||||
#else
|
||||
#define USE_NOTIFY_ME 0
|
||||
#endif
|
||||
|
||||
#ifdef BUG
|
||||
#error Please define BUG1 or BUG2 instead.
|
||||
#endif
|
||||
|
||||
active proctype notifier()
|
||||
{
|
||||
do
|
||||
:: true -> {
|
||||
req = 1;
|
||||
if
|
||||
:: !USE_NOTIFY_ME || notify_me ->
|
||||
#if defined BUG1
|
||||
/* CHECK_REQ does not detect this bug! */
|
||||
notified = 1;
|
||||
event = 1;
|
||||
#elif defined BUG2
|
||||
if
|
||||
:: !notified -> event = 1;
|
||||
:: else -> skip;
|
||||
fi;
|
||||
notified = 1;
|
||||
#else
|
||||
event = 1;
|
||||
notified = 1;
|
||||
#endif
|
||||
:: else -> skip;
|
||||
fi
|
||||
}
|
||||
:: true -> break;
|
||||
od;
|
||||
notifier_done = 1;
|
||||
}
|
||||
|
||||
#define AIO_POLL \
|
||||
notify_me++; \
|
||||
if \
|
||||
:: !req -> { \
|
||||
if \
|
||||
:: event -> skip; \
|
||||
fi; \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
notify_me--; \
|
||||
\
|
||||
atomic { old = notified; notified = 0; } \
|
||||
if \
|
||||
:: old -> event = 0; \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
\
|
||||
req = 0;
|
||||
|
||||
active proctype waiter()
|
||||
{
|
||||
bool old;
|
||||
|
||||
do
|
||||
:: true -> AIO_POLL;
|
||||
od;
|
||||
}
|
||||
|
||||
/* Same as waiter(), but disappears after a while. */
|
||||
active proctype temporary_waiter()
|
||||
{
|
||||
bool old;
|
||||
|
||||
do
|
||||
:: true -> AIO_POLL;
|
||||
:: true -> break;
|
||||
od;
|
||||
}
|
||||
|
||||
#ifdef CHECK_REQ
|
||||
never {
|
||||
do
|
||||
:: req -> goto accept_if_req_not_eventually_false;
|
||||
:: true -> skip;
|
||||
od;
|
||||
|
||||
accept_if_req_not_eventually_false:
|
||||
if
|
||||
:: req -> goto accept_if_req_not_eventually_false;
|
||||
fi;
|
||||
assert(0);
|
||||
}
|
||||
|
||||
#else
|
||||
/* There must be infinitely many transitions of event as long
|
||||
* as the notifier does not exit.
|
||||
*
|
||||
* If event stayed always true, the waiters would be busy looping.
|
||||
* If event stayed always false, the waiters would be sleeping
|
||||
* forever.
|
||||
*/
|
||||
never {
|
||||
do
|
||||
:: !event -> goto accept_if_event_not_eventually_true;
|
||||
:: event -> goto accept_if_event_not_eventually_false;
|
||||
:: true -> skip;
|
||||
od;
|
||||
|
||||
accept_if_event_not_eventually_true:
|
||||
if
|
||||
:: !event && notifier_done -> do :: true -> skip; od;
|
||||
:: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
|
||||
fi;
|
||||
assert(0);
|
||||
|
||||
accept_if_event_not_eventually_false:
|
||||
if
|
||||
:: event -> goto accept_if_event_not_eventually_false;
|
||||
fi;
|
||||
assert(0);
|
||||
}
|
||||
#endif
|
||||
@@ -0,0 +1,140 @@
|
||||
/*
|
||||
* This model describes a bug in aio_notify. If ctx->notifier is
|
||||
* cleared too late, a wakeup could be lost.
|
||||
*
|
||||
* Author: Paolo Bonzini <[email protected]>
|
||||
*
|
||||
* This file is in the public domain. If you really want a license,
|
||||
* the WTFPL will do.
|
||||
*
|
||||
* To verify the buggy version:
|
||||
* spin -a -DBUG docs/aio_notify_bug.promela
|
||||
* gcc -O2 pan.c
|
||||
* ./a.out -a -f
|
||||
*
|
||||
* To verify the fixed version:
|
||||
* spin -a docs/aio_notify_bug.promela
|
||||
* gcc -O2 pan.c
|
||||
* ./a.out -a -f
|
||||
*
|
||||
* Add -DCHECK_REQ to test an alternative invariant and the
|
||||
* "notify_me" optimization.
|
||||
*/
|
||||
|
||||
int notify_me;
|
||||
bool event;
|
||||
bool req;
|
||||
bool notifier_done;
|
||||
|
||||
#ifdef CHECK_REQ
|
||||
#define USE_NOTIFY_ME 1
|
||||
#else
|
||||
#define USE_NOTIFY_ME 0
|
||||
#endif
|
||||
|
||||
active proctype notifier()
|
||||
{
|
||||
do
|
||||
:: true -> {
|
||||
req = 1;
|
||||
if
|
||||
:: !USE_NOTIFY_ME || notify_me -> event = 1;
|
||||
:: else -> skip;
|
||||
fi
|
||||
}
|
||||
:: true -> break;
|
||||
od;
|
||||
notifier_done = 1;
|
||||
}
|
||||
|
||||
#ifdef BUG
|
||||
#define AIO_POLL \
|
||||
notify_me++; \
|
||||
if \
|
||||
:: !req -> { \
|
||||
if \
|
||||
:: event -> skip; \
|
||||
fi; \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
notify_me--; \
|
||||
\
|
||||
req = 0; \
|
||||
event = 0;
|
||||
#else
|
||||
#define AIO_POLL \
|
||||
notify_me++; \
|
||||
if \
|
||||
:: !req -> { \
|
||||
if \
|
||||
:: event -> skip; \
|
||||
fi; \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
notify_me--; \
|
||||
\
|
||||
event = 0; \
|
||||
req = 0;
|
||||
#endif
|
||||
|
||||
active proctype waiter()
|
||||
{
|
||||
do
|
||||
:: true -> AIO_POLL;
|
||||
od;
|
||||
}
|
||||
|
||||
/* Same as waiter(), but disappears after a while. */
|
||||
active proctype temporary_waiter()
|
||||
{
|
||||
do
|
||||
:: true -> AIO_POLL;
|
||||
:: true -> break;
|
||||
od;
|
||||
}
|
||||
|
||||
#ifdef CHECK_REQ
|
||||
never {
|
||||
do
|
||||
:: req -> goto accept_if_req_not_eventually_false;
|
||||
:: true -> skip;
|
||||
od;
|
||||
|
||||
accept_if_req_not_eventually_false:
|
||||
if
|
||||
:: req -> goto accept_if_req_not_eventually_false;
|
||||
fi;
|
||||
assert(0);
|
||||
}
|
||||
|
||||
#else
|
||||
/* There must be infinitely many transitions of event as long
|
||||
* as the notifier does not exit.
|
||||
*
|
||||
* If event stayed always true, the waiters would be busy looping.
|
||||
* If event stayed always false, the waiters would be sleeping
|
||||
* forever.
|
||||
*/
|
||||
never {
|
||||
do
|
||||
:: !event -> goto accept_if_event_not_eventually_true;
|
||||
:: event -> goto accept_if_event_not_eventually_false;
|
||||
:: true -> skip;
|
||||
od;
|
||||
|
||||
accept_if_event_not_eventually_true:
|
||||
if
|
||||
:: !event && notifier_done -> do :: true -> skip; od;
|
||||
:: !event && !notifier_done -> goto accept_if_event_not_eventually_true;
|
||||
fi;
|
||||
assert(0);
|
||||
|
||||
accept_if_event_not_eventually_false:
|
||||
if
|
||||
:: event -> goto accept_if_event_not_eventually_false;
|
||||
fi;
|
||||
assert(0);
|
||||
}
|
||||
#endif
|
||||
@@ -0,0 +1,225 @@
|
||||
/*
|
||||
* This model describes the implementation of exclusive sections in
|
||||
* cpu-common.c (start_exclusive, end_exclusive, cpu_exec_start,
|
||||
* cpu_exec_end).
|
||||
*
|
||||
* Author: Paolo Bonzini <[email protected]>
|
||||
*
|
||||
* This file is in the public domain. If you really want a license,
|
||||
* the WTFPL will do.
|
||||
*
|
||||
* To verify it:
|
||||
* spin -a docs/tcg-exclusive.promela
|
||||
* gcc pan.c -O2
|
||||
* ./a.out -a
|
||||
*
|
||||
* Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX,
|
||||
* TEST_EXPENSIVE.
|
||||
*/
|
||||
|
||||
// Define the missing parameters for the model
|
||||
#ifndef N_CPUS
|
||||
#define N_CPUS 2
|
||||
#warning defaulting to 2 CPU processes
|
||||
#endif
|
||||
|
||||
// the expensive test is not so expensive for <= 2 CPUs
|
||||
// If the mutex is used, it's also cheap (300 MB / 4 seconds) for 3 CPUs
|
||||
// For 3 CPUs and the lock-free option it needs 1.5 GB of RAM
|
||||
#if N_CPUS <= 2 || (N_CPUS <= 3 && defined USE_MUTEX)
|
||||
#define TEST_EXPENSIVE
|
||||
#endif
|
||||
|
||||
#ifndef N_EXCLUSIVE
|
||||
# if !defined N_CYCLES || N_CYCLES <= 1 || defined TEST_EXPENSIVE
|
||||
# define N_EXCLUSIVE 2
|
||||
# warning defaulting to 2 concurrent exclusive sections
|
||||
# else
|
||||
# define N_EXCLUSIVE 1
|
||||
# warning defaulting to 1 concurrent exclusive sections
|
||||
# endif
|
||||
#endif
|
||||
#ifndef N_CYCLES
|
||||
# if N_EXCLUSIVE <= 1 || defined TEST_EXPENSIVE
|
||||
# define N_CYCLES 2
|
||||
# warning defaulting to 2 CPU cycles
|
||||
# else
|
||||
# define N_CYCLES 1
|
||||
# warning defaulting to 1 CPU cycles
|
||||
# endif
|
||||
#endif
|
||||
|
||||
|
||||
// synchronization primitives. condition variables require a
|
||||
// process-local "cond_t saved;" variable.
|
||||
|
||||
#define mutex_t byte
|
||||
#define MUTEX_LOCK(m) atomic { m == 0 -> m = 1 }
|
||||
#define MUTEX_UNLOCK(m) m = 0
|
||||
|
||||
#define cond_t int
|
||||
#define COND_WAIT(c, m) { \
|
||||
saved = c; \
|
||||
MUTEX_UNLOCK(m); \
|
||||
c != saved -> MUTEX_LOCK(m); \
|
||||
}
|
||||
#define COND_BROADCAST(c) c++
|
||||
|
||||
// this is the logic from cpu-common.c
|
||||
|
||||
mutex_t mutex;
|
||||
cond_t exclusive_cond;
|
||||
cond_t exclusive_resume;
|
||||
byte pending_cpus;
|
||||
|
||||
byte running[N_CPUS];
|
||||
byte has_waiter[N_CPUS];
|
||||
|
||||
#define exclusive_idle() \
|
||||
do \
|
||||
:: pending_cpus -> COND_WAIT(exclusive_resume, mutex); \
|
||||
:: else -> break; \
|
||||
od
|
||||
|
||||
#define start_exclusive() \
|
||||
MUTEX_LOCK(mutex); \
|
||||
exclusive_idle(); \
|
||||
pending_cpus = 1; \
|
||||
\
|
||||
i = 0; \
|
||||
do \
|
||||
:: i < N_CPUS -> { \
|
||||
if \
|
||||
:: running[i] -> has_waiter[i] = 1; pending_cpus++; \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
i++; \
|
||||
} \
|
||||
:: else -> break; \
|
||||
od; \
|
||||
\
|
||||
do \
|
||||
:: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex); \
|
||||
:: else -> break; \
|
||||
od; \
|
||||
MUTEX_UNLOCK(mutex);
|
||||
|
||||
#define end_exclusive() \
|
||||
MUTEX_LOCK(mutex); \
|
||||
pending_cpus = 0; \
|
||||
COND_BROADCAST(exclusive_resume); \
|
||||
MUTEX_UNLOCK(mutex);
|
||||
|
||||
#ifdef USE_MUTEX
|
||||
// Simple version using mutexes
|
||||
#define cpu_exec_start(id) \
|
||||
MUTEX_LOCK(mutex); \
|
||||
exclusive_idle(); \
|
||||
running[id] = 1; \
|
||||
MUTEX_UNLOCK(mutex);
|
||||
|
||||
#define cpu_exec_end(id) \
|
||||
MUTEX_LOCK(mutex); \
|
||||
running[id] = 0; \
|
||||
if \
|
||||
:: pending_cpus -> { \
|
||||
pending_cpus--; \
|
||||
if \
|
||||
:: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
MUTEX_UNLOCK(mutex);
|
||||
#else
|
||||
// Wait-free fast path, only needs mutex when concurrent with
|
||||
// an exclusive section
|
||||
#define cpu_exec_start(id) \
|
||||
running[id] = 1; \
|
||||
if \
|
||||
:: pending_cpus -> { \
|
||||
MUTEX_LOCK(mutex); \
|
||||
if \
|
||||
:: !has_waiter[id] -> { \
|
||||
running[id] = 0; \
|
||||
exclusive_idle(); \
|
||||
running[id] = 1; \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
MUTEX_UNLOCK(mutex); \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi;
|
||||
|
||||
#define cpu_exec_end(id) \
|
||||
running[id] = 0; \
|
||||
if \
|
||||
:: pending_cpus -> { \
|
||||
MUTEX_LOCK(mutex); \
|
||||
if \
|
||||
:: has_waiter[id] -> { \
|
||||
has_waiter[id] = 0; \
|
||||
pending_cpus--; \
|
||||
if \
|
||||
:: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
MUTEX_UNLOCK(mutex); \
|
||||
} \
|
||||
:: else -> skip; \
|
||||
fi
|
||||
#endif
|
||||
|
||||
// Promela processes
|
||||
|
||||
byte done_cpu;
|
||||
byte in_cpu;
|
||||
active[N_CPUS] proctype cpu()
|
||||
{
|
||||
byte id = _pid % N_CPUS;
|
||||
byte cycles = 0;
|
||||
cond_t saved;
|
||||
|
||||
do
|
||||
:: cycles == N_CYCLES -> break;
|
||||
:: else -> {
|
||||
cycles++;
|
||||
cpu_exec_start(id)
|
||||
in_cpu++;
|
||||
done_cpu++;
|
||||
in_cpu--;
|
||||
cpu_exec_end(id)
|
||||
}
|
||||
od;
|
||||
}
|
||||
|
||||
byte done_exclusive;
|
||||
byte in_exclusive;
|
||||
active[N_EXCLUSIVE] proctype exclusive()
|
||||
{
|
||||
cond_t saved;
|
||||
byte i;
|
||||
|
||||
start_exclusive();
|
||||
in_exclusive = 1;
|
||||
done_exclusive++;
|
||||
in_exclusive = 0;
|
||||
end_exclusive();
|
||||
}
|
||||
|
||||
#define LIVENESS (done_cpu == N_CPUS * N_CYCLES && done_exclusive == N_EXCLUSIVE)
|
||||
#define SAFETY !(in_exclusive && in_cpu)
|
||||
|
||||
never { /* ! ([] SAFETY && <> [] LIVENESS) */
|
||||
do
|
||||
// once the liveness property is satisfied, this is not executable
|
||||
// and the never clause is not accepted
|
||||
:: ! LIVENESS -> accept_liveness: skip
|
||||
:: 1 -> assert(SAFETY)
|
||||
od;
|
||||
}
|
||||
@@ -0,0 +1,98 @@
|
||||
/*
|
||||
* This model describes the implementation of QemuEvent in
|
||||
* util/qemu-thread-win32.c.
|
||||
*
|
||||
* Author: Paolo Bonzini <[email protected]>
|
||||
*
|
||||
* This file is in the public domain. If you really want a license,
|
||||
* the WTFPL will do.
|
||||
*
|
||||
* To verify it:
|
||||
* spin -a docs/event.promela
|
||||
* gcc -O2 pan.c -DSAFETY
|
||||
* ./a.out
|
||||
*/
|
||||
|
||||
bool event;
|
||||
int value;
|
||||
|
||||
/* Primitives for a Win32 event */
|
||||
#define RAW_RESET event = false
|
||||
#define RAW_SET event = true
|
||||
#define RAW_WAIT do :: event -> break; od
|
||||
|
||||
#if 0
|
||||
/* Basic sanity checking: test the Win32 event primitives */
|
||||
#define RESET RAW_RESET
|
||||
#define SET RAW_SET
|
||||
#define WAIT RAW_WAIT
|
||||
#else
|
||||
/* Full model: layer a userspace-only fast path on top of the RAW_*
|
||||
* primitives. SET/RESET/WAIT have exactly the same semantics as
|
||||
* RAW_SET/RAW_RESET/RAW_WAIT, but try to avoid invoking them.
|
||||
*/
|
||||
#define EV_SET 0
|
||||
#define EV_FREE 1
|
||||
#define EV_BUSY -1
|
||||
|
||||
int state = EV_FREE;
|
||||
|
||||
int xchg_result;
|
||||
#define SET if :: state != EV_SET -> \
|
||||
atomic { /* xchg_result=xchg(state, EV_SET) */ \
|
||||
xchg_result = state; \
|
||||
state = EV_SET; \
|
||||
} \
|
||||
if :: xchg_result == EV_BUSY -> RAW_SET; \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
:: else -> skip; \
|
||||
fi
|
||||
|
||||
#define RESET if :: state == EV_SET -> atomic { state = state | EV_FREE; } \
|
||||
:: else -> skip; \
|
||||
fi
|
||||
|
||||
int tmp1, tmp2;
|
||||
#define WAIT tmp1 = state; \
|
||||
if :: tmp1 != EV_SET -> \
|
||||
if :: tmp1 == EV_FREE -> \
|
||||
RAW_RESET; \
|
||||
atomic { /* tmp2=cas(state, EV_FREE, EV_BUSY) */ \
|
||||
tmp2 = state; \
|
||||
if :: tmp2 == EV_FREE -> state = EV_BUSY; \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
} \
|
||||
if :: tmp2 == EV_SET -> tmp1 = EV_SET; \
|
||||
:: else -> tmp1 = EV_BUSY; \
|
||||
fi; \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
assert(tmp1 != EV_FREE); \
|
||||
if :: tmp1 == EV_BUSY -> RAW_WAIT; \
|
||||
:: else -> skip; \
|
||||
fi; \
|
||||
:: else -> skip; \
|
||||
fi
|
||||
#endif
|
||||
|
||||
active proctype waiter()
|
||||
{
|
||||
if
|
||||
:: !value ->
|
||||
RESET;
|
||||
if
|
||||
:: !value -> WAIT;
|
||||
:: else -> skip;
|
||||
fi;
|
||||
:: else -> skip;
|
||||
fi;
|
||||
assert(value);
|
||||
}
|
||||
|
||||
active proctype notifier()
|
||||
{
|
||||
value = true;
|
||||
SET;
|
||||
}
|
||||
Reference in New Issue
Block a user