<div dir="ltr">Hi Ryan,<div><br></div><div>I have similar concerns with safety and STM.  In particular, lazy validation allows for execution after inconsistent reads from TVars.  The obvious problem to avoid is falling into an infinite loop.  As long as -fno-omit-yields is used (on every module?) and maybe some other conditions like eventually GC happens, the transaction will be validated and killed off. But other problems can happen.  Consider a transactional hash table with an array and some hashes already computed to be inside the array.  If an execution sees updated hashes, but not the updated array, then using unsafeRead could lead to a segfault.  I don't think this is completely obvious, especially when people will reach for STM precisely to avoid this sort of problem.  I worry about code that abstracts over mutable variables that work given sequential execution, but could fail with STM.  ByteString can lead to similar issues.  Data.ByteString.replicate can be asked to allocate very large pinned data leading to immediate heap overflow.  But if the request is from an inconsistent view of data it seams the programmer has already done their due diligence in preventing this from happening!</div><div><br></div><div>Anyway, I would like to work toward reasoning about these things more precisely.</div></div><div class="gmail_extra"><br><div class="gmail_quote">On Wed, Aug 10, 2016 at 10:23 AM, Ryan Newton <span dir="ltr"><<a href="mailto:rrnewton@gmail.com" target="_blank">rrnewton@gmail.com</a>></span> wrote:<br><blockquote class="gmail_quote" style="margin:0 0 0 .8ex;border-left:1px #ccc solid;padding-left:1ex"><div dir="ltr">Hi Edward,<div><br><div><div class="gmail_extra"><div class="gmail_quote"><span class="">On Tue, Aug 9, 2016 at 11:58 PM, Edward Kmett <span dir="ltr"><<a href="mailto:ekmett@gmail.com" target="_blank">ekmett@gmail.com</a>></span> wrote:<blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr">1.) If you remove IO from being able to be compiled inside Safe code _at all_ most packages I have that bother to expose Safe information will have to stop bothering. </div></blockquote><div><br></div></span><div>I definitely wouldn't argue for removing it entirely.  But it's good to know that there are instances where IO functions get mixed up in safe modules.  I'll try to systematically find all of these on hackage, but in the meantime do you have a sample list of modules?</div><div><br></div><div>My modest starting proposal is marking certain Foreign.* modules as Unsafe rather than Trustworthy.  We'll find all the modules affected.  But, again, are there any modules you know of offhand that are affected?  They should fall into two categories:</div><div><ol><li>Safe modules that must become Trustworthy (if they import Foreign bits, but don't expose the ability to corrupt memory to the clients of their APIs).</li><li>Safe modules that must become Unsafe or be split further into smaller modules.</li></ol></div><div>Obviously (2) is the biggest source of potential disruption. </div><div><br></div><div>I wouldn't ask anyone to accept a patch on GHC until we'd explored these impacts pretty thoroughly.</div><span class=""><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr">I'd have to cut up too many APIs into too many fine-grained pieces. </div></blockquote><div><br></div></span><div>Yeah, the module-level business is pretty annoying.  "vector' removed ".Safe" modules and no one has gotten around to adding the ".Unsafe".</div><span class=""><div> </div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>2.) Assuming instead that you're talking about a stronger-than-Safe additional language extension, say ReallySafe or SafeIO, it all comes down to what the user is allowed to do in IO, doesn't it? What effects are users granted access to? We don't have a very fine-grained system for IO-effect management, and it seems pretty much any choice you pick for what to put in the sandbox will be wrong for some users, so you'd need some sort of pragma for each IO operation saying what bins it falls into and to track that while type checking, etc. </div></div></blockquote><div><br></div></span><div>Well, <i>maybe</i> it is a slippery slope that leads to a full effect system.  But I'd like to see these issues enumerated.  Does memory safety as a goal really involve so many different effects?  Do you think there will be 1, 3, 10, or 100 things beyond Foreign.Ptr to worry about?  </div><span class=""><div><br></div><blockquote class="gmail_quote" style="margin:0px 0px 0px 0.8ex;border-left-width:1px;border-left-style:solid;border-left-color:rgb(204,204,204);padding-left:1ex"><div dir="ltr"><div>3.) On the other hand, someone could _build_ an effect system in Haskell that happens to sit on top of IO, holding effects in an HList, undischarged nullary class constraint, etc.</div></div></blockquote><div><br></div></span><div>Well, sure, I hope we will continue to aim for this as well.  This is effectively what we do with our "LVish" Par monad, where we use Safe Haskell to ensure users cannot break the effect system in -XSafe code.</div><div><br></div><div>Best, </div><span class="HOEnZb"><font color="#888888"><div> -Ryan</div></font></span></div></div></div></div></div>
<br>______________________________<wbr>_________________<br>
ghc-devs mailing list<br>
<a href="mailto:ghc-devs@haskell.org">ghc-devs@haskell.org</a><br>
<a href="http://mail.haskell.org/cgi-bin/mailman/listinfo/ghc-devs" rel="noreferrer" target="_blank">http://mail.haskell.org/cgi-<wbr>bin/mailman/listinfo/ghc-devs</a><br>
<br></blockquote></div><br></div>