Debug ChainDB QSM failure where only the SUT iterator is exhausted

[nfrisby]

$ (cd ouroboros-network; git lg -1; git status -suno)
407146bdb - (HEAD, origin/master, origin/bors/staging, origin/HEAD) Merge #3996 (12 hours ago) <iohk-bors[bot]>

$ cabal run test-storage -- -p 'ChainDB q-s-m' --quickcheck-replay=845234

That fails (after about 10seconds of test execution) with:

    Resp {getResp = Right (IterResultGCed (IteratorResultGCed {real = True , iterResult = IteratorExhausted}))}
:/= Resp {getResp = Right (IterResultGCed (IteratorResultGCed {real = False, iterResult = IteratorResult ...}))}

This Issue is to determine the cause of the failure (I suggest checking for related comments/TODOs in the test code) and fix it.

[bartfrenk]

The sequence of commands in the failing example looks like this.

1. AddBlock
2. AddBlock
3. AddBlock
4. AddBlock
5. Stream [B2, B4]
6. AddBlock
7. IteratorNext returns B2
8. AddBlock
9. AddBlock
10. AddBlock
11. PersistBlocksThenGC
12. IteratorNextGCed returns B3
13. IteratorNextGCed; the model returns B4, while the SUT returns that the iterator is exhausted.

The value of the security parameter is 2 (TODO: check this). The diagram depicts the presumed state of the system just after step 11. Note that:

• block Bi is the block added in step i of the above sequence of commands,
• gray blocks are invalid,
• rounded blocks are in the volatile DB,
• square blocks are in the immutable DB,
• red blocks have been streamed by the iterator,
• blocks with a red border are in the interval specified on creation of the iterator.

graph LR
G-->B1(B1)
G-->B2
B2-->B3(B3)
B3-->B4(B4)
B2-->B8
B8-->B6
B6-->B9(B9)
B9-->B10(B10)
classDef streamed fill:red,stroke:red, stroke-width:3px
class B2 streamed
classDef invalid fill:gray
class B1 invalid
classDef to_stream stroke:red, stroke-width:3px
class B3 to_stream
class B4 to_stream

Loading

[bartfrenk]

This is a simpler example that fails in the same way:

graph LR
G-->B1
B1-->B2(B2)
B2-->B3(B3)
B1-->B4
B4-->B5
B5-->B6(B6)
B6-->B7(B7)
classDef to_stream stroke:red, stroke-width:3px
class B1 to_stream
class B2 to_stream
class B3 to_stream

Loading

Strangely enough, the SUT iterator is not exhausted in the following example. Here the observable behaviour of the model and the SUT is the same:

graph LR
G-->B1
B1-->B2(B2)
B2-->B3(B3)
B1-->B4
B4-->B5(B5)
B5-->B6(B6)
classDef to_stream stroke:red, stroke-width:3px
class B1 to_stream
class B2 to_stream
class B3 to_stream

Loading