333 lines
17 KiB
Text
333 lines
17 KiB
Text
------------------------------- MODULE Cloud -------------------------------
|
|
EXTENDS Naturals, FiniteSets, TLC
|
|
|
|
CONSTANTS Mode, Scenario, ResourceKind, LoseReply, RestartOnce, DelayLists
|
|
|
|
(* This projection separates OCI resource state, API observations, and publication. *)
|
|
(* cloud.Client.Reconcile supplies the create/select/cleanup protocol for each kind. *)
|
|
|
|
Kinds == {"CPE", "VPN"}
|
|
Modes == {"Current", "Fixed"}
|
|
Cases == {"Retry", "Routes"}
|
|
Ids == 1..3
|
|
WANs == {"A", "B"}
|
|
VIPs == {"X", "Y"}
|
|
Attempts == 0..2
|
|
Keys == WANs \X Attempts
|
|
Lives == {"Unused", "Provisioning", "Available", "Terminating", "Terminated", "Absent"}
|
|
Phases == {"read", "create", "reply", "inspect", "clean", "admit", "publish", "pause"}
|
|
|
|
ASSUME /\ Mode \in Modes
|
|
/\ Scenario \in Cases
|
|
/\ ResourceKind \in Kinds
|
|
/\ Scenario = "Routes" => ResourceKind = "VPN"
|
|
/\ LoseReply \in BOOLEAN
|
|
/\ RestartOnce \in BOOLEAN
|
|
/\ DelayLists \in BOOLEAN
|
|
|
|
VARIABLES objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
phase, seen, selected, attempt, reply, routeSeen, pending,
|
|
health, published, admitted, todo, refs, dropped, restarted, badPublish
|
|
|
|
vars == <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
phase, seen, selected, attempt, reply, routeSeen, pending,
|
|
health, published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
LastEpoch == IF Scenario = "Retry" THEN 2 ELSE 1
|
|
WAN == IF Scenario = "Retry" /\ epoch = 1 THEN "B" ELSE "A"
|
|
VIP == IF Scenario = "Routes" /\ epoch = 1 THEN "Y" ELSE "X"
|
|
Key == <<WAN, attempt>>
|
|
Active == {i \in Ids : objects[i].life \in {"Provisioning", "Available"}}
|
|
Present == {i \in Ids : objects[i].life \notin {"Unused", "Absent"}}
|
|
Current == {i \in seen : objects[i].wan = WAN /\
|
|
(ResourceKind = "CPE" \/
|
|
objects[i].life \notin {"Terminating", "Terminated", "Absent"})}
|
|
Old == {i \in seen : i # selected}
|
|
|
|
Init == /\ objects = [i \in Ids |-> [life |-> "Unused", wan |-> "A", route |-> "X"]]
|
|
/\ visible = {}
|
|
/\ tokens = [k \in Keys |-> 0]
|
|
/\ invalid = {}
|
|
/\ issued = {}
|
|
/\ nextId = 1
|
|
/\ epoch = 0
|
|
/\ phase = "read"
|
|
/\ seen = {}
|
|
/\ selected = 0
|
|
/\ attempt = 0
|
|
/\ reply = 0
|
|
/\ routeSeen = "X"
|
|
/\ pending = [i \in Ids |-> "None"]
|
|
/\ health = {}
|
|
/\ published = [epoch |-> 3, id |-> 0, route |-> "X"]
|
|
/\ admitted = {}
|
|
/\ todo = {}
|
|
/\ refs = {}
|
|
/\ dropped = FALSE
|
|
/\ restarted = FALSE
|
|
/\ badPublish = FALSE
|
|
|
|
(* cloud.Client.Reconcile lists before selecting a CPE or a non-terminating VPN. *)
|
|
Read == /\ phase = "read"
|
|
/\ seen' = visible
|
|
/\ phase' = "inspect"
|
|
/\ selected' = 0
|
|
/\ attempt' = 0
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
reply, routeSeen, pending, health, published, admitted, todo,
|
|
refs, dropped, restarted, badPublish>>
|
|
|
|
Select == /\ phase = "inspect" /\ selected = 0
|
|
/\ IF Cardinality(Current) = 1
|
|
THEN /\ selected' = CHOOSE i \in Current : TRUE
|
|
/\ routeSeen' = objects[selected'].route
|
|
/\ phase' = "inspect"
|
|
ELSE /\ selected' = 0
|
|
/\ UNCHANGED routeSeen
|
|
/\ phase' = IF Current = {} THEN "create" ELSE "pause"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, attempt, reply, pending, health, published, admitted,
|
|
todo, refs, dropped, restarted, badPublish>>
|
|
|
|
(* OCI Retry Token and InvalidatedRetryToken define these three create outcomes. *)
|
|
(* https://docs.oracle.com/en-us/iaas/Content/API/References/apierrors.htm *)
|
|
Create == /\ phase = "create"
|
|
/\ Key \notin invalid
|
|
/\ tokens[Key] = 0
|
|
/\ nextId \in Ids
|
|
/\ objects' = [objects EXCEPT ![nextId] =
|
|
[life |-> IF ResourceKind = "VPN" THEN "Provisioning" ELSE "Available",
|
|
wan |-> WAN, route |-> VIP]]
|
|
/\ tokens' = [tokens EXCEPT ![Key] = nextId]
|
|
/\ issued' = issued \cup {<<Key, nextId>>}
|
|
/\ reply' = nextId
|
|
/\ nextId' = nextId + 1
|
|
/\ visible' = IF DelayLists THEN visible ELSE visible \cup {nextId}
|
|
/\ phase' = "reply"
|
|
/\ UNCHANGED <<invalid, epoch, seen, selected, attempt, routeSeen, pending,
|
|
health, published, admitted, todo, refs, dropped,
|
|
restarted, badPublish>>
|
|
|
|
Replay == /\ phase = "create" /\ Key \notin invalid /\ tokens[Key] # 0
|
|
/\ reply' = tokens[Key]
|
|
/\ phase' = "reply"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
(* Fixed follows a deterministic successor only on InvalidatedRetryToken; restart replays that chain. *)
|
|
Reject == /\ phase = "create" /\ Key \in invalid
|
|
/\ IF Mode = "Fixed" /\ attempt < 2
|
|
THEN /\ attempt' = attempt + 1 /\ phase' = "create"
|
|
ELSE /\ UNCHANGED attempt /\ phase' = "pause"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, reply, routeSeen, pending, health, published,
|
|
admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
Receive == /\ phase = "reply"
|
|
/\ selected' = reply
|
|
/\ routeSeen' = objects[reply].route
|
|
/\ seen' = seen \cup {reply}
|
|
/\ phase' = "inspect"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
attempt, reply, pending, health, published, admitted, todo,
|
|
refs, dropped, restarted, badPublish>>
|
|
|
|
(* A timed-out create may already have committed; only its response is lost. *)
|
|
DropReply == /\ LoseReply /\ ~dropped /\ phase = "reply"
|
|
/\ dropped' = TRUE
|
|
/\ phase' = "read"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, restarted, badPublish>>
|
|
|
|
Restart == /\ RestartOnce /\ ~restarted
|
|
/\ restarted' = TRUE
|
|
/\ phase' = "read"
|
|
/\ selected' = 0
|
|
/\ attempt' = 0
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, reply, routeSeen, pending, health, published, admitted,
|
|
todo, refs, dropped, badPublish>>
|
|
|
|
(* UpdateIPSecConnectionDetails.StaticRoutes replaces the managed route set. *)
|
|
UpdateRoute == /\ phase = "inspect" /\ selected # 0
|
|
/\ objects[selected].life = "Available"
|
|
/\ ResourceKind = "VPN" /\ Mode = "Fixed" /\ routeSeen # VIP
|
|
/\ pending' = [pending EXCEPT ![selected] = VIP]
|
|
/\ phase' = "pause"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId,
|
|
epoch, seen, selected, attempt, reply, routeSeen, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
(* CPE unavailability here represents a rejected child-IPsec call, not a readable CPE lifecycle. *)
|
|
WaitReady == /\ phase = "inspect" /\ selected # 0
|
|
/\ objects[selected].life # "Available"
|
|
/\ phase' = "pause"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
BeginClean == /\ phase = "inspect" /\ selected # 0
|
|
/\ objects[selected].life = "Available"
|
|
/\ ResourceKind = "CPE" \/ Mode = "Current" \/ routeSeen = VIP
|
|
/\ todo' = IF selected \in health THEN Old ELSE {}
|
|
/\ phase' = "clean"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, refs, dropped, restarted, badPublish>>
|
|
|
|
(* CPE disposal follows child-IPsec retirement; this abstracts that completed subprotocol. *)
|
|
RetireChild(i) == /\ ResourceKind = "CPE" /\ phase = "clean" /\ i \in todo /\ i \in refs
|
|
/\ refs' = refs \ {i}
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId,
|
|
epoch, phase, seen, selected, attempt, reply, routeSeen,
|
|
pending, health, published, admitted, todo, dropped,
|
|
restarted, badPublish>>
|
|
|
|
Delete(i) == /\ phase = "clean" /\ i \in todo /\ i \notin refs
|
|
/\ objects' = IF i \in Active
|
|
THEN [objects EXCEPT ![i].life = "Terminating"]
|
|
ELSE objects
|
|
/\ todo' = todo \ {i}
|
|
/\ health' = health \ {i}
|
|
/\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch, phase,
|
|
seen, selected, attempt, reply, routeSeen, pending,
|
|
published, admitted, refs, dropped, restarted, badPublish>>
|
|
|
|
CleanDone == /\ phase = "clean" /\ todo = {}
|
|
/\ phase' = "admit"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
Admit == /\ phase = "admit"
|
|
/\ admitted' = {i \in seen : objects[i].life = "Available"}
|
|
/\ phase' = "publish"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
(* controller.Runner.step publishes after admission and two retrievable peer configurations. *)
|
|
Publish == /\ phase = "publish"
|
|
/\ published' = [epoch |-> epoch, id |-> selected, route |-> VIP]
|
|
/\ badPublish' = (badPublish \/ (ResourceKind = "VPN" /\ routeSeen # VIP))
|
|
/\ refs' = IF ResourceKind = "CPE" THEN refs \cup {selected} ELSE refs
|
|
/\ phase' = "pause"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
admitted, todo, dropped, restarted>>
|
|
|
|
Poll == /\ phase = "pause" /\ phase' = "read"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, epoch,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
Provision(i) == /\ objects[i].life = "Provisioning"
|
|
/\ objects' = [objects EXCEPT ![i].life = "Available"]
|
|
/\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch,
|
|
phase, seen, selected, attempt, reply, routeSeen, pending,
|
|
health, published, admitted, todo, refs, dropped,
|
|
restarted, badPublish>>
|
|
|
|
Expose(i) == /\ i \in Present /\ i \notin visible
|
|
/\ visible' = visible \cup {i}
|
|
/\ UNCHANGED <<objects, tokens, invalid, issued, nextId, epoch, phase,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
Finish(i) == /\ objects[i].life = "Terminating"
|
|
/\ objects' = [objects EXCEPT ![i].life =
|
|
IF ResourceKind = "VPN" THEN "Terminated" ELSE "Absent"]
|
|
/\ invalid' = invalid \cup {k \in Keys : tokens[k] = i}
|
|
/\ UNCHANGED <<visible, tokens, issued, nextId, epoch, phase, seen,
|
|
selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
Purge(i) == /\ objects[i].life = "Terminated"
|
|
/\ objects' = [objects EXCEPT ![i].life = "Absent"]
|
|
/\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch, phase,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
Forget(i) == /\ objects[i].life = "Absent" /\ i \in visible
|
|
/\ visible' = visible \ {i}
|
|
/\ UNCHANGED <<objects, tokens, invalid, issued, nextId, epoch, phase,
|
|
seen, selected, attempt, reply, routeSeen, pending, health,
|
|
published, admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
ApplyRoute(i) == /\ pending[i] \in VIPs /\ objects[i].life = "Available"
|
|
/\ objects' = [objects EXCEPT ![i].route = pending[i]]
|
|
/\ pending' = [pending EXCEPT ![i] = "None"]
|
|
/\ UNCHANGED <<visible, tokens, invalid, issued, nextId, epoch,
|
|
phase, seen, selected, attempt, reply, routeSeen,
|
|
health, published, admitted, todo, refs, dropped,
|
|
restarted, badPublish>>
|
|
|
|
(* health denotes both associated IPsec tunnels being up; CPE itself has no health field. *)
|
|
Establish(i) == /\ published.id = i /\ objects[i].life = "Available"
|
|
/\ objects[i].wan = WAN /\ i \notin health
|
|
/\ health' = health \cup {i}
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId,
|
|
epoch, phase, seen, selected, attempt, reply, routeSeen,
|
|
pending, published, admitted, todo, refs, dropped,
|
|
restarted, badPublish>>
|
|
|
|
Converged == /\ published.epoch = epoch /\ published.id \in health
|
|
/\ objects[published.id].wan = WAN
|
|
/\ ResourceKind = "CPE" \/ objects[published.id].route = VIP
|
|
|
|
Advance == /\ epoch < LastEpoch /\ phase = "pause" /\ Converged
|
|
/\ \A i \in Ids : i = published.id \/ objects[i].life \in {"Unused", "Absent"}
|
|
/\ visible = {published.id}
|
|
/\ epoch' = epoch + 1
|
|
/\ health' = {}
|
|
/\ phase' = "read"
|
|
/\ UNCHANGED <<objects, visible, tokens, invalid, issued, nextId, seen,
|
|
selected, attempt, reply, routeSeen, pending, published,
|
|
admitted, todo, refs, dropped, restarted, badPublish>>
|
|
|
|
Work == Read \/ Select \/ Create \/ Replay \/ Reject \/ Receive \/ UpdateRoute \/
|
|
WaitReady \/ BeginClean \/ CleanDone \/ Admit \/ Publish \/ Poll \/
|
|
(\E i \in Ids : RetireChild(i) \/ Delete(i))
|
|
|
|
Provider(i) == Provision(i) \/ Expose(i) \/ Finish(i) \/ Purge(i) \/ Forget(i) \/
|
|
ApplyRoute(i) \/ Establish(i)
|
|
|
|
Next == Work \/ Advance \/ DropReply \/ Restart \/ (\E i \in Ids : Provider(i))
|
|
|
|
(* Liveness assumes a stable final target and eventual API visibility, provisioning, and tunnel progress. *)
|
|
Fairness == /\ WF_vars(Work)
|
|
/\ SF_vars(Advance)
|
|
/\ \A i \in Ids : /\ WF_vars(Provision(i)) /\ WF_vars(Expose(i))
|
|
/\ WF_vars(Finish(i)) /\ WF_vars(Purge(i))
|
|
/\ WF_vars(Forget(i)) /\ WF_vars(ApplyRoute(i))
|
|
/\ WF_vars(Establish(i))
|
|
|
|
Spec == Init /\ [][Next]_vars /\ Fairness
|
|
|
|
TypeOK == /\ objects \in [Ids -> [life : Lives, wan : WANs, route : VIPs]]
|
|
/\ visible \subseteq Ids /\ seen \subseteq Ids
|
|
/\ tokens \in [Keys -> (Ids \cup {0})] /\ invalid \subseteq Keys
|
|
/\ issued \subseteq (Keys \X Ids) /\ nextId \in 1..4
|
|
/\ epoch \in 0..LastEpoch /\ phase \in Phases
|
|
/\ selected \in Ids \cup {0} /\ reply \in Ids \cup {0}
|
|
/\ attempt \in Attempts /\ routeSeen \in VIPs
|
|
/\ pending \in [Ids -> VIPs \cup {"None"}]
|
|
/\ health \subseteq Ids /\ admitted \subseteq Ids
|
|
/\ todo \subseteq Ids /\ refs \subseteq Ids
|
|
/\ published \in [epoch : 0..3, id : Ids \cup {0}, route : VIPs]
|
|
/\ dropped \in BOOLEAN /\ restarted \in BOOLEAN /\ badPublish \in BOOLEAN
|
|
|
|
(* OCI Retry Token guarantees expire after 24 hours; expiry is outside this projection. *)
|
|
(* https://docs.oracle.com/en-us/iaas/Content/API/Concepts/usingapi.htm *)
|
|
OCIRetry == \A a, b \in issued : a[1] = b[1] => a[2] = b[2]
|
|
(* DeleteCpe requires the CPE to be disconnected from its DRG. *)
|
|
(* https://docs.oracle.com/en-us/iaas/tools/python/latest/api/core/client/oci.core.VirtualNetworkClient.html#oci.core.VirtualNetworkClient.delete_cpe *)
|
|
OCIDelete == \A i \in refs : objects[i].life \notin {"Terminating", "Terminated", "Absent"}
|
|
OCITokens == \A k \in invalid : tokens[k] # 0
|
|
|
|
RoutePublish == ~badPublish
|
|
Admission == phase = "publish" => selected \in admitted
|
|
Recovery == <>[](epoch = LastEpoch /\ Converged)
|
|
=============================================================================
|