Bluish Coder

While using the libevent API from ATS I came across a scenario where it was important to call a function to release objects in a particular order. I wanted to have ATS enforce at compile time that the destruction occurs safely in the right order. The following example uses the built in libevent HTTP API for creating simple web servers. It uses the ATS libevent wrapper I wrote about previously.

fn cb {l1,l2:agz} (request: !evhttp_request l1, arg: !event_base l2): void = let
  val () = printf("here\n", @())
in
 ()
end

fn server () = let
  val _ = signal (SIGPIPE, SIG_IGN)
  val base = event_base_new ()
  val () = assert_errmsg (~base, "event_base_new failed")

  val http = evhttp_new (base)
  val () = assert_errmsg (~http, "evhttp_new failed")

  val r = evhttp_set_cb_with_base (http, "/", cb, base)
  val () = assert_errmsg (r = 0, "evhttp_set_cb_with_base failed")

  val r = evhttp_bind_socket (http, "0.0.0.0", uint16_of_int(8080))
  val () = assert_errmsg (r = 0, "evhttp_bind_socket failed")

  val r = event_base_dispatch (base)
  val () = assert_errmsg (r >= 0, "event_base_dispatch failed")

  val () = evhttp_free (http)
  val () = event_base_free (base)
in
  ()
end

implement main () = server ()

The call to http_new requires an event_base object. Internally, inside the C API, the returned evhttp object holds a pointer to this event_base. This results in the pointer being shared in two places and requires careful destruction to prevent using a destroyed object.

Later I call evhttp_free to destroy and release resources associated with the evhttp object, followed by event_base_free to do the same with the event_base object. I do it in this order to prevent a dangling reference to the event_base inside the evhttp object. The evhttp object is associated with that particular event_base and it's important not to pass an incorrect base to functions that use the http object. Ideally code like the following shouldn't compile:

val base = event_base_new ()
val base2 = event_base_new ()
val http = evhttp_new (base)

// Wrong event_base passed, fail compilation
val r = evhttp_set_cb_with_base (http, "/", cb, base2)

// Destruction out of order, fail compilation
val () = event_base_free (base)
val () = evhttp_free (http)

To model this in ATS I changed the ATS definition of evhttp to have an event_base associated with it at the type level and modified evhttp_new to return this relationship (agz is an address that cannot be NULL, agez is an address that can be NULL):

absviewtype evhttp (l:addr, l2:addr)
fun http_new {l1:agz} (base: !event_base l1): [l2:agez] evhttp (l2,l1) = "mac#evhttp_new"

With this change the type for evhttp depends on the value of the pointer to the event_base given as an argument. Now we can use this in the definition of evhttp_set_cb_with_base to ensure that the correct event_base object is used:

fun evhttp_set_cb_with_base {l1,l2:agz}
       (http: !evhttp (l1, l2),
        path: string,
        callback: {l3:agz} (!evhttp_request l3, !event_base l2) -> void,
        arg: !event_base l2): int = "mac#evhttp_set_cb"

This definition states that the event_base given as the arg paramater, and as the second argument to the callback, must be the same as that associated with the http object. This is done by using the same l2 dependent type argument with these types. This gives us the desired error checking in the first 'fail compilation' test above.

The next step is to prevent out of order destruction. This is done by passing the event_base object as a proof argument to the evhttp_free function:

fun evhttp_free {l1,l2:agz} (base: !event_base l1 | http: evhttp (l2, l1)): void = "mac#evhttp_free"

By adding this as proof argument I'm stating that the caller of evhttp_free must have a usable event_base object that was used to create this evhttp object to prove we can safely destroy it. The following is now a compile time error:

val () = event_base_free (base)
val () = evhttp_free (base | http)

This is due to event_base_free consuming the base linear object. The type of base following this call is no longer defined. The evhttp_free call is now an error due to using an undefined base. The following will work:

val () = evhttp_free (base | http)
val () = event_base_free (base)

This method of ensuring correct order of destruction and resource usage requires no changes to the libevent C code. Everything occurs during type checking. The generated C code looks exactly like normal libevent C usage with no runtime overhead for tracking the association between evhttp and event_base objects.