docs: create config/, devel/ and spin/ subdirectories

Developer documentation should be its own manual.  As a start, move all
developer-oriented files to a separate directory.

Also move non-text files to their own directories: docs/config/ for
QEMU -readconfig input, and docs/spin/ for formal models to be used
with the SPIN model checker.

Reviewed-by: Daniel P. Berrange <berrange@redhat.com>
Signed-off-by: Paolo Bonzini <pbonzini@redhat.com>

1 files changed, 0 insertions, 225 deletions

diff --git a/docs/tcg-exclusive.promela b/docs/tcg-exclusive.promela
deleted file mode 100644
index c91cfca9f7..0000000000
--- a/docs/tcg-exclusive.promela
+++ /dev/null
@@ -1,225 +0,0 @@
-/*
- * 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, USE_MUTEX,
- *                           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 <= 2 CPUs
-// If the mutex is used, it's also cheap (300 MB / 4 seconds) for 3 CPUs
-// For 3 CPUs and the lock-free option it needs 1.5 GB of RAM
-#if N_CPUS <= 2 || (N_CPUS <= 3 && defined USE_MUTEX)
-#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;                                                           \
-    MUTEX_UNLOCK(mutex);
-
-#define end_exclusive()                                           \
-    MUTEX_LOCK(mutex);                                            \
-    pending_cpus = 0;                                             \
-    COND_BROADCAST(exclusive_resume);                             \
-    MUTEX_UNLOCK(mutex);
-
-#ifdef USE_MUTEX
-// Simple version using mutexes
-#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;                                                                      \
-    MUTEX_UNLOCK(mutex);
-#else
-// Wait-free fast path, only needs mutex when concurrent with
-// an exclusive section
-#define cpu_exec_start(id)                                                   \
-    running[id] = 1;                                                         \
-    if                                                                       \
-        :: pending_cpus -> {                                                 \
-            MUTEX_LOCK(mutex);                                               \
-            if                                                               \
-                :: !has_waiter[id] -> {                                      \
-                    running[id] = 0;                                         \
-                    exclusive_idle();                                        \
-                    running[id] = 1;                                         \
-                }                                                            \
-                :: else -> skip;                                             \
-            fi;                                                              \
-            MUTEX_UNLOCK(mutex);                                             \
-        }                                                                    \
-        :: else -> skip;                                                     \
-    fi;
-
-#define cpu_exec_end(id)                                                     \
-    running[id] = 0;                                                         \
-    if                                                                       \
-        :: pending_cpus -> {                                                 \
-            MUTEX_LOCK(mutex);                                               \
-            if                                                               \
-                :: has_waiter[id] -> {                                       \
-                    has_waiter[id] = 0;                                      \
-                    pending_cpus--;                                          \
-                    if                                                       \
-                        :: pending_cpus == 1 -> COND_BROADCAST(exclusive_cond); \
-                        :: else -> skip;                                     \
-                    fi;                                                      \
-                }                                                            \
-                :: else -> skip;                                             \
-            fi;                                                              \
-            MUTEX_UNLOCK(mutex);                                             \
-        }                                                                    \
-        :: else -> skip;                                                     \
-    fi
-#endif
-
-// 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;
-}