search

tlaplus / azure-cosmos-tla

Azure Cosmos TLA+ specifications
https://learn.microsoft.com/en-us/azure/cosmos-db/consistency-levels
MIT License
20 stars 5 forks source link

[Scenario1,Scenario2] Session property holds despite Cosmos operating under Eventual consistency #3

Open lemmy opened 2 years ago

lemmy commented 2 years ago

"In session consistency, within a single client session reads are guaranteed to honor the consistent-prefix, monotonic reads, monotonic writes, read-your-writes, and write-follows-reads guarantees." https://docs.microsoft.com/en-us/azure/cosmos-db/consistency-levels#session-consistency.

Checking the property Session with constant Consistency = "Eventual" in scenario1/swscop.tla (and scenario2/swscrw.tla) does not cause a violation (Session holds), even though reads are not monotonic. With the definition of Session strengthened by asserting monotonic reads, the property no longer holds, which is the expected behavior. Note that the original definition of Session is not violated by non-monotonic reads because the value of ses[1](session token) will be non-monotonic under eventual consistency.

Original variant of Session:

$ java -jar ../tools/tla2tools.jar swscop.tla -note
TLC2 Version 2.18 of Day Month 20?? (rev: 59b6efd)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 109 and seed -6790380810290992309 with 1 worker on 4 cores with 1990MB heap and 64MB offheap memory [pid: 7278] (Linux 5.4.0-1069-azure amd64, Oracle Corporation 17.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspaces/azure-cosmos-tla/scenario1/swscop.tla
Parsing file /tmp/tlc-12674584995417415540/Naturals.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-12674584995417415540/Integers.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-12674584995417415540/Sequences.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-12674584995417415540/FiniteSets.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-12674584995417415540/TLC.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-12674584995417415540/Bags.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Bags.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Bags
Semantic processing of module swscop
Starting... (2022-03-02 05:43:18)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2022-03-02 05:43:18.
Model checking completed. No error has been found.
  Estimates of the probability that TLC did not check all reachable states
  because two distinct states had the same fingerprint:
  calculated (optimistic):  val = 0.0
143 states generated, 143 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 26.
The average outdegree of the complete state graph is 1 (minimum is 0, the maximum 4 and the 95th percentile is 3).
Finished in 00s at (2022-03-02 05:43:18)
$ java -jar ../tools/tla2tools.jar swscop.tla -note
TLC2 Version 2.18 of Day Month 20?? (rev: 59b6efd)
Warning: Please run the Java VM, which executes TLC with a throughput optimized garbage collector, by passing the "-XX:+UseParallelGC" property.
(Use the -nowarning option to disable this warning.)
Running breadth-first search Model-Checking with fp 35 and seed -4922802926910969154 with 1 worker on 4 cores with 1990MB heap and 64MB offheap memory [pid: 8024] (Linux 5.4.0-1069-azure amd64, Oracle Corporation 17.0.1 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /workspaces/azure-cosmos-tla/scenario1/swscop.tla
Parsing file /tmp/tlc-7146957781892970965/Naturals.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/tlc-7146957781892970965/Integers.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/tlc-7146957781892970965/Sequences.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/tlc-7146957781892970965/FiniteSets.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/tlc-7146957781892970965/TLC.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/tlc-7146957781892970965/Bags.tla (jar:file:/workspaces/azure-cosmos-tla/tools/tla2tools.jar!/tla2sany/StandardModules/Bags.tla)
Semantic processing of module Naturals
Semantic processing of module Integers
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module TLC
Semantic processing of module Bags
Semantic processing of module swscop
Starting... (2022-03-02 05:44:28)
Computing initial states...
Finished computing initial states: 1 distinct state generated at 2022-03-02 05:44:28.
Error: Invariant Session is violated.
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ ses = <<1>>
/\ msg = (0 :> <<>>)
/\ op = <<0>>
/\ m = <<<<>>>>
/\ pc = (0 :> "D" @@ 1 :> "CW")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0>>)

State 2: <CW line 147, col 13 to line 154, col 62 of module swscop>
/\ ses = <<1>>
/\ msg = (0 :> <<>>)
/\ op = <<1>>
/\ m = <<<<>>>>
/\ pc = (0 :> "D" @@ 1 :> "CWA")
/\ chan = (0 :> <<[ses |-> 1, type |-> "Write", dat |-> 1, orig |-> 1]>> @@ 1 :> <<>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0>>)

State 3: <D line 88, col 12 to line 107, col 50 of module swscop>
/\ ses = <<1>>
/\ msg = (0 :> [ses |-> 1, type |-> "Write", dat |-> 1, orig |-> 1])
/\ op = <<1>>
/\ m = <<<<>>>>
/\ pc = (0 :> "DW" @@ 1 :> "CWA")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0, 1>>)

