oleg | 12 Apr 10:24 2013

unsafeInterleaveST (and IO) is really unsafe


Timon Gehr wrote:
> I am not sure that the two statements are equivalent. Above you say that
> the context distinguishes x == y from y == x and below you say that it
> distinguishes them in one possible run.

I guess this is a terminological problem. The phrase `context
distinguishes e1 and e2' is the standard phrase in theory of
contextual equivalence. Here are the nice slides
        http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf

Please see adequacy on slide 17. An expression relation between two
boolean expressions M1 and M2 is adequate if for all program runs (for
all initial states of the program s), M1
evaluates to true just in case M2 does. If in some circumstances M1
evaluates to true but M2 (with the same initial state) evaluates to
false, the expressions are not related or the expression relation is
inadequate.

See also the classic
        http://www.ccs.neu.edu/racket/pubs/scp91-felleisen.ps.gz
(p11 for definition and Theorem 3.8 for an example of a
distinguishing, or witnessing context).

> In essence, lazy IO provides unsafe constructs that are not named
> accordingly. (But IO is problematic in any case, partly because it
> depends on an ideal program being run on a real machine which is based
> on a less general model of computation.)

I'd agree with the first sentence. As for the second sentence, all
(Continue reading)

Timon Gehr | 13 Apr 00:37 2013
Picon
Picon

Re: unsafeInterleaveST (and IO) is really unsafe

On 04/12/2013 10:24 AM, oleg <at> okmij.org wrote:
>
> Timon Gehr wrote:
>> I am not sure that the two statements are equivalent. Above you say that
>> the context distinguishes x == y from y == x and below you say that it
>> distinguishes them in one possible run.
>
> I guess this is a terminological problem.

It likely is.

> The phrase `context
> distinguishes e1 and e2' is the standard phrase in theory of
> contextual equivalence. Here are the nice slides
>          http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf
>

The only occurrence of 'distinguish' is in the Leibniz citation.

> Please see adequacy on slide 17. An expression relation between two
> boolean expressions M1 and M2 is adequate if for all program runs (for
> all initial states of the program s), M1
> evaluates to true just in case M2 does. If in some circumstances M1
> evaluates to true but M2 (with the same initial state) evaluates to
> false, the expressions are not related or the expression relation is
> inadequate.
>

In my mind, 'evaluates-to' is an existential statement. The adequacy 
notion given there is inadequate if the program execution is 
(Continue reading)

David Sabel | 15 Apr 20:44 2013
Picon
Picon

Re: unsafeInterleaveST (and IO) is really unsafe


