Parallelism: contention and portability

Parallel code is safe only when overlapping work cannot race on mutable state. This section uses fork_join2 and spawn to show how OxCaml expresses that rule with contention and portability modes.

By the end, you should be able to:

run work with structured fork/join and spawn;
explain why overlapping reads and writes of shared mutable state can cause data races;
use contention modes to predict which direct reads and writes are allowed;
explain how modes propagate through function calls and record fields;
read mode requirements on explicit function arguments;
understand why function values need portability requirements, especially when they hide mutable state in a closure environment;
read higher-order mode requirements such as ('a @ shared -> 'b) @ shareable;
explain that fork_join2 and spawn are ordinary functions whose types require shareable or portable function arguments.

The notes below cover the same ground as the lecture slides, in more depth. The exercises are collected at the end of the page. If you attended the lecture, you can work through the exercises directly; each exercise points back to the section of the notes that explains its concept.

The parallel functions we will use

Before we talk about modes, it helps to know the two functions that motivate them: fork/join for work that must finish before the parent continues, and spawn for work that may keep running after the parent returns from the call.

`Toy.fork_join2`

Run two pieces of work, wait for both to finish, and return both results.

`Toy.spawn`

Start one piece of work and let the parent continue immediately.

Fork/join returns after both child computations finish; spawn may return while its worker is still running.

The examples below use a toy API with the same mode requirements as the real parallel APIs, but without scheduler and scope arguments.

Fork/join: pass two worker functions to Toy.fork_join2.

(* Worker code: ordinary code we want to run in parallel. *) let bits_to_string bits = let buf = Buffer.create 0 in List.iter (fun bit -> Buffer.add_char buf (if bit then '1' else '0')) bits; Buffer.contents buf (* Parallel computation: fork two workers and join their results. *) let strings_in_parallel () = let (left, right) = Toy.fork_join2 (fun () -> bits_to_string [true; false; true; true]) (fun () -> bits_to_string [false; true; false; false]) in left ^ "\n" ^ right let () = print_endline "The output is:"; print_endline (strings_in_parallel ())

Toy.fork_join2 returns an ordinary pair. The mode story is in the function arguments: both workers must be available as @ shareable.

Spawn: pass one worker function to Toy.spawn.

(* Worker code: ordinary code we want to run in parallel. *) let bits_to_string bits = let buf = Buffer.create 0 in List.iter (fun bit -> Buffer.add_char buf (if bit then '1' else '0')) bits; Buffer.contents buf (* Spawn: start the worker function and let the parent continue. *) let () = print_endline "The output is:"; Toy.spawn (fun () -> print_endline (bits_to_string [true; false; true; true])); print_endline (bits_to_string [false; true; false; false])

Two people each working at their own computer, with separate code on separate screens. — Fresh per-call buffers: each parallel call mutates only its own scratch state.

In both examples, bits_to_string creates its buffer inside the function. Each call gets a fresh buffer, so the compiler infers that this function can be called in parallel.

Parallelism plus mutation can cause bugs

Parallel computations may access the same object at overlapping times. If one computation writes while another reads or writes, the result may depend on scheduling.

The safe version above allocates a fresh buffer on every call. One possible optimization is to move the buffer outside the function and reuse it. That changes the allocation pattern: instead of one buffer per call, every call uses the same buffer.

If two calls overlap, they may clear and append to that shared buffer in an interleaved order. That is a data race: the string returned by one call may include bytes appended by another call.

In the version below, buf has moved from inside bits_to_string to a top-level binding. Every call to bits_to_string_shared now clears and appends to that same buffer.

(* Worker code: ordinary code we want to run in parallel. *) let buf = Buffer.create 0 let bits_to_string_shared bits = Buffer.clear buf; List.iter (fun bit -> Buffer.add_char buf (if bit then '1' else '0')) bits; Buffer.contents buf (* Spawn: start the worker function and let the parent continue. *) let () = Toy.spawn (fun () -> print_endline (bits_to_string_shared [true; false; true; true])); print_endline (bits_to_string_shared [false; true; false; false])

Two people sharing one computer with scrambled code on the screen, looking confused. — A shared buffer is one mutable object used by overlapping calls, so their writes can interfere.

OxCaml rejects the call to Toy.spawn that invokes bits_to_string_shared. The failed check is on the function value: the spawned worker would call a function that closes over the shared buffer.

What counts as a data race?

A data race happens when two pieces of work access the same mutable state at overlapping times, and at least one access writes. Two parallel writes are bad because the final value can depend on which piece of work happens to write last. A read that overlaps with a write is also bad, because the read may see either the old value or the new value depending on scheduling.

Two parallel reads are fine: neither read changes the state, so their order cannot affect the result. Reads and writes are also fine when the program gives them a defined order, either by ordinary program order or by synchronization. For example, fork_join2 synchronizes after its children finish, so parent code after the fork/join runs after both child computations are done.

Why OxCaml tracks data races in the type system

If bits_to_string_shared came from another module, the caller should not have to inspect its body to discover the captured buffer. Checked module signatures record whether calls are safe for parallel callers.

