226 lines
9.3 KiB
Promela
226 lines
9.3 KiB
Promela
/*
|
|
* This model describes the implementation of exclusive sections in
|
|
* cpus-common.c (start_exclusive, end_exclusive, cpu_exec_start,
|
|
* cpu_exec_end).
|
|
*
|
|
* Author: Paolo Bonzini <pbonzini@redhat.com>
|
|
*
|
|
* 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 cpus-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;
|
|
}
|