cleff icon indicating copy to clipboard operation
cleff copied to clipboard

Unlikely but possible segfaults

Open re-xyr opened this issue 4 years ago • 5 comments

If we return a toEff'd action directly out of an interpreter, such as something like this:

type SomeEs = ...

data Evil :: Effect where
  Evil :: m a -> Evil m a (Eff SomeEs)

runEvil :: Eff (Evil ': SomeEs) ~> Evil SomeEs
runEvil = interpret \case
  Evil m -> pure $ toEff m

and then run the returned action with another different Env, then the es that toEff gets will no longer be an updated version of ess but a completely different one, and this mismatch can lead to a segfault.

This is bad (similar root cause to hasura/eff#13) but not as devastating, nor is it as serious as #5, as we do not support coroutine and therefore have little to no reasonable use of passing effect actions out of scope, so people likely won't do that at all. (not to mention only fixed effect stacks can be used, otherwise the returned stack is existential and nothing can be done with it)

The short term solution will be to add warnings to the docs of all HO interpretation combinators; but we still need to investigate if we can rule these cases out for good (which may involve another API overhaul and painstaking performance tuning).

re-xyr avatar Feb 28 '22 15:02 re-xyr

One option is to use ST-like threads to avoid instantiating a computation with an existential (instead of universal) thread - but that involves adding a type parameter to literally all of the API (including the Eff monad itself), so we can't possibly use that without scaring people away.

re-xyr avatar Mar 01 '22 01:03 re-xyr

Another choice is to add some Opaque type to the top of the effect stack in handlers - but that has its own issue like 1) needing to rely on incoherent instances, and 2) not good ergonomics sometimes because we cannot auto lift es into Opaque : es.

re-xyr avatar Mar 01 '22 08:03 re-xyr

There are ways to partially address this in runtime:

  • create a "pid" for each emptyEnv so that only Envs with same pids can update each other
    • This is not enough, as this does not prevent older Envs update newer Envs with the same pid, which can still segfault
  • also compare the next address to allocate between Envs
    • This is still not enough, because of the presence of multithreading - which means it's possible that neither of two Envs on the same pid are another's subset

They can rule out some cases (which are extremely rare!) but also has a toll on performance so I'm inclined not to implement it until someone actually tries to do so and ran into segfaults.

re-xyr avatar Mar 01 '22 15:03 re-xyr

I'm closing this because I think this is a problem that is fundamental in theory but insignificant in practice. Similar to hasura/eff#13, the conclusion I arrived at is that it is impossible to have sound semantics for captured continuations that went out of the handler scope given the current standard of expressiveness, ergonomics and performance I have on this library.

Generally, the behavior described in this issue is very easy to avoid: just don't treat captured continuations as first-class data. Treat them like computations that can only be embedded in the current handler context, instead of being returned, or even crazier, be put in IORefs or MVars. Honestly, nobody will ever do that.

The most plausible solution to me, for now, is the Opaque type, but even that harms (mostly) performance and (slightly) ergonomics, without obvious improvements in terms of user experience. My opinion is that it's just not worth it to patch a practically impossible unsoundness with such effort and cost.

re-xyr avatar Mar 02 '22 14:03 re-xyr

We should come up with a fix of this as per Sp.

re-xyr avatar Feb 07 '23 08:02 re-xyr