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. This sequence can be copy/pasted and reused directly as a test against either the Model or the implementation as exemplified by the following sample:

@@ it "runs actions against actual nodes" $ do let Actions act = Actions [ Var 1 := Seed { seedKeys = [ (HydraSigningKey (SignKeyEd25519DSIGN "00000000000000000000000000000000000000000000000000000000000000003b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29"), "0100000008030606080507030707000607020508050000020207070508040800") , (HydraSigningKey (SignKeyEd25519DSIGN "2e00000000000000000000000000000000000000000000000000000000000000264a0707979e0d6691f74b055429b5f318d39c2883bb509310b67424252e9ef2"), "0106010101070600040403010600080805020003040508030307080706060608") , (HydraSigningKey (SignKeyEd25519DSIGN "ed785af0fb0000000000000000000000000000000000000000000000000000001c02babf6d3d51b725db8b72043823d66634b39db74836b1494bdb647073d566"), "0000070304040705060101030802010105080806050605070104030603010503") ] } , Var 2 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "3b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29")}, command = Init{contestationPeriod = -6.413670805613}} , Var 3 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "264a0707979e0d6691f74b055429b5f318d39c2883bb509310b67424252e9ef2")}, command = Commit{Input.utxo = [("0106010101070600040403010600080805020003040508030307080706060608", valueFromList [(AdaAssetId, 18470954)])]}} , Var 4 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "1c02babf6d3d51b725db8b72043823d66634b39db74836b1494bdb647073d566")}, command = Commit{Input.utxo = [("0000070304040705060101030802010105080806050605070104030603010503", valueFromList [(AdaAssetId, 19691416)])]}} , Var 5 := Command{Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "3b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29")}, command = Commit{Input.utxo = [("0100000008030606080507030707000607020508050000020207070508040800", valueFromList [(AdaAssetId, 7003529)])]}} , Var 6 := Command { Model.party = Party{vkey = HydraVerificationKey (VerKeyEd25519DSIGN "3b6a27bcceb6a42d62a3a8d02a6f0d73653215771de243a63ac048a18b59da29")} , command = NewTx { Input.transaction = Payment { from = "0100000008030606080507030707000607020508050000020207070508040800" , to = "0106010101070600040403010600080805020003040508030307080706060608" , value = valueFromList [(AdaAssetId, 7003529)] } } } ] -- env and model state are unused in perform env = []

dummyState :: WorldState (IOSim s) dummyState = WorldState{hydraParties = mempty, hydraState = Start}

loop [] = pure () loop ((Var{} := a) : as) = do void $ perform dummyState a (lookUpVar env) loop as tr = runSimTrace $ evalStateT (loop act) (Nodes mempty traceInIOSim) traceDump = printTrace (Proxy :: Proxy Tx) tr print traceDump True shouldBe True @@