State 4: <DW line 109, col 13 to line 112, col 66 of module swscop>
/\ ses = <<1>>
/\ msg = (0 :> [ses |-> 1, type |-> "Write", dat |-> 1, orig |-> 1])
/\ op = <<1>>
/\ m = <<<<>>>>
/\ pc = (0 :> "D" @@ 1 :> "CWA")
/\ chan = (0 :> <<>> @@ 1 :> <<[ses |-> 2, type |-> "Ack", dat |-> 1]>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0, 1>>)

State 5: <CWA line 156, col 14 to line 162, col 59 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 1, type |-> "Write", dat |-> 1, orig |-> 1])
/\ op = <<1>>
/\ m = <<[ses |-> 2, type |-> "Ack", dat |-> 1]>>
/\ pc = (0 :> "D" @@ 1 :> "CR")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0, 1>>)

State 6: <CR line 164, col 13 to line 167, col 66 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 1, type |-> "Write", dat |-> 1, orig |-> 1])
/\ op = <<1>>
/\ m = <<[ses |-> 2, type |-> "Ack", dat |-> 1]>>
/\ pc = (0 :> "D" @@ 1 :> "CRA")
/\ chan = (0 :> <<[ses |-> 2, type |-> "Eventual", orig |-> 1]>> @@ 1 :> <<>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0, 1>>)

State 7: <D line 88, col 12 to line 107, col 50 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 2, type |-> "Eventual", orig |-> 1])
/\ op = <<1>>
/\ m = <<[ses |-> 2, type |-> "Ack", dat |-> 1]>>
/\ pc = (0 :> "DE" @@ 1 :> "CRA")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0, 1>>)

State 8: <DE line 114, col 13 to line 118, col 66 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 2, type |-> "Eventual", orig |-> 1])
/\ op = <<1>>
/\ m = <<[ses |-> 2, type |-> "Ack", dat |-> 1]>>
/\ pc = (0 :> "D" @@ 1 :> "CRA")
/\ chan = (0 :> <<>> @@ 1 :> <<[ses |-> 2, type |-> "Reply", dat |-> 1]>>)
/\ chistory = <<<<0>>>>
/\ Database = (0 :> <<0, 1>>)

State 9: <CRA line 169, col 14 to line 176, col 49 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 2, type |-> "Eventual", orig |-> 1])
/\ op = <<1>>
/\ m = <<[ses |-> 2, type |-> "Reply", dat |-> 1]>>
/\ pc = (0 :> "D" @@ 1 :> "CW")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1>>)

State 10: <CW line 147, col 13 to line 154, col 62 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 2, type |-> "Eventual", orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 2, type |-> "Reply", dat |-> 1]>>
/\ pc = (0 :> "D" @@ 1 :> "CWA")
/\ chan = (0 :> <<[ses |-> 2, type |-> "Write", dat |-> 2, orig |-> 1]>> @@ 1 :> <<>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1>>)

State 11: <D line 88, col 12 to line 107, col 50 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 2, type |-> "Write", dat |-> 2, orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 2, type |-> "Reply", dat |-> 1]>>
/\ pc = (0 :> "DW" @@ 1 :> "CWA")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1, 2>>)