First approximation: functions passed to parallel work are checked

When a closure is passed to parallel work, OxCaml checks the closure body under restrictions that prevent data races.

For closures passed to parallel work, start with this rule of thumb:

a fork/join function may read captured mutable state, but may not write it;
a spawned function may not even read mutable fields, because that read may overlap with a later write in the parent;
fresh mutable state created inside the function is still owned by that function body.

The real check is type-based. The compiler checks mode requirements, not assignments or the names Toy.fork_join2 and Toy.spawn.

Contention modes: read and write access

A mode is a checked requirement on how a value may be used. The contention axis controls whether the mutable fields reachable through an expression can be read or written.

On this axis, uncontended access is stronger than shared access, and shared access is stronger than contended access. Stronger access permits more operations. Weaker access prevents two overlapping workers from both reaching the same mutable field as writers.

The same source variable can be available at different contention modes in different contexts. In the examples below, x is ordinary mutable state outside the function. When x is captured by a fork/join or spawned function, that function receives weaker access to x.

Ordinary closure

type t = { id : int; mutable hits : int }

let x = { id = 1; hits = 0 }

let _ =

List.iter

(

fun _ ->

uncontended

let _id = x.id in (* ok *)

let n = x.hits in (* ok *)

x.hits <- n + 1 (* ok *)

)

[1; 2; 3]

x.hits <- x.hits + 1 (* ok *)

Fork/join closure

type t = { id : int; mutable hits : int }

let x = { id = 1; hits = 0 }

let _result =

Toy.fork_join2

(

fun () ->

shared

let _id = x.id in (* ok *)

let n = x.hits in (* ok *)

x.hits <- n + 1 (* no *)

)

(

fun () ->

shared

...

)

x.hits <- x.hits + 1 (* ok *)

Spawn closure

type t = { id : int; mutable hits : int }

let x = { id = 1; hits = 0 }

let _ =

Toy.spawn

(

fun () ->

contended

let _id = x.id in (* ok *)

let n = x.hits in (* no *)

x.hits <- n + 1 (* no *)

)

()

x.hits <- x.hits + 1 (* ok *)

The final line in each example is outside the passed function, so it can still mutate x. In the spawn case, that may look surprising because spawned work may still be running. The parent-side write is allowed because inside the spawned function, captured x is treated as x @ contended: the function can use immutable fields of x, but it cannot read or write x.hits.

The mode change happens when the closure is passed: fork_join2 sees ordinary mutable captures as shared, while spawn sees them as contended.

Contention axis

Contention controls how mutable fields may be used.

x @ uncontended

we can read and write x's mutable fields
parallel users can access x's immutable fields only

x @ shared

we can read but not write x's mutable fields
parallel users may read x's mutable fields

x @ contended

we cannot read or write x's mutable fields
some other user may have write access

The arrows show the submode order on the contention axis: stronger modes can be passed where weaker modes are required. If a call site has x @ uncontended, it may pass x to a parameter that only requires x @ shared or x @ contended.

Invariant. A useful way to read these modes is that mutable fields are either under one writer or under many readers:

Single writer: one thread has write access (x @ uncontended), while any number of parallel threads have no access to the mutable parts (x @ contended).
Many readers: any number of threads have read access (x @ shared).

Parallel functions establish this invariant through their mode requirements. The invariant is what rules out parallel writes and write/read races.

How modes propagate

In OxCaml, every variable and every sub-expression has a mode, just as it has a type. A mode is not a separate kind of type; it is an extra fact about how the value at that program point may be used.

For function calls, the mode annotations on the function type say two things. The caller must provide the input at the parameter mode, and the call returns a result at the result mode.

f : a @ M -> b @ N
x : a @ M

f x : b @ N

Modes differ from types because modes are deep. For a record projection, the field type comes from the record declaration, but the field mode usually comes from the current mode of the record expression.

r : { field : a } @ M

r.field : a @ M

Those rules explain most mode propagation: variables carry modes, function calls check parameter and result modes, and ordinary data access propagates modes through the value. The one complex rule is closure formation. A fun ... -> ... expression can carry values from its environment, so the compiler also checks what modes those captured values have inside the closure.

Function calls check explicit argument mode requirements

The compiler does not try to rediscover hidden mutation by looking through every function body at every call site. Instead, the helper's type records the modes it requires for each explicit argument.

The helper functions below make those argument requirements explicit. Reading the immutable field works with any contention mode, reading the mutable field needs shared or uncontended, and writing the mutable field needs uncontended:

type t = { id : int; mutable hits : int } (* Immutable field reads work even in contended mode. *) let get_id (x @ contended) = x.id (* Mutable field reads need shared or uncontended mode. *) let get_hits (x @ shared) = x.hits (* Mutable field writes need uncontended mode. *) let bump_hits (x @ uncontended) = x.hits <- x.hits + 1

Try changing the annotations on these helper arguments. The inferred types and errors show which operations require which contention modes.

