fix(runtime): mark order dependence on chained places and same-step sibling reads

changes/unreleased/order-marks-chained-places.fixed.md

@@ -0,0 +1 @@
+- A value reached through a part (`sensor.raw` written by racing branches, `sensor.scaled = raw * 10`, a value read from either after the join) is now reported `order-dependent` where `-schedule explore` proves more than one outcome: the result surface read what a part's object holds under a fresh run, losing the run's marks, and an object's feature valued by an expression recorded nothing of what it read; the place is the part's, so two parts of one definition hold two values of its feature and `left.raw` racing leaves `right.raw` bare. A sibling branch reading a feature its sibling writes in the same step now marks what it writes from the read (`z := x` beside `x := 1`: `z` open), while the feature written once (`x`) stays bare, as does what a branch writes from no such read; a conformance test asserts over every order fixture that the names marked are exactly those exploration varies.

cmd/sysml/check_engine_test.go

@@ -576,11 +576,11 @@ func TestEngineCheckWitnessOfBehaviorsOnOneClockReplays(t *testing.T) {
 			t.Fatal(err)
 		}
 		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; order-dependent: lit)") {
+			!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; order-dependent: saw)") {
 			t.Errorf("witness %d:\n%s", c.n, content)
 		}
 		replayed := check(t, binary, lampModel, "-schedule", "replay:"+name(c.n), "-trace", "-instantiate", "Shine::Lamp", "-action", peek, "-state", glow, "-advance", "3")
-		wantReport(t, replayed, 0, "ran "+c.first+" first; order-dependent: lit)", "saw = "+c.saw, "Current state: on",
+		wantReport(t, replayed, 0, "ran "+c.first+" first; order-dependent: saw)", "saw = "+c.saw, "Current state: on",
 			"standing: value (observed: 1 run under replay:"+name(c.n)+")")
 	}
 }

docs/internals/design/scheduling.md

@@ -113,8 +113,19 @@ already uses — `check_reduce.go`, `future_footprint.go`; there is no second co
   `Footprint.DependentBy` pairwise over the footprints less control convergence (meeting at a join
   or both completing a performance changes no value). No dependent pair: the alternatives commute,
   the choice is `Independent`, and the run's values do not depend on it. A dependent pair: the
-  choice is unresolved, and `Touches` names the features a write of either meets in the other
-  (`Relation.PlaceMeets`); a pair that meets only on a channel or through a dynamic target
+  choice is unresolved, and `Touches` names the places whose values the order decides
+  (`touchMeeting`, `Relation.PlaceMeets`): a place both alternatives write, and, where a write of
+  one meets a *read* of the other, what the reading alternative writes from that read — the
+  statements of its body whose flow reads the place (`lower.Footprint.Flows`, one data flow per
+  statement, `Footprint.WritesReading`), or every write of the alternative when the read is not a
+  statement's (a guard's) or the move is described whole. The rule throughout: a value is marked
+  if and only if exploration proves more than one outcome for it. So the place read is not
+  touched by the meeting — a once-written feature read by a racing sibling holds one value
+  whichever order ran, and a mark on it would assert an openness exploration refutes — while
+  what the reader writes from it is (`action_order_sibling_read_of_racing_write`: `z` open, `x`
+  bare). A pin is
+  each performance's own, delivered to rather than raced for, and is neither touched nor a read
+  that touches (`shared`). A pair that meets only on a channel or through a dynamic target
   (`Footprint.Dynamic`: a property read or a chained target the declarations do not decide) touches
   every write of both, conservatively.
 - `classifyExclusive` is for alternatives of which one runs and the others do not — a decision's
@@ -172,7 +183,19 @@ tracker and never by re-reading declarations in the runtime:
   the places behind `Touches`) with itself (`orderMarks.seed`, from `Context.noteFrom`): another
   order may have written them otherwise. A value reported under a name reads the marks of the
   places that name denotes as `choiceTouches` resolves them (`placeNamed`: a bare name is the
-  behavior's own feature, `this.<name>` the performing object's).
+  behavior's own feature, `this.<name>` the performing object's, `<part>.<name>` a feature of the
+  object a part of the behavior denotes, which no performer owns). A place is the feature written
+  whatever path reaches it: `assign sensor.raw := 1` through the part `sensor` writes the place of
+  `Sensor::raw` (`footprintBuilder.path`), the same place a later `sensor.raw` reads, so a chained
+  feature stands open where a plain one would (`action_order_chained_write_of_racing_writers`,
+  `action_order_chained_two_level_write`). The place remembers the feature it was reached
+  through (`Place.Via`, the part's object `Instance.heldBy` for a write or derivation the run
+  makes); whether two such places hold one value is the run's to say (`Context.heldAlike`: the
+  parts denote an object in common), not the declarations' (`Place.Conflicts` stays
+  conservative for the checker's reduction, as features may alias). So `left.raw` racing
+  leaves `right.raw`, `right.scaled` and a read of them bare, while `twin = cell` writing
+  `twin.mark` races `cell.mark` (`action_order_chained_parts_apart`,
+  `action_order_chained_alias_of_racing_writers`).
 - **Propagate.** A move with footprint `fp` that writes `w` leaves `w` standing on what `fp` read
   — the union of the marks of every place in `fp.Reads` — together with the *control* the move
   runs under; a footprint the declarations do not decide (`fp.Dynamic`: a property read, a chained
@@ -182,7 +205,14 @@ tracker and never by re-reading declarations in the runtime:
   performance's inputs stand on what they are bound from as it begins and its outputs, as it ends,
   on those and on what its body left on its own pins (`performances.markPerformance` over
   `BindingFootprints`: features, pin bindings, flows and the accepted payload, less the body's
-  statements, which are recorded one by one).
+  statements, which are recorded one by one). A feature valued by an expression is rewritten with
+  what its expression read as it is derived, the behavior's own (`deriveBodyCell`) and an object's
+  (`Instance.materializeDerived`: `sensor.scaled = raw * 10` stands where `raw` does) alike
+  (`Context.deriveMarks` over `lower.ExpressionFootprint`). Reporting reads under the run that
+  produced the values: `ActionExecutor.ResultsWithError` derives what a part's object holds under
+  the executor's own run state (`enterRun`), since a derivation begun as a run of its own would
+  install a fresh state and the marks of the run just ended would be gone before the surface read
+  them — which is how a value reached through a part was once reported bare.
 - **Clear.** Since the write *replaces* the marks of `w`, a write that reads nothing
   order-dependent, under no control, clears `w` from that point on: the mark describes the value.
   It replaces the marks of the one declaration it writes (`samePlace`): a same-named feature of

