Optimizations for mutable structures?

[Simon Marlow]

On 07 December 2005 15:21, Claus Reinke wrote:

>> (assuming 'acts' doesn't modify 'r').
> 
> this remark is the problem.
> 
>> No, Jan's transformation is correct even in a multithreaded setting.
>> It might eliminate some possible outcomes from a non-deterministic
>> program, but that's ok.  There's no requirement that all
>> interleavings according to the semantics have to be implemented. ..
> 
> not implementing traces promised as possible by the semantics is not
> a good idea, imho, as programmers have some control over the set of
> traces themselves.

It's unreasonable to expect an implementation to provide *all*
transitions specified by the semantics.  How could you tell, for one
thing?  For example, what if the compiler doesn't allow a context switch
between two adjacent operations:

    writeIORef r e
    x <- readIORef r 

this is a good example, in fact, because GHC will quite possibly compile
this code into a single basic block that doesn't allow a context switch
between the two statements.  However, the semantics certainly allows a
context switch between these two operations.  Is GHC wrong?  No way!  So
how do you specify which transitions an implementation must provide?
Perhaps there's a good formulation, but I don't know what it is.

> in this case, acts could implement the synchronisation with another
> thread working on r, ie., even if acts does not modify r itself, it
> might reliably cause another thread to modify r before acts can end.
> if such synchronisations depend on traces you have eliminated, the
> code 
> would just block (without apparent reason), whereas in this case, r
> will have a value after acts that shouldn't have been possible, due
> to the explicit synchronisation code (again, happy debugging) ..

I should have said that if 'acts' blocks, then the transformation is
invalid.  When I say "acts doesn't modify r", I mean to include all ways
of modifying r, including synchronising with another thread, or calling
an unknown function.

> of course, you could try to infer non-sequential interference with r
> resulting from act, but that is what Malcolm pointed out - you have
> to take the full semantics into account when doing such
> transformations (btw, java originally made a mess of this- hope that
> has been fixed by now). 

I don't think so.  Malcolm asserted that the transformation was invalid
in a multi-threaded implementation; I disagree - it's just as valid in a
multi-threaded implementation as a single-threaded one.  You don't have
to preserve non-deterministic interactions with other threads, because
they're non-deterministic!

Cheers,
	Simon