[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Qemu-devel] [PATCH 10/16] docs: include formal model for TCG exclus
From: |
Alex Bennée |
Subject: |
Re: [Qemu-devel] [PATCH 10/16] docs: include formal model for TCG exclusive sections |
Date: |
Mon, 26 Sep 2016 09:24:32 +0100 |
User-agent: |
mu4e 0.9.17; emacs 25.1.50.1 |
Paolo Bonzini <address@hidden> writes:
> Signed-off-by: Paolo Bonzini <address@hidden>
> ---
> docs/tcg-exclusive.promela | 176
> +++++++++++++++++++++++++++++++++++++++++++++
> 1 file changed, 176 insertions(+)
> create mode 100644 docs/tcg-exclusive.promela
>
> diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela
> new file mode 100644
> index 0000000..360edcd
> --- /dev/null
> +++ b/docs/tcg-exclusive.promela
> @@ -0,0 +1,176 @@
> +/*
> + * 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 <address@hidden>
> + *
> + * 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
> + * ./a.out -a
> + *
> + * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, TEST_EXPENSIVE.
> + */
I made some comments on the comments when this was part of the other patch:
> + *
> + * Author: Paolo Bonzini <address@hidden>
> + *
> + * 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
wrong docs name
> + * ./a.out -a
Which version of spin did you run? I grabbed the latest src release
(http://spinroot.com/spin/Src/src645.tar.gz) and had to manually build
the output:
~/src/spin/Src6.4.5/spin -a docs/tcg-exclusive.promela
gcc pan.c
../a.out
> + *
> + * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, USE_MUTEX,
> + * TEST_EXPENSIVE.
> + */
How do you pass these? I tried:
~/src/spin/Src6.4.5/spin -a docs/tcg-exclusive.promela -DN_CPUS=4
~/src/spin/Src6.4.5/spin -a docs/tcg-exclusive.promela -DN_CPUS 4
without any joy.
> +
> +// 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;
> +}
--
Alex Bennée
- [Qemu-devel] [PATCH 06/16] cpus-common: move CPU list management to common code, (continued)
- [Qemu-devel] [PATCH 06/16] cpus-common: move CPU list management to common code, Paolo Bonzini, 2016/09/23
- [Qemu-devel] [PATCH 05/16] linux-user: Add qemu_cpu_is_self() and qemu_cpu_kick(), Paolo Bonzini, 2016/09/23
- [Qemu-devel] [PATCH 07/16] cpus-common: move CPU work item management to common code, Paolo Bonzini, 2016/09/23
- [Qemu-devel] [PATCH 08/16] cpus-common: fix uninitialized variable use in run_on_cpu, Paolo Bonzini, 2016/09/23
- [Qemu-devel] [PATCH 10/16] docs: include formal model for TCG exclusive sections, Paolo Bonzini, 2016/09/23
- Re: [Qemu-devel] [PATCH 10/16] docs: include formal model for TCG exclusive sections,
Alex Bennée <=
- [Qemu-devel] [PATCH 09/16] cpus-common: move exclusive work infrastructure from linux-user, Paolo Bonzini, 2016/09/23
- [Qemu-devel] [PATCH 11/16] cpus-common: always defer async_run_on_cpu work items, Paolo Bonzini, 2016/09/23
- [Qemu-devel] [PATCH 13/16] cpus-common: simplify locking for start_exclusive/end_exclusive, Paolo Bonzini, 2016/09/23
- [Qemu-devel] [PATCH 15/16] tcg: Make tb_flush() thread safe, Paolo Bonzini, 2016/09/23