Touring the Living Library

Hi there,

Based on my previous blog post, I’ve decided to go ahead and try my hand at fixing the lifetime issues I’ve been having with Ctypes. This will be dog-fooded into my own Godotcaml library — which is still coming along, by the way! Basically I had to take this detour because I was getting segfaults due to lifetime issues when dealing with Godot Signals and Callables. This new library is called living, and can be found here.

I give a brief overview of the library in its current form, and specifically the guarantees it intends to give (and which it can’t give, with discussion on what language and library features might help). This blog post will likely be of interest to anyone who has to interface the OCaml garbage collector with some external resource (such as foreign memory!).

Definition of Soundness

We define the use of the Ctypes FFI to be sound when:

1. There are no use-after-free errors, and
2. There are no double-free errors, and
3. These are true no matter when the garbage collector runs.

In particular, we make no mention of dereferencing of null pointers, use of uninitialized memory, or screwing up the bounds of an array. These are problems that are outside the scope of the living library to solve.

Definition of Proper Dependence

We now turn to lifetimes. Rust afficionados will be well aware of the concepts here.

Consider two values, p and q. We say p depends on q if the lifetime of q must exceed that of p, for whatever reason. We write this as p => q, which should be read as “if p is alive, so too much be q”. This relation is trivially reflexive and transitive. In an FFI, this can happen a number of ways:

1. q is a struct or pointer to struct and p points to some field of q.
2. q is an array and p is a pointer to the nth element of that array.
3. More generally, q is a “thing” and p is a pointer into that “thing”.

In each of these cases, it would be disasterous if q were freed and then p was dereferenced. Such a bug we classify as use-after-free.

For technical reasons, it is also a bug if you free memory more than once, but this doesn’t really come up much with a garbage collector. It simply means that if we use a garbage collector, we have to be a little careful with the finalizers if we don’t want to mess things up.

Given a (foreign) C function f that takes a pointer and returns a pointer, we say it exhibits dependence if the returned pointer depends on the argument. Generalizing the arity of f, and allowing arguments to be return values (as is common with pointers in C), we assert without proof that there exists a minimal dependence set documenting the dependence of the various arguments on the various return values for f, in the sense that all other dependence sets which correctly capture the dependence of the arguments are supersets of this one. If a_0, ..., a_k are the arguments and r_0, ..., r_m are the return values, we can find this minimal dependence set by iterating through the r_js and writing, say r_j => (a_i_{0}, ..., a_i_{k'}, r_l_{0}, ..., r_l_{m'}), where this relationship is the minimal dependence of r_j on the arguments and return values.

