fix(runtime): interleave executors due at one instant move by move

changes/unreleased/explore-executor-turns.fixed.md

@@ -0,0 +1 @@
+- **Executors due at one instant interleave move by move under `explore`, `check`, `replay` and seeded schedules.** An executor drawn from the due order used to run all its work at the instant before another could move, so two actions reading a shared feature and then writing it never reached the lost update. The executor drawn now makes one move and keeps its turn only while its next move is independent of everything each other due executor may still do at the instant; otherwise the due order is drawn again. Explore runs and check state counts grow on models whose messages cannot be resolved statically. `declared` and `reverse` keep their order.

cmd/sysml/check_engine_test.go

@@ -510,13 +510,13 @@ func TestEngineCheckSearchesBehaviorsOnOneClock(t *testing.T) {
 	// Named apart, each behavior is its own search; the action's clock runs to its
 	// end, and the machine stops at its initial transition.
 	wantReport(t, check(t, binary, lampModel, "-engine", "check", "-action", peek, "-state", glow),
-		1, "✗ Action Shine::Lamp::peek: divergent (10 states, 9 moves, depth 5)", "divergent: saw ends as false or true",
+		1, "✗ Action Shine::Lamp::peek: divergent (9 states, 8 moves, depth 5)", "divergent: saw ends as false or true",
 		"✓ State machine Shine::Lamp::glow: no violation, exhaustive (1 states, 0 moves, depth 0)")
 
 	// With -advance they are one invocation: the machine's timer and the action's
 	// wait are due together, and the order the search draws decides what peek saw.
 	got := check(t, binary, lampModel, "-engine", "check", "-action", peek, "-state", glow, "-advance", "3")
-	wantReport(t, got, 1, "✗ Behaviors Shine::Lamp::peek, Shine::Lamp::glow: divergent up to t=3.0 (10 states, 9 moves, depth 5)",
+	wantReport(t, got, 1, "✗ Behaviors Shine::Lamp::peek, Shine::Lamp::glow: divergent up to t=3.0 (9 states, 8 moves, depth 5)",
 		"divergent: Shine::Lamp::peek.saw ends as false or true",
 		`outcome: Shine::Lamp::glow finalState = "on"; Shine::Lamp::glow visits = "off, on"; Shine::Lamp::peek.saw = false; this.isSolid = true; this.lit = true`,
 		`outcome: Shine::Lamp::glow finalState = "on"; Shine::Lamp::glow visits = "off, on"; Shine::Lamp::peek.saw = true; this.isSolid = true; this.lit = true`)
@@ -561,7 +561,7 @@ func TestEngineCheckWitnessOfBehaviorsOnOneClockReplays(t *testing.T) {
 	got := check(t, binary, lampModel, "-engine", "check", "-action", peek, "-state", glow, "-advance", "3", "-check-witness", dir)
 	wantReport(t, got, 1, "divergent: Shine::Lamp::peek.saw ends as false or true",
 		"Shine::Lamp::peek.saw = false (witness "+name(1)+")", "Shine::Lamp::peek.saw = true (witness "+name(2)+")",
-		"standing: sensitive (witnessed: 10 states, 9 moves searched, witness of 1 choice replayed)")
+		"standing: sensitive (witnessed: 9 states, 8 moves searched, witness of 2 choices replayed)")
 
 	for _, c := range []struct {
 		n     int
@@ -575,7 +575,7 @@ func TestEngineCheckWitnessOfBehaviorsOnOneClockReplays(t *testing.T) {
 		if err != nil {
 			t.Fatal(err)
 		}
-		if !strings.HasPrefix(string(content), "object #1 = Shine::Lamp#1\nt=3.0: "+c.first+" first of action peek of object #1, state machine glow of object #1\n\n") ||
+		if !strings.HasPrefix(string(content), "object #1 = Shine::Lamp#1\nt=3.0: action peek of object #1 first of action peek of object #1, state machine glow of object #1\nt=3.0: "+c.first+" first of action peek of object #1, state machine glow of object #1\n\n") ||
 			!strings.Contains(string(content), "choice at t=3.0: due action peek of object #1, state machine glow of object #1 (unordered; ran "+c.first+" first)") {
 			t.Errorf("witness %d:\n%s", c.n, content)
 		}

cmd/sysml/explore_nested_test.go

@@ -75,9 +75,9 @@ func TestExploreRunsAMachineOnANestedObject(t *testing.T) {
 
 	got := check(t, binary, linkedPairModel, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5")
 	wantReport(t, got, 0, "✓ explored Comms::Ground::listen: 2 outcomes",
-		"finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 3              | possible    | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4",
-		"finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 2 | 1              | possible    | t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; events at t=3.0: accept Frame first of time listening 1->quiet, accept Frame; at t=3.0: do listening first of do listening, dispatch time listening 1->quiet",
-		"complete (4 runs)")
+		"finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 1 | 4              | possible    | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4",
+		"finalState quiet; visits idle, listening, quiet; this.isSolid = true; this.received = 2 | 1              | possible    | t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4; events at t=3.0: accept Frame first of time listening 1->quiet, accept Frame; at t=3.0: do listening first of do listening, dispatch time listening 1->quiet",
+		"complete (5 runs)")
 	for _, jobs := range []string{"1", "4"} {
 		again := check(t, binary, linkedPairModel, "-jobs", jobs, "-schedule", "explore", "-state", "Comms::Ground::listen Comms::pair.ground", "-advance", "5")
 		if again.output() != got.output() {
@@ -101,9 +101,9 @@ func TestExploreRunsSiblingsOnOneAssembly(t *testing.T) {
 	binary := buildCLI(t)
 
 	outcomes := []string{
-		"Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 1 | 3              | possible    | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4",
+		"Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 1 | 4              | possible    | t=3.0: state machine listen of object #2 first of state machine listen of object #2, state machine modes of object #4",
 		"Comms::pair.craft.isSolid = true; Comms::pair.craft.sent = 4; Comms::pair.ground.isSolid = true; Comms::pair.ground.received = 2 | 1              | possible    | t=3.0: state machine modes of object #4 first of state machine listen of object #2, state machine modes of object #4",
-		"complete (4 runs)",
+		"complete (5 runs)",
 	}
 	byPath := check(t, binary, linkedPairModel, "-schedule", "explore",
 		"-state", "Comms::Ground::listen Comms::pair.ground", "-state", "Comms::Craft::modes Comms::pair.craft", "-advance", "5")

cmd/sysml/explore_turns_test.go

@@ -0,0 +1,131 @@
+package main
+
+import (
+	"fmt"
+	"regexp"
+	"strings"
+	"testing"
+)
+
+var seenLine = regexp.MustCompile(`seen = \d+`)
+
+// lostUpdateModel has two actions due at one instant, each reading a shared
+// counter in one step and writing it from what it read in the next.
+const lostUpdateModel = `package Race {
+    private import ScalarValues::*;
+
+    part def Counter { attribute count : Integer = 0; }
+    part counter : Counter;
+
+    action left {
+        attribute seen : Integer = 0;
+        first start;
+        then action wait accept after 1 [SI::s];
+        then action read assign seen := counter.count;
+        then action write assign counter.count := seen + 1;
+        then done;
+    }
+
+    action right {
+        attribute seen : Integer = 0;
+        first start;
+        then action wait accept after 1 [SI::s];
+        then action read assign seen := counter.count;
+        then action write assign counter.count := seen + 1;
+        then done;
+    }
+}
+`
+
+// TestExploreInterleavesExecutorsMoveByMove checks that executors due at one
+// instant interleave between their moves: both reads may run before either write,
+// so explore, check and a seed reach the lost update, while declared and reverse
+// keep running each executor through its turn.
+func TestExploreInterleavesExecutorsMoveByMove(t *testing.T) {
+	binary := buildCLI(t)
+	invocation := []string{"-instantiate", "Race::counter", "-action", "Race::left", "-action", "Race::right", "-advance", "1"}
+	lost, leftFirst, rightFirst := "Race::left.seen = 0; Race::right.seen = 0", "Race::left.seen = 0; Race::right.seen = 1", "Race::left.seen = 1; Race::right.seen = 0"
+
+	explored := check(t, binary, lostUpdateModel, append([]string{"-schedule", "explore"}, invocation...)...)
+	wantReport(t, explored, 0, "✓ explored Race::left, Race::right: 3 outcomes", lost+" |", leftFirst+" |", rightFirst+" |", "complete (")
+
+	checked := check(t, binary, lostUpdateModel, append([]string{"-engine", "check", "-check-diverge", "Race::left.seen"}, invocation...)...)
+	wantReport(t, checked, 1, "divergent: Race::left.seen ends as 0 or 1",
+		"outcome: "+lost, "outcome: "+leftFirst, "outcome: "+rightFirst, "witness of 6 choices replayed")
+
+	results := func(policy string) string {
+		got := check(t, binary, lostUpdateModel, append([]string{"-schedule", policy}, invocation...)...)
+		wantReport(t, got, 0, "Action completed")
+		return strings.Join(seenLine.FindAllString(got.output(), -1), ", ")
+	}
+	if got := results("declared"); got != "seen = 0, seen = 1" {
+		t.Errorf("declared runs left through its turn first, want seen = 0, seen = 1, got %s", got)
+	}
+	if got := results("reverse"); got != "seen = 1, seen = 0" {
+		t.Errorf("reverse runs right through its turn first, want seen = 1, seen = 0, got %s", got)
+	}
+	seeded := map[string]bool{}
+	for seed := 1; seed <= 12; seed++ {
+		seeded[results(fmt.Sprintf("seed:%d", seed))] = true
+	}
+	for _, want := range []string{"seen = 0, seen = 0", "seen = 0, seen = 1", "seen = 1, seen = 0"} {
+		if !seeded[want] {
+			t.Errorf("no seed of 1..12 reaches %s: %v", want, seeded)
+		}
+	}
+}
+
+// heldEntryModel has a machine whose timer transition holds work's entry cascade
+// while the Go it sends is still to be dispatched, and an action due at the same
+// instant that reads what the cascade writes.
+const heldEntryModel = `package Held {
+    private import ScalarValues::*;
+    item def Go;
+    part def P {
+        attribute order : Integer = 0;
+        attribute seen : Integer = 0;
+        state m parallel {
+            state left {
+                entry; then prep;
+                state prep;
+                state work {
+                    ref :>> runToCompletionScope = self;
+                    state inner { entry action { assign order := order * 10 + 1; } }
+                    entry action { send new Go() to m; } then inner;
+                }
+                transition first prep accept after 1 [SI::s] then work;
+            }
+            state right {
+                entry; then a;
+                state a;
+                state b { entry action { assign order := order * 10 + 2; } }
+                transition first a accept Go then b;
+            }
+        }
+        action peek {
+            first start;
+            then action wait accept after 1 [SI::s];
+            then action read assign seen := order;
+            then done;
+        }
+    }
+    part p : P;
+}
+`
+
+// TestExploreRunsAHeldEntryAsAMove checks that resuming a held entry counts as the
+// machine's move, so the Go queued behind it is still dispatched at the instant.
+func TestExploreRunsAHeldEntryAsAMove(t *testing.T) {
+	binary := buildCLI(t)
+	invocation := []string{"-instantiate", "Held::p", "-state", "Held::P::m Held::p", "-action", "Held::P::peek Held::p", "-advance", "1"}
+
+	explored := check(t, binary, heldEntryModel, append([]string{"-schedule", "explore"}, invocation...)...)
+	wantReport(t, explored, 0, "✓ explored Held::P::peek, Held::P::m: 10 outcomes", "this.order = 12; this.seen = 1", "complete (")
+	if strings.Contains(explored.output(), `finalState = "inner+a"`) {
+		t.Errorf("an explored run left Go undispatched at the instant it was sent:\n%s", explored.output())
+	}
+	for seed := 1; seed <= 8; seed++ {
+		got := check(t, binary, heldEntryModel, append([]string{"-schedule", fmt.Sprintf("seed:%d", seed)}, invocation...)...)
+		wantReport(t, got, 0, "Current state: inner | b")
+	}
+}

cmd/sysml/run_test.go

@@ -1287,7 +1287,7 @@ func TestExploreAdvanceRunsBehaviorsOnOneClock(t *testing.T) {
 		`Due::Beacon::blinking finalState = "shining"; Due::Beacon::blinking visits = "dark, shining"; Due::watcher.sawLit = false; this.isSolid = true; this.lit = true`,
 		`Due::Beacon::blinking finalState = "shining"; Due::Beacon::blinking visits = "dark, shining"; Due::watcher.sawLit = true; this.isSolid = true; this.lit = true`,
 		"possible",
-		"complete (2 runs)")
+		"complete (3 runs)")
 
 	// Advanced short of the instant, neither is due: one outcome, no choice, and
 	// the action that did not complete is the run's error.