[Date Prev][Date Next][Thread Prev][Thread Next][Date Index][Thread Index]
Re: [Qemu-devel] [PATCH 12/12] cpus-common: lock-free fast path for cpu_
From: |
Paolo Bonzini |
Subject: |
Re: [Qemu-devel] [PATCH 12/12] cpus-common: lock-free fast path for cpu_exec_start/end |
Date: |
Mon, 5 Sep 2016 18:57:25 +0200 |
User-agent: |
Mozilla/5.0 (X11; Linux x86_64; rv:45.0) Gecko/20100101 Thunderbird/45.2.0 |
On 05/09/2016 17:25, Alex Bennée wrote:
>> diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela
>> new file mode 100644
>> index 0000000..293b530
>> --- /dev/null
>> +++ b/docs/tcg-exclusive.promela
>> @@ -0,0 +1,224 @@
>> +/*
>> + * This model describes the implementation of exclusive sections in
>> + * cpus-common.c (start_exclusive, end_exclusive, cpu_exec_start,
>> + * cpu_exec_end).
>
> \o/ nice to have a model ;-)
Yeah, in my tree actually I have a couple optimizations that patch both
cpus-common.c and the model.
>> + *
>> + * 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
Yes, that's how you use it. You'd better use -O2, too.
>> + *
>> + * 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
This should work... Maybe put -D before the file name.
Paolo
- [Qemu-devel] [PATCH 08/12] cpus-common: move exclusive work infrastructure from, (continued)
- [Qemu-devel] [PATCH 08/12] cpus-common: move exclusive work infrastructure from, Paolo Bonzini, 2016/09/01
- [Qemu-devel] [PATCH 03/12] cpus: Rename flush_queued_work(), Paolo Bonzini, 2016/09/01
- [Qemu-devel] [PATCH 07/12] cpus-common: move CPU work item management to common, Paolo Bonzini, 2016/09/01
- [Qemu-devel] [PATCH 06/12] cpus-common: move CPU list management to common code, Paolo Bonzini, 2016/09/01
- [Qemu-devel] [PATCH 12/12] cpus-common: lock-free fast path for cpu_exec_start/end, Paolo Bonzini, 2016/09/01
- [Qemu-devel] [PATCH 11/12] tcg: Make tb_flush() thread safe, Paolo Bonzini, 2016/09/01
- [Qemu-devel] [PATCH 09/12] cpus-common: always defer async_run_on_cpu work items, Paolo Bonzini, 2016/09/01
- [Qemu-devel] [PATCH 10/12] cpus-common: Introduce async_safe_run_on_cpu(), Paolo Bonzini, 2016/09/01
- Re: [Qemu-devel] [PATCH 10/12] cpus-common: Introduce async_safe_run_on_cpu(), Pranith Kumar, 2016/09/12
- Re: [Qemu-devel] [PATCH v6 00/12] cpu-exec: Safe work in quiescent state, Alex Bennée, 2016/09/05