Am 13.04.2013 00:37, schrieb Timon Gehr:
> On 04/12/2013 10:24 AM, oleg <at> okmij.org wrote:
>>
>> Timon Gehr wrote:
>>> I am not sure that the two statements are equivalent. Above you say 
>>> that
>>> the context distinguishes x == y from y == x and below you say that it
>>> distinguishes them in one possible run.
>>
>> I guess this is a terminological problem.
>
> It likely is.
>
>> The phrase `context
>> distinguishes e1 and e2' is the standard phrase in theory of
>> contextual equivalence. Here are the nice slides
>> http://www.cl.cam.ac.uk/teaching/0910/L16/semhl-15-ann.pdf
>>
>
> The only occurrence of 'distinguish' is in the Leibniz citation.
>
>> Please see adequacy on slide 17. An expression relation between two
>> boolean expressions M1 and M2 is adequate if for all program runs (for
>> all initial states of the program s), M1
>> evaluates to true just in case M2 does. If in some circumstances M1
>> evaluates to true but M2 (with the same initial state) evaluates to
>> false, the expressions are not related or the expression relation is
>> inadequate.
>>
(Continue reading)

Duncan Coutts | 18 Apr 15:17 2013

Re: unsafeInterleaveST (and IO) is really unsafe

On Mon, 2013-04-15 at 20:44 +0200, David Sabel wrote:

> A very interesting discussion,  I may add my 2 cents:
>     making unsafeInterleaveIO nondeterministic indeed seems to make it safe,
>     more or less this was proved in our paper:
> 
> http://www.ki.informatik.uni-frankfurt.de/papers/sabel/chf-conservative-lics.pdf
> slides: 
> http://www.ki.informatik.uni-frankfurt.de/persons/sabel/chf-conservative.pdf
> 
> there we proposed an extension to Concurrent Haskell which adds a primitive
> 
> future :: IO a -> IO a
> 
> Roughly speaking future is like unsafeInterleaveIO, but creates a new 
> concurrent thread
> to compute the result of the IO-action interleaved without any fixed order.

That's very interesting to hear. It has always been my intuition that
the right way to understand unsafeInterleaveIO is using a concurrency
semantics (with a demonic scheduler). And whenever this
"unsafeInterleaveIO is unsound" issue comes up, that's the argument I
make to whoever will listen! ;-)

That intuition goes some way to explain why unsafeInterleaveIO is fine
but unsafeInterleaveST is right out: ST is supposed to be deterministic,
but IO can be non-deterministic.

> We have shown that adding this primitive to the functional core language 
> is 'safe' in the sense
(Continue reading)

David Sabel | 18 Apr 20:32 2013
Picon
Picon

Re: unsafeInterleaveST (and IO) is really unsafe

Am 18.04.2013 15:17, schrieb Duncan Coutts:
> On Mon, 2013-04-15 at 20:44 +0200, David Sabel wrote:
>
>> A very interesting discussion,  I may add my 2 cents:
>>      making unsafeInterleaveIO nondeterministic indeed seems to make it safe,
>>      more or less this was proved in our paper:
>>
>> http://www.ki.informatik.uni-frankfurt.de/papers/sabel/chf-conservative-lics.pdf
>> slides:
>> http://www.ki.informatik.uni-frankfurt.de/persons/sabel/chf-conservative.pdf
>>
>> there we proposed an extension to Concurrent Haskell which adds a primitive
>>
>> future :: IO a -> IO a
>>
>> Roughly speaking future is like unsafeInterleaveIO, but creates a new
>> concurrent thread
>> to compute the result of the IO-action interleaved without any fixed order.
> That's very interesting to hear. It has always been my intuition that
> the right way to understand unsafeInterleaveIO is using a concurrency
> semantics (with a demonic scheduler). And whenever this
> "unsafeInterleaveIO is unsound" issue comes up, that's the argument I
> make to whoever will listen! ;-)
>
> That intuition goes some way to explain why unsafeInterleaveIO is fine
> but unsafeInterleaveST is right out: ST is supposed to be deterministic,
> but IO can be non-deterministic.
I agree.
>
>> We have shown that adding this primitive to the functional core language
(Continue reading)

Alexander Solla | 19 Apr 19:24 2013
Picon

Re: unsafeInterleaveST (and IO) is really unsafe




On Fri, Apr 12, 2013 at 3:37 PM, Timon Gehr <timon.gehr <at> gmx.ch> wrote:

Please see Sec
10.2 Unique supply trees -- you might see some familiar code. Although
my example was derived independently, it has the same kernel of
badness as the example in Launchbury and Peyton-Jones. The authors
point out a subtlety in the code, admitting that they fell into the
trap themselves.

They informally note that the final result depends on the order of evaluation and is therefore not always uniquely determined. (because the order of evaluation is only loosely specified.)

If the final result depends on the order of evaluation, then the context in which the result is defined is not referentially transparent.  If a context is referentially opaque, then equational reasoning "can fail" -- i.e., it is no longer a valid technique of analysis, since the axioms on which it depends are no longer satisfied: 

"It is necessary that four and four is eight"

"The number of planets is eight"

does not imply

"It is necessary that the number of planets is eight", as "equational reasoning" (or, better put, "substitution of equals", the first order axiom for equality witnessing Leibniz equality) requires.

In particular, quotation marks, necessity, and unsafeInterleaveST are referentially opaque contexts.
_______________________________________________
Haskell-Cafe mailing list
Haskell-Cafe <at> haskell.org
http://www.haskell.org/mailman/listinfo/haskell-cafe

Gmane