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
_______________________________________________
Glasgow-haskell-users mailing list
Glasgow-haskell-users@haskell.org
http://www.haskell.org/mailman/listinfo/glasgow-haskell-users
