Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

Sign up for GitHub

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Jump to bottom

Counterexample too short with StateDeque #913

Open
lemmy opened this issue Apr 24, 2024 · 3 comments
Open

Counterexample too short with StateDeque #913

lemmy opened this issue Apr 24, 2024 · 3 comments
Labels
bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...

Comments

@lemmy
Copy link
Member

lemmy commented Apr 24, 2024 •
edited

Running trace validation with the new StateDeque on the spec TraceMultiNodesReads from https://github.com/achamayou/CCF/tree/tlc-repro yields a counterexample that is two states shorter compared to TLC running with DiskStateQueue.

Running breadth-first search Model-Checking with fp 38 and seed 8225302872081556446 with 1 worker on 8 cores with 14290MB heap and 64MB offheap memory [pid: 178660] (Linux 5.15.0-1059-azure amd64, Ubuntu 11.0.22 x86_64, MSBDiskFPSet, StateDeque).

...

51: <BackfillLedgerBranch line 128, col 5 to line 141, col 24 of module TraceMultiNodeReads>
/\ history = <<[type |-> RwTxRequest, tx |-> 0], [type |-> RwTxResponse, tx |-> 0, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> TxStatusReceived, tx_id |-> <<2, 29>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 1], [type |-> RoTxResponse, tx |-> 1, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> RwTxRequest, tx |-> 2], [type |-> RwTxResponse, tx |-> 2, tx_id |-> <<2, 31>>, observed |-> <<0, 2>>], [type |-> TxStatusReceived, tx_id |-> <<2, 31>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 3], [type |-> RoTxResponse, tx |-> 3, tx_id |-> <<2, 32>>, observed |-> <<0, 2>>], [type |-> RwTxRequest, tx |-> 4], [type |-> RwTxResponse, tx |-> 4, tx_id |-> <<2, 34>>, observed |-> <<0, 2, 4>>], [type |-> TxStatusReceived, tx_id |-> <<2, 34>>, status |-> InvalidStatus], [type |-> RwTxRequest, tx |-> 5]>>
/\ l = 18
/\ ledgerBranches = << <<>>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2] >>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2],
      [view |-> 3] >> >>
52: <IsRwTxExecuteAction line 58, col 5 to line 68, col 67 of module TraceMultiNodeReads>
/\ history = <<[type |-> RwTxRequest, tx |-> 0], [type |-> RwTxResponse, tx |-> 0, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> TxStatusReceived, tx_id |-> <<2, 29>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 1], [type |-> RoTxResponse, tx |-> 1, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> RwTxRequest, tx |-> 2], [type |-> RwTxResponse, tx |-> 2, tx_id |-> <<2, 31>>, observed |-> <<0, 2>>], [type |-> TxStatusReceived, tx_id |-> <<2, 31>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 3], [type |-> RoTxResponse, tx |-> 3, tx_id |-> <<2, 32>>, observed |-> <<0, 2>>], [type |-> RwTxRequest, tx |-> 4], [type |-> RwTxResponse, tx |-> 4, tx_id |-> <<2, 34>>, observed |-> <<0, 2, 4>>], [type |-> TxStatusReceived, tx_id |-> <<2, 34>>, status |-> InvalidStatus], [type |-> RwTxRequest, tx |-> 5]>>
/\ l = 19
/\ ledgerBranches = << <<>>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2],
      [tx |-> 5, view |-> 2] >>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2],
      [view |-> 3] >> >>
Assumption line 190, col 5 to line 190, col 29 of module TraceMultiNodeReads is false.
Progress(54) at 2024-04-23 13:47:31: 55 states generated (4,940 s/min), 55 distinct states found (4,940 ds/min), 0 states left on queue.
55 states generated, 55 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 54.
Finished in 672ms at (2024-04-23 13:47:31)
Running breadth-first search Model-Checking with fp 70 and seed -3924861561106052578 with 1 worker on 8 cores with 14290MB heap and 64MB offheap memory [pid: 180627] (Linux 5.15.0-1059-azure amd64, Ubuntu 11.0.22 x86_64, MSBDiskFPSet, DiskStateQueue).

...

