mirrors/qemu
1
0
Fork 0
Code Issues Pull Requests Packages Projects Releases Wiki Activity

docs: include formal model for TCG exclusive sections

Browse Source 
Reviewed-by: Richard Henderson <rth@twiddle.net>
Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>
This commit is contained in:
Paolo Bonzini 2016-09-02 23:35:55 +02:00
parent ab129972c8
commit a200f2fb57
1 changed files with 177 additions and 0 deletions
Show Stats Download Patch File Download Diff File Expand all files Collapse all files

177
docs/tcg-exclusive.promela Normal file
View File

@ -0,0 +1,177 @@
/*
* 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, 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 <= 3 CPUs
#if N_CPUS <= 3
#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
#define end_exclusive() \
pending_cpus = 0; \
COND_BROADCAST(exclusive_resume); \
MUTEX_UNLOCK(mutex);
#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; \
exclusive_idle(); \
MUTEX_UNLOCK(mutex);
// 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;
}