Use io-classes instead of unliftio

[jasagredo]

io-classes is a drop-in replacement for IO that allows to run code in IOSim which can simulate most aspects of IO (see).

[stevana]

If this is a drop-in replacement, then why is it a 1.6KLOC change?

[jasagredo]

Stylish-haskell accidentally replaced all LF with CRLF in a couple of long files. I will amend that probably tomorrow. You can see the diff excluding whitespace changes in GitHub in the meantime.

[jasagredo]

Much better now, without \rs 👍

[stevana]

Thanks, but I still don't understand why this change is needed. Can you give an example of what this allows you to do that you couldn't do before?

[jasagredo]

This allows us to run tests where the SUT runs in IOSim. We can now inject artificial file-system failures, exceptions, make time progress at different speed that real time, trace changes in TVars, or finding race conditions via IOSimPOR.

In IOG we are using this to run some tests and we use IOSim extensively, we vendored temporarily a version of Sequential.hs for this purpose.

[stevana]

Think you can provide an example that makes use of any of what you just mentioned? I don't see how finding races with IOSimPOR can work wth Sequentail.hs (nor Parallel.hs).

At the very least the changelog should be updated to mention these possibilities with links to docs.

[jasagredo]

Let me write what I think would be useful for Sequential execution. First of all keep in mind this doesn't diminish the capabilities of running tests in normal IO.

If tests are run in IOSim we can gather a trace of execution of any semantics step, observing changes to *Vars, getting say traces, or how blocking are some operations, like how much time is an operation taking at least. Provide that sequence of traces as counterexample information. This would add inspection capabilities for the SUT. Right now we only know what the SUT responded, this could tell us how it changed inside.

If tests are run in IOSimPOR, we can (on top of all the above) check for race conditions inside each specific semantics step. It is not unthinkable that a single command on the SUT forks multiple threads, which could deadlock. There is no way to currently check this, nor there is a way to inspect what an how this happens. One would have to find out in which step this happens, then introduce further inspection capabilities. With IOSimPOR, if a deadlock happens in any of the identified interleavings, then the program will halt immediately and we can observe a trace of the deadlock.

For the parallel case, we wouldn't need to repeat the tests many times, as they would be deterministic (based on the generated commands). Also we would now be able to provide counterexample information/traces more accurately as parallel execution offers just one of the failing executions. And in general IOSimPOR will now be able to find races between different commands.

I think these are extremely useful scenarios. I plan on writing a test-case that makes use of this machinery to exemplify what I mean.

[stevana]

I plan on writing a test-case that makes use of this machinery to exemplify what I mean.

Good, looking forward to seeing it!

[jasagredo]

I have been working a bit on this. The approach I followed is somewhat deeper than the one in this PR, and I now doubt that this PR is doing what we would want it to do.

The fact that the whole test runs in IOSim, albeit useful for simulating the tests, is also simulating the QSM machinery directly, which is probably not what one wants. For example the sending of events via the TChans could be reordered if we were to run this in IOSimPOR.

I have implemented some functions in this PR input-output-hk/io-sim#179 in the Execute.hs module, which run a QSM-like execution via IOSim/IOSimPOR. See the tests added in the PR to get a sense of what can this framework do. There are still some outstanding issues, like messages not being delivered promptly input-output-hk/io-sim#180 but in general this looks quite useful.

In short, I needed to add a new function initSut to the state machine, I reuse all the generating code, and this can deterministically find logic bugs, races inside commands and races between parallel commands, with shrinking and deterministic exploration.

It is still a WIP, but maybe you want to take a look.