docs: include formal model for TCG exclusive sections

Reviewed-by: Richard Henderson <rth@twiddle.net>
Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>

1 files changed, 177 insertions, 0 deletions

diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela
new file mode 100644
index 0000000000..5889b40638
--- /dev/null
+++ b/docs/tcg-exclusive.promela
@@ -0,0 +1,177 @@
+/*
+ * 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 <pbonzini@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/tcg-exclusive.promela
+ *     gcc pan.c -O2
+ *     ./a.out -a
+ *
+ * Tunable processor macros: N_CPUS, N_EXCLUSIVE, N_CYCLES, TEST_EXPENSIVE.
+ */
+
+// 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;
+}