Improve garbage-collection/cleaning-up

[kderme]

I think this is a very common issue many users face: Since q-s-m is used to test monadic code, it's possible that there is some interference between consecutive tests, or betweeen shrinking trials and proper cleaning up of resources is hard.

I faced this issue mainly on my rqlite tests https://github.com/advancedtelematic/quickcheck-state-machine/tree/rqlite, where I spawn new unix processes which listen on ports.
The solution I found there was to use the final Model returned from runCommands and do the cleaning up using this. For the parallel case, I extended the runParallelCommands, so that it also returns the final Environment and do the cleanup. It works, but if the re is an unexpected exception the cleanup won't happen. That's why I have disabled shrinking for now.

Another idea, is to get a cleanup function from the user and install handlers whenever suitable. Not sure how feasible this is and how big of a breaking change.

[mrBliss]

I have wanted this too (while working on https://github.com/input-output-hk/ouroboros-network/).

@edsko and I have come up with the following workaround: add a new command, e.g., Reset, that does the clean-up for the model in transition and the clean-up for the real implementation in semantics. Don't generate this command (so that the shrinker can never get its hands on it), but just append it to the list of parallel commands (something like: forAllParallelCommands sm $ \cmds -> monadicIO $ runParallelCommandsNTimes 100 sm (snoc cmds Reset)).

[stevana]

I've used pkill in some tests, it's ugly but got the job done...

In older versions of the library, setup and cleanup functions used to be part of the StateMachine record. I removed them in order to try to simplify things, but it could very well be that cleanup needs to be part of that interface...

[kderme]

I think asking for a user function to do the cleanup is a good idea. During execution we should be careful to evaluate everything with proper exception handles (similar to what QuickCheck does http://hackage.haskell.org/package/QuickCheck-2.13.1/docs/src/Test.QuickCheck.Exception.html#tryEvaluate) and in case of exceptions we should do the cleanup before propagating. This is possible in all executeXX commands, since they live in IO, but not possible for all shrinkXX and generateXX commands. That's not an issue though, since there should be no running user recourses while shrinking or generating, User interrupts and async exceptions should also trigger the cleanup process before being propagated.

I think the type of the user function should be something like Environment -> IO (). An alternative idea, having Model Conrete -> IO () is not that good, since in parallel execution the current Model is unreliable (but the environment is still reliable). What I'm mostly concerned is whether the Environment has enough information for the user to do the proper cleanup. In my example of rqlite it is enough, but not sure if it's enough all cases.

[stevana]

not that good, since in parallel execution the current Model is unreliable (but the environment is still reliable)

Why is the model unreliable? Can we not make it:

cleanup :: { prefix :: Model Concrete, suffixes :: [Model Concrete] } -> IO ()

?

I'm a bit hesitant to expose Environment to the user. It feels like an internal type...

[kderme]

In the parallel case executeCommands is called with the initModel as intial state. Inside executeCommands there is no precondition check and the final Model (result of transition) is usually just an unevaluated exception or something completely wrong.

(reason, (env', _, _, _)) <- (runStateT (executeCommands sm hchan (Pid i) check cmds) (env, initModel, newCounter, initModel))

I replaced this with

reason, (env', _, _, cmodel)) <- (runStateT (executeCommands sm... -same-
liftIO $ evaluate cmodel

and there were many failures.
The issue is that there is no way we can know the real Model after a suffix is executed, so whatever result executeCommands returns is unreliable. What we know however is the Environment, or the references that were created (the random order does not affect this).

[stevana]

In the parallel case executeCommands is called with the initModel as intial state.

Yes, but that would be easy to change: pass in the model that's the result of executing the prefix. The problem to me seems to be that after executing one batch of suffixes, we cannot combine the resulting models and continue executing the next batch with the combined model. Unlike environments which have a monoid structure.

Or is there some other problem you're seeing?

[kderme]

I think it's the same problem. What you mention

pass in the model that's the result of executing the prefix

can only work for the first suffix. Next suffixes can't get a correct inital Model, because as you mention we can;t combine Models.

[stevana]

So another option would be to require Monoid (model r). Also a bit awkward...

[kderme]

Yes I don't think this will work either. Assume in MemoryReference, one threads runs Increment ref and the other Write ref 2. In the one Model the reference would become 1, while in the other 2 and there is no proper way to combine them.

Another option is to somehow have the user keep an environment which is Monoidal and make sure that this transitions correctly even in parallel tests. Something like it was done here https://github.com/input-output-hk/ouroboros-network/blob/master/ouroboros-consensus/test-util/Test/Util/RefEnv.hs#L35 and the model uses it in this way https://github.com/input-output-hk/ouroboros-network/blob/master/ouroboros-consensus/test-storage/Test/Ouroboros/Storage/ImmutableDB/StateMachine.hs#L301. Then this part of the Model transitions by a simple union.

[stevana]

In the one Model the reference would become 1, while in the other 2 and there is no proper way to combine them.

True, that's really ugly.

How about getting the references from the history? Our run functions return histories already... Or build a model from the histories and then pass it to the cleanup function?

[kderme]

Indeed, I think History would also work and is a good idea.
Building the general Model seems hard though.

[stevana]

Building the general Model seems hard though.

Why so?

The history contains all commands and their responses, using the initial model and the transition functions should let us build a model similar to how linearise does it.

This model might not be consistent unless the history linearises, but this shouldn't matter for the cleanup (we only care that all references are there).

Likewise in case of an exception (and a missing response) the reference has probably not been created and hence doesn't need to be cleaned up. It's up to the user to clean up inside the semantics function in this case.

[kderme]

linearise stops if there is no postcondition that can hold, so any references created after that will not be visible on the Model. Do you think we can overcome this?