From 9517c1bd60771d068a53c8a52ab953e304ec3b74 Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 01:05:48 -0700 Subject: [PATCH 1/9] Add the initial Promela model for watch.Value Of course, this is useless without documenting how it maps to the real watch implementation. I'll get around to that. --- internal/watch/model.pml | 47 ++++++++++++++++++++++++++++++++++++ internal/watch/model_test.go | 9 +++++++ 2 files changed, 56 insertions(+) create mode 100644 internal/watch/model.pml create mode 100644 internal/watch/model_test.go diff --git a/internal/watch/model.pml b/internal/watch/model.pml new file mode 100644 index 0000000..ba3456e --- /dev/null +++ b/internal/watch/model.pml @@ -0,0 +1,47 @@ +byte w_next = 0; +bool w_running = false; + +proctype writer(byte val) { + atomic { + w_next = val; + if + :: (w_running == false) -> w_running = true; run handler() + :: else -> skip + fi + } +} + +byte g_handling = 0; +byte g_sum = 0; + +proctype handler() { + byte next; + bool stop; + + do + :: + atomic { + next = w_next; + stop = (next == 0); + w_next = 0; + w_running = !stop + } + if + :: (stop == true) -> break + :: else -> + g_handling = g_handling + 1; + atomic { + g_sum = g_sum + next; + assert(g_sum == 11 || g_sum == 12 || g_sum == 23); + assert(g_handling == 1); + g_handling = 0 + } + fi + od +} + +init { + run writer(11); + run writer(12); + (g_sum > 0) +} diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go new file mode 100644 index 0000000..6ac540f --- /dev/null +++ b/internal/watch/model_test.go @@ -0,0 +1,9 @@ +//go:build modeltest + +package watch + +import "testing" + +func TestWatchModel(t *testing.T) { + t.SkipNow() +} From b4052937c916c9b7b00899d3dc61b535fd47ba88 Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 01:27:33 -0700 Subject: [PATCH 2/9] Start adding a Go test harness for the model Part of the "documentation" is around how to run Spin in the first place. --- internal/watch/model_test.go | 68 ++++++++++++++++++++++++++++++++++-- 1 file changed, 66 insertions(+), 2 deletions(-) diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go index 6ac540f..84ab3d2 100644 --- a/internal/watch/model_test.go +++ b/internal/watch/model_test.go @@ -2,8 +2,72 @@ package watch -import "testing" +import ( + _ "embed" + "os" + "os/exec" + "path/filepath" + "strings" + "testing" +) + +//go:embed model.pml +var modelFile string func TestWatchModel(t *testing.T) { - t.SkipNow() + var missingCmds bool + needCmds := []string{"spin", "cc"} + for _, cmd := range needCmds { + if _, err := exec.LookPath(cmd); err != nil { + t.Logf("cannot find %q on this system", cmd) + missingCmds = true + } + } + if missingCmds { + t.SkipNow() + } + + spinDir, err := os.MkdirTemp("", "hypcast-spin-*") + if err != nil { + t.Fatalf("failed to create spin compilation directory: %v", err) + } + t.Logf("compiling model under %v", spinDir) + defer func() { + if t.Failed() { + t.Logf("keeping %v due to test failure", spinDir) + } else { + t.Log("cleaning up compilation directory due to successful test") + os.RemoveAll(spinDir) + } + }() + + err = os.Chdir(spinDir) + if 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 + err = spin.Run() + if 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 + err = cc.Run() + if err != nil { + t.Fatalf("failed to compile pan.c: %v", err) + } + + pan := exec.Command(filepath.Join(spinDir, "pan")) + pan.Stdout, pan.Stderr = os.Stdout, os.Stderr + err = pan.Run() + if err != nil { + t.Fatalf("failed to run pan: %v", err) + } + + // TODO: Finish this part. + t.Fatalf("the test does not yet know how to check for trail files") } From 932944476f4962dd0adbb7156989b49ddae005ed Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 01:37:22 -0700 Subject: [PATCH 3/9] Simplify various parts of the model test harness --- internal/watch/model_test.go | 38 +++++++++++++++--------------------- 1 file changed, 16 insertions(+), 22 deletions(-) diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go index 84ab3d2..288018f 100644 --- a/internal/watch/model_test.go +++ b/internal/watch/model_test.go @@ -15,56 +15,50 @@ import ( var modelFile string func TestWatchModel(t *testing.T) { - var missingCmds bool - needCmds := []string{"spin", "cc"} - for _, cmd := range needCmds { + for _, cmd := range []string{"spin", "cc"} { if _, err := exec.LookPath(cmd); err != nil { - t.Logf("cannot find %q on this system", cmd) - missingCmds = true + t.Fatalf("cannot find %v on this system", cmd) } } - if missingCmds { - t.SkipNow() - } - spinDir, err := os.MkdirTemp("", "hypcast-spin-*") + 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", spinDir) + + t.Logf("compiling model under %v", tmpdir) defer func() { if t.Failed() { - t.Logf("keeping %v due to test failure", spinDir) + 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.Log("cleaning up compilation directory due to successful test") - os.RemoveAll(spinDir) + t.Logf("failed to clean up %v", tmpdir) } }() - err = os.Chdir(spinDir) - if err != nil { + 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 - err = spin.Run() - if err != nil { + 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 - err = cc.Run() - if err != nil { + if err := cc.Run(); err != nil { t.Fatalf("failed to compile pan.c: %v", err) } - pan := exec.Command(filepath.Join(spinDir, "pan")) + pan := exec.Command(filepath.Join(tmpdir, "pan")) pan.Stdout, pan.Stderr = os.Stdout, os.Stderr - err = pan.Run() - if err != nil { + if err := pan.Run(); err != nil { t.Fatalf("failed to run pan: %v", err) } From 41f678f427a50c49afe8c415e4c63d78e9d5e636 Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 01:45:46 -0700 Subject: [PATCH 4/9] Fail the model test when trail files exist Still need to print the trail, though. --- internal/watch/model_test.go | 8 ++++++-- 1 file changed, 6 insertions(+), 2 deletions(-) diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go index 288018f..f91ebbe 100644 --- a/internal/watch/model_test.go +++ b/internal/watch/model_test.go @@ -62,6 +62,10 @@ func TestWatchModel(t *testing.T) { t.Fatalf("failed to run pan: %v", err) } - // TODO: Finish this part. - t.Fatalf("the test does not yet know how to check for trail files") + matches, _ := filepath.Glob("*.trail") // Error-free for well-formed patterns. + if len(matches) == 0 { + return + } + + t.Fatalf("found trail files: %v", matches) // TODO: Print the trail. } From 6a08215d16ec640c8ec5d78155341223a6626778 Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 01:53:41 -0700 Subject: [PATCH 5/9] Print the trail files Okay, this actually wasn't that hard. --- internal/watch/model_test.go | 8 +++++++- 1 file changed, 7 insertions(+), 1 deletion(-) diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go index f91ebbe..98a6da8 100644 --- a/internal/watch/model_test.go +++ b/internal/watch/model_test.go @@ -67,5 +67,11 @@ func TestWatchModel(t *testing.T) { return } - t.Fatalf("found trail files: %v", matches) // TODO: Print the trail. + t.Errorf("found trail files: %v", 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) + } } From da26be121c35603b3c636ddd5f523caeee222b2d Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 12:10:57 -0700 Subject: [PATCH 6/9] Add comments to the Promela model I tried not to overdo it, but I'm also trying to be reasonably friendly to anyone who's never seen Spin or Promela before. --- internal/watch/model.pml | 61 ++++++++++++++++++++++++++++++++++------ 1 file changed, 52 insertions(+), 9 deletions(-) diff --git a/internal/watch/model.pml b/internal/watch/model.pml index ba3456e..fcd22a1 100644 --- a/internal/watch/model.pml +++ b/internal/watch/model.pml @@ -1,38 +1,79 @@ +/** + * 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; -proctype writer(byte val) { - atomic { +/* 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 - :: (w_running == false) -> w_running = true; run handler() + :: 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 { + atomic { /* Performed under w.mu. */ next = w_next; stop = (next == 0); w_next = 0; w_running = !stop } - if + if /* Performed outside w.mu. */ :: (stop == true) -> break :: else -> g_handling = g_handling + 1; atomic { g_sum = g_sum + next; - assert(g_sum == 11 || g_sum == 12 || g_sum == 23); + assert(g_sum == 2 || g_sum == 3 || g_sum == 5); assert(g_handling == 1); g_handling = 0 } @@ -41,7 +82,9 @@ proctype handler() { } init { - run writer(11); - run writer(12); + 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) } From e6e945863a757c028390101a8a9db5011bcb988d Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 12:25:47 -0700 Subject: [PATCH 7/9] Add docs about the test harness --- internal/watch/model_test.go | 23 ++++++++++++++++++++++- 1 file changed, 22 insertions(+), 1 deletion(-) diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go index 98a6da8..ffca4bc 100644 --- a/internal/watch/model_test.go +++ b/internal/watch/model_test.go @@ -14,6 +14,27 @@ import ( //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. +// +// go test -v -tags modeltest [...] +// +// [Spin]: https://spinroot.com/ func TestWatchModel(t *testing.T) { for _, cmd := range []string{"spin", "cc"} { if _, err := exec.LookPath(cmd); err != nil { @@ -67,7 +88,7 @@ func TestWatchModel(t *testing.T) { return } - t.Errorf("found trail files: %v", matches) + 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 From d204ad233acc61baf3ef7e2b7dc1846a12766a21 Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 12:29:34 -0700 Subject: [PATCH 8/9] Small tweaks to the model harness --- internal/watch/model_test.go | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go index ffca4bc..943f009 100644 --- a/internal/watch/model_test.go +++ b/internal/watch/model_test.go @@ -30,12 +30,12 @@ var modelFile string // 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. +// include the "-v" flag to display the model checker's output. For example: // -// go test -v -tags modeltest [...] +// go test -v -tags modeltest -run Model ./internal/watch // // [Spin]: https://spinroot.com/ -func TestWatchModel(t *testing.T) { +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) From 0c491ff2d0e3eb6213cfb71b6706fa31d0917dea Mon Sep 17 00:00:00 2001 From: Alex Hamlin Date: Sat, 31 Aug 2024 12:31:59 -0700 Subject: [PATCH 9/9] Print the error for Spin tmpdir cleanup failures --- internal/watch/model_test.go | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/internal/watch/model_test.go b/internal/watch/model_test.go index 943f009..12071de 100644 --- a/internal/watch/model_test.go +++ b/internal/watch/model_test.go @@ -56,7 +56,7 @@ func TestModel(t *testing.T) { if err := os.RemoveAll(tmpdir); err == nil { t.Logf("cleaned up %v", tmpdir) } else { - t.Logf("failed to clean up %v", tmpdir) + t.Logf("failed to clean up %v: %v", tmpdir, err) } }()