Defining a message-passing data structure in OxCaml

Learning
1

Hi everyone,

We are currently (with @Lyrm) trying to define a simple message-passing data structure that exposes two main functions put_and_wait and send_and_clear. This is our current code :

open! Core
open! Await

module Shared : sig @@ portable
  type ('msg : immutable_data) t

  val create : unit -> 'a t
  val send_and_wait : 'a t -> 'a -> unit
  val recv_clear : 'a t -> 'a
end = struct
  type ('msg : immutable_data, 'k) inner = {
    data : ('msg option ref, 'k) Capsule.Data.t;
    mutex : 'k Mutex.t;
    cond : 'k Mutex.Condition.t;
  }

  type 'msg t = P : ('msg, 'k) inner -> 'msg t [@@unboxed]

  let create () =
    let (P { data; mutex }) = Capsule.With_mutex.create (fun () -> ref None) in
    P { data; mutex; cond = Mutex.Condition.create () }

  let send_and_wait (P t) msg =
    Await_blocking.with_await Terminator.never ~f:(fun await ->
        Mutex.with_key await t.mutex ~f:(fun key ->
            let new_msg = Some msg in
            let #((), key) =
              Capsule.Expert.Key.access key ~f:(fun access ->
                  let value = Capsule.Data.unwrap ~access t.data in
                  value := new_msg)
            in
            Mutex.Condition.signal t.cond;
            let key = Mutex.Condition.wait await t.cond ~lock:t.mutex key in
            let rec waiting_loop key =
              let #(is_unchanged, key) =
                Capsule.Expert.Key.access key ~f:(fun access ->
                    phys_equal !(Capsule.Data.unwrap ~access t.data) new_msg)
              in
              if is_unchanged then
                let key = Mutex.Condition.wait await t.cond ~lock:t.mutex key in
                waiting_loop key [@nontail]
              else #((), key)
            in
            waiting_loop key [@nontail])
        [@nontail])

  let recv_clear (P t) =
    Await_blocking.with_await Terminator.never ~f:(fun await ->
        (Mutex.with_key await t.mutex ~f:(fun key ->
             let rec loop key =
               let #(value, key) =
                 Capsule.Expert.Key.access key ~f:(fun access ->
                     {
                       Modes.Aliased.aliased =
                         !(Capsule.Data.unwrap ~access t.data);
                     })
               in
               match value.aliased with
               | None ->
                   let key =
                     Mutex.Condition.wait await t.cond ~lock:t.mutex key
                   in
                   loop key [@nontail]
               | Some value -> #({ Modes.Aliased.aliased = value }, key)
             in
             let #(value, key) = loop key in
             let #((), key) =
               Capsule.Expert.Key.access key ~f:(fun access ->
                   Capsule.Data.unwrap ~access t.data := None)
             in
             Mutex.Condition.signal t.cond;
             #(value, key)))
          .aliased)
end

We would obviously like this structure to be portable so that it can be used in parallel. We have added a @@portable annotation at the top of the module signature. However, we still get a nonportable error on the values of type Shared.t when calling Shared.recv_clear for example. Do we need to annotate the type of t in the .mli?

1 Like
2

Hey @Tim-ats-d!

If I understand your question, you’re running into issues if you write something like:

let shared_string : string Shared.t = Shared.create ()
let (send_string @ portable) msg = Shared.send_and_wait shared_string msg
let (receive_string @ portable) () = Shared.recv_clear shared_string

because the compiler complains that shared_string isn’t portable. Is that right?

If so, then yes you’re right that you need to write a kind annotation on the type of t in the .mli. You’ll need to expose the fact that Shared.t “mode-crosses” the portability and contention axes. (Note that if you only add an annotation for portability, then you’ll get a new error about shared_string being contended.) This is written like type ('msg : immutable_data) t : value mod contended portable. (relevant docs)

To elaborate some more on why this is necessary, the functions being portable are insufficient to prove that using a Shared.t in this way is safe. Without it, you’d be able to smuggle a nonportable function across domains via the Shared.t type. To illustrate, here’s an alternate implementation of that module that is accepted but would cause a data race if the kind annotation wasn’t necessary (for simplicity, I removed the polymorphism, but the principle is still the same):

module Bad_shared : sig @@ portable
  type t

  val create : unit -> t
  val send_and_wait : t -> unit -> unit
  val recv_clear : t -> unit
end = struct
  type t = unit -> unit

  let create () =
    let counter = ref 0 in
    fun () ->
      (* This increment is racy *)
      incr counter
  ;;

  let send_and_wait t () = t ()
  let recv_clear t = t ()
end

The : value mod portable annotation essentially says “values of this type are always portable,” which is true of any type that can’t contain functions. Since Bad_shared.t contains an arrow type, adding : value mod portable here would result in an error.

The story is similar for contention, except the concern there is that Shared.t might contain non-synchronized mutable data.

2 Likes
3

I should maybe point out that the : value mod contended portable is mostly a convenience. Instead, of adding that annotation, you could instead track that:

  • create returns a portable Shared.t
  • send_and_wait and recv_clear can accept a contended Shared.t

Here’s what that’d look like:

module Shared : sig @@ portable
  type ('msg : immutable_data) t

  val create : unit -> 'a t @ portable
  val send_and_wait : 'a t @ contended -> 'a -> unit
  val recv_clear : 'a t @ contended -> 'a
end

My experience has been that adding these annotations in all the relevant spots can get quite tedious and that taking advantage of kind annotations is way more ergonomic.

1 Like
4

I understand it’s not central to your question but I would be interested in a bit more context what problem is being solved here. I was expecting “a simple message-passing data structure” to be easier. What is passed here between what and why is using something like Atomic not part of the solution?

5

Use an Atomic should work as expected and maybe reduce the boilerplate needed for data race safety in OxCaml, but we didn’t choose it because this data structure acts as both a synchronization point and a message sender. In our case, the tasks we perform in parallel are rather time-consuming, and using the Atomic approach would require active waiting.

2 Likes
6

Hi! I have a follow-up question: the type t is unboxed. I guess we added [@@unboxed] mechanically (copying what is done in the documentation), but out of curiosity, I tried to remove it, and it resulted in an error message about the kind of t. Why is this related?

1 Like