Re-creating a stalling property test

Clash Help
1

Hello all

I have been trying to figure out a slightly elusive bug. One of my hedgehog property tests (that uses the clash Hedgehog test harness) is stalling - as in, the test is going on for ever and not getting anywhere.

I’ve tried to reduce this down to a minimal example, and I’ve put that in a repo, here: GitHub - harris-chris/clash-stall-example

I’ve created a very simple circuit (simpleTestCircuit) that has a single PacketStream input channel, and two PacketStream output channels. It’s a combinational circuit and all it does is forward the input channel to the second of the two output channels, and ouputs Nothing on the other one.

There’s then a single test, which:

  • instantiates simpleTestCircuit
  • combines it with a stall circuit, of the type that gets used in the clash hedgehog test harness. The stall circuit doesn’t actually stall (because it’s initiated with no stall cycles).
  • puts out debug output which shows that:
    • simpleTestCircuit works by itself
    • the stall circuit works by itself
    • they don’t work together - it stalls (the bad kind of stall)

The stalling seems to occur when an m2s or s2m output of the “combined circuit” - ie simple test circuit |> the stall circuit - is evaluated.

It may seem like a slightly weird and contrived test, but I’ve tried to create a minimal example of what seemed to be going wrong with the actual failing property test.

A nix flake is included in the repo so you should be able to do nix develop .#; cabal test to see the issue.

2 
diff --git a/src/SimpleTestCircuit.hs b/src/SimpleTestCircuit.hs
index 3f75011..44a3783 100644
--- a/src/SimpleTestCircuit.hs
+++ b/src/SimpleTestCircuit.hs
@@ -19,7 +19,7 @@ simpleTestCircuit
   => Circuit
       ( PacketStream dom dw () )
       ( PacketStream dom dw (), PacketStream dom dw () )
-simpleTestCircuit = Circuit $ \(fwdIn, (bwd1, bwd2)) ->
+simpleTestCircuit = Circuit $ \(fwdIn, ~(bwd1, bwd2)) ->
   let
     -- Channel 1 output is always Nothing
     ch1Out = pure Nothing

The “bug” is that you’re matching on the tuple right away, while the production of the tuple is (apparently) dependent on the production of your output tuple. You can read more about lazy pattern matches (~) here: Lazy pattern match - HaskellWiki.

Whether this is a bug in simpleTestCircuit or other functions is hard to say. I think we don’t have a good understanding yet what the strategy should be here. Usually this problem is side-stepped by using the circuit notation plugin: it will insert these lazy matches everywhere by default.

3

Thanks Martijn! A single unicode character might be the shortest bug-fix I’ve ever seen.

I understand why lazy pattern matching would be needed here, but being conscious of when to use it does add a bit to the overhead of writing these circuits. All else equal, is it better to use the circuit-notation syntax, for this reason? I like it because it also makes the circuit layout clearer, but on the downside, it currently has no documentation and gives quite mysterious error messages.

4

I like the circuit notation plugin for the reasons you mention, yeah. I’m using it in a medium sized project and issues like these have yet to crop up. You’re very right on the error messages though, they can be incredibly bad. This is nothing fundamental AFAIK. It would take a couple of weeks of developer time to go through the GHC API proper and make sure the plugin moves around source code context correctly, but so far we haven’t been able to allocate resources to it.