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 <pbonz...@redhat.com> >> + * >> + * 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
