RE: Can strict ST break referential transparency?

[Simon Peyton Jones via ghc-devs]

If the conclusion is that there's a bug here, could someone distil the example 
into a ticket?

Thanks

Simon

| -Original Message-
| From: ghc-devs [mailto:ghc-devs-boun...@haskell.org] On Behalf Of Ben
| Gamari
| Sent: 23 November 2017 15:20
| To: Yuras Shumovich <shumovi...@gmail.com>; ghc-devs 
| Subject: Re: Can strict ST break referential transparency?
| 
| Yuras Shumovich <shumovi...@gmail.com> writes:
| 
| > Hello,
| >
| Hello,
| 
| Sorry for the late reply; this required a bit of reflection. The
| invariants surrounding the suspension of ST computations is a rather
| delicate and poorly documented area.
| 
| I believe the asynchronous exception case which you point out is
| precisely #13615. The solution there was, as David suggests, ensure that
| no resulting thunk could be entered more than once by a very strict
| blackholing protocol. Note that this isn't normal "eager" blackholing
| protocol, which still might allow multiple entrancy. It's rather a more
| strict variant, requiring two atomic operations.
| 
| I can't be certain that there aren't more cases like this, but I suspect
| not since most asynchronous suspensions where the resulting thunk might
| "leak" back into the program go through the raiseAsync codepath that was
| fixed in #13615.
| 
| Cheers,
| 
| - ben

___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Can strict ST break referential transparency?

[Yuras Shumovich]

So my theory is correct, but it is already fixed in 8.2. Nice!

Thank you for clarification!

Yuras.

23-11-2017, Чцв а 10:20 -0500, Ben Gamari напісаў:
> Yuras Shumovich  writes:
> 
> > Hello,
> > 
> 
> Hello,
> 
> Sorry for the late reply; this required a bit of reflection. The
> invariants surrounding the suspension of ST computations is a rather
> delicate and poorly documented area.
> 
> I believe the asynchronous exception case which you point out is
> precisely #13615. The solution there was, as David suggests, ensure
> that
> no resulting thunk could be entered more than once by a very strict
> blackholing protocol. Note that this isn't normal "eager" blackholing
> protocol, which still might allow multiple entrancy. It's rather a
> more
> strict variant, requiring two atomic operations.
> 
> I can't be certain that there aren't more cases like this, but I
> suspect
> not since most asynchronous suspensions where the resulting thunk
> might
> "leak" back into the program go through the raiseAsync codepath that
> was
> fixed in #13615.
> 
> Cheers,
> 
> - ben
> 
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Can strict ST break referential transparency?

[Yuras Shumovich]

22-11-2017, Срд а 15:37 -0500, David Feuer напісаў:
> If there is indeed a problem, I suspect the right way to fix it is to
> make sure that no partially evaluated thunk is ever resumed twice.
> Inter-thread exceptions are presumably rare enough that we don't have
> to worry *too* much about their cost.

Sounds reasonable. But probably it already works that way? Though it
doesn't seem to be covered in the papers, and looks like nobody knows
an answer to my question. It makes me worry a bit.

On the other hand, right now resuming frozen thunk usually
crashes/hangs as discovered in #14497. Nobody noticed that so far in
the wild, so probably the subject is just a dark corner case, not worse
the efforts.

