You signed in with another tab or window. Reload to refresh your session.You signed out in another tab or window. Reload to refresh your session.You switched accounts on another tab or window. Reload to refresh your session.Dismiss alert
Copy file name to clipboardExpand all lines: tests/mbt/driver/README.md
+130-1Lines changed: 130 additions & 1 deletion
Original file line number
Diff line number
Diff line change
@@ -2,4 +2,133 @@ This folder contains the driver for the MBT framework.
2
2
It is responsible for running traces generated by the model against the actual implementation.
3
3
4
4
The driver runs the system in-memory, using the ["IBC testing"](https://github.com/cosmos/ibc-go/tree/release/v7.0.x/testing)
5
-
library to simulate the network.
5
+
library to simulate the network.
6
+
This means that we can test the implementation of the app without needing to worry about consensus, relayers, etc.
7
+
8
+
## How to run
9
+
### Generating traces
10
+
11
+
To generate traces, run
12
+
```
13
+
./generate_traces.sh
14
+
```
15
+
16
+
This will generate several "families" of traces in the `traces` folder.
17
+
18
+
Here is what one of the lines from `./generate traces` looks like:
19
+
```
20
+
go run ./... -modelPath=../model/ccv_boundeddrift.qnt -step stepBoundedDrift -invariant CanTimeoutConsumer -traceFolder traces/bound_timeout -numTraces 10 -numSteps 200 -numSamples 200
21
+
```
22
+
23
+
One very useful concept is the given `-invariant`. This is a property written in Quint which the trace generator tries to *violate*.
24
+
For example, the invariant `CanTimeoutConsumer` is a property that says "No consumer can ever time out".
25
+
If we *violate* the property, we thus find a trace where we *can* time out a consumer.
26
+
The "sanity checks" from the model make for great invariants to target here, since they
27
+
are properties that essentially specify interesting behaviour.
28
+
29
+
30
+
You may adjust the `numTraces`, `numSteps`, and `numSamples` parameters to generate more or fewer traces,
31
+
with more or fewer steps. `numSamples` is only important when you want to generate traces that find a violation
32
+
for a given invariant (in this case, used to generate traces that reach an interesting state, i.e. where a consumer has timed out).
33
+
Then a higher `numSamples` will give a higher likelihood to actually find a trace that reaches the interesting state.
34
+
35
+
As a rule of thumb to know how many traces to generate, assume generating a trace with 200 steps takes about 20 seconds, and running it against the actual implementation takes about 10 seconds.
36
+
37
+
#### Trace families
38
+
39
+
By default, I chose to generate 5 different "families" of traces:
40
+
41
+
* Bounded Drift Traces with Timeouts (`bound_timeout`): This trace family is generated to test the behavior of the system when a consumer times out. It aims to generate traces that reach an interesting state where a consumer has timed out.
42
+
43
+
* Long Bounded Drift Traces without Invariants (`bound_noinv`): This trace family focuses on generating longer traces without specific invariants. It can be useful for exploring the behavior of the system over an extended period of time.
44
+
45
+
* Bounded Drift Traces with Maturations (`bound_mat`): This trace family is designed to test the behavior of the system when VSCMaturedPackets are received on the provider.
46
+
47
+
* Synced Traces with Maturations (`sync_mat`): This trace family is designed to test the behavior of the system when VSCMaturedPackets are received on the provider. It is similar to the Bounded Drift Traces with Maturations family, but it generates traces where the chains are synchronized.
48
+
49
+
* Long Synced Traces without Invariants (`sync_noinv`): This trace family generates longer traces without specific invariants for synchronized behavior. It is similar to the Long Bounded Drift Traces without Invariants family, but it generates traces where the chains are synchronized.
50
+
51
+
52
+
### Running against traces
53
+
54
+
Once you have populated the `traces` folder with traces, you can run the traces against the actual implementation
55
+
by running
56
+
57
+
```
58
+
go test -v -timeout 30m
59
+
```
60
+
61
+
Make sure to set an appropriate timeout.
62
+
As a rule of thumb, assume running one trace with 100 steps takes about 10 second,
63
+
so for 50 traces, you might want to schedule 600 seconds to allow some buffer.
64
+
65
+
## Testing other apps
66
+
67
+
By default, we are testing with the provider and consumer apps that are provided by Interchain security.
68
+
69
+
While I have not tested it yet, it should, in principle, be very easy to plug in other applications -
70
+
simply change the `icstestingutils.ProviderAppIniter` or `icstestingutils.ConsumerAppIniter` in `setup.go`
71
+
to use the apps you are interested in.
72
+
73
+
## State comparisons
74
+
75
+
The driver is responsible for comparing the state of the model and the implementation.
76
+
This is done by comparing the state of the model and the implementation after each step of the trace.
77
+
78
+
Right now, it compares the following parts of the state:
79
+
* It checks that the consumer chains that are considered running by the provider in the system are the same as the consumers running in the model.
80
+
* It checks that the actual timestamps of all running chains match the timestamps in the model (to a second precision, see Limitations).
81
+
* It checks that the validator sets of all running chains match the validator sets in the model.
82
+
* It checks that the packet queues where both receiver and sender are running match those packet queues in the model.
83
+
It ensures the timeout timestamps of packets match, but does not check any further packet data.
84
+
* It checks that the VSCSendTimestamps on the provider match the ones from the model.
85
+
86
+
## Statistics
87
+
88
+
The driver also produces some statistics about the traces it runs.
89
+
These are relatively minimal at the moment, but can be extended as needed.
90
+
91
+
Right now, the statistics look, for example, like this, printed after running the traces:
mbt_test.go:69: Average summed block time delta passed per trace: 876h46m29.361303503s
102
+
```
103
+
104
+
Some notes are:
105
+
* We count a timeout when a consumer times out either due to the VSCTimeout, or when we attempt to deliver a packet sent from/to the consumer to a chain where its timeout timestamp has passed (and thus the channel would be closed).
106
+
* Started chains - stopped chains - timeouts is not 0, because we often just leave chains running until the end of the trace, in which case they are neither stopped nor timed out.
107
+
* The average summed block time delta passed per trace is the total time passed in all trace (as measured by the sum of time increments we have performed) divided by the number of traces.
108
+
* The number of transactions is how many VotingPowerChanges we have seen in total.
109
+
110
+
## Limitations
111
+
112
+
The driver has some limitations and quirks that are documented here.
113
+
114
+
#### One Block in the model is not one block in the implementation
115
+
In the model, we assume that when a consumer chain is started,
116
+
it takes just 1 block to get it connected to the provider, i.e. everything happens in the same block.
117
+
In reality, an IBC connection takes several blocks to be established.
118
+
Similarly, due to the limitations of light clients, we need to produce 2 blocks
119
+
to produce packets that can be received on the consumer (to accept a package from height H, the light client
120
+
needs to have seen a header of height H+1).
121
+
122
+
#### Block times are not accurate to nanoseconds
123
+
124
+
In the model, we have a notion of time that is expressed in seconds.
125
+
In the actual system, we produce blocks whose timestamps match the ones from the model,
126
+
but for technical reasons inside the ibc-go testing framework, we sometimes need to produce many
127
+
blocks in the system (e.g. when we set up an IBC connection), and those blocks need
128
+
to have different, increasing timestamps.
129
+
We solve this problem by only comparing timestamps to a second precision, and
130
+
producing "extra blocks" with only single nanosecond increments between block times.
131
+
Thus, to the coarse second precision, the timestamps match, but to the nanosecond precision,
132
+
they are different.
133
+
This will cause problems in practice if we produce on the order of tens of millions of blocks in one trace,
134
+
but as long as we produce only a few thousand blocks per trace, this should not be a problem.
0 commit comments