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

On MacOS, lablgtk2 runs OCaml code inside a blocking section, causing a crash in caml_memprof_handle_postponed_exn #141

Closed
btj opened this issue Nov 13, 2021 · 1 comment · Fixed by verifast/vfdeps#2

Comments

@btj
Copy link
Contributor

btj commented Nov 13, 2021

Since recently, I am seeing my VeriFast application (using lablgtk2) crash sometimes on MacOS in caml_memprof_handle_postponed_exn. See verifast/verifast#252 .

The chain of events is as follows:

  • In ml_poll
    static gint ml_poll (GPollFD *ufds, guint nfsd, gint timeout)
    , lablgtk calls caml_enter_blocking_section and then calls the Gdk Quartz default poll_func https://gitlab.gnome.org/GNOME/gtk/-/blob/2.24.33/gdk/quartz/gdkeventloop-quartz.c#L709
  • It calls AppKit's nextEventMatchingMask with the NSDefaultRunLoopMode.
  • Apparently, in this mode, the run loop dispatches paint events. lablgtk (correctly, I think) does not expect this. The paint event is dispatched into OCaml code, which is not allowed inside a blocking section.

So, while I believe lablgtk is not "to blame" for this bug, any help or advice would of course be appreciated.

One (hacky) solution would be to add code to marshal to check if we are in a blocking section and, if so, temporarily exit it. Would that make sense?

I am curious as to why I am seeing these crashes only now. One recent change is that I recently switched from OCaml 4.6 to OCaml 4.13. Perhaps 4.13 is more sensitive to calling into OCaml while inside a blocking section?

@btj
Copy link
Contributor Author

btj commented Nov 13, 2021

I just realized that this bug could cause not just crashes, but data races as well, in multithreaded programs. (VeriFast is not multithreaded but there may be multithreaded lablgtk2 apps out there.)

@btj btj changed the title lablgtk2 on MacOS: crash in caml_memprof_handle_postponed_exn On MacOS, lablgtk2 runs OCaml code inside a blocking section, causing a crash in caml_memprof_handle_postponed_exn Nov 13, 2021
btj added a commit to verifast/vfdeps that referenced this issue Nov 17, 2021
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

Successfully merging a pull request may close this issue.

1 participant