State 12: <DW line 109, col 13 to line 112, col 66 of module swscop>
/\ ses = <<2>>
/\ msg = (0 :> [ses |-> 2, type |-> "Write", dat |-> 2, orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 2, type |-> "Reply", dat |-> 1]>>
/\ pc = (0 :> "D" @@ 1 :> "CWA")
/\ chan = (0 :> <<>> @@ 1 :> <<[ses |-> 3, type |-> "Ack", dat |-> 2]>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1, 2>>)

State 13: <CWA line 156, col 14 to line 162, col 59 of module swscop>
/\ ses = <<3>>
/\ msg = (0 :> [ses |-> 2, type |-> "Write", dat |-> 2, orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 3, type |-> "Ack", dat |-> 2]>>
/\ pc = (0 :> "D" @@ 1 :> "CR")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1, 2>>)

State 14: <CR line 164, col 13 to line 167, col 66 of module swscop>
/\ ses = <<3>>
/\ msg = (0 :> [ses |-> 2, type |-> "Write", dat |-> 2, orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 3, type |-> "Ack", dat |-> 2]>>
/\ pc = (0 :> "D" @@ 1 :> "CRA")
/\ chan = (0 :> <<[ses |-> 3, type |-> "Eventual", orig |-> 1]>> @@ 1 :> <<>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1, 2>>)

State 15: <D line 88, col 12 to line 107, col 50 of module swscop>
/\ ses = <<3>>
/\ msg = (0 :> [ses |-> 3, type |-> "Eventual", orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 3, type |-> "Ack", dat |-> 2]>>
/\ pc = (0 :> "DE" @@ 1 :> "CRA")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1, 2>>)

State 16: <DE line 114, col 13 to line 118, col 66 of module swscop>
/\ ses = <<3>>
/\ msg = (0 :> [ses |-> 3, type |-> "Eventual", orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 3, type |-> "Ack", dat |-> 2]>>
/\ pc = (0 :> "D" @@ 1 :> "CRA")
/\ chan = (0 :> <<>> @@ 1 :> <<[ses |-> 1, type |-> "Reply", dat |-> 0]>>)
/\ chistory = <<<<0, 1>>>>
/\ Database = (0 :> <<0, 1, 2>>)

State 17: <CRA line 169, col 14 to line 176, col 49 of module swscop>
/\ ses = <<1>>
/\ msg = (0 :> [ses |-> 3, type |-> "Eventual", orig |-> 1])
/\ op = <<2>>
/\ m = <<[ses |-> 1, type |-> "Reply", dat |-> 0]>>
/\ pc = (0 :> "D" @@ 1 :> "CW")
/\ chan = (0 :> <<>> @@ 1 :> <<>>)
/\ chistory = <<<<0, 1, 0>>>>
/\ Database = (0 :> <<0, 1, 2>>)

33 states generated, 33 distinct states found, 5 states left on queue.
The depth of the complete state graph search is 17.
Finished in 00s at (2022-03-02 05:44:28)

Reproducible with the following TLC config file swscop.cfg: 

SPECIFICATION Spec
\* Add statements after this line.
CONSTANT
    NumClients = 1
    MaxNumOp = 3
    Consistency = "Eventual"
    K = 1
INVARIANT
    Session
CHECK_DEADLOCK 
    FALSE
ailidani commented 2 years ago

The issue in general-model was, we only allow clients writes to its own region. The write() macro should be fix with this:

    (* Regular write at write region *)
    macro write(v)
    {
        with (w \in WriteRegions)
        {
            when \A i, j \in Regions : Data[i] - Data[j] < Bound;
            Database[w] := Append(@, v);
            Data[w] := v;
            History := Append(History, [type |-> "write",
                                        data |-> v,
                                      region |-> w,
                                      client |-> self]);
            session_token := v;
        }
    }

It seems my account cannot send PR for this or original repo. Can you please help verify and update? Thanks.

lemmy commented 2 years ago

The spec general-model/cosmos_client.tla intentionally models only one process per region and, thus, provides monotonic reads even under eventual consistency. This differs from scenario1/swscop.tla and scenario2/swscrw.tla, which model non-monotonic reads.