> 
> 
> David FeuerWell-Typed, LLP
>  Original message From: Yuras Shumovich  mail.com> Date: 11/21/17  12:43 PM  (GMT-05:00) To: ghc-devs  s...@haskell.org> Subject: Can strict ST break referential
> transparency? 
> 
> Hello,
> 
> I was evaluating a possibility that linear types can break
> referential
> transparency [1], exactly like lazy ST [2].
> 
> But on the way I realized that even strict ST may suffer from the
> same
> issue. If ST computation is interrupted by e.g. async exception,
> runtime will "freeze" it at the point where it was interrupted [3].
> 
> So the question: is the "freezed" computation just a normal thunk?
> Note
> that the runtime doesn't guarantee that a thunk will be evaluated
> only
> once [4]. If the "freezed" thunk captures e.g. STRef, and will be
> evaluated twice, its effect could become observable from outside,
> just
> like in case of lazy ST.
> 
> I tried to check the theory by stress testing RTS. Unfortunately I
> immediately discovered a runtime crash [5], which is probably not
> related to my question.
> 
> Hope someone will be able to clarify things for me.
> 
> Thanks,
> Yuras.
> 
> [1] https://github.com/ghc-proposals/ghc-proposals/pull/91#issuecomme
> nt
> -345553071
> [2] https://ghc.haskell.org/trac/ghc/ticket/14497
> [3] See section 8 there: https://www.microsoft.com/en-us/research/wp-
> co
> ntent/uploads/2016/07/asynch-exns.pdf
> [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2005/
> 09
> /2005-haskell.pdf
> [5] https://ghc.haskell.org/trac/ghc/ticket/14497
> ___
> ghc-devs mailing list
> ghc-devs@haskell.org
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Can strict ST break referential transparency?

[David Feuer]

If there is indeed a problem, I suspect the right way to fix it is to make sure 
that no partially evaluated thunk is ever resumed twice. Inter-thread 
exceptions are presumably rare enough that we don't have to worry *too* much 
about their cost.


David FeuerWell-Typed, LLP
 Original message From: Yuras Shumovich  
Date: 11/21/17  12:43 PM  (GMT-05:00) To: ghc-devs  
Subject: Can strict ST break referential transparency? 

Hello,

I was evaluating a possibility that linear types can break referential
transparency [1], exactly like lazy ST [2].

But on the way I realized that even strict ST may suffer from the same
issue. If ST computation is interrupted by e.g. async exception,
runtime will "freeze" it at the point where it was interrupted [3].

So the question: is the "freezed" computation just a normal thunk? Note
that the runtime doesn't guarantee that a thunk will be evaluated only
once [4]. If the "freezed" thunk captures e.g. STRef, and will be
evaluated twice, its effect could become observable from outside, just
like in case of lazy ST.

I tried to check the theory by stress testing RTS. Unfortunately I
immediately discovered a runtime crash [5], which is probably not
related to my question.

Hope someone will be able to clarify things for me.

Thanks,
Yuras.

[1] https://github.com/ghc-proposals/ghc-proposals/pull/91#issuecomment
-345553071
[2] https://ghc.haskell.org/trac/ghc/ticket/14497
[3] See section 8 there: https://www.microsoft.com/en-us/research/wp-co
ntent/uploads/2016/07/asynch-exns.pdf
[4] https://www.microsoft.com/en-us/research/wp-content/uploads/2005/09
/2005-haskell.pdf
[5] https://ghc.haskell.org/trac/ghc/ticket/14497
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

Re: Can strict ST break referential transparency?

[Yuras Shumovich]

Sorry, link [2] meant to be
https://ghc.haskell.org/trac/ghc/ticket/11760

21-11-2017, Аўт а 20:43 +0300, Yuras Shumovich напісаў:
> Hello,
> 
> I was evaluating a possibility that linear types can break
> referential
> transparency [1], exactly like lazy ST [2].
> 
> But on the way I realized that even strict ST may suffer from the
> same
> issue. If ST computation is interrupted by e.g. async exception,
> runtime will "freeze" it at the point where it was interrupted [3].
> 
> So the question: is the "freezed" computation just a normal thunk?
> Note
> that the runtime doesn't guarantee that a thunk will be evaluated
> only
> once [4]. If the "freezed" thunk captures e.g. STRef, and will be
> evaluated twice, its effect could become observable from outside,
> just
> like in case of lazy ST.
> 
> I tried to check the theory by stress testing RTS. Unfortunately I
> immediately discovered a runtime crash [5], which is probably not
> related to my question.
> 
> Hope someone will be able to clarify things for me.
> 
> Thanks,
> Yuras.
> 
> [1] https://github.com/ghc-proposals/ghc-proposals/pull/91#issuecomme
> nt
> -345553071
> [2] https://ghc.haskell.org/trac/ghc/ticket/14497
> [3] See section 8 there: https://www.microsoft.com/en-us/research/wp-
> co
> ntent/uploads/2016/07/asynch-exns.pdf
> [4] https://www.microsoft.com/en-us/research/wp-content/uploads/2005/
> 09
> /2005-haskell.pdf
> [5] https://ghc.haskell.org/trac/ghc/ticket/14497
___
ghc-devs mailing list
ghc-devs@haskell.org
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs