Make it possible to generate schedules

[ghost]

I understand that running IOSim s computations is purely deterministic: Every run will trigger the exact same scheduling of threads. This is great as it provides fast execution, but unless one wants to invest time and energy in IOSimPOR it does not actually help us spot the kind of problems in concurrent code stemming from "surprising" reordering of executions.

It seems to me that quick-checking code with IOSim would be even more powerful if the runtime was able to randomly select among runnable actions, generating and covering more possible execution schedules. I have only a vague understanding of io-sim's internals but this could be exposed at the API level through a function with an additional argument, like:

runSimTraceRandom :: forall g a . RandomGen g => g -> (forall s . IOSim s a) -> Trace a

Are you willing to implement it?

• Are you? 😃

[bolt12]

Thanks for opening this issue! This would indeed be a great addition! This feature is something io-sim is lacking when compared with other similar libraries like dejafu . In the meantime, can I recommend that different order of executions can still be achieved if you introduce explicit delays and attenuation in your program. You can randomly generate these to allow for different interleaving of threads to happen and possibly explore more of the state space. IOSimPOR will then find the possible races that could still happen and check them more thorougly

[ghost]

Thanks @bolt12 for the encouraging comment :)
Adding randomness inside the code can be useful when you suspect some issue, but quite painful to deal with in terms of ergonomics. Hence the proposal to do this in a more systematic way, leveraging QC's capabilities. I could even imagine that quick-checking a propery on IOSim traces could lead to automated shrinking of those traces, perhaps?

[bolt12]

I understand, depending on the program introducing delays can be quite a hassle. For networking code that comes quite naturally. With this being said, I think that if a solution a la dejafu could be achieved, where they have an explicit Scheduler type that can be passed to the simulator would be better. This way you could have QC generate different Schedulers and shrink them

[coot]

TLDR: a random scheduler is a nice addition but to IOSimPOR rather than IOSim.

A random scheduler would be something nice to add but let me mention that one can already achieve something similar by instrumenting different delays, e.g. making your IO calls like readFile or network's receive calls block for different amount of time.

As of implementation, one can pass an rng to the scheduler and let it randomly pick next thread to execute rather than pop first one from the queue. This has an advantage over generating schedules which requires IOSimPOR capabilities.

On the other hand IOSimPOR is much more robust than a random walk through all schedules. The POR part is important especially since the spaces grows exponentially with number of execution steps. Random schedule will explore all of the schedules, where most of them will not result in exploring new application state, while POR makes it efficient: one only runs new schedules which makes a difference.

There's a reason to add randomness to IOSimPOR scheduler though. It learns new schedules while it executes the simulation. Exploring them in different order will lead to finding new schedules in different order, which matters as by default we limit the number of new schedules to 100 (which is configurable). Another benefit would be that it will likely catch more bugs in IOSimPOR itself, and thus give us a chance to make it more robust.

[coot]

I realised that if we are just interested in reordering of two events if there are N threads running, the chance to revert them can be even greater than 1/N, so random scheduling in IOSim could actually be quite effective.