From 33fa3a03eee184df2beb69ea8e034f0d33fc3df6 Mon Sep 17 00:00:00 2001 From: brynmailer-mdc Date: Fri, 30 Oct 2026 16:19:52 +1000 Subject: [PATCH] docs(ebs-spec): spec ListVolumes and ListSnapshots --- spec/EBSProvider/EBSProvider.tla | 9 ++++++++- spec/EBSProvider/README.md | 15 +++++++++++++++ spec/EBSProvider/Snapshots.tla | 32 ++++++++++++++++++++++++++++++++ spec/EBSProvider/Volumes.tla | 30 ++++++++++++++++++++++++++++++ 4 files changed, 85 insertions(+), 1 deletion(-) diff --git a/spec/EBSProvider/EBSProvider.tla b/spec/EBSProvider/EBSProvider.tla index 532c99df7..0692afe0a 100644 --- a/spec/EBSProvider/EBSProvider.tla +++ b/spec/EBSProvider/EBSProvider.tla @@ -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 diff --git a/spec/EBSProvider/README.md b/spec/EBSProvider/README.md index d12a06a1f..dabc017b4 100644 --- a/spec/EBSProvider/README.md +++ b/spec/EBSProvider/README.md @@ -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? diff --git a/spec/EBSProvider/Snapshots.tla b/spec/EBSProvider/Snapshots.tla index baa3947a2..eae7d3769 100644 --- a/spec/EBSProvider/Snapshots.tla +++ b/spec/EBSProvider/Snapshots.tla @@ -96,6 +96,38 @@ CopySnapshot(req, val, err) == /\ UNCHANGED <> +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)] diff --git a/spec/EBSProvider/Volumes.tla b/spec/EBSProvider/Volumes.tla index 25fbb9ea3..f7bff9365 100644 --- a/spec/EBSProvider/Volumes.tla +++ b/spec/EBSProvider/Volumes.tla @@ -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]