Could Data.Vault be used for mutable variables?

[barrucadu]

Currently, IORef or STRef is used as the backing store for CRef, MVar, and TVar during test execution. The values containing the rest of the state are not sufficient to exactly reproduce the current state, due to this underlying use of mutable variables.

Data.Vault is a type-safe heterogeneous map. Could it be used to make self-contained states? This would allow, for instance, storing these states as normal data and even rewinding an execution.

If a trace of states could be produced, it might be possible to greatly speed up the SCT implementation by not needing to re-execute common prefixes. The state immediately before the point of divergence is just resumed, with a new scheduler.

Some thoughts:

• Data.Vault does use mutability, to create the keys. Variables in the user program would just store a key. If a state is resumed, all non-garbage keys must be valid.
• We can't access the garbage collector, so we might keep keys in a vault longer than necessary, as we can never assume that a key is garbage.
• The obvious downside is that this would use more memory, probably making #64 even more important.

[barrucadu]

Note: SCT is sometimes called stateless model checking precisely because it doesn't keep these potentially very large states.

That doesn't mean having the option is inherently bad though.

[barrucadu]

The heap branch has an implementation of using Data.Vault for storing all mutable variables, though it doesn't expose these in the trace. This is a breaking change, and needs tidying up before putting in to next-major. Profiling results of dejafu-tests on my VPS:

master:

        total time  =      144.69 secs   (144693 ticks @ 1000 us, 1 processor)
        total alloc = 57,918,052,040 bytes  (excludes profiling overheads)

heap:

        total time  =      147.33 secs   (147333 ticks @ 1000 us, 1 processor)
        total alloc = 58,179,981,968 bytes  (excludes profiling overheads)

[barrucadu]

Answer: it could, but it makes the types more complicated and doesn't really gain us anything.