[rgamba]

Stacked on #46 (base: feat/child-workflow-builder).

Problem

For a due task, SchedulerExecutionQueue.schedule writes a backstop row that honours any active lease, then queues an in-memory copy in this JVM. It queued that copy no matter what the write did. So when the row was already leased, by a worker that fetched it or by a copy queued in another JVM, the workflow ran twice at once. Three paths get there:

• an in-process startWorkflow of a running workflow with CREATE_EXISTING_WORKFLOW_IS_NOOP off;
• an in-process signal (FORCE_SIGNAL_WORKFLOW_EXEC_IN_SCHEDULER off), including one sent while this JVM's own copy is running;
• a start that stalls between its two writes for longer than a lease while another start recovers it.

#46 sidestepped this for the stranded-start recovery only (scheduleAfterLease). This fixes it in the queue.

Approach

• The scheduler reports what it did. Scheduler.scheduleWithOutcome returns ScheduleOutcome(task, leaseHonored). The lease check and the write are one transaction, so only the store can answer this without a race. SQLite and MySQL implement it, and schedule delegates to it. The interface default reports "not honoured", so a third-party Scheduler keeps today's behaviour until it overrides it.
• The queue keeps no copy on an honoured lease. It also returns Scheduled(task, queuedInMemory), so callers know whether a copy carrying their payload will run here.
• The workflow is still driven. With BUMP_TASK_VERSION_ON_HONORED_LEASE (on by default), the honoured write bumps the row version. The holder's final remove then fails, and finishTask reruns the task at once. A row that nobody is running is delivered when it comes due or its lease lapses.
• Callers don't hang. When an in-process start or signal queued no copy, the engine fails the instance's result future with ResultUnavailable, as a runAsync start does. The proxy then reads the result from storage. Without this, a synchronous caller would wait forever on a future nobody completes. This also covers the existing "a copy is already queued here" case, which had the same problem.

Trade-offs

• An in-process call on an instance that is running elsewhere now polls storage for its result (resultPollingTimeLimit, 30 s by default) instead of getting it from a second, concurrent run. A run that takes longer surfaces as a TimeoutException, as it does for runAsync.
• Task.hasActiveLease also holds for a row that is only due within a lease: a short retry backoff, or feat: retry the parent when a child workflow started with asChildOf fails to start #46's after-a-lease row. An in-process schedule now waits for that row instead of running at once. The persistent path already has this latency, and it can't double-run.
• With this fix, feat: retry the parent when a child workflow started with asChildOf fails to start #46's scheduleAfterLease is no longer needed for safety: the model passes with the stranded start scheduled like any other start. I left it alone to keep this change narrow. Switching the recovery back to the ordinary path would be a small follow-up, and it would also make the recovering caller's result available again.
• Kotlin by delegation doesn't forward Java default methods, so a Scheduler wrapper must forward scheduleWithOutcome itself. The interface Javadoc says so, and the three test wrappers that use by now do.

Testing

Unit

• QueueBasedSchedulerTest (two queues sharing one persistent scheduler, i.e. two nodes):

  • both schedule in memory, and only one holds a copy;
  • a second schedule from the node whose copy is running queues nothing;
  • an honoured schedule bumps the version, so the holder's remove fails, which is the rerun signal;
  • feat: retry the parent when a child workflow started with asChildOf fails to start #46's scheduleAfterLease-then-in-memory case is updated: the row now delivers the task after the lease.

  All four fail with the honour check disabled.

• BaseSchedulerTest covers scheduleWithOutcome on SQLite and MySQL.

• SkipperEngineTest checks that an in-process start with no copy queued gets ResultUnavailable.

Integration

• New InMemoryScheduleOnLeasedTaskTest: an in-process signal arrives during an in-process run. With the check disabled it fails with expected: <1> but was: <2> executions, a real second run entering the action. With the fix it passes.

Full suite: green locally, except the MySQL suites: MariaDB4j can't start on my machine, and CI runs them. spotlessCheck is clean.

Model check (formal/tla/check.sh, tla2tools v1.7.4). All 16 models match their expected verdicts. What changed:

Model	Before	After
inmem_overlap (new): two JVMs start a running workflow in process, plus an in-process signal; NoLongPauses	NoOverlappingRuns violated in 8 steps (= the calibration)	ok, liveness included (996,207 distinct states)
inmem_overlap_unguarded (new calibration: copy queued on an honoured lease)	–	NoOverlappingRuns violated
start_race_unguarded with only RecoverAfterLease off	NoOverlappingRuns violated	ok. Recorded as new model start_race_recover_in_memory; start_race_unguarded now turns off both guards and still fails
start_race / inmem_overlap, with NoLongPauses no longer assuming a start never stalls between its two writes	–	ok. The model now drops that half of the assumption
inmem_start	RunningIsDriven	RunningIsDriven (unchanged)
inmem_start + NoOverlappingRuns (side experiment, not committed)	violated	still violated: a lease lapses under a copy that waits in its queue (finding 3), which this change doesn't address

All other models are unchanged.

Trace validation (record_traces.sh, then check_traces.sh --self-test):

• 111 of 111 in-scope runs accepted, 122 skipped, and 545 of 545 mutants rejected.
• None of the existing traced runs went through the honoured-lease path (0 of 118 in-memory schedules), which is why the new integration test exists. Its trace is accepted. With the engine changed back to queueing the copy, that trace is rejected at the second run's first read.