Taking the (tuple) product of the r_js on the left, and the (tuple) product of their dependencies on the right, we arrive at a (non-minimal) dependency set r := (r_0, ..., r_m) => ((a_i_{0,0}, ..., r_l_{m',0}), (a_i_{0,1}, ... r_l_{m',1}), ... (a_i_{0,m}, ..., r_l_{m',m})) =: d, i.e. r is the product of the return values and d is the product of their dependencies. We call this the proper dependency set of the function f. We are now ready to state the soundness criteria of living:

Soundness of Living

If for each foreign function f, we write the proper dependency set of y := f x as r => d, then if you encode this dependence using the living (=>) operator interface of the functions, you will obtain a sound program.

In other words, the use of properly dependent functions is sound.

Indeed, we don’t even need to use the proper dependency set, as any correct (including the minimal) dependency set will do. It’s just simpler to work with this way, since we only have to worry about a simple application of the (=>) operator.

Caveats

Note that living contains a function named unsafe_free, whose use can violate this soundness property, but careful use will preserve it. I will discuss this below.

Freeing Memory Safely

So far all we’ve done is said “if you never free memory, you can’t get a use-after-free error”. While this is technically true, it’s not exactly what we’d like when writing robust, long running software (like a video game).

One might hope that we are finished at this point though, since all we have to do now is allow our 'a Living_core.t to be garbage collected, but this is not the case. In fact, this would be a mistake, which it seems can only be fixed by an affine type-system. Consider the following program, assuming each of the functions is properly dependent:

let my_global_ptr_ptr : int ptr ptr Living_core.Default.t = get_c_ptr ()

let () =
    let _ = 
        let* global_ptr_ptr = my_global_ptr in
        let* int_ptr = Living_ctypes.Default.allocate Living_ctypes.Default.int 5 in
        let* () = global_ptr_ptr <-@ int_ptr in
        Living_core.Default.return ()
    in ()

let () =
    let _ = 
        let () = Gc.compact () in
        let* my_int_ptr = !@ my_global_ptr_ptr in
        let* my_int = !@ my_int_ptr in
        Printf.printf "%d <> %d\n" my_int 5;
        Living_core.Default.return ()
    in ()

my_global_ptr_ptr holds a pointer from C via get_c_ptr that can store a pointer to int. We allocate a pointer and write it to the global, and then allow that Living_core.Default.t to fall out of scope. We next run the garbage collector (which will collect the int_ptr in the previous top level item) take the same pointer that has been written to, and read from it, comparing it to 5. Since the original pointer has been collected, this is unlikely to print “5 <> 5” since it will be filled with garbage memory.

The problem is that we let the Living_core.Default.t in the first let () = item get collected when it was still referencing the important int_ptr. Affine types would allow us to demand that this value be “used” later, and so could prevent this issue. But we don’t have affine types, so to preserve soundness we must reach for a kludgier hammer. We will simply prevent all Living_core.Default.ts from being garbage collected by attaching a finalizer that sticks them in some globally accessible value.

This (somewhat trivially) ensures soundness by ensuring memory is never freed, but again, we’d like to be able to free memory sometimes. For that we use Living_core.Default.unsafe_free : 'a Living_core.Default.t -> 'a, which removes the finalizer mentioned above (or rather, renders it inert), but we must be careful. Luckily there is a relatively simple process that you can follow to ensure soundness.

Disjoint Values

We say two values v and w are disjoint if there exists no pointers in v into w and vice versa. Our goal is to use Living_core.Default.bind and/or Living_core.Default.map to map the inner value to a value that is disjoint from its dependencies. The process for doing so is application-specific; let us examine the above example again.

First of all, we can simply store the ptr directly in my_global_ptr_ptr, since it has no dependencies. Second, we must bind the internal result of the first let () = block to the second. Finally, once we dereference the pointer, we are free to unsafe_free it, since int is a scalar value and the Ctypes API always copies these values for us.

let my_global_ptr_ptr : int ptr ptr = Living_core.Default.unsafe_free (get_c_ptr ())

let () =
    let my_living_int = 
        let* int_ptr = Living_ctypes.Default.allocate Living_ctypes.Default.int 5 in
        let* () = my_global_ptr_ptr <-@ int_ptr in
        let () = Gc.compact () in
        let* my_int_ptr = !@ my_global_ptr_ptr in
        let* my_int = !@ my_int_ptr in
        Living_core.Default.return my_int
    in
    let my_plain_int = Living_core.Default.unsafe_free my_living_int
    (* let () = Gc.compact () in *)
    in
    Printf.printf "%d = %d\n" my_plain_int 5

Though this example is artificial, it illustrates the general idea: you stay in the Living_core.Default.t context until you’ve mapped to either a scalar or an OCaml object that doesn’t point into the dependencies anymore, and then you unsafe_free and continue with this value outside of the Living_core.Default.t. Uncommenting the commented Gc.compact () call will allow int_ptr to be collected, but this is okay since my_plain_int has already copied everything it needs from the foreign heap.

Conclusion

If you apply Living_core.Default.unsafe_free to values disjoint from their dependencies, then soundness can be preserved while allowing data to be garbage collected. In conclusion, if you can localize to some extent your use of foreign memory, then living provides a useful interface for ensuring you do not make use-after-free errors, and specifically localizes the functions you can make big mistakes in to those on the border of the foreign interface (which will always be the case, regardless of what library you use), and those that call Living_core.Default.unsafe_free.

Aside

There are other properties of this library, like it’s functor interface (we have been using the Default implementation which prevents you from leaking if you make a mistake apart from unsafe_free and warns you if you leak anything else) and it’s use of named_return if you want to give names to Living_core.t values to make debugging leaks more explicit and easier, but I’ll leave it there for now.

Thanks for reading.

Matt

EDIT:

I’ve noticed a mistake in the final example, namely that my_global_ptr_ptr still contains garbage at the end of the program, and so accessing it is still a use-after-free error. I think this is fixable, possibly by imposing a partial ordering on the lifetimes, and disallowing “setting” a larger lifetime object to a smaller. More specifically, the issue seems to stem from my_global_ptr_ptr having an unbounded (i.e. static) lifetime by virtue of being a top-level definition. Thus, only items which also have static lifetimes can be set.

Consider the following modified example, where we have moved the my_global_ptr_ptr inside the Living_core.Default.t for my_living_int:

let () =
    let my_living_int = 
        let* my_global_ptr_ptr : int ptr ptr = get_c_ptr () in
        let* int_ptr = Living_ctypes.Default.allocate Living_ctypes.Default.int 5 in
        let* () = my_global_ptr_ptr <-@ int_ptr in
        let () = Gc.compact () in
        let* my_int_ptr = !@ my_global_ptr_ptr in
        let* my_int = !@ my_int_ptr in
        Living_core.Default.return my_int
    in
    let my_plain_int = Living_core.Default.unsafe_free my_living_int
    (* let () = Gc.compact () in *)
    in
    Printf.printf "%d = %d\n" my_plain_int 5

This example doesn’t exhibit the mistake the previous example did, as my_global_ptr_ptr no longer has a static lifetime; it’s also no longer global, which could be a problem!

However, consider the following similar example:

let () =
    let my_living_global_ptr_ptr : int ptr ptr Living_core.Default.t = get_c_ptr () in
    let my_living_int = 
        let* int_ptr = Living_ctypes.Default.allocate Living_ctypes.Default.int 5 in
        let* my_global_ptr_ptr = my_living_global_ptr_ptr in
        let* () = my_global_ptr_ptr <-@ int_ptr in
        let () = Gc.compact () in
        let* my_int_ptr = !@ my_global_ptr_ptr in
        let* my_int = !@ my_int_ptr in
        Living_core.Default.return my_int
    in
    let my_plain_int = Living_core.Default.unsafe_free my_living_int
    (* let () = Gc.compact () in *)
    in
    Printf.printf "%d = %d\n" my_plain_int 5

Where we have given my_living_global_ptr_ptr a non-static lifetime, but still one that out-lives int_ptr. We are again in hot water! Perhaps this issue is too much for this technique to handle. I will have to see.