In the inferred interface, focus on the argument modes: t @ contended, t @ shared, and plain t. Plain t means the caller must provide ordinary, uncontended access.

You may also see inferred promises such as @@ stateless or @@ observing. Ignore those for now; they are not needed for the contention examples.

Worked example: function calls on parent variable `x`

Now combine the closure-boundary rule with the helper argument modes. Suppose x is defined outside the List.iter/fork_join2/spawn. Then the function calls are allowed as follows:

List.iter (fun _ ->
  ignore (get_id x);
  ignore (get_hits x);
  bump_hits x) [()]

Toy.fork_join2 (fun () ->
  ignore (get_id x);
  ignore (get_hits x);
  bump_hits x) (fun () -> ())

Toy.spawn (fun () ->
  ignore (get_id x);
  ignore (get_hits x);
  bump_hits x)

Call on parent variable `x`	`List.iter`	`fork_join2`	`spawn`
`get_id x`	yes	yes	yes
`get_hits x`	yes	yes	no
`bump_hits x`	yes	no	no

List.iter uses an ordinary function, so captured x stays uncontended. In a function passed to fork_join2, captured x becomes shared: mutable reads are allowed, mutable writes are not. In a function passed to spawn, captured x becomes contended: immutable-field reads are allowed, but mutable reads and writes are not.

Portability modes: function values and hidden captures

A call such as bump_hits x passes the mutable value as an explicit argument. But closures can also capture mutable state in their closure environment, and OxCaml needs to check that hidden access too.

If we define helpers first, then call them later, those helpers still carry their captured x with them:

type t = { id : int; mutable hits : int } let x = { id = 1; hits = 0 } let id_x () = x.id (* a portable function *) let read_x () = x.hits (* a shareable function *) let write_x v = x.hits <- v (* a nonportable function *) let _ = Toy.spawn (fun () -> write_x 1); write_x 2

Moving access into helpers does not change the rule

OxCaml rejects the call that would let spawned work run write_x 1 while the parent can also use write_x. The call has no explicit x argument, so the relevant check is on the function value write_x itself. write_x is nonportable because it writes captured mutable state.

The portability axis describes which parallel contexts a function value can be used in. For closures, portability depends on the values captured by the closure.

Portability axis

Which parallel contexts a value can be used in, and what access closure values keep to captures.

portable

can be used in spawned parallel work
for closures: only immutable-field access to ordinary mutable captures

shareable

can be used in structured fork/join work
for closures: read-only access to mutable fields of captures

nonportable

not promised safe for parallel use
for closures: may keep ordinary read/write access to captured mutable state

The arrows mean “can be passed to” on the portability axis: a value available as portable may be passed to a position that only requires shareable or nonportable.

`List.iter`

type t = { id : int; mutable hits : int }

let x = { id = 1; hits = 0 }

let id_x () = x.id

let read_x () = x.hits

let write_x v = x.hits <- v

let _ =

List.iter

(

fun _ ->

uncontended

let _id = id_x () in (* ok *)

let n = read_x () in (* ok *)

write_x (n + 1) (* ok *)

)

[1; 2; 3]

`Toy.fork_join2`

type t = { id : int; mutable hits : int }

let x = { id = 1; hits = 0 }

let id_x () = x.id

let read_x () = x.hits

let write_x v = x.hits <- v

let _ =

Toy.fork_join2

(

fun () ->

shared

let _id = id_x () in (* ok *)

let n = read_x () in (* ok *)

write_x (n + 1) (* no *)

)

(

fun () ->

shared

...

)

`Toy.spawn`

type t = { id : int; mutable hits : int }

let x = { id = 1; hits = 0 }

let id_x () = x.id

let read_x () = x.hits

let write_x v = x.hits <- v

let _ =

Toy.spawn

(

fun () ->

contended

let _id = id_x () in (* ok *)

let n = read_x () in (* no *)

write_x (n + 1) (* no *)

)

()

The helper modes can also be written directly. These three functions close over the same x, but each one keeps a different amount of access to it:

type t = { id : int; mutable hits : int } let x = { id = 1; hits = 0 } let (id_x @ portable) () = x.id let (read_x @ shareable) () = x.hits let (write_x @ nonportable) v = x.hits <- v

id_x is portable because it only uses the immutable field. read_x is shareable because it reads mutable state. write_x is nonportable because it writes mutable state.

List.iter (fun _ ->
  ignore (id_x ());
  ignore (read_x ());
  write_x 1) [()]

Toy.fork_join2 (fun () ->
  ignore (id_x ());
  ignore (read_x ());
  write_x 1) (fun () -> ())

Toy.spawn (fun () ->
  ignore (id_x ());
  ignore (read_x ());
  write_x 1)

Explicit argument vs hidden capture

These two failures look similar but are checked for different reasons.

Explicit argument:

let bump_hits (x @ uncontended) =
  x.hits <- x.hits + 1

fun () -> bump_hits x

The captured value x is passed explicitly. The call is checked against bump_hits's parameter mode. In a fork/join function, captured x is available only as shared, but bump_hits requires uncontended.

