Annotation to assert no GC run (allocation?) in a function

Ecosystem
,
1

I was wondering:

  1. Would it be possible to have some sort of annotation to assert that a GC will not run in some function, or block, of code?
  2. Would that be useful?

There are is various bits of knowledge about how to construct a bit of code to not allocate, and thus no GC occur. But accomplishing this seems to rely on understanding the underlying runtime pretty well. Additionally, it seems hard to know if you’ve done it right. And if someone less experienced comes along to make a change, they could accidentally add an allocation.

3 Likes
2

One way is to dynamically measure that in tests and use something like require_no_allocation from the JS libs.

1 Like
3

An annotation that just omits running GC (by assuming allocations don’t happen) or an annotation that actually proves that no allocation happens?

The former sounds overly dangerous: if that less experienced someone makes a change in such annotated code and introduces an allocation, then you’re still screwed (in the worst case).

The latter sounds overly difficult: to prove that you need to know that every (transitively) called function in however far library doesn’t allocate, which requires whole-program analysis.

1 Like
4

I am thinking the latter. A lot of useful optimizations are difficult for a compiler to write but easy (easier?) to verify. I think things like these where you’re trying to coerce the runtime to do the thing in the way you want might have good opportunities to assert behaviour to help the developer achieve it.

1 Like
5

Those is something we’re working on internally, and hope to have an internal release of in the next couple of weeks. I agree this would be very valuable upstream, though it’s even better in combination with support for stack allocation, which for now is only on our branch.

Happy to report more news on this when we have it.

7 Likes
6

Wow that sounds awesome! I hope it makes it upstream!

2 Likes
7

There’s actually an annotation [@poll error] we added after poll points that will cause a compile error if the annotated function includes a poll/allocation (that is something that could lead to a GC) or calls to OCaml/C functions that could allocate. It may do what you want. There’s some examples in the merged PR: https://github.com/ocaml/ocaml/pull/10462

I’ve added myself a TODO to actually add it to the manual…

2 Likes