Can strict ST break referential transparency?

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

Can strict ST break referential transparency?

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#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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Can strict ST break referential transparency?

David Feuer-2
In reply to this post by Yuras Shumovich
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 Feuer
Well-Typed, LLP

-------- Original message --------
From: Yuras Shumovich <[hidden email]>
Date: 11/21/17 12:43 PM (GMT-05:00)
To: ghc-devs <[hidden email]>
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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Can strict ST break referential transparency?

Yuras Shumovich
In reply to this post by 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 <shumovichy@g
> mail.com> Date: 11/21/17  12:43 PM  (GMT-05:00) To: ghc-devs <ghc-dev
> [hidden email]> 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
> [hidden email]
> http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
_______________________________________________
ghc-devs mailing list
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

Re: Can strict ST break referential transparency?

Ben Gamari-2
In reply to this post by Yuras Shumovich
Yuras Shumovich <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs

signature.asc (497 bytes) Download Attachment
Reply | Threaded
Open this post in threaded view
|

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 <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs
Reply | Threaded
Open this post in threaded view
|

RE: Can strict ST break referential transparency?

GHC - devs mailing list
In reply to this post by Ben Gamari-2
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:[hidden email]] On Behalf Of Ben
| Gamari
| Sent: 23 November 2017 15:20
| To: Yuras Shumovich <[hidden email]>; ghc-devs <ghc-
| [hidden email]>
| Subject: Re: Can strict ST break referential transparency?
|
| Yuras Shumovich <[hidden email]> 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
[hidden email]
http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs