diff --git a/handson_activity/act02_gensym_atomics/gensym_atomics.ml b/handson_activity/act02_gensym_atomics/gensym_atomics.ml
index 6c55d8b..d81fe2d 100644
--- a/handson_activity/act02_gensym_atomics/gensym_atomics.ml
+++ b/handson_activity/act02_gensym_atomics/gensym_atomics.ml
@@ -11,7 +11,7 @@ let gensym =
(* Here's an example of how to use fork_join2 *)
let fork_join_demo par =
- let (l,r) =
+ let #(l,r) =
Parallel.fork_join2 par
(fun _ -> "left")
(fun _ -> "right")
@@ -33,8 +33,7 @@ let gensym_pair par =
let run_parallel ~f =
let module Scheduler = Parallel_scheduler_work_stealing in
let scheduler = Scheduler.create () in
- let monitor = Parallel.Monitor.create_root () in
- let result = Scheduler.schedule scheduler ~monitor ~f in
+ let result = Scheduler.parallel scheduler ~f in
Scheduler.stop scheduler;
result
diff --git a/handson_activity/act03_gensym_capsules/gensym_capsules.ml b/handson_activity/act03_gensym_capsules/gensym_capsules.ml
index 608667b..cb4c17a 100644
--- a/handson_activity/act03_gensym_capsules/gensym_capsules.ml
+++ b/handson_activity/act03_gensym_capsules/gensym_capsules.ml
@@ -2,25 +2,23 @@
stick with the non-atomic references in `gensym`. Use capsules to ensure that
gensym is safe for parallel access (and the code will compile). *)
-open Basement
+open Await
(* Here is an example snippet to show how to create and use capsules. *)
let safe_ref (init : int) =
- (* Create capsule and extract key to bind the type variable *)
- let (P key) = Capsule.create () in
+ (* Create a capsule guarded by a mutex and extract the latter *)
+ let (P mutex) = Capsule.Mutex.create () in
(* Create encapsulated data bound to the same key type *)
let r = Capsule.Data.create (fun () -> ref init) in
- (* Create mutex from key *)
- let mutex = Capsule.Mutex.create key in
(* Access with lock *)
- let read () =
- Capsule.Mutex.with_lock mutex ~f:(fun password ->
- Capsule.Data.extract r ~password ~f:(fun (r : int ref) -> !r))
+ let read (w : Await.t) =
+ Capsule.Mutex.with_lock w mutex ~f:(fun access ->
+ let r = Capsule.Data.unwrap r ~access in !r)
in
- let write (v : int) =
- Capsule.Mutex.with_lock mutex ~f:(fun password ->
- Capsule.Data.extract r ~password ~f:(fun r -> r := v))
+ let write (w : Await.t) v =
+ Capsule.Mutex.with_lock w mutex ~f:(fun access ->
+ let r = Capsule.Data.unwrap r ~access in r := v)
in
(read, write)
@@ -33,21 +31,22 @@ let gensym =
let parallel_read_write par =
let r = safe_ref 0 in
let read, write = r in
- Parallel.fork_join2 par
- (fun _ ->
- for _ = 1 to 1000 do
- ignore (read ())
- done)
- (fun _ ->
- for i = 1 to 1000 do
- write i
- done)
- |> ignore
+ let #((), ()) =
+ Parallel.fork_join2 par
+ (fun _ -> Await_blocking.with_await Terminator.never ~f:(fun w ->
+ for _ = 1 to 1000 do
+ ignore (read w)
+ done))
+ (fun _ -> Await_blocking.with_await Terminator.never ~f:(fun w ->
+ for i = 1 to 1000 do
+ write w i
+ done))
+ in ()
(* Test that gensym produces distinct symbols in parallel *)
let gensym_pair par =
- let s1, s2 =
+ let #(s1, s2) =
Parallel.fork_join2 par (fun _ -> gensym ()) (fun _ -> gensym ())
in
assert (s1 <> s2)
@@ -56,8 +55,7 @@ let gensym_pair par =
let run_parallel ~f =
let module Scheduler = Parallel_scheduler_work_stealing in
let scheduler = Scheduler.create () in
- let monitor = Parallel.Monitor.create_root () in
- let result = Scheduler.schedule scheduler ~monitor ~f in
+ let result = Scheduler.parallel scheduler ~f in
Scheduler.stop scheduler;
result
diff --git a/slides/index.html b/slides/index.html
index fed89dc..37e072a 100644
--- a/slides/index.html
+++ b/slides/index.html
@@ -1,10 +1,20 @@
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
-
OxCaml: safe control over program behavior
-
ICFP’25 Tutorial
-
Gavin Gray, Anil Madhavapeddy, KC Sivaramkrishnan, Richard Eisenberg, Chris Casinghino,
-Will Crichton, Shriram Krishnamurthi, Patrick Ferris, Max Slater, Megan Del Vecchio, Nadia Razek
Safe control over performance-critical aspects of program behavior, in OCaml
-
-
-
Control: over allocation and memory layout
-
-
-
-
Safe: data-race freedom, memory safety
-
-
-
-
in OCaml: OxCaml is a superset of OCaml, so every OCaml program is a valid OxCaml program
-
-
-
Example 1: Safe Stack Allocation
-
let gensym =
+;"object"==typeof exports&&"undefined"!=typeof module&&(module.exports=hljs);</script>
+<script>/*! `ocaml` grammar compiled for Highlight.js 11.9.0 */
+(()=>{var e=(()=>{"use strict";return e=>({name:"OCaml",aliases:["ml"],
+keywords:{$pattern:"[a-z_]\\w*!?",
+keyword:"and as assert asr begin class constraint do done downto else end exception external for fun function functor if in include inherit! inherit initializer land lazy let lor lsl lsr lxor match method!|10 method mod module mutable new object of open! open or private rec sig struct then to try type val! val virtual when while with parser value",
+built_in:"array bool bytes char exn|5 float int int32 int64 list lazy_t|5 nativeint|5 string unit in_channel out_channel ref",
+literal:"true false"},illegal:/\/\/|>>/,contains:[{className:"literal",
+begin:"\\[(\\|\\|)?\\]|\\(\\)",relevance:0},e.COMMENT("\\(\\*","\\*\\)",{
+contains:["self"]}),{className:"symbol",begin:"'[A-Za-z_](?!')[\\w']*"},{
+className:"type",begin:"`[A-Z][\\w']*"},{className:"type",
+begin:"\\b[A-Z][\\w']*",relevance:0},{begin:"[a-z_]\\w*'[\\w']*",relevance:0
+},e.inherit(e.APOS_STRING_MODE,{className:"string",relevance:0
+}),e.inherit(e.QUOTE_STRING_MODE,{illegal:null}),{className:"number",
+begin:"\\b(0[xX][a-fA-F0-9_]+[Lln]?|0[oO][0-7_]+[Lln]?|0[bB][01_]+[Lln]?|[0-9][0-9_]*([Lln]|(\\.[0-9_]*)?([eE][-+]?[0-9_]+)?)?)",
+relevance:0},{begin:/->/}]})})();hljs.registerLanguage("ocaml",e)})();</script>
+ </head>
+ <body>
+ <div id="slipshow-main">
+ <div id="slipshow-content">
+ <svg id="slipshow-drawing-elem" style="overflow:visible; position: absolute; z-index:1000"></svg>
+ <div class="slipshow-rescaler" slip enter-at-unpause>
+<div class="slip">
+<div class="slip-body">
+<div>
+<h1 id="oxcaml-safe-control-over-program-behavior"><a class="anchor" aria-hidden="true" href="#oxcaml-safe-control-over-program-behavior"></a><span>OxCaml: </span><em><span>safe control over program behavior</span></em><span> </span><img style="position: absolute; top:0.5em;left:0.5em;rotate:-15deg;" src="./assets/oxcaml-normal.svg" width="150" height="150" /></h1>
+<h2 id="icfp25-tutorial"><a class="anchor" aria-hidden="true" href="#icfp25-tutorial"></a><span>ICFP’25 Tutorial</span></h2>
+<p><span>Gavin Gray, Anil Madhavapeddy, KC Sivaramkrishnan, Richard Eisenberg, Chris Casinghino,</span>
+<span>Will Crichton, Shriram Krishnamurthi, Patrick Ferris, Max Slater, Megan Del Vecchio, Nadia Razek</span></p>
+<div style="display: grid; grid-template-columns: auto auto;">
+<p><em><span>Before we start, answer this quick question!</span></em></p>
+ <figure>
+ <img src="./assets/qr.svg" width="400" height="400" />
+ <figcaption>
+ <a href="https://tinyurl.com/icfp25-oxcaml"><code>tinyurl.com/icfp25-oxcaml</code></a>
+ </figcaption>
+ </figure>
+</div>
+<div up-at-unpause pause></div>
+<h2 id="oxcaml-provides"><a class="anchor" aria-hidden="true" href="#oxcaml-provides"></a><span>OxCaml provides</span></h2>
+<p><em><span>Safe control</span></em><span> over performance-critical aspects of program behavior, </span><em><span>in OCaml</span></em></p>
+<div pause></div>
+<ul>
+<li><strong><span>Control:</span></strong><span> over allocation and memory layout</span></li>
+</ul>
+<div pause></div>
+<ul>
+<li><strong><span>Safe:</span></strong><span> data-race freedom, memory safety</span></li>
+</ul>
+<div pause></div>
+<ul>
+<li><strong><span>in OCaml:</span></strong><span> OxCaml is a superset of OCaml, so every OCaml program is a valid OxCaml program</span></li>
+</ul>
+<div up-at-unpause pause></div>
+<h1 id="example-1-safe-stack-allocation"><a class="anchor" aria-hidden="true" href="#example-1-safe-stack-allocation"></a><span>Example 1: Safe Stack Allocation</span></h1>
+<pre><code class="language-ocaml">let gensym =
let count = ref 0 in
- fun () ->
+ fun () ->
count := !count + 1;
- "gsym_" ^ (Int.to_string !count)
-
-
-
let perf_critical () =
+ "gsym_" ^ (Int.to_string !count)
+</code></pre>
+<div pause></div>
+<pre><code class="language-ocaml">let perf_critical () =
let symbols = [| gensym (); gensym () |] in
...
-
-
-
-
-
-
-
-
-
-
-
What “bad thing” could happen given these allocations? garbage-collection cycle
-
-
What does the compiler need to know/do to avoid these heap allocations?
-
-
-
Escape analysis: does symbols escape this function region?
-
-
-
-
Update the code to allocate the array on the stack
-
-
-
OxCaml Escape Analysis
-
-
let perf_critical () =
+slip.setClass(el, "correct", true)</script>
+<div pause></div>
+<p><span>What “bad thing” could happen given these allocations? </span><span pause></span><span> </span><em><span>garbage-collection cycle</span></em></p>
+<div center-at-unpause pause></div>
+<p><span>What does the compiler need to know/do to avoid these heap allocations?</span></p>
+<div pause></div>
+<ol>
+<li><span>Escape analysis: does </span><code>symbols</code><span> escape this function region?</span></li>
+</ol>
+<div pause></div>
+<ol start="2">
+<li><span>Update the code to allocate the array on the stack</span></li>
+</ol>
+<div up-at-unpause pause></div>
+<h2 id="oxcaml-escape-analysis"><a class="anchor" aria-hidden="true" href="#oxcaml-escape-analysis"></a><span>OxCaml Escape Analysis</span></h2>
+<div pause></div>
+<pre><code class="language-ocaml">let perf_critical () =
let symbols = [| gensym (); gensym () |] in
...
-
-
-
let perf_critical () =
+</code></pre>
+<div pause></div>
+<pre><code class="language-ocaml">let perf_critical () =
let symbols @ local = [| gensym (); gensym () |] in
...
-
-
-
Every value is either @ local or @ global, the latter is the OCaml default
-
-
A value is @ local if it doesn’t escape the current region
-
-
A value @ localcould be locally allocated
-
-
OxCaml Local Allocation
-
let perf_critical () =
+</code></pre>
+<div pause></div>
+<p><span>Every value is either </span><code>@ local</code><span> or </span><code>@ global</code><span>, the latter is the </span><em><span>OCaml default</span></em></p>
+<div pause></div>
+<p><span>A value is </span><code>@ local</code><span> if it doesn’t escape the current region</span></p>
+<div pause></div>
+<p><span>A value </span><code>@ local</code><span> </span><em><span>could be locally allocated</span></em></p>
+<div up-at-unpause pause></div>
+<h2 id="oxcaml-local-allocation"><a class="anchor" aria-hidden="true" href="#oxcaml-local-allocation"></a><span>OxCaml Local Allocation</span></h2>
+<pre><code class="language-ocaml">let perf_critical () =
let symbols @ local = [| gensym (); gensym () |] in
...
-
-
We assert that symbols is local and doesn’t escape the current region
-
How can we ensure that it’s locally allocated?
-
-
OxCaml provides new keywords for allocation: stack_ and exclave_
-
-
Using stack_
-
let perf_critical () =
+</code></pre>
+<p><span>We assert that </span><code>symbols</code><span> is local and doesn’t escape the current region</span></p>
+<p><em><span>How can we ensure that it’s locally allocated?</span></em></p>
+<div pause></div>
+<p><span>OxCaml provides new keywords for allocation: </span><code>stack_</code><span> and </span><code>exclave_</code></p>
+<div pause></div>
+<h3 id="using-stack_"><a class="anchor" aria-hidden="true" href="#using-stack_"></a><span>Using </span><code>stack_</code></h3>
+<pre><code class="language-ocaml">let perf_critical () =
let symbols @ local = stack_ [| gensym (); gensym () |] in
...
-
-
-
This turns the allocation site for [| |] into a local allocation
-
-
The Local Region
-
The local region is still dynamically sized, but not GC managed. It's cleaned up on function exit
-
-
let perf_critical () =
+</code></pre>
+<div pause></div>
+<p><span>This turns the allocation site for </span><code>[| |]</code><span> into a </span><em><span>local allocation</span></em></p>
+<div center-at-unpause pause></div>
+<h4 id="the-local-region"><a class="anchor" aria-hidden="true" href="#the-local-region"></a><span>The Local Region</span></h4>
+<p><span>The local region is still dynamically sized, but not GC managed. It's cleaned up on function exit</span></p>
+<div style="position: relative; display: grid; grid-template-columns: 1fr 1fr; gap: 1em;">
+<pre><code class="language-ocaml">let perf_critical () =
let symbols = stack_
[| gensym (); gensym () |] in
...
-
stack_ controls the allocation only for the [| |], gensym still allocates the strings on the heap!
-
-
val gensym : unit -> string
-
-
-
val gensym : unit -> string @ global
-
-
-
Local allocation requires cooperation from all callees!
-
-
Using exclave_
-
We may want to use a helper function to create the array
-
let gensym_2 () =
+</code></pre>
+</div>
+<div center-at-unpause pause></div>
+<div style="display: grid; grid-template-rows: 1fr 1fr;">
+<div id="memory-layout-local-correct">
+ <img src="./assets/symbols-local-to-heap.svg" />
+</div>
+ <img src="./assets/symbols-local-inlined.svg" />
+</div>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#memory-layout-local-correct")
+slip.setClass(el, "correct", true)</script>
+<div center-at-unpause pause></div>
+<p><code>stack_</code><span> controls the allocation </span><em><span>only</span></em><span> for the </span><code>[| |]</code><span>, </span><code>gensym</code><span> still allocates the strings on the heap!</span></p>
+<div pause></div>
+<pre><code class="language-ocaml">val gensym : unit -> string
+</code></pre>
+<div pause></div>
+<pre><code class="language-ocaml">val gensym : unit -> string @ global
+</code></pre>
+<div pause></div>
+<p><span>Local allocation requires cooperation from </span><em><span>all callees!</span></em></p>
+<div up-at-unpause pause></div>
+<h3 id="using-exclave_"><a class="anchor" aria-hidden="true" href="#using-exclave_"></a><span>Using </span><code>exclave_</code></h3>
+<p><span>We may want to use a helper function to create the array</span></p>
+<pre id="stack-not-allocation-site"><code class="language-ocaml">let gensym_2 () =
[| gensym (); gensym () |]
let perf_critical () =
let symbols @ local = stack_ (gensym_2 ()) in
...
-
-
-
| let symbols @ local = stack_ (gensym_2 ()) in
+</code></pre>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#stack-not-allocation-site")
+slip.setClass(el, "does-not-compile", true)</script>
+<pre><code> | let symbols @ local = stack_ (gensym_2 ()) in
^^^^^^^^^^^^^
Error: This expression is not an allocation site.
-
-
-
let gensym_2 () =
+</code></pre>
+<div pause></div>
+<pre id="stack-allocation-escapes"><code class="language-ocaml">let gensym_2 () =
stack_ [| gensym (); gensym () |]
let perf_critical () =
let symbols @ local = gensym_2 () in
...
-
stack_ allocates the array local to gensym_2, but we actually want it to be allocated local to perf_critical, the caller.
-
-
let gensym_2 () =
+</code></pre>
+</div>
+</div>
+<div center-at-unpause pause></div>
+<p><code>stack_</code><span> allocates the array local to </span><code>gensym_2</code><span>, but we actually want it to be allocated local to </span><code>perf_critical</code><span>, </span><em><span>the caller.</span></em></p>
+<div up-at-unpause pause></div>
+<pre><code class="language-ocaml">let gensym_2 () =
exclave_ [| gensym (); gensym () |]
-
-
exclave_ allocates the value in the caller’s local region
-
-
-
-
-
-
-
-
-
let perf_critical () =
+</code></pre>
+<p><code>exclave_</code><span> allocates the value in the caller’s local region</span></p>
+<div pause></div>
+<div id="carousel-memory">
+<img class="first" style="display: block;" src="./assets/symbols-to-callers-local-1.svg" />
+<img class="second" style="display: none;" src="./assets/symbols-to-callers-local-2.svg" />
+</div>
+<script type=slip-script exec-at-unpause pause>
+let first = document.querySelector("#carousel-memory .first")
+let second = document.querySelector("#carousel-memory .second")
+slip.setStyle(first, "display", "none")
+slip.setStyle(second, "display", "block")</script>
+<div pause></div>
+<div style="display: grid; grid-template-columns: 1fr 1fr; gap: 0.5em">
+<pre class="does-not-compile"><code class="language-ocaml">let perf_critical () =
let (f, s) = stack_
(gensym (), gensym ()) in
...
f
-
-
let genint =
+</code></pre>
+<pre pause><code class="language-ocaml">let genint =
let count = ref 0 in
- fun () ->
+ fun () ->
count := !count + 1;
!count
@@ -2100,132 +2138,132 @@
@zero_alloc
-
You may want to know if your function is truly zero_alloc
-
let[@zero_alloc] gensym_n n =
- exclave_ Array.init n ~f:(fun _ -> gensym ())
-
-
-
| Array.init n ~f:(fun _ -> gensym ())
+</code></pre>
+</div>
+<div center-at-unpause pause></div>
+<p><span>Integers aren't allocated, so there's no meaningful difference between </span><code>int @ local</code><span> and </span><code>int @ global</code></p>
+<div up-at-unpause pause></div>
+<h3 id="zero_alloc"><a class="anchor" aria-hidden="true" href="#zero_alloc"></a><code>@zero_alloc</code></h3>
+<p><span>You may want to know if your function is truly </span><code>zero_alloc</code></p>
+<pre id="zero-alloc-check"><code class="language-ocaml">let[@zero_alloc] gensym_n n =
+ exclave_ Array.init n ~f:(fun _ -> gensym ())
+</code></pre>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#zero-alloc-check")
+slip.setClass(el, "does-not-compile", true)</script>
+<pre><code> | Array.init n ~f:(fun _ -> gensym ())
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: called function may allocate (external call to caml_make_vect)
-
-
[@zero_alloc] uses an abstract interpreter to check if the extent of your function is zero alloc
-
-
let[@zero_alloc] gensym_n n =
- exclave_ (Array.init[@alloc stack]) n ~f:(fun _ -> gensym ())
-
-
-
| gensym ()
+</code></pre>
+<p><code>[@zero_alloc]</code><span> uses an abstract interpreter to check if the extent of your function is zero alloc</span></p>
+<div pause></div>
+<pre id="zero-alloc-check-2"><code class="language-ocaml">let[@zero_alloc] gensym_n n =
+ exclave_ (Array.init[@alloc stack]) n ~f:(fun _ -> gensym ())
+</code></pre>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#zero-alloc-check-2")
+slip.setClass(el, "does-not-compile", true)</script>
+<pre><code> | gensym ()
^^^^^^^^^
Error: called function may allocate
-
-
Making gensym zero alloc is left as an exercise
-
-
OxCaml So Far
-
We’ve seen new keywords like stack_ and exclave_ that provide control over memory allocation
-
-
We’ve also seen new annotations, like @ local and @ global
-
-
Which can appear on let bindings
-
let perf_critical () =
+</code></pre>
+<p><span>Making </span><code>gensym</code><span> zero alloc is left as an exercise</span></p>
+<div up-at-unpause pause></div>
+<h2 id="oxcaml-so-far"><a class="anchor" aria-hidden="true" href="#oxcaml-so-far"></a><span>OxCaml So Far</span></h2>
+<p><span>We’ve seen new keywords like </span><code>stack_</code><span> and </span><code>exclave_</code><span> that provide control over memory allocation</span></p>
+<div pause></div>
+<p><span>We’ve also seen new annotations, like </span><code>@ local</code><span> and </span><code>@ global</code></p>
+<div pause></div>
+<p><span>Which can appear on let bindings</span></p>
+<pre><code class="language-ocaml">let perf_critical () =
let symbols @ local = gensym_2 () in
...
-
-
And in type signatures
-
val gensym_2 : unit -> string array @ local
+</code></pre>
+<p><span>And in type signatures</span></p>
+<pre><code class="language-ocaml">val gensym_2 : unit -> string array @ local
-val Array.init : int -> f:(int -> 'a) -> 'a array @ global
-
-
-
local and global are instances of OxCaml modes
-
Modes are how how OxCaml provides safety
-
-
A Conceptual Overview of Modes
-
-
-
-
-
Modes are deep properties of values. They refine how values of a type may be used - you can think of types as dividing the universe of values into different buckets, and modes capture cross-cutting properties (e.g., whether a value is stack allocated) that make sense for values of any type.
-
-
Example properties
-
-
-
A value doesn’t escape the region
-
-
-
A value is unique
-
-
-
-
-
A function can be called from any domain (i.e., thread)
-
-
-
-
A function can be invoked at most once
-
-
-
-
and many more ...
-
-
-
Modes provide safety to OxCaml: data-race freedom, and memory safety
Every mode axis has a default value for backwards compatibility with OCaml
-
The default for locality is the global mode
-
-
Mode Crossing: When Modes and Types Work Together
-
let genint =
+</code></pre>
+<div role="region"><table>
+<tr>
+<th><span>Mode</span></th>
+<th><span>Property</span></th>
+</tr>
+<tr>
+<td><code>local</code></td>
+<td><span>Value doesn’t escape the region</span></td>
+</tr>
+<tr>
+<td><strong><code>global</code></strong></td>
+<td></td>
+</tr>
+</table></div></div>
+<p><span>The </span><code>@ local</code><span> is a </span><em><span>mode annotation</span></em></p>
+<div pause></div>
+<p><span>Every mode axis has a default value for backwards compatibility with OCaml</span></p>
+<p><span>The default for locality is the </span><code>global</code><span> mode</span></p>
+<div up-at-unpause pause></div>
+<h3 id="mode-crossing-when-modes-and-types-work-together"><a class="anchor" aria-hidden="true" href="#mode-crossing-when-modes-and-types-work-together"></a><span>Mode Crossing: When Modes and Types Work Together</span></h3>
+<pre><code class="language-ocaml">let genint =
let count = ref 0 in
- fun () ->
+ fun () ->
count := !count + 1;
!count
@@ -2233,38 +2271,38 @@
-
This works because integers cross locality
-
-
Locality property: local values don’t escape the region
-
-
In other words, locally allocated values don’t escape the region
-
If a type upholds the properties of a mode axis, values of that type mode cross
-
-
Example 2: Safe Parallelism
-
OCaml 5 introduced parallel programming with a multicore-aware runtime and effects
-
-
it also unleashed chaos: race conditions, nondeterministic bugs, and hard-to-reason-about code.
-
-
OxCaml introduces two mode axes for data-race freedom: contention and portability
-
-
OCaml 5 introduced a new class of error: Data Races
-
module Par_array = Parallel.Arrays.Array
+</code></pre>
+<p><span>This works because integers </span><em><span>cross</span></em><span> locality</span></p>
+<div pause></div>
+<p><span>Locality property: local values don’t escape the region</span></p>
+<div pause></div>
+<p><span>In other words, </span><em><span>locally allocated</span></em><span> values don’t escape the region</span></p>
+<p class="theorem"><span>If a type upholds the properties of a mode axis, values of that type mode cross</span></p>
+<div up-at-unpause pause></div>
+<h1 id="example-2-safe-parallelism"><a class="anchor" aria-hidden="true" href="#example-2-safe-parallelism"></a><span>Example 2: Safe Parallelism</span></h1>
+<p><span>OCaml 5 introduced parallel programming with a multicore-aware runtime and effects</span></p>
+<div pause></div>
+<p><strong><span>it also unleashed chaos:</span></strong><span> race conditions, nondeterministic bugs, and hard-to-reason-about code.</span></p>
+<div pause></div>
+<p><span>OxCaml introduces two mode axes for data-race freedom: contention and portability</span></p>
+<div up-at-unpause pause></div>
+<h2 id="ocaml-5-introduced-a-new-class-of-error-data-races"><a class="anchor" aria-hidden="true" href="#ocaml-5-introduced-a-new-class-of-error-data-races"></a><span>OCaml 5 introduced a new class of error: Data Races</span></h2>
+<pre id="unsafe-gensym-n"><code class="language-ocaml">module Par_array = Parallel.Arrays.Array
let gensym =
let count = ref 0 in
- fun () ->
+ fun () ->
count := !count + 1;
- "gsym_" ^ (Int.to_string !count)
+ "gsym_" ^ (Int.to_string !count)
let gensym_n par n =
- Par_array.init par n ~f:(fun _ -> gensym ())
-
-
What could happen if gensym_n is called with \(n \geq 2\)?
-
-
Domain 1 Domain 2
+ Par_array.init par n ~f:(fun _ -> gensym ())
+</code></pre>
+<p><span>What could happen if </span><code>gensym_n</code><span> is called with </span>\(n \geq 2\)<span>?</span></p>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#unsafe-gensym-n");
+slip.setClass(el, "does-not-compile", true)</script>
+<pre><code class="language-text">Domain 1 Domain 2
---------------------------------
!count (0)
---------------------------------
@@ -2277,292 +2315,284 @@
It is unsafe to run gensym on multiple domains, we want to statically prevent this from happening
-
-
The code does not compile in OxCaml, but does in OCaml
-
-
Data races require 4 ingredients
-
-
Parallel execution - Code running in different parallel domains (read, threads)
-
Shared memory - A location accessible by multiple domains
-
At least one write - One domain is modifying the data
-
No synchronization - No atomics, etc
-
-
-
let gensym =
+</code></pre>
+<p><span>Resulting array: </span><code>[| "gsym_1"; "gsym_1" |]</code><span> Duplicate symbols? Unexpected!</span></p>
+<div center-at-unpause pause></div>
+<p><span>It is </span><em><span>unsafe</span></em><span> to run </span><code>gensym</code><span> on multiple domains, we want to statically prevent this from happening</span></p>
+<div pause></div>
+<p><span>The code does not compile in OxCaml, but does in OCaml</span></p>
+<div up-at-unpause pause></div>
+<h3 id="data-races-require-4-ingredients"><a class="anchor" aria-hidden="true" href="#data-races-require-4-ingredients"></a><span>Data races require 4 ingredients</span></h3>
+<ol>
+<li><strong><span>Parallel execution</span></strong><span> - Code running in different parallel domains (read, threads)</span></li>
+<li><strong><span>Shared memory</span></strong><span> - A location accessible by multiple domains</span></li>
+<li><strong><span>At least one write</span></strong><span> - One domain is modifying the data</span></li>
+<li><strong><span>No synchronization</span></strong><span> - No atomics, etc</span></li>
+</ol>
+<div pause></div>
+<pre><code class="language-ocaml">let gensym =
let count = ref 0 in (* (2) shared memory *)
(* ^^^^^
(4) bare ref: no synchronization *)
- fun () ->
+ fun () ->
count := !count + 1; (* (3) a write *)
- "gsym_" ^ (Int.to_string !count)
+ "gsym_" ^ (Int.to_string !count)
let gen_many par n =
- (* (1) parallel execution, when n > 1 *)
- Par_array.init par n ~f:(fun _ -> gensym ())
-
-
-
The lambda (fun _ -> gensym ()) must be safe to share across domains
-
-
The function gensym must also be safe to share across domains
-
-
gensym closes over a non-synchronized mutable reference, and reads and writes to it
-
-
Therefore, gensym is not safe to share across domains
-
(fun _ -> gensym ()) is not safe to share across domains
-
-
Modes for Safe Parallelism
-
There are two key mode axes for expressing parallelism constraints
-
-
-
-
Portability: Is this value (function) safe to share across domains?
-
-
portable < nonportable
-
-
-
Mode
-
Property
-
-
-
nonportable
-
Value isn’t shared across domains
-
-
-
portable
-
-
-
-
-
let gensym @ portable =
+ (* (1) parallel execution, when n > 1 *)
+ Par_array.init par n ~f:(fun _ -> gensym ())
+</code></pre>
+<div center-at-unpause pause></div>
+<p><span>The lambda </span><code>(fun _ -> gensym ())</code><span> must be safe to share across domains</span></p>
+<div pause></div>
+<p><span>The function </span><code>gensym</code><span> must also be safe to share across domains</span></p>
+<div pause></div>
+<p><code>gensym</code><span> closes over a non-synchronized mutable reference, and </span><em><span>reads</span></em><span> and </span><em><span>writes</span></em><span> to it</span></p>
+<div pause></div>
+<p><span>Therefore, </span><code>gensym</code><span> is not safe to share across domains</span></p>
+<p><code>(fun _ -> gensym ())</code><span> is not safe to share across domains</span></p>
+<div up-at-unpause pause></div>
+<h2 id="modes-for-safe-parallelism"><a class="anchor" aria-hidden="true" href="#modes-for-safe-parallelism"></a><span>Modes for Safe Parallelism</span></h2>
+<p><span>There are two key mode axes for expressing parallelism constraints</span></p>
+<div pause></div>
+<div id="contention-portability-container">
+<div class="port-area">
+<h3 id="portability is-this-value-function-safe-to-share-across-domains"><a class="anchor" aria-hidden="true" href="#portability is-this-value-function-safe-to-share-across-domains"></a><span>Portability</span><span class="subtitle"><span>: Is this value (function) safe to share across domains?</span></span></h3>
+<div style="display: grid; place-items: center;">
+<p><code>portable < nonportable</code></p>
+<div role="region"><table>
+<tr>
+<th><span>Mode</span></th>
+<th><span>Property</span></th>
+</tr>
+<tr>
+<td><strong><code>nonportable</code></strong></td>
+<td><span>Value isn’t shared across domains</span></td>
+</tr>
+<tr>
+<td><code>portable</code></td>
+<td></td>
+</tr>
+</table></div></div>
+<div id="gensym-par-array-aside" pause-block>
+<pre class="does-not-compile"><code class="language-ocaml">let gensym @ portable =
let count = ref 0 in
- fun () ->
+ fun () ->
count := !count + 1;
- "gsym_" ^ (Int.to_string !count)
+ "gsym_" ^ (Int.to_string !count)
let gen_many par n =
- Par_array.init par n ~f:(fun _ -> gensym ())
-
-
val Par_array.init : Parallel_kernel.t -> int
- -> f:(int -> 'a @ portable) @ portable (* <-- *)
- -> Par_array.t
-
-
-
-
-
-
Contention: What access do I have to this shared memory?
-
-
uncontended < shared < contended
-
-
-
Mode
-
Property
-
-
-
contended
-
Value isn’t read or written
-
-
-
shared
-
Value isn’t written
-
-
-
uncontended
-
-
-
-
-
-
-
-
References captured by portable functions are contended
-
-
let gensym @ portable =
+ Par_array.init par n ~f:(fun _ -> gensym ())
+</code></pre>
+<pre pause><code class="language-ocaml">val Par_array.init : Parallel_kernel.t -> int
+ -> f:(int -> 'a @ portable) @ portable (* <-- *)
+ -> Par_array.t
+</code></pre>
+</div>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#gensym-par-array-aside")
+slip.setStyle(el, "display", "none")</script>
+</div>
+<div class="cont-area">
+<h3 id="contention what-access-do-i-have-to-this-shared-memory"><a class="anchor" aria-hidden="true" href="#contention what-access-do-i-have-to-this-shared-memory"></a><span>Contention</span><span class="subtitle"><span>: What access do I have to this shared memory?</span></span></h3>
+<div style="display: grid; place-items: center;">
+<p><code>uncontended < shared < contended</code></p>
+<div role="region"><table>
+<tr>
+<th><span>Mode</span></th>
+<th><span>Property</span></th>
+</tr>
+<tr>
+<td><code>contended</code></td>
+<td><span>Value isn’t read or written</span></td>
+</tr>
+<tr>
+<td><code>shared</code></td>
+<td><span>Value isn’t written</span></td>
+</tr>
+<tr>
+<td><strong><code>uncontended</code></strong></td>
+<td></td>
+</tr>
+</table></div></div>
+</div>
+</div>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#contention-portability-container")
+slip.setClass(el, "cont-port-container", true)</script>
+<div pause></div>
+<p class="corollary"><span>References captured by portable functions are </span><code>contended</code></p>
+<div style="display: grid; grid-template-columns: 1fr 1fr; gap: 1em; align-items: start;">
+<pre id="gensym-par-array-code"><code class="language-ocaml">let gensym @ portable =
let count = ref 0 in
- fun () ->
+ fun () ->
count := !count + 1;
- "gsym_" ^ (Int.to_string !count)
-
-
-
count := !count + 1;
+ "gsym_" ^ (Int.to_string !count)
+</code></pre>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#gensym-par-array-code")
+slip.setClass(el, "does-not-compile", true)</script>
+<pre><code> count := !count + 1;
^^^^^
Error: This value is contended but
expected to be uncontended.
-
-
-
-
Safely Working with Mutable State
-
Sometimes we actually need shared mutable state, OxCaml provides two types:
-
-
Atomics for simple operations
-
Capsules atomizing complex operations
-
-
-
Atomics
-
let gensym @ portable =
+</code></pre>
+</div>
+<div up-at-unpause pause></div>
+<h2 id="safely-working-with-mutable-state"><a class="anchor" aria-hidden="true" href="#safely-working-with-mutable-state"></a><span>Safely Working with Mutable State</span></h2>
+<p><span>Sometimes we actually need shared mutable state, OxCaml provides two types:</span></p>
+<ol>
+<li><strong><span>Atomics</span></strong><span> for simple operations</span></li>
+<li><strong><span>Capsules</span></strong><span> atomizing complex operations</span></li>
+</ol>
+<div pause></div>
+<h3 id="atomics"><a class="anchor" aria-hidden="true" href="#atomics"></a><span>Atomics</span></h3>
+<pre><code class="language-ocaml">let gensym @ portable =
let count = Atomic.make 0 in
- fun () ->
+ fun () ->
let n = Atomic.fetch_and_add count 1 in
- "gsym_" ^ (Int.to_string n)
-
-
-
Why is using Atomic safe but ref was not? Why does this code type check?
-
-
Atomic.t provides synchronization, therefore it crosses portability and contention
-
-
let make_gensym ?(prefix = "gsym_") () =
+ "gsym_" ^ (Int.to_string n)
+</code></pre>
+<div pause></div>
+<p><em><span>Why is using </span><code>Atomic</code><span> safe but </span><code>ref</code><span> was not? Why does this code type check?</span></em></p>
+<div pause></div>
+<p><code>Atomic.t</code><span> provides synchronization, therefore it </span><strong><span>crosses portability and contention</span></strong></p>
+<div pause></div>
+<pre><code class="language-ocaml">let make_gensym ?(prefix = "gsym_") () =
let count = Atomic.make 0 in
- fun () ->
+ fun () ->
let n = Atomic.fetch_and_add count 1 in
prefix ^ (Int.to_string n)
-
-
-
Can’t race on immutable types, they cross contention
-
-
What if fetch_and_add didn’t exist?
-
let gensym @ portable =
+</code></pre>
+<div pause></div>
+<p><span>Can’t race on immutable types, they cross contention</span></p>
+<div center-at-unpause pause></div>
+<p><span>What if </span><code>fetch_and_add</code><span> didn’t exist?</span></p>
+<pre><code class="language-ocaml">let gensym @ portable =
let count = Atomic.make 0 in
- fun () ->
+ fun () ->
Atomic.incr count;
let n = Atomic.get count in
- "gsym_" ^ (Int.to_string n)
-
-
-
Atomics prevent data races, but not race conditions. What we need is for the read and write to be a single atomic operation
-
-
Capsules
-
If the Atomic.fetch_and_add function didn’t exist, could we still write gensym?
-
-
Associate mutable state with locks, ensuring exclusive access. Capsules use the type system to track which values have access.
-
-
⚠️ A simpler interface is coming, the following may hurt your eyes ⚠️
-
-
let gensym =
- (* 1. Create capsule and get key *)
- let (P key) = Capsule.create () in
-
- (* 2. Create encapsulated data *)
- let counter = Capsule.Data.create (fun () -> ref 0) in
+ "gsym_" ^ (Int.to_string n)
+</code></pre>
+<div pause></div>
+<p><span>Atomics prevent data races, </span><em><span>but not race conditions.</span></em><span> What we need is for the read and write to be a single atomic operation</span></p>
+<div up-at-unpause pause></div>
+<h3 id="capsules"><a class="anchor" aria-hidden="true" href="#capsules"></a><span>Capsules</span></h3>
+<p><span>If the </span><code>Atomic.fetch_and_add</code><span> function didn’t exist, could we still write </span><code>gensym</code><span>?</span></p>
+<div pause></div>
+<p id="capsules" class="definition" title="Capsules"><span>Associate mutable state with locks, ensuring exclusive access. Capsules use the type system to track which values have access.</span></p>
+<div id="capsules" pause></div>
+<pre><code class="language-ocaml">let gensym =
+ (* Create a capsule guarded by a mutex and unpack to get the brand. *)
+ let (P mutex) = Capsule.Mutex.create () in
- let mutex = Capsule.Mutex.create key in (* 3. Create mutex from key *)
+ (* Create encapsulated data bound to the same key brand. *)
+ let counter = Capsule.Data.create (fun () -> ref 0) in
- (* 4. Access with lock *)
- let fetch_and_incr () =
- Capsule.Mutex.with_lock mutex ~f:(fun password ->
- Capsule.Data.extract counter ~password ~f:(fun c ->
- c := !c + 1; !c))
+ (* Access the data, requiring a capability to wait/block. *)
+ let fetch_and_incr (w : Await.t) =
+ Capsule.Mutex.with_lock w mutex ~f:(fun access ->
+ let c = Capsule.Data.unwrap ~access counter in
+ c := !c + 1; !c)
in
- fun () -> "gsym_" ^ (Int.to_string (fetch_and_incr ()))
-
-
-
Activity!
-
We’ve prepared a short activity to help you gauge your understanding of OxCaml
OxCaml “office hours” daily: 3-4 @ the Jane Street booth
-Can’t make it? Email me at gavinleroy@brown.edu
-
-
OxCaml provides safe control over performance-critical aspects of program behavior
-
-
-
New keywords (e.g., stack_ and exclave_) provide control over memory
-
-
-
Modes provide the safety: for memory and parallelism
-
-
-
-
let gensym_n par n =
+ fun w -> "gsym_" ^ Int.to_string (fetch_and_incr w)
+</code></pre>
+<div up-at-unpause pause></div>
+<h1 id="activity"><a class="anchor" aria-hidden="true" href="#activity"></a><span>Activity!</span></h1>
+<p><span>We’ve prepared a short activity to help you gauge your understanding of OxCaml</span></p>
+<div style="display: grid; place-items: center;">
+<p><a href="https://tinyurl.com/oxcaml-icfp25-activity"><code>tinyurl.com/oxcaml-icfp25-activity</code></a></p>
+<img src="./assets/qr-activity.svg" width="500px" height="500px" />
+</div>
+<div up-at-unpause pause></div>
+<h1 id="oxcaml-summary"><a class="anchor" aria-hidden="true" href="#oxcaml-summary"></a><span>OxCaml Summary </span><img style="float: right;" src="./assets/oxcaml-normal.svg" width="200px" height="200px" /></h1>
+<div class="remark">
+<p><span>We have programming activities for those who want to muck around:</span></p>
+<div style="display:grid; place-items:center;"><a href="https://github.com/oxcaml/tutorial-icfp25"><code>github.com/oxcaml/tutorial-icfp25</code></a></div>
+<p><strong><span>OxCaml “office hours” daily:</span></strong><span> 3-4 @ the Jane Street booth</span><br/>
+<em><span>Can’t make it?</span></em><span> Email me at </span><a href="mailto:gavinleroy@brown.edu"><code>gavinleroy@brown.edu</code></a></p>
+</div>
+<p><span>OxCaml provides </span><em><span>safe control</span></em><span> over performance-critical aspects of program behavior</span></p>
+<ul>
+<li>
+<p><span>New keywords (e.g., </span><code>stack_</code><span> and </span><code>exclave_</code><span>) provide control over memory</span></p>
+</li>
+<li>
+<p><span>Modes provide the </span><em><span>safety:</span></em><span> for memory and parallelism</span></p>
+</li>
+</ul>
+<div style="display: flex; flex-direction: row; gap: 0.25em; flex-wrap: wrap; font-size: 1em;">
+<pre><code class="language-ocaml">let gensym_n par n =
Par_array.init par n
- ~f:(fun _ -> gensym ())
+ ~f:(fun _ -> gensym ())
^^^^^^
Error: The value gensym is nonportable,
so cannot be used inside a function
that is portable.
-
-
let[@zero_alloc] gensym_n n = exclave_
+</code></pre>
+<pre><code class="language-ocaml">let[@zero_alloc] gensym_n n = exclave_
(Array.init[@alloc stack])
- n ~f:(fun _ -> gensym ())
+ n ~f:(fun _ -> gensym ())
let perf_critical () =
let symbols @ local = gensym_2 () in
...
-
- 
-
-
-
-
-
-
-
-
-
-
-