Simon Marlow wrote: [snip]
Don't you run into a problem even if the two threads use the same ordering? Suppose
- thread 1 does the atomicModifyIORef, and gets preempted before doing the seq - thread 2 does its own atomicModifyIORef, and the seq. Thread 2 gets an inconsistent view of the IORefs.
No. At the time of the seq in thread 2, the thunk (call it Thunk 2) returned by the second atomicModifyIORef will refer to the thunk (Thunk 1) put in there by the first atomicModifyIORef. The seq will cause the unsafePerformIO from the second atomicModifyIORef to be evaluated. This will come to the "if" statement which will demand the value of Thunk 1. This will in turn provoke the evaluation of Thunk1. This will cause the action of thread 1's simpleToggle2 to be evaluated to completion.
Ok, so it relies crucially on the fact that the 'if' causes evaluation. (you might have written it to be more lazy, so that the pair was returned immediately without evaluating contents1 first, for example). In that case, yes I agree it is horrible :) Cheers, Simon
Simon Marlow wrote: [snip]
Ok, so it relies crucially on the fact that the 'if' causes evaluation. (you might have written it to be more lazy, so that the pair was returned immediately without evaluating contents1 first, for example).
In that case, yes I agree it is horrible :)
[snip] Flattery like that will get you nowhere. However in general I think we can hide some of the horribleness from the user: modify2IORefs :: IORef a -> IORef b -> (a -> b -> (a,b,c)) -> IO c modify2IORefs ioRefA ioRefB updateFn = do res <- atomicModifyIORef ioRefA (\ a0 -> unsafePerformIO (do atomicModifyIORef ioRefB (\ b0 -> let (a1,b1,c) = updateFn a0 b0 in a0 `seq` b0 `seq` (b1,(a1,c)) ) ) ) block (res `seq` return res) Modulo whatever stupid type errors I have made, I think this should provide a safe atomic update of two IORefs, except that you can get non-termination should you set up circular dependencies. However the latter problem (except that you will get deadlock) can occur if you try to write modify2MVars :: MVar a -> MVar b -> (a -> b -> (a,b,c)) -> IO c and are I fear unsolvable, without a global lock. I am not sure if all those seqs are necessary, but as Simon PJ would say, my brain is hurting.
However in general I think we can hide some of the horribleness from the user:
modify2IORefs :: IORef a -> IORef b -> (a -> b -> (a,b,c)) -> IO c [horrible code deleted]
And if they need to update 3 IORefs or a list of IORefs? Writing code like that yourself and getting it right and portable between compilers seems to be ludicrously hard. I can't tell if that code is right (my gut says no). Worse though, I don't even know what semantic framework to use to reason about it if we want to be sure the code will work in the presence of strictness analyzers, eager evaluation, parallel evaluation, fully-lazy evaluation, etc. Operational reasoning and reasoning by example struggle with such a task. -- Alastair
Alastair Reid wrote:
However in general I think we can hide some of the horribleness from the user:
modify2IORefs :: IORef a -> IORef b -> (a -> b -> (a,b,c)) -> IO c [horrible code deleted]
And if they need to update 3 IORefs or a list of IORefs?
It would be a fairly trivial matter to generalise the code I posted to such cases. But in my own experience three-way or multi-way synchronisations are only required very rarely. I have yet to come across a case where we needed them here at Bremen, and we do use concurrency an awful lot.
Writing code like that yourself and getting it right and portable between compilers seems to be ludicrously hard.
I can't tell if that code is right (my gut says no).
Well I'm afraid my gut disagrees. Also I think I've adequately addressed all the specific concerns raised so far.
Worse though, I don't even know what semantic framework to use to reason about it if we want to be sure the code will work in the presence of strictness analyzers, eager evaluation, parallel evaluation, fully-lazy evaluation, etc. Operational reasoning and reasoning by example struggle with such a task. Well I don't think we have a theoretical semantic framework for reasoning about most of the FFI, including especially unsafePerformIO. However the main assumption that is being made by the code I gave is that the thunks containing the unsafePerformIO's do not get multiply evaluated. I think this is a reasonable assumption to make. I am not scared by any of the buzzwords you give. For example, a strictness analyzer which wrongly attempted to evaluate the unsafePerformIO "inside the lock" and got into trouble as a result would in my opinion only have itself to blame. The same would apply to eager evaluation. For example, such methods might also get into trouble with the perfectly reasonable code:
x <- takeMVar y let z = seq x (error "Not to be evaluated") putMVar y z seq z since it would presumably raise an error prematurely when the MVar was empty. This is of course without any use of unsafePerformIO; one would expect eager evaluators/strictness evaluators to be especially careful about going round unsafePerformIO, if they did it at all. As for parallel evaluation I just don't see the problem, provided precautions are taken to make sure unsafePerformIO's are not multiply evaluated. I don't know what "fully-lazy evaluation" is, and how it differs from the normally lazy variety.
Worse though, I don't even know what semantic framework to use to reason about it if we want to be sure the code will work in the presence of strictness analyzers, eager evaluation, parallel evaluation, fully-lazy evaluation, etc. Operational reasoning and reasoning by example struggle with such a task.
However the main assumption that is being made by the code I gave is that the thunks containing the unsafePerformIO's do not get multiply evaluated. I think this is a reasonable assumption to make. I am not scared by any of the buzzwords you give.
The essence of all those is that they have been implemented for Haskell and that they either change evaluation order or increase or decrease the number of times expressions are evaluated. Most of them have non-local effects: by analyzing how a function is written, we can decide to treat the argument differently. The compiler can do this because the typesystem tells it the code is pure. Uses of unsafePerformIO may result in the typesystem saying something is pure when it is not but in those cases, the blame lies with the person who used unsafePerformIO for writing the code (that's part of the spec of unsafePerformIO). -- Alastair
participants (3)
-
Alastair Reid -
George Russell -
Simon Marlow