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