model

README

Formal Protocol Model

Package model is a deterministic reference implementation of the ShiftLock ownership protocol. It performs no backend I/O. Use it to:

• Continuously verify ownership invariants under randomized action sequences
• Produce minimal reproducible failure sequences (JSON)
• Drive internal/simulation scenarios

Invariants (15)

1. At most one committed owner per claim fencing-token epoch
2. Fencing tokens never decrease
3. Stale generation cannot release newer ownership
4. Failed/expired transfer cannot remain pending forever (bounded by timeout)
5. Aborted transfer restores prior owner without token advance
6. Committed transfer advances token exactly once
7. Unowned claims retain last fencing token
8. Reserved claims still have a controlling owner generation
9. Crash of candidate before commit does not discard ownership
10. Concurrent acquire yields exactly one winner per epoch
11. Expire clears owner but not token
12. Overflow refuses further acquires (claim unavailable)
13. Idempotent ops with same OperationID do not double-advance tokens
14. Disconnect does not invent local lease extensions
15. Only current fencing-token epoch may modify protected resources (model tracks Accept)

Reproduction

On failure, tests print:

go test ./model -run TestRandom -shiftlock.seed=12345

And write testdata/failures/<seed>.json.

Documentation

Index

• Constants
• func CheckTokenMonotonic(prev, cur map[string]uint64) (string, string)
• type Action
• type ActionType
• type Claim
• type ClaimPhase
• type FailureRecord
  • func (f FailureRecord) JSON() string
  • func (f FailureRecord) ReproduceCmd() string
• type GenState
• type Generation
• type Generator
  • func NewGenerator(seed int64, claim string, gens []string) *Generator
  • func (g *Generator) Next() Action
  • func (g *Generator) Sequence(n int) []Action
• type World
  • func NewWorld(leaseTTL, transferTO int64) *World
  • func (w *World) Apply(a Action) error
  • func (w *World) CheckInvariants() (string, string)
  • func (w *World) TokenSnapshot() map[string]uint64

Constants

const (
	InvSingleOwner         = "single_committed_owner"
	InvTokenMonotonic      = "token_monotonic"
	InvStaleRelease        = "stale_release_rejected"
	InvTransferBounded     = "transfer_not_pending_forever"
	InvAbortNoAdvance      = "abort_no_token_advance"
	InvCommitAdvancesOnce  = "commit_advances_once"
	InvUnownedKeepsToken   = "unowned_keeps_token"
	InvReservedHasOwner    = "reserved_has_owner"
	InvCrashKeepsOwnership = "crash_candidate_keeps_ownership"
	InvSingleAcquireWinner = "single_acquire_winner"
	InvExpireKeepsToken    = "expire_keeps_token"
	InvOverflowTerminal    = "overflow_terminal"
	InvIdempotentNoDouble  = "idempotent_no_double_advance"
	InvNoLocalLeaseInvent  = "no_local_lease_extension_while_disconnected"
	InvProtectedEpoch      = "protected_resource_epoch"
)

Invariant names for failure records.

Functions

func CheckTokenMonotonic

func CheckTokenMonotonic(prev, cur map[string]uint64) (string, string)

CheckTokenMonotonic compares previous snapshot tokens.

Types

type Action

type Action struct {
	Type       ActionType    `json:"type"`
	Generation string        `json:"generation,omitempty"`
	Claim      string        `json:"claim,omitempty"`
	Successor  string        `json:"successor,omitempty"`
	OpID       string        `json:"operation_id,omitempty"`
	Delta      time.Duration `json:"delta,omitempty"`
}

Action is a single protocol step.

type ActionType

type ActionType string

ActionType enumerates protocol actions.

