gsadmin/spinifex
1
0
Fork 0
mirror of https://github.com/mulgadc/spinifex.git synced 2026-11-02 09:13:33 +00:00
Code Issues Packages Projects Releases Wiki Activity

docs(ebs-spec): spec ListVolumes and ListSnapshots

Browse Source
This commit is contained in:
brynmailer-mdc
2026-10-30 16:19:52 +10:00
parent 749ec956d9
commit 33fa3a03ee
4 changed files with 85 additions and 1 deletions
Download Patch File Download Diff File Expand all files Collapse all files
spec/EBSProvider/EBSProvider.tla
+8 -1
View File
@@ -19,6 +19,7 @@ CONSTANTS
SnapshotIDs, SnapshotHandles,
AvailabilityZones, Timestamps,
Parameters, ProviderData,
ListTokens, MaxListResults,
\* The optional behaviour that the implementation advertises, which never changes.
Capabilities,
\* Whether the provider may fail to answer at any point in a behaviour.
@@ -30,8 +31,11 @@ ASSUME MaxBytes \in Nat \ {0}
ASSUME VolumeIDs /= {} /\ VolumeHandles /= {}
ASSUME NodeIDs /= {} => NBDURIs /= {} \/ DevicePaths /= {}
ASSUME SnapshotIDs /= {} => SnapshotHandles /= {} /\ Timestamps /= {}
ASSUME ListTokens /= {}
ASSUME MaxListResults \in Nat \ {0}
ASSUME ListTokens /= {}
ASSUME None \notin UNION {VolumeIDs, VolumeHandles, NodeIDs, SnapshotIDs, SnapshotHandles,
AvailabilityZones, Timestamps, Parameters, ProviderData}
AvailabilityZones, Timestamps, Parameters, ProviderData, ListTokens}
ASSUME Capabilities \in [online_expansion : BOOLEAN,
sparse_extent_reporting : BOOLEAN,
crash_consistent_snapshot : BOOLEAN,
@@ -138,6 +142,9 @@ PublicationView(volID, nodeID) == [volume_id |-> volID,
\* The part of a snapshot that the implementation returns.
SnapshotView(snapID) == ("id" :> snapID) @@ snapshots[snapID]
\* The number of refs that a page may hold, with an omitted or oversized request clamped to the maximum.
PageSize(m) == IF m <= 0 \/ m > MaxListResults THEN MaxListResults ELSE m
-----------------------------------------------------------------------------------------------------------------------
\* Invariants
spec/EBSProvider/README.md
+15
View File
@@ -56,6 +56,15 @@ The contract that every implementation of the `EBSProvider` interface must meet.
The Viperblock implementation ignores it.
- Is `not_found` the right error for a volume that was deleted and recreated under the same ID?
#### ListVolumes
- Must following next tokens list every volume that exists throughout the walk exactly once?
The conformance suite tests it, but the specification describes each call alone, so it does not say how one page relates to the next.
- What should a starting token that the implementation never issued do?
Every implementation treats any token as a position to resume after, while CSI refuses an invalid one with `ABORTED`.
- May a page hold fewer refs than requested yet carry a next token?
AWS and CSI allow it, but here a next token comes only with a full page, so that a walk cannot stall on empty pages.
#### ExpandVolume
- Should a request below the current capacity succeed without change, as CSI recommends, rather than be refused with `invalid_argument`?
@@ -113,6 +122,12 @@ The contract that every implementation of the `EBSProvider` interface must meet.
- What state does a copy start in?
The memory implementation always returns `completed`, while AWS starts a copy as `pending`.
#### ListSnapshots
- The questions for ListVolumes apply here too.
- Must a ref carry the source volume ID?
The Viperblock implementation leaves it empty, since reading it costs a fetch per snapshot, yet reconciliation needs it to act on a snapshot whose metadata is lost.
#### DeleteSnapshot
- Is the handle check part of the contract?
spec/EBSProvider/Snapshots.tla
+32
View File
@@ -96,6 +96,38 @@ CopySnapshot(req, val, err) ==
/\ UNCHANGED <<volumes, publications>>
ListSnapshotsRequests == [max_results : -1..(MaxListResults + 1),
starting_token : Optional(ListTokens)]
ListSnapshots(req, val, err) ==
(*******************************************************************************************************************)
(* Some of the snapshots are listed, a page at a time, and nothing changes. A call with no starting token that *)
(* returns no next token lists every snapshot. *)
(*******************************************************************************************************************)
LET Errors ==
LET checks == [unsupported_capability |-> ~Capabilities.snapshot_enumeration]
IN {e \in DOMAIN checks : checks[e]}
\* The request was rejected, or the provider failed to answer.
IN \/ /\ val = None
/\ err \in Errors \union ProviderErrors
/\ UNCHANGED vars
\* The request was accepted.
\/ /\ Errors = {}
/\ LET refs == {[id |-> id,
source_volume_id |-> snapshots[id].source_volume_id,
handle |-> snapshots[id].handle] : id \in DOMAIN snapshots}
\* The page and the next token are the implementation's choice.
IN \E page \in SUBSET refs, next \in Optional(ListTokens) :
/\ Cardinality(page) <= PageSize(req.max_results)
/\ next /= None => Cardinality(page) = PageSize(req.max_results)
/\ req.starting_token = None /\ next = None => page = refs
/\ val = [snapshots |-> page, next_token |-> next]
/\ err = None
/\ UNCHANGED vars
DeleteSnapshotRequests == [snapshot_id : Optional(SnapshotIDs),
handle : Optional(SnapshotHandles)]
spec/EBSProvider/Volumes.tla
+30
View File
@@ -104,6 +104,36 @@ GetVolume(req, val, err) ==
/\ UNCHANGED vars
ListVolumesRequests == [max_results : -1..(MaxListResults + 1),
starting_token : Optional(ListTokens)]
ListVolumes(req, val, err) ==
(*******************************************************************************************************************)
(* Some of the volumes are listed, a page at a time, and nothing changes. A call with no starting token that *)
(* returns no next token lists every volume. *)
(*******************************************************************************************************************)
LET Errors ==
LET checks == [unsupported_capability |-> ~Capabilities.volume_enumeration]
IN {e \in DOMAIN checks : checks[e]}
\* The request was rejected, or the provider failed to answer.
IN \/ /\ val = None
/\ err \in Errors \union ProviderErrors
/\ UNCHANGED vars
\* The request was accepted.
\/ /\ Errors = {}
/\ LET refs == {[id |-> id, handle |-> volumes[id].handle] : id \in DOMAIN volumes}
\* The page and the next token are the implementation's choice.
IN \E page \in SUBSET refs, next \in Optional(ListTokens) :
/\ Cardinality(page) <= PageSize(req.max_results)
/\ next /= None => Cardinality(page) = PageSize(req.max_results)
/\ req.starting_token = None /\ next = None => page = refs
/\ val = [volumes |-> page, next_token |-> next]
/\ err = None
/\ UNCHANGED vars
ExpandVolumeRequests == [volume_id : Optional(VolumeIDs),
handle : Optional(VolumeHandles),
capacity_range : CapacityRanges]