diff --git a/internal/runner/composition_reread_test.go b/internal/runner/composition_reread_test.go index 5847d8e..f052582 100644 --- a/internal/runner/composition_reread_test.go +++ b/internal/runner/composition_reread_test.go @@ -133,22 +133,25 @@ func TestRunner_AStepWhoseTreeChangedBetweenReadsIsNotVerified(t *testing.T) { }) } -// submitsOnTapDriver commits a transaction on every tap, shows the running -// total in the tree, and grows a row under the hierarchy read that follows the -// paired Snapshot: on one chosen step, or on every one of them. +// submitsOnTapDriver commits commitsPerTap transactions on every tap, shows the +// running total in the tree, and grows a row under the hierarchy read that +// follows the paired Snapshot: on one chosen step, on the run of steps from +// composingRead through composingThrough, or on every one of them. type submitsOnTapDriver struct { *mockdriver.Driver - composingRead int64 - everyRead bool - reads atomic.Int64 - committed atomic.Int64 + commitsPerTap int64 + composingRead int64 + composingThrough int64 + everyRead bool + reads atomic.Int64 + committed atomic.Int64 } func (d *submitsOnTapDriver) Tap(context.Context, int, int) error { return d.commit() } func (d *submitsOnTapDriver) TapSelector(context.Context, string) error { return d.commit() } func (d *submitsOnTapDriver) commit() error { - d.committed.Add(1) + d.committed.Add(d.commitsPerTap) return nil } @@ -157,7 +160,10 @@ func (d *submitsOnTapDriver) Snapshot(context.Context) (string, driver.Image, er } func (d *submitsOnTapDriver) Hierarchy(context.Context) (string, error) { - if read := d.reads.Add(1); d.everyRead || read == d.composingRead { + read := d.reads.Add(1) + composing := d.everyRead || read == d.composingRead || + (read >= d.composingRead && read <= d.composingThrough) + if composing { return fmt.Sprintf(homeWithTxnCountComposing, d.committed.Load()), nil } return fmt.Sprintf(homeWithTxnCount, d.committed.Load()), nil @@ -188,7 +194,11 @@ func TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt(t *testing.T) { run := func(t *testing.T, composingRead int64) (Summary, int64) { t.Helper() state := newHarnessWithSpec(t, spec) - device := &submitsOnTapDriver{Driver: state.mock, composingRead: composingRead} + device := &submitsOnTapDriver{ + Driver: state.mock, + commitsPerTap: 1, + composingRead: composingRead, + } ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second) defer cancel() @@ -243,13 +253,92 @@ func TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt(t *testing.T) { }) } -// Holding an action back is bounded. A screen that changes shape under every -// pair of reads (a live list, a spinner mounting and unmounting) would -// otherwise take the whole run: nothing verified, nothing tapped, and a green -// summary at the end of it. -func TestRunner_AScreenThatNeverSettlesDoesNotStallTheRun(t *testing.T) { +// One skipped step is held; a run of them has to be held too. A bound that lets +// the runner act again while the verifier is still being skipped puts back the +// exact swallow the hold exists to prevent, only later: the action drawn on the +// step past the bound overwrites the one the hold was carrying, and the carried +// action is never reported to any spec. +// +// The screen composes on steps 3 through 5 of 6 and the device commits one +// transaction per tap throughout, so the property has a clean pair to judge +// (step 2 to step 6) and nothing in between it can be told about except the +// action step 2 applied. +func TestRunner_ARunOfSkippedStepsReportsEveryActionItApplied(t *testing.T) { + spec := specWithFolioPredicates(t) + + run := func(t *testing.T, commitsPerTap int64) (Summary, int64) { + t.Helper() + state := newHarnessWithSpec(t, spec) + device := &submitsOnTapDriver{ + Driver: state.mock, + commitsPerTap: commitsPerTap, + composingRead: 3, + composingThrough: 5, + } + + ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second) + defer cancel() + summary, err := Run(ctx, Options{ + Duration: time.Hour, + IdleTimeout: 20 * time.Millisecond, + MaxSteps: 6, + Driver: device, + Verifier: state.verifier, + TraceWriter: state.writer, + }) + if err != nil { + t.Fatalf("Run: %v", err) + } + if summary.Steps != 6 { + t.Fatalf("steps = %d, want 6", summary.Steps) + } + if summary.SkippedVerification != 3 { + t.Fatalf("the run skipped %d step(s), want 3; the reread never fired across "+ + "the run this test is about", summary.SkippedVerification) + } + return summary, device.committed.Load() + } + + t.Run("no submit is lost to the run of skipped steps", func(t *testing.T) { + summary, committed := run(t, 1) + if committed == 0 { + t.Fatal("the device committed nothing; a runner that never acts passes this " + + "test without meaning anything") + } + if len(summary.Violations) != 0 { + t.Errorf("the counting property convicted a healthy app: %v\n"+ + "one transaction per submit rose, and a submit went unreported because "+ + "the runner acted on a step the verifier skipped", summary.Violations) + } + if committed != 3 { + t.Errorf("the device committed %d transaction(s), want 3: one per verified "+ + "step (1, 2 and 6) and none from a step nothing would judge", committed) + } + }) + + // The control. Without it a green above proves nothing: a property handed + // no comparable pair is silently vacuous and reports the same empty list. + t.Run("two transactions per tap still convicts across the same run", func(t *testing.T) { + summary, _ := run(t, 2) + if len(summary.Violations) == 0 { + t.Fatal("the counting property missed a double submit; the skipped steps left " + + "it with nothing to judge, so the case above proves nothing") + } + if got := summary.Violations[0].Properties[0]; got != "submitCommitsOneTransactionPerAction" { + t.Errorf("violated %v, want submitCommitsOneTransactionPerAction", + summary.Violations[0].Properties) + } + }) +} + +// A screen that changes shape under every pair of reads (a live list, a spinner +// mounting and unmounting) costs the run its actions: an action applied onto it +// would be the one the next verified step never hears about, and there is no +// next verified step. What the run must not do is come back green off that, +// which is what the "judged by nothing" count and the run's outcome are for. +func TestRunner_AScreenThatNeverSettlesActsOnNothingAndSaysSo(t *testing.T) { state := newHarnessWithSpec(t, specWithFolioPredicates(t)) - device := &submitsOnTapDriver{Driver: state.mock, everyRead: true} + device := &submitsOnTapDriver{Driver: state.mock, commitsPerTap: 1, everyRead: true} ctx, cancel := context.WithTimeout(context.Background(), 30*time.Second) defer cancel() @@ -264,13 +353,17 @@ func TestRunner_AScreenThatNeverSettlesDoesNotStallTheRun(t *testing.T) { if err != nil { t.Fatalf("Run: %v", err) } + if summary.Steps != 5 { + t.Fatalf("steps = %d, want 5; the run stalled instead of finishing its budget", + summary.Steps) + } if summary.SkippedVerification != 5 { t.Fatalf("the run verified some step of a screen that never settled: skipped %d of 5", summary.SkippedVerification) } - if device.committed.Load() == 0 { - t.Error("the fuzzer never acted across 5 steps; a screen that keeps moving must " + - "cost the run a step or two, not all of them") + if got := device.committed.Load(); got != 0 { + t.Errorf("the fuzzer applied %d action(s) onto a screen no property would judge; "+ + "each one is an action no spec will ever be told about", got) } } diff --git a/internal/runner/runner.go b/internal/runner/runner.go index a7aac31..36f8ef8 100644 --- a/internal/runner/runner.go +++ b/internal/runner/runner.go @@ -100,7 +100,6 @@ func Run(ctx context.Context, options Options) (Summary, error) { deadline := summary.StartTime.Add(options.Duration) stepIndex := 0 consecutiveApplyFailures := 0 - heldSteps := 0 var lastAction *verifier.Action var lastLogTime time.Time for time.Now().Before(deadline) { @@ -287,16 +286,16 @@ func Run(ctx context.Context, options Options) (Summary, error) { // their effects would then see an effect whose cause the runner // swallowed. See TestRunner_ASkippedStepDoesNotSwallowTheActionBeforeIt. // - // Bounded, because a screen that never settles must not stall the whole - // run: past the bound the runner acts anyway, which is where it was - // before this held anything back. - held := skippedVerification && heldSteps < maxHeldSteps + // Unbounded, because lastAction holds exactly one action: any bound that + // let the runner act again while the verifier was still being skipped + // would overwrite the action the hold was carrying, and that is the same + // swallow arriving one step later. A screen that keeps moving therefore + // costs the run its actions rather than its soundness, and a run that + // verified nothing says so in its outcome (internal/testrun). + held := skippedVerification if held { - heldSteps++ logger.Warn("screen still moving; holding this step's action back", - "step", stepIndex, "held", heldSteps) - } else { - heldSteps = 0 + "step", stepIndex) } var nextAction verifier.Action @@ -401,7 +400,16 @@ func Run(ctx context.Context, options Options) (Summary, error) { // concurrent fetches observe a stable post-action state. A transient // apply error means nothing landed, so the idle poll has nothing to // settle and may itself hang on the same device condition. - if nextErr == nil && !applySkipped && nextAction.Kind != verifier.ActionKindWait { + // + // A held step settles too, and it is the only case here that waits with + // nothing applied. The reread that held it takes its two reads a round + // trip apart, which is a tighter window than the one the detector was + // measured over (an action and a settle); looping straight back into it + // would compare two reads of a composing screen closer together still, + // so the screen that most needs to settle is the one given least room. + applied := nextErr == nil && !applySkipped && + nextAction.Kind != verifier.ActionKindWait + if held || applied { idleCtx, idleCancel := context.WithTimeout(ctx, options.IdleTimeout) idleErr := options.Driver.WaitForIdle(idleCtx, options.IdleTimeout) if idleErr != nil && idleCtx.Err() == nil { @@ -1316,14 +1324,6 @@ func encodeResiduals(residuals map[string]ltl.Formula) (map[string]json.RawMessa // would be spent doing nothing. const maxConsecutiveApplyFailures = 3 -// maxHeldSteps bounds how many steps in a row the runner will decline to act on -// because their screen was still moving. It is a livelock bound, not a settle -// budget: a screen that changes shape under every pair of reads (a live list, a -// spinner that mounts and unmounts) would otherwise take the whole run without -// the fuzzer ever touching it. Two is what the measured cases need, which came -// one step at a time and never twice in a row. -const maxHeldSteps = 2 - // isWDADrop reports that the sidecar could not restart the iOS XCTest // runner: the channel is gone for good and the run must abort. Transient // drops are classified by the sidecar itself (it reconnects and surfaces