doc request: can dejafu find deadlocks in code that runs `forever`?

[jwaldmann]

E.g., this straightforward dining philosophers implementation: https://github.com/jwaldmann/dejafu/blob/master/dejafu/examples/Diner.hs has

 forM [1..n] $ \ p ->
    (if p < n then void . forkIO else id ) $ forever $ do

and when I run it under dejavu, nothing happens for a long time (for n >= 2), while I would hope the deadlock is detected.

[barrucadu]

The problem here is that the program isn't terminating which, sadly, is the assumption underlying the entire testing methodology. A possible work-around I could add would be to add an execution length bound, at which point the program would just be stopped, and this indicated in the output. What do you think?

[jwaldmann]

how do you detect deadlocks? (detecting them should not need termination?)

Execution length bound: yes please. (You could also increase it gradually, thus simulating BFS by truncated DFSs.)

[barrucadu]

It executes the program using a non-pre-emptive scheduler, and then examines the trace afterwards for places where alternative scheduling decisions could lead to different results. It then tries again making those alternative decisions, and so on, until there are no remaining interesting alternatives to take.

The problem here is that this dining philosophers implementation doesn't terminate if there are no pre-emptions, so the first run never completes.

[barrucadu]

I've added a default length bound of 250, which may be too much as the dining philosophers example still takes a long time. Here's the output with a bound of 50:

[fail] Never Deadlocks (checked: 7)
        [deadlock] S0--------------P1-----S0-
[pass] No Exceptions (checked: 91)
[fail] Consistent Result (checked: 90)
        [abort] S0-------------P1-------------------------------------
        [deadlock] S0--------------P1-----S0-

autocheck displays the simplest trace it can find for each outcome, so it shows one deadlock, and one aborted execution - which is where the length bound was exceeded.

[barrucadu]

There is now an example in the test suite: https://github.com/barrucadu/dejafu/commit/0ff053eaae3650c8b112b962dbddf505c8339d5b