Add simple-model.

Azure · Aug 26, 2022 · 23f2c1c · 23f2c1c
1 parent 37509db
commit 23f2c1c
Show file tree

Hide file tree

Showing 39 changed files with 3,375 additions and 50 deletions.
diff --git a/.github/Regressions.tla b/.github/Regressions.tla
@@ -23,19 +23,21 @@ Consistency ==
 Check(conf, isWeaker, folder, model) ==
     LET ret == IOEnvExecTemplate(conf, Cmd, <<AbsolutePathOfTLC, folder, model>>).exitValue
     IN CASE ret =  0 ->
-                IF isWeaker THEN TRUE ELSE
-                \* Consistency-level is weaker than the property.
-                Print(<<folder, conf, "Missing violation">>, TRUE)
+                IF   isWeaker
+                THEN Print(<<folder, model, conf, "OK">>, TRUE)
+                ELSE \* Consistency-level is weaker than the property.
+                     Print(<<folder, model, conf, "Missing violation">>, FALSE)
          [] ret = 10 -> 
-                Print(<<folder, conf, "Assumption violation">>, FALSE)
+                Print(<<folder, model, conf, "Assumption violation">>, FALSE)
          [] ret = 12 -> 
-                IF ~isWeaker THEN TRUE ELSE
-                \* Consistency-level is equal to or stronger than the property.
-                Print(<<folder, conf, "Safety violation">>, TRUE)
+                IF   ~isWeaker
+                THEN Print(<<folder, model, conf, "OK: Expected safety violation">>, TRUE)
+                ELSE \* Consistency-level is equal to or stronger than the property.
+                     Print(<<folder, model, conf, "Safety violation">>, FALSE)
          [] ret = 13 -> 
-                Print(<<folder, conf, "Liveness violation">>, FALSE)
+                Print(<<folder, model, conf, "Liveness violation">>, FALSE)
          [] OTHER    -> 
-                Print(<<folder, conf, IOEnvExecTemplate(conf, Cmd, <<AbsolutePathOfTLC, folder, model>>), "Error">>, FALSE)
+                Print(<<folder, model, conf, IOEnvExecTemplate(conf, Cmd, <<AbsolutePathOfTLC, folder, model>>), "Error">>, FALSE)
 
 ASSUME 
     \A comb \in ((DOMAIN Consistency) \X (DOMAIN Consistency)) :
@@ -57,17 +59,47 @@ ASSUME
                        \/ /\ conf.mcConsistency = "Session" \* With one writer, Session => Strong
                           /\ conf.mcProperty = "Strong", "scenario2", "MCswscrw.tla")
 
