← All compilation units

Flyology.Process_Generations

Description

Nonzero stable identity of one coordinator lifetime.

Candidate_Role

type Candidate_Role is (Canary_Safe, Fenced, Active_Only, Shadow);

Candidate role supplied to application topology reconstruction.

Enumeration literals
Canary_Safe

May perform work concurrently with the previous image

Fenced

Effects require an exact active deployment-epoch check

Active_Only

Work begins only after promotion

Shadow

Work may observe or compute but must not commit effects

Compensation_Result

type Compensation_Result is
  (Not_Required,
   Nothing_To_Do,
   Compensated,
   Compensation_Pending,
   Irreversible_Effects,
   Compensation_Failed);

Outcome of application compensation after candidate quiescence.

Enumeration literals
Not_Required

Compensation has not been requested

Nothing_To_Do

No candidate effect required compensation

Compensated

Candidate effects were reversed

Compensation_Pending

The outcome is unknown and needs recovery

Irreversible_Effects

Some candidate effects cannot be reversed

Compensation_Failed

Compensation completed unsuccessfully

Coordinator_Id

type Coordinator_Id is new Interfaces.Unsigned_64 range 1 .. Interfaces.Unsigned_64'Last;

Nonzero stable identity of one coordinator lifetime.

Image_Generation

type Image_Generation is new Interfaces.Unsigned_64 range 1 .. Interfaces.Unsigned_64'Last;

Nonzero identity of one executable process generation. Values do not wrap within a coordinator lifetime.

Same_Upgrade

function Same_Upgrade (Left, Right : Upgrade_Handle) return Boolean

Report whether two values grant authority over the same transaction.

Parameters
Left

First authority

Right

Second authority

Return value

True only when every authority component matches

Upgrade_Command

type Upgrade_Command is
  (Start_Upgrade,
   Candidate_Started,
   Candidate_Prepared,
   Start_Canary,
   Cancel_Upgrade,
   Candidate_Stopped,
   Admission_Revoked,
   Candidate_Drained,
   …,
   Require_Rollback);

Exact commands consumed by the proved transition policy.

Enumeration literals
Start_Upgrade

Begin a candidate transaction

Candidate_Started

Record successful candidate launch

Candidate_Prepared

Record successful candidate preparation

Start_Canary

Grant candidate admission

Cancel_Upgrade

Begin reversible cancellation

Candidate_Stopped

Record candidate server termination

Admission_Revoked

Record that new admission is disabled

Candidate_Drained

Record candidate quiescence

Compensation_Finished

Record the compensation outcome

Promote_Upgrade

Cross the promotion commitment boundary

Previous_Drain_Started

Begin previous-image retirement

Previous_Drained

Record previous-image quiescence

Commit_Finished

Complete promotion bookkeeping

Record_Failure

Record a pre-commit failure

Require_Rollback

Record a post-commit failure

Upgrade_Handle

type Upgrade_Handle is record
   Coordinator : Coordinator_Id;
   Upgrade     : Upgrade_Id;
   Candidate   : Image_Generation;
end record;

Exact authority for one candidate transaction.

Record fields
Coordinator

Coordinator that allocated the transaction

Upgrade

Exact upgrade transaction

Candidate

Candidate process generation

Upgrade_Id

type Upgrade_Id is new Interfaces.Unsigned_64 range 1 .. Interfaces.Unsigned_64'Last;

Nonzero transaction identity allocated by one coordinator. Values do not wrap; exhaustion requires a fresh coordinator identity.

Upgrade_Phase

type Upgrade_Phase is
  (Stable,
   Starting,
   Provisioning,
   Prepared,
   Canary,
   Cancelling,
   Revoking_Admission,
   Draining_Candidate,
   …,
   Rollback_Required);

Lifecycle phase of one coordinator or upgrade transaction. Stable has no candidate. Completed, Cancelled, Failed, and Rollback_Required are terminal transaction observations; a coordinator starts a later transaction from a fresh Stable state.

Enumeration literals
Stable

No candidate transaction is active

Starting

A candidate launch is beginning

Provisioning

The candidate is reconstructing its local topology

Prepared

The candidate is provisioned but not admitting work

Canary

The candidate may admit work under its declared role

Cancelling

Candidate cancellation has begun

Revoking_Admission

New candidate admission is being revoked

Draining_Candidate

Existing candidate work is draining

Compensating

Candidate effects are being compensated

Cancelled

Cancellation completed

Promoting

The candidate crossed the promotion boundary

Draining_Previous

The previous active image is draining

Committing

Promotion bookkeeping is being committed

Completed

Promotion completed

Failed

The transaction failed before promotion committed

Rollback_Required

Promotion failed after commitment