Hidden capture:

let write_x v =
  x.hits <- v

fun () -> write_x 1

Here x is not passed explicitly. The mutable access comes from the closure environment of write_x. The call is checked against the portability mode of the function value write_x.

For any call inside parallel work, ask two questions:

Are the explicit arguments available at the modes required by the callee?
Is the callee value itself available at the portability mode required by this context?

Back to the shared buffer

The shared-buffer example fails because the buffer is captured by the function value bits_to_string_shared.

let buf = Buffer.create 0

let bits_to_string_shared bits =
  Buffer.clear buf;
  ...

Inside the implementation, Buffer.clear buf and Buffer.add_char buf require buf @ uncontended.

Since buf is captured by bits_to_string_shared, the function value is not portable. A spawned function may only call portable-enough function values, so this use is rejected:

Toy.spawn
  (fun () -> bits_to_string_shared bits)

If the buffer were passed explicitly instead, the failure would be at the buffer argument:

let write_bits (buf @ uncontended) bits =
  Buffer.clear buf;
  ...

fun () -> write_bits buf bits

In that version, the spawned function has a weakened buf, but write_bits requires an uncontended buffer argument.

How captures cross a closure boundary

The closure-boundary rule applies to three cases:

direct access to a captured value;
passing a captured value as an explicit argument;
calling a captured function value that hides mutable state.

The same rule explains all three cases. When a value from the outer scope is used inside a closure with a parallel-safety promise, the value crosses a closure boundary. The closure's required portability mode determines which modes the captured value is available at inside the body.

The diagrams below summarize that boundary behavior. They are not special rules for fork_join2 or spawn; those functions merely require function-argument modes that trigger these checks.

`shareable` closure

A structured fork/join closure may still use captures in shared/read-only mode, but not in uncontended/write-capable mode.

let n = 10 immutable data

let b @ uncontended = (...) uncontended

let a @ shared = (...) shared

let c @ contended = (...) contended

let f : (int -> int) @ portable = (...) portable

let g : (int -> int) @ shareable = (...) shareable

let h : (int -> int) @ nonportable = (...) nonportable

let worker : (unit -> unit) @ shareable =

shareable Closure Boundary

fun () ->

let n' = n in stays unchanged

let b' @ shared = b in uncontended becomes shared

let a' @ shared = a in shared stays shared

let c' @ contended = c in contended stays contended

let _ = f 0 in can use portable

let _ = g 0 in can use shareable

let _ = h 0 in cannot use nonportable

...

let (_left, _right) = fork/join

Toy.fork_join2 worker worker

let b'' @ uncontended = b outside: still uncontended

`portable` closure

A spawned closure is checked even more conservatively: shared/read-only mutable access is not available inside the closure.

let n = 10 immutable data

let b @ uncontended = (...) uncontended

let a @ shared = (...) shared

let c @ contended = (...) contended

let f : (int -> int) @ portable = (...) portable

let g : (int -> int) @ shareable = (...) shareable

let h : (int -> int) @ nonportable = (...) nonportable

let worker : (unit -> unit) @ portable =

portable Closure Boundary

fun () ->

let n' = n in stays unchanged

let b' @ contended = b in uncontended becomes contended

let a' @ contended = a in shared becomes contended

let c' @ contended = c in contended stays contended

let _ = f 0 in can use portable

let _ = g 0 in cannot use shareable

let _ = h 0 in cannot use nonportable

...

ignore (Toy.spawn worker) spawn

let a'' @ shared = a outside: still shared

let b'' @ uncontended = b outside: still uncontended

Mutable captures lose write access. A portable closure sees captured mutable state as contended, so it cannot read or write mutable fields. A shareable closure sees captured mutable state at most as shared, so it may read mutable fields but cannot write them.

The same boundary behavior can be summarized by asking which mode each captured value has inside each kind of closure.

@ uncontended

@ shared

@ contended

@ portable

@ shareable

@ nonportable

in portable closure

contended

portable

error

in shareable closure

shared

contended

portable

shareable

error

in nonportable closure

uncontended

shared

contended

portable

shareable

nonportable

A closure boundary keeps captured variables' types the same, but it can weaken their contention mode inside the closure: uncontended may become shared or contended depending on the closure mode.

A captured function value must be at least as portable as the closure context requires. Explicit arguments are checked separately against the callee's parameter modes.

A portable closure gives up mutable-field access to captures because spawned work can overlap later parent writes.

Parallel functions are ordinary typed functions

The compiler does not recognize Toy.fork_join2 or Toy.spawn by name. They are ordinary functions whose types require particular modes on function arguments.

Fork/join's API can ask for shareable worker functions, while spawn's API asks for a portable worker function.

The toy API puts only the relevant function-argument modes in the type:

