| 1 | package host |
| 2 | |
| 3 | import ( |
| 4 | "testing" |
| 5 | |
| 6 | "github.com/carlosframework/platform/internal/hostclaim" |
| 7 | ) |
| 8 | |
| 9 | func plan9D1Session(phase string, session uint64) hostclaim.Observed { |
| 10 | return hostclaim.Observed{Host: recoveryHost, Claim: &hostclaim.Claim{Host: recoveryHost, |
| 11 | Holder: &hostclaim.Holder{Incarnation: "inc", Location: "instances/" + recoveryHost, Generation: "m1", Stamp: 10, Session: session, WriterBox: "uk-box"}, |
| 12 | Op: hostclaim.Op{Kind: hostclaim.KindLanding, ID: "m1", Phase: phase, Exec: "uk-box"}}} |
| 13 | } |
| 14 | |
| 15 | // The wake's write identity follows the session table one adjacent step at |
| 16 | // a time (M9): a probe session checked at probing is itself at probed for |
| 17 | // Prepare, not at committed, and nothing else is. Its stop identity follows |
| 18 | // the row forward to any later phase (R1): stopping grants no authority, so a |
| 19 | // probe that reached committed unseen is still stopped as itself. Neither |
| 20 | // follows a new session or a step back. |
| 21 | func TestPlan9D1WriterIdentityFollowsTheSessionTable(t *testing.T) { |
| 22 | probing := plan9D1Session(hostclaim.PhaseLandingProbing, 11) |
| 23 | for _, tc := range []struct { |
| 24 | name string |
| 25 | later hostclaim.Observed |
| 26 | continues, reaches func(string, string, string) bool |
| 27 | write, stop bool |
| 28 | }{ |
| 29 | {"same", plan9D1Session(hostclaim.PhaseLandingProbing, 11), nil, nil, true, true}, |
| 30 | {"main-equality", plan9D1Session(hostclaim.PhaseLandingProbed, 11), nil, nil, false, false}, |
| 31 | {"probed", plan9D1Session(hostclaim.PhaseLandingProbed, 11), hostclaim.SessionContinues, hostclaim.SessionReaches, true, true}, |
| 32 | {"skipped", plan9D1Session(hostclaim.PhaseLandingCommitted, 11), hostclaim.SessionContinues, hostclaim.SessionReaches, false, true}, |
| 33 | {"new-session", plan9D1Session(hostclaim.PhaseLandingCommitted, 12), hostclaim.SessionContinues, hostclaim.SessionReaches, false, false}, |
| 34 | {"backward", plan9D1Session("restored", 11), hostclaim.SessionContinues, hostclaim.SessionReaches, false, false}, |
| 35 | } { |
| 36 | if got := claimSameWriter(probing, tc.later, tc.continues); got != tc.write { |
| 37 | t.Errorf("%s: claimSameWriter = %v, want %v", tc.name, got, tc.write) |
| 38 | } |
| 39 | if got := sameStopWriter(probing, tc.later, tc.reaches); got != tc.stop { |
| 40 | t.Errorf("%s: sameStopWriter = %v, want %v", tc.name, got, tc.stop) |
| 41 | } |
| 42 | } |
| 43 | probed, committed := plan9D1Session(hostclaim.PhaseLandingProbed, 11), plan9D1Session(hostclaim.PhaseLandingCommitted, 11) |
| 44 | if !claimSameWriter(probed, committed, hostclaim.SessionContinues) || !sameStopWriter(probed, committed, hostclaim.SessionReaches) { |
| 45 | t.Fatal("probed to committed ended the session") |
| 46 | } |
| 47 | for _, back := range []hostclaim.Observed{probing, probed} { |
| 48 | if claimSameWriter(committed, back, hostclaim.SessionContinues) || sameStopWriter(committed, back, hostclaim.SessionReaches) { |
| 49 | t.Fatalf("a later observation stepped back to %s and kept the session", back.Claim.Op.Phase) |
| 50 | } |
| 51 | } |
| 52 | // The stop predicate is bound with the session table and only then. |
| 53 | if (ClaimAssembly{}).stopReaches() != nil || (ClaimAssembly{Wake: &ClaimWakeAssembly{}}).stopReaches() != nil { |
| 54 | t.Fatal("stop reachability bound without the moves C1 session table") |
| 55 | } |
| 56 | if r := (ClaimAssembly{Wake: &ClaimWakeAssembly{Continue: hostclaim.SessionContinues}}).stopReaches(); r == nil || !r(hostclaim.KindLanding, hostclaim.PhaseLandingProbing, hostclaim.PhaseLandingCommitted) || r(hostclaim.KindLanding, hostclaim.PhaseLandingCommitted, hostclaim.PhaseLandingProbing) || r(hostclaim.KindServing, "a", "b") { |
| 57 | t.Fatal("bound stop predicate is not forward reachability on the row") |
| 58 | } |
| 59 | } |
| 60 | |