-ASSUME
-    \A comb \in ((DOMAIN Consistency) \X (DOMAIN Consistency) \X {2} \X {1,2} \X {1,2}) : \* Due to the way the spec is modeled, a single region provides strong consistency. Thus, do not chec a single region.
-        LET conf == [ 
-                        mcConsistency |-> Consistency[comb[1]], 
-                        mcProperty |-> Consistency[comb[2]],
-                        mcNumRegions |-> comb[3],
-                        mcNumWriteRegions |-> comb[4],
-                        mcNumClientsPerRegion |-> comb[5]
-                    ]
-        IN conf.mcNumRegions >= conf.mcNumWriteRegions =>
-                Check(conf, comb[1] >= comb[2], "general-model", "MCcosmos_client.tla")
+\* ASSUME
+\*     \A comb \in ((DOMAIN Consistency) \X (DOMAIN Consistency) \X {2} \X {1,2} \X {1,2}) : \* Due to the way the spec is modeled, a single region provides strong consistency. Thus, do not chec a single region.
+\*         LET conf == [ 
+\*                         mcConsistency |-> Consistency[comb[1]], 
+\*                         mcProperty |-> Consistency[comb[2]],
+\*                         mcNumRegions |-> comb[3],
+\*                         mcNumWriteRegions |-> comb[4],
+\*                         mcNumClientsPerRegion |-> comb[5]
+\*                     ]
+\*         IN conf.mcNumRegions >= conf.mcNumWriteRegions =>
+\*                 Check(conf, comb[1] >= comb[2], "general-model", "MCcosmos_client.tla")
+
+\* not sure why this doesn't work?
+\* ASSUME Check(<<>>, TRUE, "general-model", "MCcosmos_client")
+
+SimpleModelSpecs == {
+    "AnomaliesCosmosDB",
+    "MCCosmosDBProps",
+    "SimCosmosDBProps",
+    "MCCosmosDBClient",
+    "MCCosmosDBWithAllReads",
+    "CosmosDBLinearizability",
+
+    "StrongConsistencyRefinesBoundedStaleness",
+    "SessionConsistencyRefinesConsistentPrefix",
+    "BoundedStalenessRefinesSessionConsistency",
+    "ConsistentPrefixRefinesEventualConsistency"
+}
+
+ASSUME \A spec \in SimpleModelSpecs :
+    Check(<<>>, TRUE, "simple-model", spec)
+
+ExpectedFailingSimpleModelSpecs == {
+    "show521677",
+    "show521677PCal",
+    "show521677simple",
+    "show521677simplePCal"
+}
+
+ASSUME \A spec \in ExpectedFailingSimpleModelSpecs :
+    Check(<<>>, FALSE, "simple-model", spec)
 
 =============================================================================
 -------- CONFIG Regressions --------

diff --git a/.gitignore b/.gitignore
@@ -338,3 +338,6 @@ tools/
 */*.out
 */*.dot
 _apalache-out/
+*/*.toolbox/
+.ammonite/
+.metals/
diff --git a/.vscode/settings.json b/.vscode/settings.json
@@ -1,7 +1,6 @@
 {
-    "tlaplus.tlc.modelChecker.options": "-gzip -metadir /tmp -cleanup -workers 1",
+    "tlaplus.tlc.modelChecker.options": "-gzip -metadir /tmp -cleanup -workers auto",
     "tlaplus.tlc.statisticsSharing": "share",
-    "tlaplus.java.options": "-XX:+UseParallelGC",
     "[tlaplus]": {"editor.codeActionsOnSave": {"source": true} },
     "extensions.autoCheckUpdates": false,
     "extensions.autoUpdate": false,
@@ -10,25 +9,27 @@
     "editor.useTabStops": false,
     "redhat.telemetry.enabled": false,
         "files.exclude": {
-        "_apalache-out": true,
-        ".gitignore": true,
-        ".gitpod.yml": true,
-        ".devcontainer": true,
-        ".github": true,
-        ".vscode": true,
-        "LICENSE": true,
-        "figures": true,
-        ".tlacache": true,
-        "*.tlaps": true,
-        "states": true,
-        "x": true,
-        "log0.smt": true,
-        "profile-rules.txt": true,
-        "detailed.log": true,
-        "*.toolbox": true,
-        "*.aux": true,
-        "*.dvi": true,
-        "*.log": true,
-        "*.tex": true
+            "_apalache-out": true,
+            ".devcontainer": true,
+            ".gitignore": true,
+            ".gitpod.yml": true,
+            ".tlacache": true,
+            ".vscode": true,
+            "*.aux": true,
+            "*.dvi": true,
+            "*.log": true,
+            "*.tex": true,
+            "*.tlaps": true,
+            "*.toolbox": true,
+            "detailed.log": true,
+            "figures": true,
+            "LICENSE": true,
+            "log0.smt": true,
+            "profile-rules.txt": true,
+            "states": true,
+            "x": true
+        },
+    "files.watcherExclude": {
+        "**/target": true
     }
 }
diff --git a/general-model/cosmos_client.tla b/general-model/cosmos_client.tla
@@ -35,9 +35,9 @@ ASSUME NumClientsPerRegion \in Nat
 (* (4) prefix (Consistent Prefix)                                          *)
 (* (5) eventual                                                            *)
 (***************************************************************************)
