Skip to content
New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Unlikely but possible segfaults #15

Open
re-xyr opened this issue Feb 28, 2022 · 5 comments
Open

Unlikely but possible segfaults #15

re-xyr opened this issue Feb 28, 2022 · 5 comments

Comments

@re-xyr
Copy link
Owner

re-xyr commented Feb 28, 2022

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
Copy link
Owner Author

re-xyr commented Mar 1, 2022

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
Copy link
Owner Author

re-xyr commented Mar 1, 2022

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
Copy link
Owner Author

re-xyr commented Mar 1, 2022

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
Copy link
Owner Author

re-xyr commented Mar 2, 2022

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 re-xyr closed this as completed Mar 2, 2022
@re-xyr
Copy link
Owner Author

re-xyr commented Feb 7, 2023

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

@re-xyr re-xyr reopened this Feb 7, 2023
@re-xyr re-xyr mentioned this issue Feb 7, 2023
Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
None yet
Projects
None yet
Development

No branches or pull requests

1 participant