[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: |
Paolo Bonzini |
Subject: |
Re: [Qemu-devel] [PATCH 10/16] docs: include formal model for TCG exclusive sections |
Date: |
Mon, 26 Sep 2016 10:34:04 +0200 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.3.0 |
On 26/09/2016 10:24, Alex Bennée wrote:
> > + * 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
Oops, fixed now (-a is needed by the way).
Paolo
> > + *
> > + * 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.
- Re: [Qemu-devel] [PATCH 06/16] cpus-common: move CPU list management to common code, (continued)
- [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
- [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