mirror of
https://github.com/Motorhead1991/qemu.git
synced 2025-08-07 09:43:56 -06:00
c95b08106b
After the docs directory restructuring, several comments refer to paths that no longer exist. Replace these references to the current file locations so readers can find the correct files. Related commits ---------------189c099f75(Jul 2021) docs: collect the disparate device emulation docs into one section Rename docs/system/{ => devices}/nvme.rst5f4c96b779(Feb 2023) docs/system/loongarch: update loongson3.rst and rename it to virt.rst Rename docs/system/loongarch/{loongson3.rst => virt.rst}fe0007f3c1(Sep 2023) exec: Rename cpu.c -> cpu-target.c Rename cpus-common.c => cpu-common.c42fa9665e5(Apr 2025) exec: Restrict 'cpu_ldst.h' to accel/tcg/ Rename include/{exec/cpu_ldst.h => accel/tcg/cpu-ldst.h} Signed-off-by: Sean Wei <me@sean.taipei> Message-ID: <20250616.qemu.relocated.06@sean.taipei> Reviewed-by: Thomas Huth <thuth@redhat.com> Signed-off-by: Thomas Huth <thuth@redhat.com>
225 lines
9.3 KiB
Promela
225 lines
9.3 KiB
Promela
/*
|
|
* 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 <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 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;
|
|
}
|