const (
	ActRegisterGeneration ActionType = "register_generation"
	ActPassReadiness      ActionType = "pass_readiness"
	ActFailReadiness      ActionType = "fail_readiness"
	ActRequestClaim       ActionType = "request_claim"
	ActRenewClaim         ActionType = "renew_claim"
	ActBeginDrain         ActionType = "begin_drain"
	ActCompleteDrain      ActionType = "complete_drain"
	ActPrepareTransfer    ActionType = "prepare_transfer"
	ActCommitTransfer     ActionType = "commit_transfer"
	ActAbortTransfer      ActionType = "abort_transfer"
	ActPause              ActionType = "pause"
	ActResume             ActionType = "resume"
	ActDisconnect         ActionType = "disconnect"
	ActReconnect          ActionType = "reconnect"
	ActExpireLease        ActionType = "expire_lease"
	ActCrashOwner         ActionType = "crash_owner"
	ActCrashCandidate     ActionType = "crash_candidate"
	ActRestartBackend     ActionType = "restart_backend"
	ActForceRevoke        ActionType = "force_revoke"
	ActAdvanceTime        ActionType = "advance_time"
	ActReleaseClaim       ActionType = "release_claim"
)

type Claim

type Claim struct {
	Name             string
	Owner            string
	Token            uint64
	Phase            ClaimPhase
	PendingSuccessor string
	ExpiresAt        int64 // model time units
	TransferDeadline int64
	LastOpID         string
	OpResults        map[string]opSnap // idempotency
}

Claim is model ownership state.

type ClaimPhase

type ClaimPhase string

ClaimPhase mirrors shiftlock claim phases.

const (
	PhaseUnowned  ClaimPhase = "unowned"
	PhaseOwned    ClaimPhase = "owned"
	PhaseReserved ClaimPhase = "reserved"
	PhaseDraining ClaimPhase = "draining"
)

type FailureRecord

type FailureRecord struct {
	Seed      int64    `json:"seed"`
	Claim     string   `json:"claim"`
	Actions   []Action `json:"actions"`
	Invariant string   `json:"invariant"`
	Detail    string   `json:"detail"`
}

FailureRecord is a minimal reproducible sequence.

func (FailureRecord) JSON

func (f FailureRecord) JSON() string

func (FailureRecord) ReproduceCmd

func (f FailureRecord) ReproduceCmd() string

type GenState

type GenState string

GenState mirrors shiftlock generation states.

const (
	GenJoining      GenState = "joining"
	GenStandby      GenState = "standby"
	GenPreparing    GenState = "preparing"
	GenActive       GenState = "active"
	GenDraining     GenState = "draining"
	GenTransferring GenState = "transferring"
	GenRetired      GenState = "retired"
	GenFailed       GenState = "failed"
)

type Generation

type Generation struct {
	ID        string
	State     GenState
	Paused    bool
	Connected bool
	Ready     bool
	Draining  bool
}

Generation is model state for one process generation.

type Generator

type Generator struct {
	// contains filtered or unexported fields
}

Generator produces randomized legal-ish action sequences.

func NewGenerator

func NewGenerator(seed int64, claim string, gens []string) *Generator

NewGenerator creates a sequence generator.

func (*Generator) Next

func (g *Generator) Next() Action

Next returns the next random action.

func (*Generator) Sequence

func (g *Generator) Sequence(n int) []Action

Sequence returns n actions, ensuring gens are registered first.

type World

type World struct {
	Now            int64
	LeaseTTL       int64
	TransferTO     int64
	Gens           map[string]*Generation
	Claims         map[string]*Claim
	ProtectedEpoch map[string]uint64 // last accepted fencing token per claim (resource)
	History        []Action
}

World is the deterministic protocol world.

func NewWorld

func NewWorld(leaseTTL, transferTO int64) *World

NewWorld creates an empty model world.

func (*World) Apply

func (w *World) Apply(a Action) error

Apply executes one action against the world. Returns error on illegal transition.

func (*World) CheckInvariants

func (w *World) CheckInvariants() (string, string)

CheckInvariants verifies all 15 invariants. Returns invariant name + detail on failure.

func (*World) TokenSnapshot

func (w *World) TokenSnapshot() map[string]uint64