State 53: <IsRwTxResponseAction line 71, col 5 to line 77, col 43 of module TraceMultiNodeReads>
/\ history = <<[type |-> RwTxRequest, tx |-> 0], [type |-> RwTxResponse, tx |-> 0, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> TxStatusReceived, tx_id |-> <<2, 29>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 1], [type |-> RoTxResponse, tx |-> 1, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> RwTxRequest, tx |-> 2], [type |-> RwTxResponse, tx |-> 2, tx_id |-> <<2, 31>>, observed |-> <<0, 2>>], [type |-> TxStatusReceived, tx_id |-> <<2, 31>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 3], [type |-> RoTxResponse, tx |-> 3, tx_id |-> <<2, 32>>, observed |-> <<0, 2>>], [type |-> RwTxRequest, tx |-> 4], [type |-> RwTxResponse, tx |-> 4, tx_id |-> <<2, 34>>, observed |-> <<0, 2, 4>>], [type |-> TxStatusReceived, tx_id |-> <<2, 34>>, status |-> InvalidStatus], [type |-> RwTxRequest, tx |-> 5], [type |-> RwTxResponse, tx |-> 5, tx_id |-> <<3, 36>>, observed |-> <<0, 2, 4, 5>>]>>
/\ l = 20
/\ ledgerBranches = << <<>>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2] >>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2],
      [view |-> 3],
      [tx |-> 5, view |-> 3] >> >>

State 54: <IsStatusCommittedResponseAction line 80, col 5 to line 86, col 43 of module TraceMultiNodeReads>
/\ history = <<[type |-> RwTxRequest, tx |-> 0], [type |-> RwTxResponse, tx |-> 0, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> TxStatusReceived, tx_id |-> <<2, 29>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 1], [type |-> RoTxResponse, tx |-> 1, tx_id |-> <<2, 29>>, observed |-> <<0>>], [type |-> RwTxRequest, tx |-> 2], [type |-> RwTxResponse, tx |-> 2, tx_id |-> <<2, 31>>, observed |-> <<0, 2>>], [type |-> TxStatusReceived, tx_id |-> <<2, 31>>, status |-> CommittedStatus], [type |-> RoTxRequest, tx |-> 3], [type |-> RoTxResponse, tx |-> 3, tx_id |-> <<2, 32>>, observed |-> <<0, 2>>], [type |-> RwTxRequest, tx |-> 4], [type |-> RwTxResponse, tx |-> 4, tx_id |-> <<2, 34>>, observed |-> <<0, 2, 4>>], [type |-> TxStatusReceived, tx_id |-> <<2, 34>>, status |-> InvalidStatus], [type |-> RwTxRequest, tx |-> 5], [type |-> RwTxResponse, tx |-> 5, tx_id |-> <<3, 36>>, observed |-> <<0, 2, 4, 5>>], [type |-> TxStatusReceived, tx_id |-> <<3, 36>>, status |-> CommittedStatus]>>
/\ l = 21
/\ ledgerBranches = << <<>>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2] >>,
   << [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 0, view |-> 2],
      [view |-> 2],
      [tx |-> 2, view |-> 2],
      [view |-> 2],
      [view |-> 2],
      [tx |-> 4, view |-> 2],
      [view |-> 3],
      [tx |-> 5, view |-> 3] >> >>

Error: Assumption line 190, col 5 to line 190, col 29 of module TraceMultiNodeReads is false.
55 states generated, 55 distinct states found, 0 states left on queue.
The depth of the complete state graph search is 54.
Finished in 00s at (2024-04-23 13:49:45)
@lemmy lemmy added bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ... labels Apr 24, 2024
@lemmy
Copy link
Member Author

lemmy commented Apr 24, 2024

@achamayou Could you please commit a corresponding trace.ndjson to your tlc-repro branch?

@lemmy
Copy link
Member Author

lemmy commented May 8, 2024

Related: TLC should not print "Running breadth-first search Model-Checking..." when configured to run with StateDeque.

@achamayou
Copy link

@lemmy my bad, I thought I had, but I was working with symlinks and I ended up checking the symlink (!).

Anyway the trace is at https://github.com/achamayou/CCF/blob/tlc-repro/tla/trace.ndjson, and a repro script showing the different counter examples at https://github.com/achamayou/CCF/blob/tlc-repro/tla/repro.sh

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Assignees
No one assigned
Labels
bug error, glitch, fault, flaw, ... Tools The command line tools - TLC, SANY, ...
Milestone
No milestone
Development

No branches or pull requests
2 participants
@lemmy @achamayou