io-sim: Fix flushTQueue implementation

[ch1bo]

Fixes #133 and also another issue found while fixing.

Now flushTQueue actually empties the queue and also maintains FIFO order.

[coot]

This is wrong, because f has access to either side (read / write) of the queue, rather than all its elements. This is the reason why I kept the default implementation of TQueueDefault in a single TVar instead of two. This approach requires more substantial changes to io-sim.

I think it's much simpler to just fix flushTQueueDefault.

[ch1bo]

So you suggest keeping the differing implementation using a single TVar? Why is tracing a deciding factor here - can't we implement this on the standard implementation of read/write end queues?

[coot]

Because it is designed for verification purposes, so it's quite crucial for the library.

So you suggest keeping the differing implementation using a single TVar?

Yes, keep the current implementation which btw is based on a standard queue data type (see Okasaki's book). stm splits it into two TVar's I think for optimisation purposes, e.g. some operations will only need access one of the TVars which might change the contention in a parallel scenario - in io-sim we don't have any parallelism, so it's not a factor.

[coot]

One invariant that one might want to be able to verify is the number of elements in a queue (if the application has such an invariant). It will be impossible to write it with the proposed traceTQueueDefault.

[ch1bo]

Okay, let me try to write a flushTQueue which works on the single TVar.

I don't understand traceTQueueDefault and if you say we cannot implement it correctly for the standard double TVar implementation, I need to trust you.

But I do see the continued risk of maintaining a "differing" implementation on io-sim which does not correspond to the IO/STM variant semantics - if we could "just" keep lifted copies of the base and stm implementations around, that would be much more maintainable by casual contributors like me.

[ch1bo]

Addressed in ch1bo@9e2444d, but while doing so I discovered another bug (which underlines my worry of having non-standard implementation): #136

[abailly-iohk]

Would it not make sense to have an "equivalence property" written for all io-sim functions that "guarantees" the semantics is consistent with what's provided by the IO instance?

[coot]

@abailly-iohk that's a good idea.

[coot]

I created an issue for this: #137.

[coot]

I don't understand traceTQueueDefault and if you say we cannot implement it correctly for the standard double TVar implementation, I need to trust you.

Just for the sake of explanation:

traceTVar guarantees that its callback is called when the TVar is committed in an stm transaction and receives the current (and previous) data stored in the TVar. If TQueueDefault is using two TVars io-sim will need to know that not only the committed TVar matters but also the other one. That's the reason why two TVars are problematic.

traceTVar is designed for writing properties when order of events matters but one cannot relay on order of trace messages (i.e. in concurrent scenario order of trace messages will depend on the scheduler). traceTVar callbacks are guaranteed to be called right after an atomic transaction is committed in this since they do not depend on the scheduler. If you do readTVarIO >>= traceM . show, io-sim will deschedule the thread after readTVarIO and you're no longer guaranteed that multiple concurrent traceM calls will be done in the same order as the atomic transactions.

[ch1bo]

All comments addressed on this one @coot

[coot]

LGTM