docs/project/behavior-semantic-oracle.md

@@ -2451,6 +2451,69 @@ by an expression stands on the places its lowered expression reads, through feat
 in turn, at the moment it is read, and a write from it stands on those places as a write from
 them directly would.
 
+### A feature reached through a part stands on the choice points its writers race at
+
+Fixtures: `action_order_chained_write_of_racing_writers`, `action_order_chained_two_level_write`,
+`action_order_chained_read_of_unraced_stays_bare`, `action_order_chained_parts_apart`,
+`action_order_chained_alias_of_racing_writers` (golden, explored).
+
+```
+part def Sensor { attribute raw : Integer = 0;  attribute scaled : Integer = raw * 10; }
+part sensor : Sensor;
+start → split ⇉ a { sensor.raw := 1 } ─┐
+              ⇉ b { sensor.raw := 2 } ─┘→ sync → derive { z := sensor.raw; zz := sensor.scaled } → done
+```
+
+Derived constraints:
+
+- `sensor.raw` is a feature of the one object the action's part denotes, reached through the
+  part by a feature chain (KerML 1.1 §7.3.4.6); the two branches write that one place, and
+  `sensor.scaled` is bound to an expression over it, computed as it is read.
+- `sync` follows both writes, so the reads after it see the `raw` that stands after both:
+  `{raw = 1, scaled = 10, z = 1, zz = 10}` or `{raw = 2, scaled = 20, z = 2, zz = 20}`. A chain two
+  parts deep (`car.engine.rpm`) names one place the same way.
+
+Open: the order of the two branches, exactly as for a feature of the action's own. A place is
+the feature written whatever path reaches it, so the chained place stands open where a plain
+one would, and so does everything read or computed from it. A feature reached through a part
+that no racing branch writes (`sensor.raw` written once before the fork while `x` races) is
+fixed, and a value read from it after the join is fixed with it. Two parts of one definition
+(`left`, `right : Sensor`) hold two values of its feature: `left.raw` racing leaves `right.raw`,
+`right.scaled` and a value read from them fixed; a reference part bound to a part (`ref part twin = cell`)
+holds the same object, so `twin.mark` written beside `cell.mark` races it.
+
+Pinned outcome: the admissible set of two members in each fixture, stated as `outcomes` citing
+this section. The default run reports `sensor.raw`, `sensor.scaled`, `z` and `zz` up to the same
+two choice points (`orderDependent` states each `2`); in the two-level fixture `z` alone, the
+chained place itself not being among the results; in the unraced fixture `x` and the read of it
+alone, the chained reads bare; in the two-parts fixture `left.raw` and `left.scaled` alone.
+
+### A read racing a write of the same feature stands on the choice point between them
+
+Fixture: `action_order_sibling_read_of_racing_write` (golden, explored).
+
+```
+start → split ⇉ a { x := 1 } ─┐
+              ⇉ b { z := x } ─┘→ sync → done
+```
+
+Derived constraints:
+
+- Neither branch is ordered before the other (no HappensBefore between them), so `b` reads
+  `x` either before or after `a` writes it: `{x = 1, z = 0}` or `{x = 1, z = 1}`.
+- `x` holds `1` in every linearization: the one write of it is not raced by another write.
+
+Open: the order of the two branches, as for two writers of one feature, met here by a write
+and a read of the same place. The write cannot commute with the read, so the choice point
+touches what the reading branch writes from the place: `z` is open with the single choice
+point. `x` is not: one write of it stands whichever order ran, so a mark on it would assert an
+openness exploration refutes. A write of the reading branch standing on no read the other
+writes (`doneA := true` beside `total := total + 1`) is fixed the same way.
+
+Pinned outcome: the admissible set of two members, stated as `outcomes` citing this section.
+The default run reports `z` up to the one choice point and `x` bare (`orderDependent` states
+`z: 1`).
+
 ### A guard reading an order-dependent value leaves what its branch writes order-dependent
 
 Fixture: `action_order_guard_reads_racing_writer` (golden, explored).