amadan

carlos / platform Public

host: the probe's policy rows and the session's continuing spawn (Plan 3 Task 5, H3, H4)

probing grants held-config, held-release and spawn; the spawn carries the
launch identity bound to the pins. The admitted session's spawn selection
continues along the landing's session row (probing, probed, committed),
so the probe's replication survives the probed and committed CASes.
Co-Authored-By: Claude Opus 5.5 <noreply@anthropic.com>
claude 10511249c25bf09dfa120ddb0d629cd8f225b14b parent abcc732
3 files changed, +174 −14
  • internal/host/movespolicy.go +55 −10
  • internal/host/movespolicy_test.go +8 −4
  • internal/host/movesprobe_policy_test.go +111 −0
diff --git a/internal/host/movespolicy.go b/internal/host/movespolicy.go
index 6b6bf7885..00060ebad 100644
--- a/internal/host/movespolicy.go
+++ b/internal/host/movespolicy.go
@@ -37,13 +37,16 @@ import (
// at local; held-config, held-release, restore and install at
// configured, the phase whose work installs the database before its
// closing CAS writes restored (G8; the final review's finding 3), so
-// restored, the install complete, grants none of them. These are the
-// phases Plan 2 built (checking to restored). The probe's rights at probing (spawn, seed, writer, and the
-// held render before every probe, §7.7) and the ordinary wake rights at
-// committed (§19.1) are Plan 3's rows, added when the probe is built;
+// restored, the install complete, grants none of them. probing (Plan 3
+// Task 5) grants the held render, the held release and the spawn the
+// probe's whole admitted sequence runs under; probed grants nothing to
+// a fresh selection, and the probe's own spawn selection continues at
+// probed and committed on the same session (H3). The ordinary wake
+// rights at committed (§19.1) are Task 7's row;
// - the identity fits the action: a held-config write names the config
// and nothing else, a held-release write names the release and nothing
-// else, and every other action carries no identity;
+// else, the probe's spawn names the launch identity (the pinned config
+// and release, H4), and every other action carries no identity;
// - a held write names the move's pinned inputs (§9.1, §9.2). Policy.Inputs
// is consulted for serving claims only (wakepolicy.go), so this policy
// reads the record itself, through the reader it is built with: the
@@ -195,9 +198,30 @@ const (
// gates the release and installs the database; its closing CAS writes
// restored (G8), so restored grants nothing. A phase or action not listed is
// refused.
+//
+// probing (Plan 3 Task 5, H4) is the probe's: the held render and the held
+// release before every start (§7.7), and the spawn, which carries the launch
+// identity bound to the pins. The admitted session's restore, launch record,
+// launch and replication all run under that one spawn selection (claim Plan
+// 9 Group D), so restore, seed and writer get no row. probed grants nothing
+// to a fresh selection; committed's ordinary wake is Task 7's row.
var movesPhaseRights = map[string]map[string]bool{
provision.LandLocal: {movesActionHeldTimers: true},
provision.LandConfigured: {movesActionHeldConfig: true, movesActionHeldRelease: true, movesActionRestore: true, movesActionInstall: true},
+ provision.LandProbing: {movesActionHeldConfig: true, movesActionHeldRelease: true, movesActionSpawn: true},
+}
+
+// movesSessionContinues reports whether the claim's phase may differ from
+// the selection's (H3, claim Plan 9 D1): only the admitted session's own
+// spawn selection, and only along the landing's session row
+// (hostclaim.SessionObserves: probing, probed, committed), so the probe's
+// replication and process survive the probed and committed CASes. The
+// rights stay the ones of the phase the selection was made at.
+func movesSessionContinues(c *hostclaim.Claim, s hostbox.Selection) bool {
+ if c.Op.Phase == s.Phase {
+ return true
+ }
+ return s.Action == movesActionSpawn && hostclaim.SessionObserves(c.Op.Kind, s.Phase, c.Op.Phase)
}
// movesPolicyActions is every action the policy knows. Anything else is
@@ -239,7 +263,7 @@ func MovesClaimPolicy(read MovesRecordReader) func(context.Context, *hostclaim.C
if c.Op.ID != s.Op {
return refuse("the claim is under another op", nil)
}
- if c.Op.Kind != s.Kind || c.Op.Phase != s.Phase {
+ if c.Op.Kind != s.Kind || !movesSessionContinues(c, s) {
return refuse("the claim's kind or phase is not the selection's", nil)
}
if s.Captured.Stamp == 0 || c.Holder.Stamp != s.Captured.Stamp || c.Holder.Incarnation != s.Captured.Incarnation {
@@ -268,13 +292,18 @@ func MovesClaimPolicy(read MovesRecordReader) func(context.Context, *hostclaim.C
return refuse("this box is declared lost", nil)
}
}
- if !movesPhaseRights[c.Op.Phase][s.Action] {
+ if !movesPhaseRights[s.Phase][s.Action] {
return refuse("the phase does not permit the action", nil)
}
- if !movesIdentityFits(s.Action, id) {
+ probeSpawn := s.Phase == provision.LandProbing && s.Action == movesActionSpawn
+ if probeSpawn {
+ if !recoveryIdentityFits(s.Action, id) {
+ return refuse("the identity does not fit the action", nil)
+ }
+ } else if !movesIdentityFits(s.Action, id) {
return refuse("the identity does not fit the action", nil)
}
- if s.Action != movesActionHeldConfig && s.Action != movesActionHeldRelease {
+ if s.Action != movesActionHeldConfig && s.Action != movesActionHeldRelease && !probeSpawn {
return nil
}
// The held config and release are the move's pinned inputs (§9.1,
@@ -289,13 +318,29 @@ func MovesClaimPolicy(read MovesRecordReader) func(context.Context, *hostclaim.C
if err != nil {
return refuse("the record cannot be read", err)
}
- if rec == nil || rec.Host != c.Host || rec.Move == nil || rec.Move.ID != s.Op || rec.Move.Incarnation != c.Holder.Incarnation || rec.Move.State != provision.MoveLanding {
+ if rec == nil || rec.Host != c.Host || rec.Move == nil || rec.Move.ID != s.Op || rec.Move.Incarnation != c.Holder.Incarnation {
+ return refuse("the record is not this landing", nil)
+ }
+ switch {
+ case probeSpawn:
+ // The probe's launch is this landing's, unmarked, or the same
+ // session continuing once the record is committed (H3).
+ if (rec.Move.State != provision.MoveLanding || rec.Move.Reason != "") && rec.Move.State != provision.MoveCommitted {
+ return refuse("the record is not this landing", nil)
+ }
+ case rec.Move.State != provision.MoveLanding:
return refuse("the record is not this landing", nil)
}
in := rec.Move.Inputs
if in == nil {
return refuse("no pinned inputs", nil)
}
+ if probeSpawn {
+ if in.Release == "" || id.Config != HeldConfigIdentity(in.BundleETags, in.OverlayETag).Config || id.Release != in.Release {
+ return refuse("the launch is not the pinned one", nil)
+ }
+ return nil
+ }
switch s.Action {
case movesActionHeldRelease:
if in.Release == "" {
diff --git a/internal/host/movespolicy_test.go b/internal/host/movespolicy_test.go
index 1cce1d76f..4cbcc731d 100644
--- a/internal/host/movespolicy_test.go
+++ b/internal/host/movespolicy_test.go
@@ -99,6 +99,9 @@ func TestMovesClaimPolicyGrantsByPhase(t *testing.T) {
granted := map[string]map[string]bool{
provision.LandLocal: {"held-timers": true},
provision.LandConfigured: {"held-config": true, "held-release": true, "restore": true, "install": true},
+ // The probe's rows (Plan 3 Task 5): its spawn needs the launch
+ // identity, which mpIdentity does not give it (movesprobe_policy_test).
+ provision.LandProbing: {"held-config": true, "held-release": true},
}
phases := append(provision.LandingOrder(), "committed")
moves, reader := mpPolicy()
@@ -128,12 +131,13 @@ func TestMovesClaimPolicyGrantsByPhase(t *testing.T) {
}
}
}
- if grants != 5 {
- t.Fatalf("%d cells granted, want 5", grants)
+ if grants != 7 {
+ t.Fatalf("%d cells granted, want 7", grants)
}
// The record is read for the held config and release only: twice per
- // pass over the table (the direct call and Policy.Check), at configured.
- if reader.reads != 4 || !reflect.DeepEqual(reader.args, []string{"bab", "titogo", mpHost}) {
+ // pass over the table (the direct call and Policy.Check), at configured
+ // and at probing.
+ if reader.reads != 8 || !reflect.DeepEqual(reader.args, []string{"bab", "titogo", mpHost}) {
t.Fatalf("record reads: %d %v", reader.reads, reader.args)
}
}
diff --git a/internal/host/movesprobe_policy_test.go b/internal/host/movesprobe_policy_test.go
new file mode 100644
index 000000000..c77a5e23d
--- /dev/null
+++ b/internal/host/movesprobe_policy_test.go
@@ -0,0 +1,111 @@
+package host
+
+import (
+ "context"
+ "errors"
+ "testing"
+
+ "github.com/carlosframework/platform/internal/hostbox"
+ "github.com/carlosframework/platform/internal/hostclaim"
+ "github.com/carlosframework/platform/internal/hostwrite"
+ "github.com/carlosframework/platform/internal/provision"
+)
+
+// mpLaunch is the probe's launch identity (Plan 3 H4): the pinned config
+// and the pinned release it launches with.
+func mpLaunch() hostwrite.Identity {
+ p := mpPins()
+ return hostwrite.Identity{Config: HeldConfigIdentity(p.BundleETags, p.OverlayETag).Config, Release: p.Release}
+}
+
+func mpProbingRecord() *provision.Record {
+ rec := mpRecord()
+ rec.Move.LandingPhase = provision.LandProbing
+ return rec
+}
+
+// The probe's rows (Plan 3 Task 5, H4): at probing the held render, the
+// held release and the spawn are granted, the spawn only with the launch
+// identity bound to the pins, through hostbox.Policy.Check with the hold the
+// landing has. probed grants nothing to a fresh selection.
+func TestMovesClaimPolicyProbingRows(t *testing.T) {
+ ctx := t.Context()
+ moves := MovesClaimPolicy((&mpReader{rec: mpProbingRecord()}).read)
+ policy := hostbox.Policy{Moves: moves, Held: func(context.Context, string) (string, error) { return mpOp, nil }}
+ probing := mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbing)
+ for action, id := range map[string]hostwrite.Identity{
+ "held-config": mpIdentity("held-config"),
+ "held-release": mpIdentity("held-release"),
+ "spawn": mpLaunch(),
+ } {
+ if err := policy.Check(ctx, probing, mpSelection(probing, action), id); err != nil {
+ t.Fatalf("probing/%s: %v", action, err)
+ }
+ }
+ for _, action := range []string{"held-timers", "restore", "seed", "writer", "install"} {
+ if err := policy.Check(ctx, probing, mpSelection(probing, action), hostwrite.Identity{}); err == nil {
+ t.Fatalf("probing/%s was granted", action)
+ }
+ }
+ refused := func(err error, reason string) {
+ t.Helper()
+ var r *MovesPolicyRefusal
+ if !errors.As(err, &r) || r.Reason != reason {
+ t.Fatalf("got %v, want the refusal %q", err, reason)
+ }
+ }
+ s := mpSelection(probing, "spawn")
+ refused(moves(ctx, probing, s, hostwrite.Identity{}), "the identity does not fit the action")
+ refused(moves(ctx, probing, s, hostwrite.Identity{Config: mpLaunch().Config}), "the identity does not fit the action")
+ refused(moves(ctx, probing, s, hostwrite.Identity{Config: mpLaunch().Config, Release: "v9"}), "the launch is not the pinned one")
+ refused(moves(ctx, probing, s, hostwrite.Identity{Config: HeldConfigIdentity(nil, "x").Config, Release: mpPins().Release}), "the launch is not the pinned one")
+ noPins := mpProbingRecord()
+ noPins.Move.Inputs = nil
+ refused(MovesClaimPolicy((&mpReader{rec: noPins}).read)(ctx, probing, s, mpLaunch()), "no pinned inputs")
+ marked := mpProbingRecord()
+ marked.Move.Reason = provision.RollbackProbeAttempts
+ refused(MovesClaimPolicy((&mpReader{rec: marked}).read)(ctx, probing, s, mpLaunch()), "the record is not this landing")
+
+ probed := mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbed)
+ for _, action := range mpActions {
+ if err := policy.Check(ctx, probed, mpSelection(probed, action), mpLaunch()); err == nil {
+ t.Fatalf("a fresh probed/%s selection was granted", action)
+ }
+ }
+}
+
+// The admitted probe session survives the landing's forward steps (H3): its
+// spawn selection, made at probing, is still granted once the claim is at
+// probed and then committed, with the same session; a held render selected
+// at probing is not, and no backward or skipped step is.
+func TestMovesClaimPolicyProbeSessionContinues(t *testing.T) {
+ ctx := t.Context()
+ reader := &mpReader{rec: mpProbingRecord()}
+ moves := MovesClaimPolicy(reader.read)
+ policy := hostbox.Policy{Moves: moves, Held: func(context.Context, string) (string, error) { return mpOp, nil }}
+ selected := mpSelection(mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbing), "spawn")
+ for phase, state := range map[string][2]string{
+ hostclaim.PhaseLandingProbed: {provision.MoveLanding, provision.LandProbed},
+ hostclaim.PhaseLandingCommitted: {provision.MoveCommitted, ""},
+ } {
+ c := mpClaim(hostclaim.KindLanding, phase)
+ reader.rec = mpProbingRecord()
+ reader.rec.Move.State, reader.rec.Move.LandingPhase = state[0], state[1]
+ if err := policy.Check(ctx, c, selected, mpLaunch()); err != nil {
+ t.Fatalf("the probe's spawn at %s: %v", phase, err)
+ }
+ }
+ reader.rec = mpProbingRecord()
+ held := mpSelection(mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbing), "held-config")
+ if err := policy.Check(ctx, mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbed), held, mpIdentity("held-config")); err == nil {
+ t.Fatal("a held render selected at probing was granted at probed")
+ }
+ restored := mpSelection(mpClaim(hostclaim.KindLanding, provision.LandRestored), "spawn")
+ if err := policy.Check(ctx, mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbing), restored, mpLaunch()); err == nil {
+ t.Fatal("a spawn selected at restored was granted at probing")
+ }
+ back := mpSelection(mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbed), "spawn")
+ if err := policy.Check(ctx, mpClaim(hostclaim.KindLanding, hostclaim.PhaseLandingProbing), back, mpLaunch()); err == nil {
+ t.Fatal("a backward step was granted")
+ }
+}