unsafeInterleaveST (and IO) is really unsafe

Previous Topic Next Topic
 
classic Classic list List threaded Threaded
6 messages Options
Reply | Threaded
Open this post in threaded view
|

unsafeInterleaveST (and IO) is really unsafe

oleg-30

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
real programs are real programs executing on real machines. We may
equationally prove (at time Integer) that
        1 + 2^100000 == 2^100000 + 1
but we may have trouble verifying it in Haskell (or any other
language). That does not mean equational reasoning is useless: we just
have to precisely specify the abstraction boundaries. BTW, the
equality above is still useful even in Haskell: it says that if the
program managed to compute 1 + 2^100000 and it also managed to compute
2^100000 + 1, the results must be the same. (Of course in the above
example, the program will probably crash in both cases).  What is not
adequate is when equational theory predicts one finite result, and the
program gives another finite result -- even if the conditions of
abstractions are satisfied (e.g., there is no IO, the expression in
question has a pure type, etc).

> I think this context cannot be used to reliably distinguish x == y and y
> == x. Rather, the outcomes would be arbitrary/implementation
> defined/undefined in both cases.

My example uses the ST monad for a reason: there is a formal semantics
of ST (denotational in Launchbury and Peyton-Jones and operational in
Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury
and Peyton-Jones. The semantics is explained in Sec 6. 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. So, unsafeInterleaveST is really bad -- and the
people who introduced it know that, all too well.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: unsafeInterleaveST (and IO) is really unsafe

Timon Gehr
On 04/12/2013 10:24 AM, [hidden email] 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
indeterministic, as I would have expected it to be in this case. (They
quickly note this on slide 18, giving concurrency features as an example.)

> 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).
>

Thanks for the pointer, I will have a look. However, it seems that the
semantics the definition and the proof rely on are deterministic?

>> 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
> real programs are real programs executing on real machines. We may
> equationally prove (at time Integer) that
>          1 + 2^100000 == 2^100000 + 1
> but we may have trouble verifying it in Haskell (or any other
> language). That does not mean equational reasoning is useless: we just
> have to precisely specify the abstraction boundaries.

Which is really hard. I think equational reasoning is helpful because it
is valid for ideal programs and it seems therefore to be a good
heuristic for real ones.

> BTW, the
> equality above is still useful even in Haskell: it says that if the
> program managed to compute 1 + 2^100000 and it also managed to compute
> 2^100000 + 1, the results must be the same. (Of course in the above
> example, the program will probably crash in both cases).  What is not
> adequate is when equational theory predicts one finite result, and the
> program gives another finite result -- even if the conditions of
> abstractions are satisfied (e.g., there is no IO, the expression in
> question has a pure type, etc).
>

The abstraction bound is where exact reasoning necessarily stops.

>> I think this context cannot be used to reliably distinguish x == y and y
>> == x. Rather, the outcomes would be arbitrary/implementation
>> defined/undefined in both cases.
>
> My example uses the ST monad for a reason: there is a formal semantics
> of ST (denotational in Launchbury and Peyton-Jones and operational in
> Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury
> and Peyton-Jones. The semantics is explained in Sec 6.

InterleaveST is first referred to in chapter 10. As far as I can tell,
the construct does not have specified a formal semantics.

> 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.)

> So, unsafeInterleaveST is really bad -- and the
> people who introduced it know that, all too well.
>

I certainly do not disagree that it is bad. However, I am still not
convinced that the example actually shows a violation of equational
reasoning. The valid outputs, according to the informal specification in
chapter 10, are the same for both expressions.


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: unsafeInterleaveST (and IO) is really unsafe

David Sabel

Am 13.04.2013 00:37, schrieb Timon Gehr:

