bracketP doesn't work

[Lysxia]

Current source of bracketP

return . prop never fails, so the finalizer is never run. Using bracketOnError seems also strange. Most of the time we want to clean up resources regardless of whether the bracketed operation fails (use bracket instead). Ultimately I don't think bracketP on properties is actually needed, it operates at the wrong level of abstraction.

A consequence of its current behavior is that the CrudWebserver examples spawn servers without killing them. When the setup action is run (once per test case), I believe the following happens:

• the first call binds a constant port (8080, 8081 or 8082 depending on the test case);

• in all the others calls the new server dies because the first one is still living and using that port, but setup still returns happily.

  • CrudWebServerDb doesn't check that failure.
  • The check in CrudWebServerFile has a race condition: the server thread may be polled just before it fails, so we see Nothing and assume the server is fine.

• Thus tests continue talking with the first server, which carries data from previous runs. Tests still succeed because the preconditions in the model prevent reading data that the current test case has not (over)written.

I think there are two options here, and in both cases a simple bracket would be sufficient:

• Start and stop a new server for each run. A better place for this would be inside the StateMachine runner, rather than a bracket around the toplevel prop_* properties.
• Spawn a global server and reuse it. One must export an action to initialize it before properties are run.

Any preference for fixing the CrudWebserver examples?

[stevana]

Yeah, I recall that I couldn't get clean up to work properly, probably because of the reasons you explained. Thanks for looking into it.

I think both options might be desirable and it would be nice if we had an example of each approach. Perhaps CrudWebserverFile could be started and stopped each run, while the Db version spawned globally?

[Lysxia]

It's a good idea to demonstrate both.

Now, it looks like the current specifications for these web servers cannot be parallelized. For instance, a simple counterexample for the File version is: in the prefix, create a file; in both suffixes, delete the file. Are the parallel properties expected to fail here, and if not, what would be a good fix?

[stevana]

If we make the server implementation use removePathForcibly instead of removeFile then the fact that the file isn't there for second delete action doesn't matter. The post-condition just checks should work fine? Is there anything else that could go wrong?

By the way, this example was inspired by: https://github.com/Quviq/QuickCheckExamples/blob/master/src/crud_eqc.erl .

[Lysxia]

There could be a concurrent GetFile and DeleteFile, so if DeleteFile execute first, GetFile will fail.

There are a few points I'd like to ask about in the testing process for parallel programs.

• It seems that linearization should allow traces where, for instance, we try to read a file we just deleted. In that case, we need to relax the precondition to allow reading non existent files, and the postcondition to allow returning errors. But even the Erlang example doesn't seem to do that. Am I missing something?
• Am I right in thinking that the generation process, reusing the sequential program generator, is meant to be heuristic: the generation of the two suffixes simulates two independent single-threaded models; we hope that makes them interesting enough, even though the models will not match the subsequent parallel execution?

[stevana]

Ah yes, I now remember a discussion with @Danten where he raised a similar point about the Erlang example. I don't think we came to any satisfactory conclusion about how the Erlang version works. Do note that there is a bunch of read2_* things that are supposed to simulate failed reads. But I don't get how we can generate successful reads in the suffixes that we for sure know will succeed, because of the point you raised.

This leads to your second question. Perhaps the model should be shared when we generate the suffixes, and not independent like it is now? I don't think that makes sense though, because we don't know how the threads are scheduled or how long the operations take to execute.

I think instead what we need to do is to generalise histories. This is getting a bit off topic for this issue, so I'll create a new one.

[Lysxia]

Thanks for your answer! I'll keep looking at the literature surrounding the topic and see whether anything interesting comes up.

[stevana]

Started a bit on this in the bugfix/bracket branch.

[stevana]

This issue regarding bracket was fixed in #166.

Let's continue the discussion about what to do when the semantics of actions fails in #162.