Re: [Qemu-devel] [PATCH 10/16] docs: include formal model for TCG exclusive sections

[Alex Bennée]

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