Introduce the formal model for watch.Value

As promised in the merge commit for the new watch implementation, here's
the formal Promela model that represents its behavior, along with a Go
test harness that automatically runs Spin to validate the model. I've
tested the harness on both macOS and Debian systems, and cleaned up the
model a bit from my original version, partly to make it easier to read
and partly to make it a closer match for the current Go implementation.

For context: I first learned about Spin and Promela from Paul McKenney's
"Is Parallel Programming Hard, And, If So, What Can You Do About It?",
and thought it would be an interesting thing to try. I was also coming
up with all kinds of weird ideas for the new watch implementation at
first, involving things like atomic variables, that I was convinced were
wrong even if I didn't care to find the litmus tests that would *prove*
them wrong. Now, I know how to do that automatically.

internal/watch/model.pml

@@ -0,0 +1,90 @@
+/**
+ * The Hypcast watch implementation uses a boolean "running" variable to track
+ * whether a handler goroutine is prepared to handle new values. Writers start a
+ * goroutine if one is not running, and running goroutines handle new values as
+ * long as possible before exiting, at which point they set "running" to false.
+ *
+ * This [Promela] model is intended to formally verify several properties of
+ * this approach, by exhaustively considering every possible interleaving of the
+ * atomic statements and blocks in the model:
+ *
+ *   - A handler executes at least once after a write is performed.
+ *   - A handler does not execute for the same value more than once.
+ *   - A handler does not execute more than once concurrently.
+ *
+ * The model considers the case of one watcher in the presence of concurrent
+ * writes, and does not attempt to model registration or cancellation of
+ * additional handlers.
+ *
+ * Note that the purpose of the model is NOT to verify the implementation of
+ * watches in Hypcast, as the unit tests do. It is to validate the _concept_ of
+ * triggering handlers on the basis of a synchronized "running" variable, to
+ * ensure the above properties hold if the Go implementation faithfully reflects
+ * the model.
+ *
+ * See model_test.go for a harness that runs [Spin] to validate this model.
+ *
+ * [Promela]: https://en.wikipedia.org/wiki/Promela
+ * [Spin]: https://spinroot.com/
+ */
+
+
+/* These correspond directly to fields of the watch struct in Hypcast. w_next
+ * encodes both the next and ok fields of the struct, such that (next == 0)
+ * represents (ok == false). */
+byte w_next = 0;
+bool w_running = false;
+
+/* This corresponds to the watch.update method that writers invoke to push new
+ * values into a watch. */
+proctype update(byte val) {
+  bool start = false;
+  atomic { /* Performed under w.mu. */
+    start = !w_running;
+    w_next = val;
+    w_running = true;
+  }
+  atomic { /* Performed outside w.mu. */
+    if
+    :: start -> run handler()
+    :: else -> skip
+    fi
+  }
+}
+
+/* State for the handler to validate the properties expressed above. */
+byte g_handling = 0;
+byte g_sum = 0;
+
+proctype handler() {
+  byte next;
+  bool stop;
+  do
+  ::
+    atomic { /* Performed under w.mu. */
+      next = w_next;
+      stop = (next == 0);
+      w_next = 0;
+      w_running = !stop
+    }
+    if /* Performed outside w.mu. */
+    :: (stop == true) -> break
+    :: else ->
+      g_handling = g_handling + 1;
+      atomic {
+        g_sum = g_sum + next;
+        assert(g_sum == 2 || g_sum == 3 || g_sum == 5);
+        assert(g_handling == 1);
+        g_handling = 0
+      }
+    fi
+  od
+}
+
+init {
+  run update(2);
+  run update(3);
+  /* Enforce the handler executing at least once. If g_sum is never incremented,
+   * init will finish in an invalid end state. */
+  (g_sum > 0)
+}

internal/watch/model_test.go

@@ -0,0 +1,98 @@
+//go:build modeltest
+
+package watch
+
+import (
+	_ "embed"
+	"os"
+	"os/exec"
+	"path/filepath"
+	"strings"
+	"testing"
+)
+
+//go:embed model.pml
+var modelFile string
+
+// TestWatchModel uses the [Spin] tool to validate the formal Promela model of
+// the Hypcast watch implementation in model.pml.
+//
+// To verify a Promela model, a user will typically:
+//
+//   - Use Spin to create a C program ("pan.c") that evaluates all possible
+//     states in the model.
+//   - Compile this program with the system C compiler, and execute it.
+//   - Look for the presence of a ".trail" file demonstrating an interleaving of
+//     processes that violates the model's assertions.
+//
+// This harness automates this process within the standard Go testing framework,
+// building and executing the model checker in a temporary directory and
+// displaying the details of any generated trail.
+//
+// Use the "modeltest" build tag to include this harness in a test run, and
+// include the "-v" flag to display the model checker's output. For example:
+//
+//	go test -v -tags modeltest -run Model ./internal/watch
+//
+// [Spin]: https://spinroot.com/
+func TestModel(t *testing.T) {
+	for _, cmd := range []string{"spin", "cc"} {
+		if _, err := exec.LookPath(cmd); err != nil {
+			t.Fatalf("cannot find %v on this system", cmd)
+		}
+	}
+
+	tmpdir, err := os.MkdirTemp("", "hypcast-spin-*")
+	if err != nil {
+		t.Fatalf("failed to create spin compilation directory: %v", err)
+	}
+
+	t.Logf("compiling model under %v", tmpdir)
+	defer func() {
+		if t.Failed() {
+			t.Logf("keeping %v due to test failure", tmpdir)
+			return
+		}
+		if err := os.RemoveAll(tmpdir); err == nil {
+			t.Logf("cleaned up %v", tmpdir)
+		} else {
+			t.Logf("failed to clean up %v: %v", tmpdir, err)
+		}
+	}()
+
+	if err := os.Chdir(tmpdir); err != nil {
+		t.Fatalf("failed to change to compilation directory: %v", err)
+	}
+
+	spin := exec.Command("spin", "-a", "/dev/stdin")
+	spin.Stdin = strings.NewReader(modelFile)
+	spin.Stdout, spin.Stderr = os.Stdout, os.Stderr
+	if err := spin.Run(); err != nil {
+		t.Fatalf("failed to run spin: %v", err)
+	}
+
+	cc := exec.Command("cc", "-o", "pan", "pan.c")
+	cc.Stdout, cc.Stderr = os.Stdout, os.Stderr
+	if err := cc.Run(); err != nil {
+		t.Fatalf("failed to compile pan.c: %v", err)
+	}
+
+	pan := exec.Command(filepath.Join(tmpdir, "pan"))
+	pan.Stdout, pan.Stderr = os.Stdout, os.Stderr
+	if err := pan.Run(); err != nil {
+		t.Fatalf("failed to run pan: %v", err)
+	}
+
+	matches, _ := filepath.Glob("*.trail") // Error-free for well-formed patterns.
+	if len(matches) == 0 {
+		return
+	}
+
+	t.Errorf("found %v; run go test -v to see trail output", matches)
+	trail := exec.Command("spin", "-t", "-p", "-k", matches[0], "/dev/stdin")
+	trail.Stdin = strings.NewReader(modelFile)
+	trail.Stdout, trail.Stderr = os.Stdout, os.Stderr
+	if err := trail.Run(); err != nil {
+		t.Fatalf("failed to print trail output: %v", err)
+	}
+}