tlaplus-radix-tree icon indicating copy to clipboard operation
tlaplus-radix-tree copied to clipboard

Published 20 hours ago • verified publisher icon mitchellh

Violations in RadixSeekLowerBound and RadixIteratorValidation with |Alphabet| = 3

Open lemmy opened this issue 3 years ago • 4 comments

RadixIteratorValidation

markus@banana:~/src/TLA/_specs/tlaplus-radix-tree(main)$ java -cp CommunityModules-deps.jar:/opt/toolbox/tla2tools.jar tlc2.TLC models/RadixIteratorValidation/MC
TLC2 Version 2.16 of Day Month 20?? (rev: fb369ce)
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 100 and seed -862441656364756962 with 1 worker on 16 cores with 7956MB heap and 64MB offheap memory [pid: 46103] (Linux 5.8.0-59-generic amd64, Azul Systems, Inc. 15.0.3 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/models/RadixIteratorValidation/MC.tla
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/RadixIteratorValidation.tla
Parsing file /tmp/TLC.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/FiniteSets.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/Integers.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/RadixTrees.tla
Parsing file /tmp/Sequences.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/SequencesExt.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/Inputs.tla
Parsing file /tmp/Naturals.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/FiniteSetsExt.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /tmp/Combinatorics.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/Combinatorics.tla)
Parsing file /tmp/Randomization.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Randomization.tla)
Parsing file /tmp/Functions.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/Functions.tla)
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/RadixIterator.tla
Parsing file /tmp/Folds.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/Folds.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Integers
Semantic processing of module RadixTrees
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module TLC
Semantic processing of module Combinatorics
Semantic processing of module Randomization
Semantic processing of module Inputs
Semantic processing of module RadixIterator
Semantic processing of module RadixIteratorValidation
Semantic processing of module MC
Starting... (2021-07-08 12:56:35)
<< "actual: ",
   <<<<a, a, a>>, <<a, b>>>>,
   "expected: ",
   <<<<a, b>>, <<a, a, a>>>>,
   "input: ",
   {<<a, b>>, <<a, a, a>>} >>  FALSE
<<"|Alphabet|", 3, "|Inputs|", 36, "|InputSets|", 7770>>
FALSE
Computing initial states...
Finished computing initial states: 0 distinct states generated at 2021-07-08 12:58:25.
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
0 states generated, 0 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 1.
Finished in 01min 50s at (2021-07-08 12:58:25)

RadixSeekLowerBound

markus@banana:~/src/TLA/_specs/tlaplus-radix-tree(main)$ java -cp CommunityModules-deps.jar:/opt/toolbox/tla2tools.jar tlc2.TLC models/RadixSeekLowerBound/MC
TLC2 Version 2.16 of Day Month 20?? (rev: fb369ce)
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 92 and seed -4716416157743038947 with 1 worker on 16 cores with 7956MB heap and 64MB offheap memory [pid: 34605] (Linux 5.8.0-59-generic amd64, Azul Systems, Inc. 15.0.3 x86_64, MSBDiskFPSet, DiskStateQueue).
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/models/RadixSeekLowerBound/MC.tla
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/RadixSeekLowerBound.tla
Parsing file /tmp/TLC.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/TLC.tla)
Parsing file /tmp/FiniteSets.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/FiniteSets.tla)
Parsing file /tmp/Integers.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Integers.tla)
Parsing file /tmp/Sequences.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Sequences.tla)
Parsing file /tmp/SequencesExt.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/SequencesExt.tla)
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/Inputs.tla
Parsing file /tmp/Naturals.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Naturals.tla)
Parsing file /tmp/FiniteSetsExt.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/FiniteSetsExt.tla)
Parsing file /tmp/Combinatorics.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/Combinatorics.tla)
Parsing file /tmp/Randomization.tla (jar:file:/opt/toolbox/tla2tools.jar!/tla2sany/StandardModules/Randomization.tla)
Parsing file /tmp/Functions.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/Functions.tla)
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/RadixTrees.tla
Parsing file /home/markus/src/TLA/_specs/tlaplus-radix-tree/RadixIterator.tla
Parsing file /tmp/Folds.tla (jar:file:/opt/toolbox/CommunityModules-deps.jar!/Folds.tla)
Semantic processing of module Naturals
Semantic processing of module Sequences
Semantic processing of module FiniteSets
Semantic processing of module Integers
Semantic processing of module Folds
Semantic processing of module Functions
Semantic processing of module FiniteSetsExt
Semantic processing of module SequencesExt
Semantic processing of module TLC
Semantic processing of module Combinatorics
Semantic processing of module Randomization
Semantic processing of module Inputs
Semantic processing of module RadixTrees
Semantic processing of module RadixIterator
Semantic processing of module RadixSeekLowerBound
Semantic processing of module MC
Starting... (2021-07-08 12:11:12)
<<"|Alphabet|", 3, "|Inputs|", 39, "|InputSets|", 9880>>
Computing initial states...
Computed 2 initial states...
Computed 4 initial states...
Computed 8 initial states...
Computed 16 initial states...
Computed 32 initial states...
Computed 64 initial states...
Computed 128 initial states...
Computed 256 initial states...
Computed 512 initial states...
Computed 1024 initial states...
Computed 2048 initial states...
Computed 4096 initial states...
Computed 8192 initial states...
Computed 16384 initial states...
Computed 32768 initial states...
Computed 65536 initial states...
Computed 131072 initial states...
Computed 262144 initial states...
Finished computing initial states: 385320 distinct states generated at 2021-07-08 12:11:20.
Progress(3) at 2021-07-08 12:11:23: 999,085 states generated (999,085 s/min), 999,061 distinct states found (999,061 ds/min), 385,319 states left on queue.
Error: The first argument of Assert evaluated to FALSE; the second argument was:
"Failure of assertion at line 167, column 3."
Error: The behavior up to this point is:
State 1: <Initial predicate>
/\ node = {}
/\ prefixCmp = "UNSET"
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = {}
/\ pc = "Begin"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = <<>>
/\ result = {}
/\ key = <<a, b>>
/\ stack = <<>>

