Re: [Qemu-devel] [PATCH 12/12] cpus-common: lock-free fast path for cpu_exec_start/end

[Paolo Bonzini]

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