> On 04/12/2013 10:24 AM, [hidden email] 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
> indeterministic, as I would have expected it to be in this case. (They
> quickly note this on slide 18, giving concurrency features as an
> example.)
>
>> 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).
>>
>
> Thanks for the pointer, I will have a look. However, it seems that the
> semantics the definition and the proof rely on are deterministic?
>
>>> 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
>> real programs are real programs executing on real machines. We may
>> equationally prove (at time Integer) that
>>          1 + 2^100000 == 2^100000 + 1
>> but we may have trouble verifying it in Haskell (or any other
>> language). That does not mean equational reasoning is useless: we just
>> have to precisely specify the abstraction boundaries.
>
> Which is really hard. I think equational reasoning is helpful because
> it is valid for ideal programs and it seems therefore to be a good
> heuristic for real ones.
>
>> BTW, the
>> equality above is still useful even in Haskell: it says that if the
>> program managed to compute 1 + 2^100000 and it also managed to compute
>> 2^100000 + 1, the results must be the same. (Of course in the above
>> example, the program will probably crash in both cases).  What is not
>> adequate is when equational theory predicts one finite result, and the
>> program gives another finite result -- even if the conditions of
>> abstractions are satisfied (e.g., there is no IO, the expression in
>> question has a pure type, etc).
>>
>
> The abstraction bound is where exact reasoning necessarily stops.
>
>>> I think this context cannot be used to reliably distinguish x == y
>>> and y
>>> == x. Rather, the outcomes would be arbitrary/implementation
>>> defined/undefined in both cases.
>>
>> My example uses the ST monad for a reason: there is a formal semantics
>> of ST (denotational in Launchbury and Peyton-Jones and operational in
>> Moggi and Sabry). Please look up ``State in Haskell'' by Launchbury
>> and Peyton-Jones. The semantics is explained in Sec 6.
>
> InterleaveST is first referred to in chapter 10. As far as I can tell,
> the construct does not have specified a formal semantics.
>
>> 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.)
>
>> So, unsafeInterleaveST is really bad -- and the
>> people who introduced it know that, all too well.
>>
>
> I certainly do not disagree that it is bad. However, I am still not
> convinced that the example actually shows a violation of equational
> reasoning. The valid outputs, according to the informal specification
> in chapter 10, are the same for both expressions.
>
>
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.

We have shown that adding this primitive to the functional core language
is 'safe' in the sense
that all program equations of the pure language still hold in the
extended language
(which we call a conservative extension in the above paper)

The used equality is contextual equivalence
(with may- and a variant of must-convergence in the concurrent case).

We also showed that adding unsafeInterleaveIO (called lazy futures in
the paper..)
- which delays until its result is demanded - breaks this conservativity,
since the order of evaluation can be observed.

Best wishes,
  David





_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: unsafeInterleaveST (and IO) is really unsafe

Duncan Coutts-4
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
> that all program equations of the pure language still hold in the
> extended language
> (which we call a conservative extension in the above paper)
>
> The used equality is contextual equivalence
> (with may- and a variant of must-convergence in the concurrent case).

Ok.

> We also showed that adding unsafeInterleaveIO (called lazy futures in
> the paper..)
> - which delays until its result is demanded - breaks this conservativity,
> since the order of evaluation can be observed.

My conjecture is that with a concurrent semantics with a demonic
scheduler then unsafeInterleaveIO is still fine, essentially because the
semantics would not distinguish it from your 'future' primitive. That
said, it might not be such a useful semantics because we often want the
lazy behaviour of a lazy future.

Duncan


_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: unsafeInterleaveST (and IO) is really unsafe

David Sabel
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
>> is 'safe' in the sense
>> that all program equations of the pure language still hold in the
>> extended language
>> (which we call a conservative extension in the above paper)
>>
>> The used equality is contextual equivalence
>> (with may- and a variant of must-convergence in the concurrent case).
> Ok.
>
>> We also showed that adding unsafeInterleaveIO (called lazy futures in
>> the paper..)
>> - which delays until its result is demanded - breaks this conservativity,
>> since the order of evaluation can be observed.
> My conjecture is that with a concurrent semantics with a demonic
> scheduler then unsafeInterleaveIO is still fine, essentially because the
> semantics would not distinguish it from your 'future' primitive.
Yes our result should  hold for any scheduling.

> That
> said, it might not be such a useful semantics because we often want the
> lazy behaviour of a lazy future.
Yes I agree with that, too.

Best wishes,
  David

_______________________________________________
Haskell-Cafe mailing list
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe
Reply | Threaded
Open this post in threaded view
|

Re: unsafeInterleaveST (and IO) is really unsafe

Alexander Solla
In reply to this post by Timon Gehr



On Fri, Apr 12, 2013 at 3:37 PM, Timon Gehr <[hidden email]> 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
[hidden email]
http://www.haskell.org/mailman/listinfo/haskell-cafe