TLA+ model of instance update saga

gjcolombo · Mar 12, 2024 · 5352e40 · 5352e40
1 parent 145f25c
commit 5352e40
Show file tree

Hide file tree

Showing 2 changed files with 1,370 additions and 0 deletions.
diff --git a/docs/tla/instance-lifecycle/update.cfg b/docs/tla/instance-lifecycle/update.cfg
@@ -0,0 +1,29 @@
+SPECIFICATION Spec
+CONSTANT defaultInitValue = defaultInitValue
+\* Add statements after this line.
+
+CONSTANT NULL = NULL
+CONSTANT STARTER = STARTER
+CONSTANT VMS = {v1, v2, v3}
+CONSTANT UPDATERS = {u1, u2, u3}
+
+INVARIANT InstanceType
+INVARIANT VmType
+INVARIANT MigrationRequiresPartner
+INVARIANT OnlyOneMigrationPerVm
+INVARIANT VmResourceStatesInVmStates
+INVARIANT ActiveVmsHaveResources
+INVARIANT StoppedInstanceHasNoVms
+INVARIANT MigrationRequiresActiveVm
+INVARIANT OpteMappingsConsistentAtEnd
+INVARIANT VmsFreeAtEnd
+INVARIANT MigrationsResolveAtEnd
+
+SYMMETRY Symmetry
+
+\* PROPERTY OpteMappingsEventuallyConsistent
+\* PROPERTY DestroyedVmsStayDestroyed
+\* PROPERTY DestroyedVmsGetFreed
+\* PROPERTY UpdaterLockNotStolen
+\* PROPERTY MigrationTargetNotStolen
+\* PROPERTY MigrationsEventuallyResolve