-CONSTANT Consistency
+VARIABLE Consistency
 
-ASSUME Consistency \in {"Strong", "Bounded_staleness", "Session", "Consistent_prefix", "Eventual"}
+\* ASSUME Consistency \in {"Strong", "Bounded_staleness", "Session", "Consistent_prefix", "Eventual"}
 
 (* The bounded version differences in Bounded Staleness consistency *)
 CONSTANT K
@@ -203,6 +203,21 @@ Spec == /\ Init /\ [][Next]_vars
 
 -----------------------------------------------------------------------------
 
+CombinedInit ==
+    /\ Consistency \in {"Strong", "Bounded_staleness", "Session", "Consistent_prefix", "Eventual"}
+    /\ Init
+
+CombinedNext ==
+    /\ Next
+    /\ UNCHANGED Consistency
+
+CombinedSpec ==
+    /\ CombinedInit /\ [][CombinedNext]_<<vars, Consistency>>
+    /\ \A self \in Clients : WF_vars(client(self))
+        /\ WF_vars(CosmosDB)
+
+-----------------------------------------------------------------------------
+
 (* enable these invariants in model checker *)
 
 (* Check elements in History are type of Opertion *)
@@ -249,21 +264,26 @@ ReadAfterWrite == \A i, j \in DOMAIN History : /\ i < j
 Linearizability == \A i, j \in DOMAIN History : /\ i < j
                                                 => History[j].data >= History[i].data
 
-BoundedStaleness == /\ \A i, j \in Regions : Last(Database[i]) - Last(Database[j]) \in -K..K
+BoundedStaleness == Consistency = "Bounded_staleness" =>
+                    /\ \A i, j \in Regions : Last(Database[i]) - Last(Database[j]) \in -K..K
                     /\ \A r \in Regions : MonotonicReadPerRegion(r)
-                    /\ ReadYourWrite
+                    \* /\ ReadYourWrite
 
-ConsistentPrefix == \A r \in Regions : /\ MonotonicWritePerRegion(r)
+ConsistentPrefix == Consistency = "Consistent_prefix" =>
+                    \A r \in Regions : /\ MonotonicWritePerRegion(r)
                                        /\ AnyReadPerRegion(r)
 
-Strong == /\ Linearizability
+Strong == Consistency = "Strong" =>
+          /\ Linearizability
           /\ Monotonic(History)
           /\ ReadAfterWrite
 
-Session == /\ \A c \in Clients : MonotonicReadPerClient(c)
+Session == Consistency = "Session" =>
+           /\ \A c \in Clients : MonotonicReadPerClient(c)
            /\ ReadYourWrite
 
-Eventual == \A i \in DOMAIN History : 
+Eventual == Consistency = "Eventual" =>
+            \A i \in DOMAIN History :
             LET r == History[i].region
             IN History[i].data \in {Database[r][j] : j \in DOMAIN Database[r]} \union {0}
 

diff --git a/simple-model/AnomaliesCosmosDB.cfg b/simple-model/AnomaliesCosmosDB.cfg
@@ -0,0 +1,24 @@
+SPECIFICATION
+    Spec
+CONSTANT
+    StrongConsistency = StrongConsistency
+    BoundedStaleness = BoundedStaleness
+    SessionConsistency = SessionConsistency
+    ConsistentPrefix = ConsistentPrefix
+    EventualConsistency = EventualConsistency
+    k1 = k1
+    k2 = k2
+    Keys = {k1, k2}
+    v1 = v1
+    v2 = v2
+    v3 = v3
+    Values = {v1, v2, v3}
+    NoValue = NoValue
+    LogIndices = [CosmosDB]{1,2,3,4}
+    Checkpoints = [CosmosDB]{0,1,2,3,4}
+    Epochs = [CosmosDB]{1,2,3,4}
+    VersionBound = 4
+    StalenessBound = 2
+PROPERTIES
+    CosmosSpec
+    Live