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?
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.
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 portableShared.t
send_and_wait and recv_clear can accept a contendedShared.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.
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?
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.
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?
Hey, sorry for the slow response. I suspect what’s going on there it that your t is a GADT. Until the most recent release of OxCaml last week, we had poor kind inference for GADTs. However, we had a special case for [@@unboxed] records. So if t is a GADT, removing the [@@unboxed] annotation would cause you to go from the happy path to the sad path.
Fortunately GADT kind inference has improved a lot (although there’s still more work to be done there).
(although there’s still more work to be done there).