From a200f2fb571f337db37f865aec18f655fa3c872b Mon Sep 17 00:00:00 2001 From: Paolo Bonzini Date: Fri, 2 Sep 2016 23:35:55 +0200 Subject: docs: include formal model for TCG exclusive sections Reviewed-by: Richard Henderson Signed-off-by: Paolo Bonzini --- docs/tcg-exclusive.promela | 177 +++++++++++++++++++++++++++++++++++++++++++++ 1 file changed, 177 insertions(+) create mode 100644 docs/tcg-exclusive.promela (limited to 'docs') diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela new file mode 100644 index 0000000000..5889b40638 --- /dev/null +++ b/docs/tcg-exclusive.promela @@ -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 + * + * 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; +} -- cgit v1.2.3 From cf07da65f335b9a74e62f5413078f67280572f36 Mon Sep 17 00:00:00 2001 From: Paolo Bonzini Date: Fri, 2 Sep 2016 21:02:10 +0200 Subject: cpus-common: remove redundant call to exclusive_idle() MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit No need to call exclusive_idle() from cpu_exec_end since it is done immediately afterwards in cpu_exec_start. Any exclusive section could run as soon as cpu_exec_end leaves, because cpu->running is false and the mutex is not taken, so the call does not add any protection either. Reviewed-by: Richard Henderson Reviewed-by: Alex Bennée Signed-off-by: Paolo Bonzini --- docs/tcg-exclusive.promela | 1 - 1 file changed, 1 deletion(-) (limited to 'docs') diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela index 5889b40638..8bb0967df6 100644 --- a/docs/tcg-exclusive.promela +++ b/docs/tcg-exclusive.promela @@ -124,7 +124,6 @@ byte has_waiter[N_CPUS]; } \ :: else -> skip; \ fi; \ - exclusive_idle(); \ MUTEX_UNLOCK(mutex); // Promela processes -- cgit v1.2.3 From 758e1b2b622d7c177dc2d95e887a11aa069b7e68 Mon Sep 17 00:00:00 2001 From: Paolo Bonzini Date: Fri, 2 Sep 2016 23:33:38 +0200 Subject: cpus-common: simplify locking for start_exclusive/end_exclusive MIME-Version: 1.0 Content-Type: text/plain; charset=UTF-8 Content-Transfer-Encoding: 8bit It is not necessary to hold qemu_cpu_list_mutex throughout the exclusive section, because no other exclusive section can run while pending_cpus != 0. exclusive_idle() is called in cpu_exec_start(), and that prevents any CPUs created after start_exclusive() from entering cpu_exec() during an exclusive section. Reviewed-by: Richard Henderson Reviewed-by: Alex Bennée Signed-off-by: Paolo Bonzini --- docs/tcg-exclusive.promela | 4 +++- 1 file changed, 3 insertions(+), 1 deletion(-) (limited to 'docs') diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela index 8bb0967df6..feac679b9a 100644 --- a/docs/tcg-exclusive.promela +++ b/docs/tcg-exclusive.promela @@ -98,9 +98,11 @@ byte has_waiter[N_CPUS]; do \ :: pending_cpus > 1 -> COND_WAIT(exclusive_cond, mutex); \ :: else -> break; \ - od + od; \ + MUTEX_UNLOCK(mutex); #define end_exclusive() \ + MUTEX_LOCK(mutex); \ pending_cpus = 0; \ COND_BROADCAST(exclusive_resume); \ MUTEX_UNLOCK(mutex); -- cgit v1.2.3 From c265e976f4669fd65f5b47e6865f50d1cb66bd02 Mon Sep 17 00:00:00 2001 From: Paolo Bonzini Date: Wed, 31 Aug 2016 21:33:58 +0200 Subject: cpus-common: lock-free fast path for cpu_exec_start/end Set cpu->running without taking the cpu_list lock, only requiring it if there is a concurrent exclusive section. This requires adding a new field to CPUState, which records whether a running CPU is being counted in pending_cpus. When an exclusive section is started concurrently with cpu_exec_start, cpu_exec_start can use the new field to determine if it has to wait for the end of the exclusive section. Likewise, cpu_exec_end can use it to see if start_exclusive is waiting for that CPU. This a separate patch for easier bisection of issues. Signed-off-by: Paolo Bonzini --- docs/tcg-exclusive.promela | 53 +++++++++++++++++++++++++++++++++++++++++++--- 1 file changed, 50 insertions(+), 3 deletions(-) (limited to 'docs') diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela index feac679b9a..c91cfca9f7 100644 --- a/docs/tcg-exclusive.promela +++ b/docs/tcg-exclusive.promela @@ -13,7 +13,8 @@ * gcc pan.c -O2 * ./a.out -a * - * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, TEST_EXPENSIVE. + * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX, + * TEST_EXPENSIVE. */ // Define the missing parameters for the model @@ -22,8 +23,10 @@ #warning defaulting to 2 CPU processes #endif -// the expensive test is not so expensive for <= 3 CPUs -#if N_CPUS <= 3 +// 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 @@ -107,6 +110,8 @@ byte has_waiter[N_CPUS]; COND_BROADCAST(exclusive_resume); \ MUTEX_UNLOCK(mutex); +#ifdef USE_MUTEX +// Simple version using mutexes #define cpu_exec_start(id) \ MUTEX_LOCK(mutex); \ exclusive_idle(); \ @@ -127,6 +132,48 @@ byte has_waiter[N_CPUS]; :: 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 -- cgit v1.2.3