State 2: <Begin line 218, col 10 to line 223, col 70 of module RadixSeekLowerBound>
/\ node = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ prefixCmp = "UNSET"
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = <<a, b>>
/\ pc = "Seek"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = <<>>
/\ result = {}
/\ key = <<a, b>>
/\ stack = <<>>

State 3: <Seek line 225, col 9 to line 239, col 76 of module RadixSeekLowerBound>
/\ node = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ prefixCmp = 0
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = <<a, b>>
/\ pc = "Search"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = <<>>
/\ result = {}
/\ key = <<a, b>>
/\ stack = <<>>

State 4: <Search line 241, col 11 to line 248, col 34 of module RadixSeekLowerBound>
/\ node = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ prefixCmp = 0
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = <<a, b>>
/\ pc = "Consume"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = <<>>
/\ result = {}
/\ key = <<a, b>>
/\ stack = <<>>

State 5: <Consume line 250, col 12 to line 260, col 39 of module RadixSeekLowerBound>
/\ node = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ prefixCmp = 0
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = <<a, b>>
/\ pc = "NextEdge"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = <<>>
/\ result = {}
/\ key = <<a, b>>
/\ stack = <<>>

State 6: <NextEdge line 262, col 13 to line 275, col 81 of module RadixSeekLowerBound>
/\ node = [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>]
/\ prefixCmp = 0
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = <<a, b>>
/\ pc = "Seek"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = << [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>],
   [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] >>
/\ result = {}
/\ key = <<a, b>>
/\ stack = <<>>

State 7: <Seek line 225, col 9 to line 239, col 76 of module RadixSeekLowerBound>
/\ node = [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>]
/\ prefixCmp = -1
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = <<a, b>>
/\ pc = "Result"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = << [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>],
   [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] >>
/\ result = {}
/\ key = <<a, b>>
/\ stack = <<>>

State 8: <Result line 277, col 11 to line 281, col 34 of module RadixSeekLowerBound>
/\ node = [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>]
/\ prefixCmp = -1
/\ root = [ Edges |->
      ( a :> [Edges |-> << >>, Value |-> <<a, a>>, Prefix |-> <<a, a>>] @@
        b :> [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>] @@
        c :> [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] ),
  Value |-> <<>>,
  Prefix |-> <<>> ]
/\ search = <<a, b>>
/\ pc = "CheckResult"
/\ input = {<<b>>, <<c>>, <<a, a>>}
/\ iterStack = << [Edges |-> << >>, Value |-> <<b>>, Prefix |-> <<b>>],
   [Edges |-> << >>, Value |-> <<c>>, Prefix |-> <<c>>] >>
/\ result = <<<<c>>, <<b>>>>
/\ key = <<a, b>>
/\ stack = <<>>

Error: The error occurred when TLC was evaluating the nested
expressions at the following positions:
0. Line 283, column 16 to line 288, column 58 in RadixSeekLowerBound
1. Line 283, column 19 to line 283, column 36 in RadixSeekLowerBound
2. Line 284, column 19 to line 285, column 71 in RadixSeekLowerBound


3138880 states generated, 3128883 distinct states found, 375322 states left on queue.
The depth of the complete state graph search is 9.

lemmy avatar Jul 08 '21 20:07 lemmy

Ping

lemmy avatar Jul 19 '21 14:07 lemmy

Thank you! I've been wanting to take a closer look at this but haven't had time yet. I appreciate you spending time making this better though and I will take a look soon. 😄

mitchellh avatar Jul 19 '21 15:07 mitchellh

If there is interest and more Go code whose correctness should be validated, I'd be happy to explore the (low-level) program execution to (high-level) spec trace checking technique. It would eliminate the need to translate the Go implementation into TLA+; one would only write the high-level TLA+ spec. Since trace checking has worked in the context of Java and C/C++, there should be few surprises with Go.

lemmy avatar Jul 19 '21 15:07 lemmy

As background, the go-immutable-radix lib backs our MemDB library which is the primary in-memory datastore for Consul, Vault, Nomad, and more products (we usually then sync that data to a physical storage in SQL or some other format).

The other big thing I wanted to model in go-immutable-radix was our watch logic and ensure that seems safe from a concurrency standpoint (that watches are properly fired, mainly at-least-once guarantees). Watches power a lot of our "blocking queries" that we expose directly to users via APIs but also trigger internal logic via them as well (i.e. when indexes should get updated or so on).

I'm not trying to recruit you into it at all, just noting the background of why I started down this journey to begin with.

mitchellh avatar Jul 19 '21 18:07 mitchellh