val Toy.fork_join2 :
  (unit -> 'a) @ shareable ->
  (unit -> 'b) @ shareable ->
  'a * 'b

val Toy.spawn :
  (unit -> unit) @ portable ->
  unit

From fork_join2's shareable worker requirement, captured mutable state is read-only inside each worker:

direct writes to captured mutable state are rejected;
calls like bump_hits x are rejected if bump_hits requires x @ uncontended;
calls like write_x 1 are rejected if write_x is not shareable.

From spawn's portable worker requirement, captured mutable fields are unavailable inside the worker:

direct reads and writes of captured mutable fields are rejected;
calls are rejected if their explicit arguments require stronger modes than the function has;
called function values must themselves be portable enough.

Parallel functions express their safety requirements in modes and types, and the compiler checks those requirements compositionally.

Mode annotation syntax reference

Modes attach to binder and type positions. They are not tied to a simple syntactic category like “data” or “function.”

Examples:

x : t @ shared

The value at this position must be available with shared contention.

f : (unit -> unit) @ portable

The function value at this position must be available at the portable mode on the portability axis.

run : ((unit -> unit) @ portable -> unit) @@ portable

The explicit argument to run must be a portable function value, and the value run itself is declared portable at the module boundary.

map : ('a @ shared -> 'b) @ shareable -> 'a list @ shareable shared -> 'b list

The function argument is shareable; the function receives each element as shared; the input list position carries both portability and contention requirements.

Mode annotation syntax

OxCaml can often infer modes. We write them explicitly when we want to document an API boundary or make an error point closer to the relevant value.

On a binder, write the mode after the name: let get_count (x @ shared) = ... or let r @ uncontended = ref 0.
On a type annotation, write the mode after the type: let get_count (x : t @ shared) = ....
For a function being defined, let (worker @ portable) x = ... puts the mode on the function value worker.
For a function value with an explicit type, write the function type in parentheses: let worker : (int -> int) @ portable = ....
For a function argument, the same function-value form says what callers must provide: let run (f : (unit -> unit) @ portable) = ....
In a module signature, a val item uses @@ for the declared value itself: val f : (int -> int) @@ portable.
The same pattern is common for API functions: val run : (unit -> unit) @ portable -> unit @@ portable requires a portable function argument and declares run itself portable.
Inside a function type, the source and target can have their own modes: 'a @ uncontended -> 'b @ portable.

Worked examples: portability requirements on function values

These examples isolate the closure/function case. The question is what a closure may capture when it promises to be usable from more parallel contexts.

Portable pure functions

On the portability axis, a pure function that does not capture mutable state is the simplest case. The compiler can accept the @ portable annotation because the closure does not depend on thread-local mutable state.

let (factorial @ portable) n = let rec loop acc i = if i <= 1 then acc else loop (acc * i) (i - 1) in loop 1 n

Ordinary closures may capture ordinary refs

An ordinary closure can still capture and mutate a ref. That is fine for local use, but not for a closure used in spawned parallel work.

let r = ref 0 let ordinary () = r := !r + 1; !r let () = print_endline (string_of_int (ordinary ()))

Portable closures may capture immutable data

Portable closures may still capture immutable data. Capturing factor is safe because the closure does not get a handle to mutable state that can race with another thread.

let factor = 3 let (times_factor @ portable) x = x * factor

Portable closures reject ordinary ref captures

A portable closure cannot read an ordinary captured ref. Inside a portable closure, captured mutable state has a mode too restrictive for ordinary ref access.

let r = ref 0 let (bad @ portable) () = !r

Portable functions may use fresh local mutation

Fresh local mutation is different: each call allocates its own cell. A portable function may use that state locally and return an ordinary result. The closure itself is still portable because the fresh state is not captured from the outside.

let (fresh_ref @ portable) () = let r = ref 0 in r := !r + 1; !r let () = print_endline (string_of_int (fresh_ref ()))

Mode crossing is a property of a type

Modes usually describe how one value may be used at one program point. Mode crossing describes a type: whether values of that type can ignore a mode axis.

The simplest example is int. An integer has no mutable field, no closure environment, and no heap object whose thread access matters. That is why an int @ contended can still be used where an int @ uncontended is expected, and an int @ nonportable can still be used where an int @ portable is expected.

let int_crosses_contention (x : int @ contended) : int @ uncontended = x let int_crosses_portability (x : int @ nonportable) : int @ portable = x

Kinds are how an interface records this fact for user-defined types. For parallelism, the most useful kinds say whether a type can ignore portability, contention, or both.

mutable_data means ordinary data that contains no functions deeply. It may contain mutable fields, so contention still matters, but portability does not. The axis-specific form of that portability promise is value mod portable.
value mod contended means the type can ignore contention. In basic code, think "no ordinary mutable state"; function values may still appear, so this is not a portability promise.
immutable_data means plain immutable data: no functions and no ordinary mutable fields deeply. It crosses both portability and contention.

type immutable_pair : immutable_data = { id : int; name : string } let immutable_pair_crosses (x : immutable_pair @ nonportable contended) : immutable_pair @ portable uncontended = x type mutable_counter : value mod portable = { id : int; mutable count : int } let counter_crosses_portability (x : mutable_counter @ nonportable) : mutable_counter @ portable = x type callback_box : value mod contended = { f : int -> int } let callback_box_crosses_contention (x : callback_box @ contended) : callback_box @ uncontended = x

Parameterized types cross an axis only when their contents do

Parameterized types need one more piece. A list or box may be immutable itself, but it contains values of some element type. The kind uses with 'a to say: this container can cross an axis only when the stored 'a values can cross that axis too.

type 'a box : immutable_data with 'a = Box of 'a let int_box_crosses (x : int box @ nonportable contended) : int box @ portable uncontended = x let function_box_crosses_contention (x : (unit -> unit) box @ contended) : (unit -> unit) box @ uncontended = x

The int box example crosses both axes because int crosses both axes. The function box crosses contention because the box and the function value are immutable for this purpose, but it does not automatically cross portability: a function value may close over nonportable state.

type 'a box : immutable_data with 'a = Box of 'a let function_box_does_not_cross_portability (x : (unit -> unit) box @ nonportable) : (unit -> unit) box @ portable = x

Maps also carry comparator evidence

Real library types often have one more dependency in their representation. A Map stores keys and values, but it also stores comparator evidence. For a map with a custom key type to cross portability, the key type and the comparator evidence must both carry the right mode information.

open Base type key = { id : int ; name : string } [@@deriving compare, sexp_of] module Key = struct type t = key let compare = compare_key let sexp_of_t = sexp_of_key include Comparator.Make [@modality portable] (struct type nonrec t = t let compare = compare let sexp_of_t = sexp_of_t end) end type ('a : value mod portable) require_portable type ('a : value mod contended) require_contended type map = int Map.M(Key).t type portable_ok = map require_portable type contended_ok = map require_contended

The [@@deriving compare, sexp_of] line generates the ordinary comparison and sexp functions for the key type. Comparator.Make [@modality portable] checks that those functions are portable and exposes comparator_witness with a portable kind, so the map can cross the portability axis when its keys and values can.

open Base type key = { id : int } [@@deriving compare, sexp_of] module Key = struct type t = key let compare = compare_key let sexp_of_t = sexp_of_key include Comparator.Make (struct type nonrec t = t let compare = compare let sexp_of_t = sexp_of_t end) end type ('a : value mod portable) require_portable type does_not_cross = int Map.M(Key).t require_portable

The plain Comparator.Make version uses the same derived functions, but it does not export the comparator witness as portable. Because the Map kind depends on the comparator witness, this version of Map no longer crosses portability, even if its key and value types do.

Interface annotations make portable APIs reusable

For library APIs, mode promises belong in the interface. The implementation can use local mutation internally, but the exposed API should say which values are portable and which operations can be called from portable code.

Here, create promises to produce a portable value, and price promises to work from portable code while only requiring the value in contended mode.

module type Thing = sig type t val create : price:float -> mood:int -> t @ portable @@ portable val price : t @ contended -> float @@ portable end

Portabilizing whole API signatures

Portabilizing an API means changing its .mli so parallel callers can see the right checked promises. If most values in an interface should be callable from portable code, put @@ portable at the top of the .mli. Inside a module type, write sig @@ portable. Individual declarations can opt out with @@ nonportable.

@@ portable

type t : value mod portable

val create : int -> t
val id : t @ contended -> int
val debug_global_counter : unit -> unit @@ nonportable

For this API, most operations can be portable; only the operation that touches global mutable state opts out. That is clearer than adding @@ portable one declaration at a time, because the interface says: this module is ready for checked parallel use except where it explicitly says otherwise.

Do this bottom-up. If B.ml depends on A.mli, then A.mli has to expose portable operations before B.mli can promise that B's operations are portable.

module type Thing = sig @@ portable type t : value mod portable val create : int -> t val id : t @ contended -> int val debug_global_counter : unit -> unit @@ nonportable end module Thing : Thing = struct type t : value mod portable = { id : int; mutable count : int } let create id = { id; count = 0 } let id (x @ contended) = x.id let debug_count = ref 0 let debug_global_counter () = incr debug_count end

Exercises

These exercises check your understanding of the material from the lecture. They only assume the concepts covered above, in roughly the order the notes introduce them.

Each exercise starts with a line saying what it checks and which section of the notes to reread if you get stuck.

Exercise 1: which mode permits each field access?

Checks: which contention modes permit immutable reads, mutable reads, and mutable writes. If stuck: reread Function calls check explicit argument mode requirements.

Assume type t = { id : int; mutable hits : int } and a value x : t.

For each operation, decide which argument modes are strong enough. Click each cell to choose yes or no.

Operation on `x`	`x @ uncontended`	`x @ shared`	`x @ contended`
`x.id`
`x.hits`
`x.hits <- x.hits + 1`

Answer

Operation on `x`	`x @ uncontended`	`x @ shared`	`x @ contended`
`x.id`	yes	yes	yes
`x.hits`	yes	yes	no
`x.hits <- x.hits + 1`	yes	no	no

Immutable field reads work in any mode. Mutable field reads need x @ shared or x @ uncontended. Mutable field writes need x @ uncontended.

Exercise 3: functions that capture a parent variable

Checks: portability modes of capturing functions. If stuck: reread Portability modes: function values and hidden captures.

Three helpers close over the same mutable record, with their portability written explicitly:

type t = { id : int; mutable hits : int }

let x = { id = 1; hits = 0 }

let (id_x @ portable) () = x.id
let (read_x @ shareable) () = x.hits
let (write_x @ nonportable) v = x.hits <- v

Decide which of these functions can be called from a function passed to List.iter, fork_join2, and spawn.

Answer

id_x can be used in all three contexts. read_x can be used in List.iter and fork_join2, but not spawn. write_x can only be used in List.iter.

Exercise 4: implement `parallel_map`

Checks: applying mode requirements in a real higher-order helper. If stuck: reread Parallel functions are ordinary typed functions.

Write a polymorphic parallel_map using Toy.fork_join2, then use it to convert a list of bit-lists into a list of strings. Fill in the recursive fork/join implementation.

This exercise is about inferred modes, not efficient parallel mapping. The answer forks one tiny head task against the tail of the list, which is fine for exposing the type but too fine-grained and unbalanced for production code.

The starter leaves the modes off on purpose. After the implementation mentions Toy.fork_join2, the compiler can infer the relevant modes from how the function argument and list flow through the fork/join tree.

Hint

Handle the empty list directly. For a nonempty list, fork one branch for the head and one branch for the tail, then combine the mapped head with the mapped tail.

(* Parallel map exercise *) let bits_to_string bits = let buf = Buffer.create 0 in List.iter (fun bit -> Buffer.add_char buf (if bit then '1' else '0')) bits; Buffer.contents buf let rec parallel_map f xs = failwith "implement this" let bits_to_strings rows = parallel_map bits_to_string rows let () = let rows = [[true; false; true; true]; [false; true; false; false]] in let strings = bits_to_strings rows in print_endline "The output is:"; print_endline (String.concat "\n" strings)

Answer key

The recursive case forks one branch for the head and one branch for the tail, then reconstructs the list after both branches finish. This is intentionally simple so that the inferred type is easy to inspect; it is not how you would usually implement parallel_map in production.

let rec parallel_map f xs =
  match xs with
  | [] -> []
  | x :: xs ->
    let (y, ys) =
      Toy.fork_join2
        (fun () -> f x)
        (fun () -> parallel_map f xs)
    in
    y :: ys

Exercise 5: read the inferred type of `parallel_map`

Checks: reading higher-order mode requirements. If stuck: reread Mode annotation syntax reference.

Paste the answer-key implementation into the editor above and run it; once it compiles, the playground shows the inferred types. You should see a signature shaped like this:

val parallel_map :
  ('a @ shared -> 'b) @ shareable ->
  'a list @ shareable shared ->
  'b list @@ stateless

stateless is a stronger promise on another mode axis. Here we only need one consequence: stateless implies portable, so this implementation can be called from portable code.

For each of the three remaining mode annotations — the @ shareable on the function argument, the @ shared inside it, and the @ shareable shared on the input list — say whether it is a requirement on the caller or a promise by parallel_map, and what it allows or forbids. Then check your reading against the answer.

Answer

Read the type as a contract for moving work into a fork/join tree.

The outer @ shareable in ('a @ shared -> 'b) @ shareable is a requirement on the explicit function argument. parallel_map uses that function inside fork/join branches, so the function value must be available as shareable. This restricts functions that close over mutable state, functions, or other portability-sensitive values.
The inner 'a @ shared is the mode at which parallel_map will provide each element to the function argument. If an element contains mutable state, the function may read that state but may not mutate it. This is why a function such as fun x -> bump_hits x is rejected when bump_hits requires x @ uncontended.
The @ shareable on 'a list @ shareable shared is a portability requirement at the input-list position. Pieces of the list flow into the fork/join tree, so the input must be usable in that context. This restricts element types that contain functions or other portability-sensitive values.
The @ shared on 'a list @ shareable shared is a contention requirement at the same input-list position. parallel_map only gets read-capable access to the list and to the elements it extracts from it, so elements that contain mutable state cannot be mutated through this access.
Together, @ shareable shared shows that one type position can carry requirements from multiple mode axes.
The final @@ stateless is a promise checked against the implementation of parallel_map. stateless is stronger than the portability promise we have been focused on here; the relevant consequence is that this implementation is portable enough to be used from portable code.

Exercise 6: where does `@ portable` attach?

Checks: mode annotation precedence on function types. If stuck: reread Mode annotation syntax reference.

The two blocks below differ only by parentheses around the function type. The function body increments a captured reference, so a block fails exactly when worker itself is being checked as portable. Predict which block is accepted and which is rejected, then explain what the parentheses change about where @ portable attaches.

Answer

The first block is accepted: unit -> unit @ portable parses like unit -> (unit @ portable), so portable is on the result, not on the whole function value worker. The second block fails because (unit -> unit) @ portable does check worker as portable. When the mode belongs to a function value, put that function type in parentheses.

let r = ref 0 let worker : unit -> unit @ portable = fun () -> incr r let r = ref 0 let worker : (unit -> unit) @ portable = fun () -> incr r let r = ref 0 let make : int -> unit -> unit @ portable = fun _ -> fun () -> incr r let r = ref 0 let make : int -> (unit -> unit) @ portable = fun _ -> fun () -> incr r

Exercise 8: why does the ref capture fail?

Checks: what portable closures may capture. If stuck: reread Worked examples: portability requirements on function values.

In the notes, this capture of an immutable integer is accepted:

let factor = 3

let (times_factor @ portable) x =
  x * factor

while this capture of a reference is rejected:

let r = ref 0

let (bad @ portable) () = !r

Why is the immutable capture accepted while the reference capture is rejected?

Answer

The immutable integer cannot be mutated through the captured value. The reference can be read or written through a mutable cell, so moving the closure into a spawned parallel context would need stronger guarantees than an ordinary ref capture provides.

Exercise 9: make the map stop crossing a mode axis

Checks: how key, value, and comparator types determine mode crossing for maps. If stuck: reread Maps also carry comparator evidence.

In the editor in the Maps also carry comparator evidence section, change the key type or the value type so that the map no longer crosses portability, then re-run the block and observe where portable_ok fails. Then make a different change so that the map no longer crosses contention, and observe where contended_ok fails.

Keep Comparator.Make [@modality portable] the same while you experiment. That way the failure comes from the key or value type, not from the comparator witness.

Answer

The simplest changes go through the value type of the map.

Stop crossing portability: make the value type a function, for example type map = (int -> int) Map.M(Key).t. A function value may close over nonportable state, so the map no longer crosses portability and portable_ok is rejected. contended_ok still passes, because the closure itself is immutable.
Stop crossing contention: make the value type mutable, for example type map = int ref Map.M(Key).t. Mutable state does not cross contention, so contended_ok is rejected. portable_ok still passes, because a ref of ints contains no functions.

Changing the key record works the same way: add a function field to stop portability crossing, or a mutable field to stop contention crossing.

Exercise 10: portabilize the Counter signature

Checks: writing portable-by-default module signatures. If stuck: reread Interface annotations make portable APIs reusable.

The editor below defines a Counter module with one abstract type, two ordinary read operations, and one operation that touches global mutable state. Rewrite the signature so that portable is the default, only the global operation opts out, and the abstract type has the strongest valid kind for its representation. For the kind, ask one question per axis: the record has a mutable field, so can it cross contention? It contains no functions, so can it cross portability?

Answer

Put @@ portable on the whole sig, because most of the API should be usable from portable code. Give t the kind value mod portable: the representation has mutable state, so it is not contention-independent, but it does not contain nonportable functions. The immutable field reader can accept t @ contended; the mutable field reader needs t @ shared; the global reset operation must be @@ nonportable.

module Counter : sig @@ portable
  type t : value mod portable

  val create : int -> t
  val id : t @ contended -> int
  val count : t @ shared -> int
  val reset_for_tests : unit -> unit @@ nonportable
end = struct
  type t : value mod portable = { id : int; mutable count : int }

  let create id = { id; count = 0 }
  let id (x @ contended) = x.id
  let count (x @ shared) = x.count

  let all_created = ref []
  let reset_for_tests () = all_created := []
end

module Counter : sig type t val create : int -> t val id : t -> int val count : t -> int val reset_for_tests : unit -> unit end = struct type t = { id : int; mutable count : int } let create id = { id; count = 0 } let id x = x.id let count x = x.count let all_created = ref [] let reset_for_tests () = all_created := [] end

Parallelism: contention and portability

The parallel functions we will use

Toy.fork_join2

Toy.spawn

Parallelism plus mutation can cause bugs

What counts as a data race?

Why OxCaml tracks data races in the type system

First approximation: functions passed to parallel work are checked

Contention modes: read and write access

Ordinary closure

Fork/join closure

Spawn closure

Contention axis

How modes propagate

Function calls check explicit argument mode requirements

Worked example: function calls on parent variable x

Portability modes: function values and hidden captures

Moving access into helpers does not change the rule

Portability axis

List.iter

Toy.fork_join2

Toy.spawn

Explicit argument vs hidden capture

Back to the shared buffer

How captures cross a closure boundary

shareable closure

portable closure

Parallel functions are ordinary typed functions

Mode annotation syntax reference

Worked examples: portability requirements on function values

Portable pure functions

Ordinary closures may capture ordinary refs

Portable closures may capture immutable data

Portable closures reject ordinary ref captures

Portable functions may use fresh local mutation

Mode crossing is a property of a type

Parameterized types cross an axis only when their contents do

Maps also carry comparator evidence

Interface annotations make portable APIs reusable

Portabilizing whole API signatures

Exercises

`Toy.fork_join2`

`Toy.spawn`

Worked example: function calls on parent variable `x`

`List.iter`

`Toy.fork_join2`

`Toy.spawn`

`shareable` closure

`portable` closure