Model-Based testing of Hydra Head protocol implementation.

• Troubleshooting
• * Deadlocks

One of the most annoying problems one can face with those very high level properties involving multithreading and a lot of complex moving parts is when the test execution deadlocks. Here is a short guide on what one can do to troubleshoort this kind of issue:

• **Check generators**: suchThat combinator from QuickCheck is useful when one wants to refine another Generator's behaviour but it can lead to deadlock if the filtering leads to no value being generated. Avoid it.
• **Dump nodes' logs**: In case of a "normal" failure of the tests, the logs from the nodes are dumped. However, if the test does not even complete then no logs are produced because they are kept in memory. In this case. replacing traceInIOSim with `traceInIOSim <> traceDebug` will ensure the logs are dumped on the stderr. It could be a good idea to store them in a file as they can be quite large.
• **Use** trace liberally: Because getting a proper stack trace is hard in Haskell, esp. in pure code, sprinkling trace statements at key points might help understand what's going on and zoom in on the culprits
• **Dump IOSim trace**: In case the deadlock (or race condition) is caused by having two or more concurrent threads competing to access a resource, dumping the trace of IOSim's runtime scheduleer execution can help. io-sim generate its trace lazily which means that even when it deadlocks, one can capture at least a significant prefix of the trace and dump it to stderr. One can `map ( t -> trace (ppEvents t) t) . traceEvents` over the SimTrace returned by runSimTrace to get some pretty-printed output similar to:

@ Time 380.1s - ThreadId [4] node-94455e3e - EventThrow AsyncCancelled Time 380.1s - ThreadId [4] node-94455e3e - EventMask MaskedInterruptible Time 380.1s - ThreadId [4] node-94455e3e - EventMask MaskedInterruptible Time 380.1s - ThreadId [4] node-94455e3e - EventDeschedule Interruptable Time 380.1s - ThreadId [4] node-94455e3e - EventTxCommitted [Labelled (TVarId 25) (Just "async-ThreadId [4]")] [] Nothing Time 380.1s - ThreadId [] main - EventTxWakeup [Labelled (TVarId 25) (Just "async-ThreadId [4]")] Time 380.1s - ThreadId [4] node-94455e3e - EventUnblocked [ThreadId []] Time 380.1s - ThreadId [4] node-94455e3e - EventDeschedule Yield Time 380.1s - ThreadId [] main - EventTxCommitted [] [] Nothing Time 380.1s - ThreadId [] main - EventUnblocked [] Time 380.1s - ThreadId [] main - EventDeschedule Yield Time 380.1s - ThreadId [4] node-94455e3e - EventThreadFinished Time 380.1s - ThreadId [4] node-94455e3e - EventDeschedule Terminated Time 380.1s - ThreadId [] main - EventThreadFinished @

• * Recording trace failures

When a property fails it will dump the sequence of actions leading to the failure:

@ do action $ Seed {seedKeys = [("8bbc9f32e4faff669ed1561025f243649f1332902aa79ad7e6e6bbae663f332d",CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"})], seedContestationPeriod = 46s, seedDepositDeadline = 50s, toCommit = fromList [(Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"},[(CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"},valueFromList [(AdaAssetId,54862683)])])]} var2 <- action $ Init (Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}) action $ Commit {headIdVar = var2, party = Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, utxoToCommit = [(CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"},valueFromList [(AdaAssetId,54862683)])]} action $ Decommit {party = Party {vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, decommitTx = Payment { from = CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, to = CardanoSigningKey {signingKey = "0702050602000101050108060302010707060007020308080801060700030306"}, value = valueFromList [(AdaAssetId,54862683)] }} action $ Deposit {headIdVar = var2, utxoToDeposit = [(CardanoSigningKey {signingKey = "0400020803030302070808060405040001050408070401040604000005010603"},valueFromList [(AdaAssetId,54862683)])], deadline = 1864-06-06 08:24:08.669152896211 UTC} pure () @

Which can be turned into a unit test after resolving most of the imports. Common pitfalls are incorrect show instances (e.g. the UTCTime in deadline above). Should the variables not be bound correctly, double check HasVariables instances. A working example of the above output would be:

@ it "troubleshoot" . withMaxSuccess 1 . flip forAllDL propHydraModel $ do action $ Seed{seedKeys = [("8bbc9f32e4faff669ed1561025f243649f1332902aa79ad7e6e6bbae663f332d", CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"})], seedContestationPeriod = UnsafeContestationPeriod 46, seedDepositDeadline = UnsafeDepositDeadline 50, toCommit = fromList [(Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, [(CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, valueFromList [(AdaAssetId, 54862683)])])]} var2 <- action $ Init (Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}) action $ Commit{headIdVar = var2, party = Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, utxoToCommit = [(CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, valueFromList [(AdaAssetId, 54862683)])]} action $ Decommit{party = Party{vkey = "b4ea494b4bda6281899727bf4cfef5cdeba8fb3fec4edebc408aa72dfd6ad4f0"}, decommitTx = Payment{from = CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, to = CardanoSigningKey{signingKey = "0702050602000101050108060302010707060007020308080801060700030306"}, value = valueFromList [(AdaAssetId, 54862683)]}} action $ Deposit{headIdVar = var2, utxoToDeposit = [(CardanoSigningKey{signingKey = "0400020803030302070808060405040001050408070401040604000005010603"}, valueFromList [(AdaAssetId, 54862683)])], deadline = read "1864-06-06 08:24:08.669152896211 UTC"} pure () @