search

microsoft / CCF

Confidential Consortium Framework
https://microsoft.github.io/CCF/
Apache License 2.0
761 stars 205 forks source link

[TLC Repro] Stack overflow likely caused by large state variable #6137

Closed achamayou closed 4 weeks ago

achamayou commented 4 weeks ago

Steps:

cd tla
JSON=traces/consistency/trace.ndjson ./tlc.sh consistency/TraceMultiNodeReads.tla  > out

out then contains:

Error: This was a Java StackOverflowError. It was probably the result
of an incorrect recursive function definition that caused TLC to enter
an infinite loop when trying to compute the function or its application
to an element in its putative domain.
Error: The behavior up to this point is:

Warning: out gets large (30Mb+)

lemmy commented 4 weeks ago

InsertOtherTxnAction allows for behaviors with infinitely many consecutive AppendOtherTxnAction which leave the variable l forever unchanged. Can you come up with a (tight) bound of the number of successive AppendOtherTxnAction that can be expressed in, e.g., a state constraint?

achamayou commented 4 weeks ago

InsertOtherTxnAction allows for behaviors with infinitely many consecutive AppendOtherTxnAction which leave the variable l forever unchanged. Can you come up with a (tight) bound of the number of successive AppendOtherTxnAction that can be expressed in, e.g., a state constraint?

Yes, as described yesterday, the boundary is provided by IsRwTxExecuteAction eventually matching once a sufficient ledgerBranch prefix has been produced. This works in #6136.

Where that breaks down is when a rollback takes place, creating a second appendable ledgerBranch, for which the trace may not contain any further IsRwTxExecuteAction.