-
-
-
-
-
-
-
- Using
-Using
-
-OxCaml Summary
-
- OxCaml: safe control over program behavior
-ICFP’25 Tutorial
-Anil Madhavapeddy, KC Sivaramkrishnan, Richard Eisenberg, Chris Casinghino
-Gavin Gray, Will Crichton, Shriram Krishnamurthi, Patrick Ferris, Max Slater, Megan Del Vecchio, Nadia Razek
-
-
-
-Slides available online: gavinleroy.com/oxcaml-tutorial-icfp25
OxCaml provides
-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></h1>
+<h2 id="icfp25-tutorial"><a class="anchor" aria-hidden="true" href="#icfp25-tutorial"></a><span>ICFP’25 Tutorial</span></h2>
+<p><span>Anil Madhavapeddy, KC Sivaramkrishnan, Richard Eisenberg, Chris Casinghino</span></p>
+<p><span>Gavin Gray, Will Crichton, Shriram Krishnamurthi, Patrick Ferris, Max Slater, Megan Del Vecchio, Nadia Razek</span></p>
+<div style="margin-top: 6em;">
+<p><span>Slides available online: </span><a href="https://gavinleroy.com/oxcaml-tutorial-icfp25/"><code>gavinleroy.com/oxcaml-tutorial-icfp25</code></a></p>
+</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 do we need to know/do to avoid this?
- --
-
- Escape analysis: does
symbolsescape 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 do we need to know/do to avoid this?</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 @ local could 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="display: grid; grid-template-columns: 1fr 1fr; gap: 1em;">
+<pre><code class="language-ocaml">let perf_critical () =
let symbols = stack_
[| gensym () ; gensym () |] in
...
-fn perf_critical() {
+</code></pre>
+<pre><code class="language-rust">fn perf_critical() {
let arena = Arena::new();
let symbols =
arena.alloc([gensym(), gensym()]);
...
}
-
-
-
-
-
-
- 
-
-
-
-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_ [| gensym () ; gensym () |]
+</code></pre>
+<script type=slip-script exec-at-unpause pause>
+let el = document.querySelector("#stack-allocation-escapes")
+slip.setClass(el, "does-not-compile", true)</script>
+<div style="display: grid; grid-template-columns: 1fr 1fr; gap: 1em; position: relative;">
+<pre><code> | stack_ [| gensym () ; gensym () |]
^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^^
Error: This value escapes its region.
-fn gensym_2<'a>() -> &'a [String] {
+</code></pre>
+<img style="position: absolute; top: -0.25em; right: -0.25em; z-index:100;" src="./assets/ferris.svg" width="100px" height="100px">
+<pre class="does-not-compile"><code class="language-rust">fn gensym_2<'a>() -> &'a [String] {
let arena = Arena::new();
return arena.alloc(
[gensym(), gensym()]
);
}
-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 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
-
-
-
-
-
-
-
-
-@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>
+<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 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
-In the second half of the tutorial we’ll make gensym zero alloc
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>In the second half of the tutorial we’ll make </span><code>gensym</code><span> zero alloc</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 init : int -> f:(int -> 'a) -> 'a array @ global
+</code></pre>
+<p><span>And in type signatures</span></p>
+<pre><code class="language-ocaml">val init : int -> f:(int -> 'a) -> 'a array @ global
-val gensym_2 : unit -> string array @ local
-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 and control to OxCaml: data-race freedom, safe control over memory allocation and layout.
- -The Locality Axis
-The locality axis has two modes: local and global
with a submoding relationship of global < local
-
-
-let gensym_2 (): string array @ global =
+val gensym_2 : unit -> string array @ local
+</code></pre>
+<div pause></div>
+<p><code>local</code><span> and </span><code>global</code><span> are instances of OxCaml </span><em><span>modes</span></em></p>
+<p><span>Modes are how how OxCaml provides </span><em><span>safety</span></em></p>
+<div up-at-unpause pause></div>
+<h1 id="a-conceptual-overview-of-modes"><a class="anchor" aria-hidden="true" href="#a-conceptual-overview-of-modes"></a><span>A Conceptual Overview of Modes</span></h1>
+<p id="values-container"><svg xmlns="http://www.w3.org/2000/svg" xmlns:xlink="http://www.w3.org/1999/xlink" xmlns:lucid="lucid" width="1163" height="499.13"><g transform="translate(80 -170.9924320524919)" lucid:page-tab-id="0_0"><path id="green-circle" style="visibility: hidden;" d="M333.9 357.88c27.12 101.18-19.16 201.5-103.35 224.05C146.35 604.5 56.12 540.76 29 439.57 1.9 338.4 48.18 238.07 132.38 215.52c84.2-22.56 174.43 41.17 201.54 142.36z" stroke="#008a0e" stroke-width="6" fill="#e3fae3" opacity=".55"/><path d="M-80 218.66a6 6 0 0 1 6-6H36a6 6 0 0 1 6 6V254a6 6 0 0 1-6 6H-74a6 6 0 0 1-6-6z" fill="none"/><use xlink:href="#a" transform="matrix(1,0,0,1,-75,217.65666666666667) translate(0 29.422222222222224)"/><path id="blue-circle" style="visibility: hidden;" d="M520 450.83c309.28 0 560 41.57 560 92.84 0 51.28-250.72 92.84-560 92.84s-560-41.55-560-92.83c0-51.27 250.72-92.84 560-92.84z" stroke="#1071e5" stroke-width="6" fill="#edf5ff" opacity=".55"/><path d="M860 628.78a6 6 0 0 1 6-6h91.34a6 6 0 0 1 6 6v35.35a6 6 0 0 1-6 6H866a6 6 0 0 1-6-6z" fill="none"/><use xlink:href="#b" transform="matrix(1,0,0,1,865,627.7827910595806) translate(0 29.422222222222224)"/><path d="M181.72 380.9a6 6 0 0 1 6.5-5.48l109.6 9.33a6 6 0 0 1 5.47 6.5l-3 35.2a6 6 0 0 1-6.5 5.48l-109.6-9.34a6 6 0 0 1-5.48-6.5z" fill="none"/><use xlink:href="#c" transform="matrix(0.9963926468233906,0.08486279135332517,-0.08486279135332517,0.9963926468233906,186.7865595672082,380.3146146663196) translate(0 29.422222222222224)"/><path d="M78.1 511.1a6 6 0 0 1 4.8-7.02l144.8-27.28a6 6 0 0 1 7 4.78l6.54 34.74a6 6 0 0 1-4.8 7L91.67 550.6a6 6 0 0 1-7-4.78z" fill="none"/><use xlink:href="#d" transform="matrix(0.9827114579231514,-0.1851437022060278,0.1851437022060278,0.9827114579231514,82.8340227580915,509.1777947113727) translate(0 29.422222222222224)"/><path d="M97.82 297.22a6 6 0 0 1 4.83-6.97l108.22-19.73a6 6 0 0 1 6.98 4.83l6.34 34.77a6 6 0 0 1-4.84 6.98l-108.22 19.72a6 6 0 0 1-6.98-4.83z" fill="none"/><use xlink:href="#e" transform="matrix(0.9837957128643415,-0.17929304322739922,0.17929304322739922,0.9837957128643415,102.55982116223828,295.3438679339185) translate(0 29.422222222222224)"/><path d="M362.26 301.35a6 6 0 0 1 6.63-5.3l72.2 8.2a6 6 0 0 1 5.3 6.63l-3.98 35.1a6 6 0 0 1-6.64 5.3l-72.2-8.18a6 6 0 0 1-5.3-6.63z" fill="none"/><use xlink:href="#f" transform="matrix(0.9936523829624697,0.11249418577422304,-0.11249418577422304,0.9936523829624697,367.3374633795341,300.91817518295255) translate(0 29.422222222222224)"/><path d="M381.67 401.63a6 6 0 0 1 5.33-6.6l183.62-19.75a6 6 0 0 1 6.6 5.32l3.78 35.15a6 6 0 0 1-5.32 6.6L392.06 442.1a6 6 0 0 1-6.6-5.33z" fill="none"/><use xlink:href="#g" transform="matrix(0.9942709500440366,-0.10688909157874266,0.10688909157874266,0.9942709500440366,386.538321427676,400.0988205705683) translate(0 29.422222222222224)"/><path d="M342.8 517.38a6 6 0 0 1 6.4-5.58l128.38 8.74a6 6 0 0 1 5.58 6.4l-2.4 35.26a6 6 0 0 1-6.4 5.58L346 559.03a6 6 0 0 1-5.6-6.4z" fill="none"/><use xlink:href="#h" transform="matrix(0.9976881240025671,0.06795886420650525,-0.06795886420650525,0.9976881240025671,347.86604546006356,516.7199266899072) translate(0 29.422222222222224)"/><path d="M548.75 265.86a6 6 0 0 1 7.14-4.6l235.2 50.95a6 6 0 0 1 4.6 7.15l-7.48 34.54a6 6 0 0 1-7.13 4.58l-235.24-50.94a6 6 0 0 1-4.6-7.13z" fill="none"/><use xlink:href="#i" transform="matrix(0.977341646170929,0.21166791599082405,-0.21166791599082405,0.977341646170929,553.8494333536261,265.9450478108088) translate(0 29.422222222222224)"/><use xlink:href="#j" transform="matrix(0.977341646170929,0.21166791599082405,-0.21166791599082405,0.977341646170929,553.8494333536261,265.9450478108088) translate(74.66666666666667 29.422222222222224)"/><use xlink:href="#k" transform="matrix(0.977341646170929,0.21166791599082405,-0.21166791599082405,0.977341646170929,553.8494333536261,265.9450478108088) translate(130.66666666666669 29.422222222222224)"/><use xlink:href="#l" transform="matrix(0.977341646170929,0.21166791599082405,-0.21166791599082405,0.977341646170929,553.8494333536261,265.9450478108088) translate(186.66666666666669 29.422222222222224)"/><g><path d="M524.04 485.97a6 6 0 0 1 6.55-5.38l406.72 39.88a6 6 0 0 1 5.38 6.56l-3.45 35.17a6 6 0 0 1-6.55 5.4l-406.73-39.9a6 6 0 0 1-5.38-6.55z" fill="none"/></g><g><use xlink:href="#m" transform="matrix(0.9952232586205584,0.09762512740415365,-0.09762512740415365,0.9952232586205584,529.1098896044859,485.4642419301234) translate(0 29.422222222222224)"/><use xlink:href="#n" transform="matrix(0.9952232586205584,0.09762512740415365,-0.09762512740415365,0.9952232586205584,529.1098896044859,485.4642419301234) translate(56 29.422222222222224)"/><use xlink:href="#o" transform="matrix(0.9952232586205584,0.09762512740415365,-0.09762512740415365,0.9952232586205584,529.1098896044859,485.4642419301234) translate(112 29.422222222222224)"/><use xlink:href="#p" transform="matrix(0.9952232586205584,0.09762512740415365,-0.09762512740415365,0.9952232586205584,529.1098896044859,485.4642419301234) translate(186.66666666666669 29.422222222222224)"/><use xlink:href="#q" transform="matrix(0.9952232586205584,0.09762512740415365,-0.09762512740415365,0.9952232586205584,529.1098896044859,485.4642419301234) translate(280 29.422222222222224)"/><use xlink:href="#r" transform="matrix(0.9952232586205584,0.09762512740415365,-0.09762512740415365,0.9952232586205584,529.1098896044859,485.4642419301234) translate(373.33333333333337 29.422222222222224)"/></g><defs><path d="M283-96c58 0 110-29 79-79-30-25-62-31-117-47-91-27-162-58-164-162-3-194 323-203 445-100l-63 93c-49-30-98-45-147-45-53 0-93 23-66 64 70 49 225 51 265 131 13 21 20 49 20 82C533 57 163 54 48-63l79-89c48 37 100 56 156 56" id="s"/><path d="M327-181c-9 94 114 82 169 49l52 101C498 1 440 17 374 17c-132 1-205-70-205-198v-241H58v-109h111v-115l158-19v134h171l-16 109H327v241" id="t"/><path d="M294-412c35-79 80-132 181-135 32 0 61 5 88 16l-29 222H434v-98c-69 14-110 80-131 149v152h105V0H75v-106h70v-320H75v-105h191" id="u"/><path d="M299-809c52-2 94 38 93 89 1 52-40 90-93 89-52 2-95-38-94-89-1-51 42-91 94-89zm95 701h136V0H86v-108h150v-315H91v-108h303v423" id="v"/><path d="M321-432c-45 0-66 30-93 61V0H70v-531h138l11 61c43-46 85-77 165-79 94-1 146 63 146 159V0H372v-344c-2-57-3-88-51-88" id="w"/><path d="M292-548c116 0 174-24 250-68l36 116c-35 14-86 21-153 21 60 28 103 58 103 137 0 138-138 196-287 172-10 4-17 17-17 30 2 51 95 29 146 32 111 6 202 49 202 154 0 133-128 177-284 176-152-2-254-28-257-171h140c0 65 52 65 121 67 74-1 123-6 123-61 0-66-93-53-161-53C163 4 90-26 90-101c0-47 27-81 59-101-59-33-94-70-94-152 0-131 102-194 237-194zm4 103c-52-1-82 37-81 89-1 54 30 91 81 91 55 0 82-35 81-93 0-58-27-87-81-87" id="x"/><g id="a" style="visibility: hidden;"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#s"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#t"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#u"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#v"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,74.66666666666667,0)" xlink:href="#w"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,93.33333333333334,0)" xlink:href="#x"/></g><path d="M375 17c-126 1-186-78-186-204v-447H33v-108h314v575c-5 71 92 68 144 43l37 106c-43 23-94 35-153 35" id="y"/><path d="M300-549c163-2 258 116 258 282 0 171-91 285-258 284C133 18 40-95 42-266s89-279 258-283zm0 117c-81 0-94 69-95 166 2 98 14 167 95 167s93-71 95-168c-1-96-14-165-95-165" id="z"/><path d="M352-108c52-2 81-21 118-45l70 100c-47 39-113 70-197 70C169 14 69-89 69-262c0-174 103-283 277-287 87 1 143 25 194 67l-68 95c-39-27-78-40-119-40-79 0-119 55-119 165-1 98 32 151 118 154" id="A"/><path d="M517-153c0 38 8 53 35 64L519 15c-63-7-105-26-130-70-36 43-99 72-174 72C111 20 34-50 35-150c3-153 155-192 330-181 5-70-27-100-105-101-47 1-106 14-146 28L78-509c57-22 135-39 207-40 155 0 232 63 232 188v208zM269-96c41-1 82-27 96-58v-87c-92-6-167 15-167 80 0 42 27 65 71 65" id="B"/><g id="b" style="visibility: hidden;"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#y"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#z"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#A"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#B"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,74.66666666666667,0)" xlink:href="#y"/></g><path d="M164-739h105l-16 260h-74zm167 0h105l-15 260h-74" id="C"/><path d="M447-538c76 0 102 52 102 146V0h-77v-378c-4-59 6-89-41-94-34 0-65 21-92 63V0h-78v-378c-4-59 6-89-41-94-34 0-65 21-92 63V0H51v-527h65l6 62c29-39 54-71 114-73 49 0 81 23 95 70 29-39 56-70 116-70" id="D"/><path d="M167-234c1 104 57 173 153 175 63-1 97-20 141-47l39 56c-43 34-108 60-180 61C164 13 77-104 79-263c3-156 76-272 229-275 155-3 231 134 213 304H167zm274-64c0-99-41-171-132-171-93 0-138 73-142 171h274" id="E"/><path d="M519-27c-32 22-89 38-142 38-104 2-177-59-177-158v-314H79v-66h121v-119l84-10v129h183l-11 66H284v313C274-41 417-45 486-84" id="F"/><g id="c"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#C"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#D"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#E"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#E"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,74.66666666666667,0)" xlink:href="#F"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,93.33333333333334,0)" xlink:href="#C"/></g><path d="M553-344c1 192-75 355-253 355C119 11 46-148 47-343c3-194 67-357 253-357 179 0 255 163 253 356zm-90 0c0-158-26-283-163-283-136 0-163 126-163 284 0 157 28 281 163 281 136 0 163-124 163-282" id="G"/><path d="M56 0l194-278L79-527h100l122 196 123-196h97L350-282 544 0H442L297-226 152 0H56" id="H"/><path d="M63-345c-4-243 159-405 405-339 31 11 61 28 90 51l-49 57c-41-34-89-51-145-51-146 6-210 112-210 282S215-69 363-63c75 0 116-23 160-57l45 56c-51 50-120 75-206 75C163 3 67-136 63-345" id="I"/><path d="M478-115c0 42 12 57 43 67l-21 60c-51-7-83-32-96-75-34 44-90 74-165 74C137 13 68-51 69-151c3-149 154-179 324-169 10-103-29-151-125-148-40 0-86 9-137 27l-23-64c153-63 370-47 370 137v253zM260-52c60-1 107-35 133-75v-135c-121-4-236-1-234 110 0 67 34 100 101 100" id="J"/><path d="M378 11c-91 1-156-55-156-145v-538H60v-67h246v609c-6 82 110 83 175 53l22 61c-33 18-75 27-125 27" id="K"/><g id="d"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#C"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#G"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#H"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#I"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,74.66666666666667,0)" xlink:href="#J"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,93.33333333333334,0)" xlink:href="#D"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,112.00000000000001,0)" xlink:href="#K"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,130.66666666666669,0)" xlink:href="#C"/></g><path d="M497-619H344v550h153V0H103v-69h153v-550H103v-70h394v70" id="L"/><path d="M225-376h270v70H225V0h-87v-689h406l-10 72H225v241" id="M"/><path d="M557-477c3 190-153 233-355 221V0h-86v-689h175c157 0 265 61 266 212zm-93 1c0-139-119-152-262-144v295c147 7 262-3 262-151" id="N"/><g id="e"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#C"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#L"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#I"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#M"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,74.66666666666667,0)" xlink:href="#N"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,93.33333333333334,0)" xlink:href="#C"/></g><path d="M269-700c124 3 208 70 208 192 0 120-55 176-124 256-43 48-105 107-184 180h324L483 0H73v-68c136-135 216-196 291-327 54-94 26-241-99-234-79 4-106 26-148 73l-58-45c50-62 107-98 210-99" id="O"/><path d="M300-700c172 0 225 159 225 355 0 197-53 356-225 356S75-148 75-345c0-196 53-355 225-355zM163-345c0 192 46 288 137 288s137-96 137-288c0-191-46-287-137-287s-137 96-137 287zm137-65c36-1 67 30 66 65 1 36-30 67-66 66-36 1-66-30-65-66-1-35 29-66 65-65" id="P"/><path d="M297-368c-48 1-64 9-107 23h-68v-344h365l-12 68H203v217c35-21 68-29 118-30 120 0 192 89 189 216C507-75 421 8 277 11c-77 0-143-27-200-82l52-51c42 43 91 64 148 64 96 0 146-63 145-163 2-95-40-145-125-147" id="Q"/><g id="f"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#O"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#P"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#O"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#Q"/></g><path d="M517-68V0H120v-68h169v-529l-157 95-37-59 205-128h74v621h143" id="R"/><path d="M152-14l268-605H97v-70h408v65L230 9" id="S"/><path d="M289-699c157 0 225 106 225 266 4 298-130 391-367 454l-20-64c168-49 290-105 298-294-32 45-87 86-163 85-127-5-196-89-196-220 0-142 85-223 223-227zM154-469c-1 93 36 147 122 149 76-2 117-42 151-92 0-138-19-219-138-219-95 0-135 62-135 162" id="T"/><path d="M269-700c119 2 205 61 211 173 2 81-65 148-134 160 87 6 156 71 156 169C502-24 310 52 146-12c-38-15-69-38-94-68l56-46c32 39 87 67 153 68 92 1 153-51 153-140 4-108-79-141-200-131l10-67c98 9 171-29 171-120 0-74-57-117-130-116-71 2-103 25-146 63l-46-51c56-53 121-80 196-80" id="U"/><path d="M528-167h-89V0h-81v-167H72v-62l202-471 70 30-183 435h198l7-195h73v195h89v68" id="V"/><path d="M506-525c0 85-55 118-119 156 78 33 148 86 148 184C535-55 434 11 298 11 163 11 70-54 65-183c0-77 46-137 139-180-67-33-110-68-110-157 0-118 92-180 206-180 116 0 206 57 206 175zM300-634c-76-1-128 40-124 115 4 95 71 98 152 129 56-37 92-55 96-131 0-72-49-114-124-113zm-2 577c116 0 191-109 126-197-39-53-85-54-163-85-71 33-107 85-107 156 0 83 57 126 144 126" id="W"/><path d="M330-448c126 0 194 84 195 216-3 143-78 243-217 243C129 11 79-132 79-325c0-202 66-365 256-375 50 0 96 14 137 41l-33 56c-82-48-185-39-229 45-30 49-45 117-46 202 38-56 83-92 166-92zM308-57c92 0 132-74 131-172 0-101-41-151-122-151-75 1-121 47-152 98 4 133 26 225 143 225" id="X"/><g id="g"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#R"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#S"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#Q"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#T"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,74.66666666666667,0)" xlink:href="#U"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,93.33333333333334,0)" xlink:href="#V"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,112.00000000000001,0)" xlink:href="#V"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,130.66666666666669,0)" xlink:href="#W"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,149.33333333333334,0)" xlink:href="#V"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,168,0)" xlink:href="#X"/></g><path d="M211-77c-1-48 40-89 88-88 49-2 89 40 88 88 1 49-39 89-88 88-48 1-89-40-88-88" id="Y"/><g id="h"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#U"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#Y"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#R"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#V"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,74.66666666666667,0)" xlink:href="#R"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,93.33333333333334,0)" xlink:href="#Q"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,112.00000000000001,0)" xlink:href="#T"/></g><path d="M184-815h251v72H264V44h171v71H184v-930" id="Z"/><path d="M299-511c45-2 82 37 81 80 1 44-36 84-81 82-44 1-81-38-80-82-1-43 36-82 80-80zm0 345c79 4 94 87 62 160l-82 186h-76l48-198c-59-38-30-152 48-148" id="aa"/><g id="i"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#Z"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#O"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#aa"/></g><g id="j"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#U"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#aa"/></g><g id="k"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#S"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#aa"/></g><path d="M416 115H165V44h171v-787H165v-72h251v930" id="ab"/><g id="l"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#R"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#R"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#ab"/></g><path d="M337 102h-75v-909h75v909" id="ac"/><g id="m"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#Z"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#ac"/></g><g id="n"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#X"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#aa"/></g><g id="o"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#O"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#W"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#aa"/></g><g id="p"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#V"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#T"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#X"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#aa"/></g><g id="q"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#W"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#R"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,37.333333333333336,0)" xlink:href="#O"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,56,0)" xlink:href="#W"/></g><g id="r"><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,0,0)" xlink:href="#ac"/><use transform="matrix(0.031111111111111114,0,0,0.031111111111111114,18.666666666666668,0)" xlink:href="#ab"/></g></defs></g></svg></p>
+<script type=slip-script exec-at-unpause pause>
+let els = document.querySelectorAll(`#values-container > svg g[id='a'], path[id='green-circle']`);
+console.debug("Showing", els);
+els.forEach((el) => {
+ slip.setStyle(el, "visibility", "visible");
+});</script>
+<script type=slip-script exec-at-unpause pause>
+let els = document.querySelectorAll(`#values-container > svg g[id='b'], path[id='blue-circle']`);
+console.debug("Showing", els);
+els.forEach((el) => {
+ slip.setStyle(el, "visibility", "visible");
+});</script>
+<div pause></div>
+<p class="definition" title="What are Modes?"><strong><span>Modes are deep properties of values.</span></strong><span> 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.</span></p>
+<div center-at-unpause pause></div>
+<p><span>Example properties</span></p>
+<ul>
+<li>
+<p><span>A value doesn’t escape the region</span></p>
+</li>
+<li>
+<p><span>A value is unique</span></p>
+</li>
+</ul>
+<div center-at-unpause pause></div>
+<ul>
+<li><span>A function can be called from any domain (i.e., thread)</span></li>
+</ul>
+<div center-at-unpause pause></div>
+<ul>
+<li><span>A function can be invoked at most once</span></li>
+</ul>
+<div center-at-unpause pause></div>
+<ul>
+<li><em><span>and many more ...</span></em></li>
+</ul>
+<div pause></div>
+<p><span>Modes provide safety and control to OxCaml: data-race freedom, safe control over memory allocation and layout.</span></p>
+<div up-at-unpause pause></div>
+<h2 id="the-locality-axis"><a class="anchor" aria-hidden="true" href="#the-locality-axis"></a><span>The Locality Axis</span></h2>
+<p><span>The locality axis has two modes: </span><code>local</code><span> and </span><code>global</code></p>
+<p><span>with a </span><em><span>submoding</span></em><span> relationship of </span><code>global < local</code></p>
+<div style="display: grid; place-items: center;">
+<pre><code class="language-ocaml">let gensym_2 (): string array @ global =
[| gensym () ; gensym () |]
let perf_critical () =
let symbols @ local = gensym_2 () in
(* Type checks because of submoding *)
...
-| Mode | -Property | -
|---|---|
local |
-Value doesn’t escape the region | -
global |
-- |
The @ local is a mode annotation
Every mode axis has a default value for backwards compatibility with OCaml
-The default for locality is the global mode
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>
+<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><code>global</code></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>
+<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)
---------------------------------
@@ -2225,133 +2263,133 @@
Resulting array: [| "gsym_1"; "gsym_1" |] Duplicate symbols? Unexpected!
It is unsafe to run gensym on multiple domains, we want to statically prevent his 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 his 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 |
-Cannot be 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><code>nonportable</code></td>
+<td><span>Cannot be 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 (* <-- *)
- -> t
-
-
-Contention: What access do I have to this shared memory?
-
-
-
-uncontended < shared < contended
| Mode | -Property | -
|---|---|
contended |
-Cannot read or write | -
shared |
-Cannot write | -
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 (* <-- *)
+ -> 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>Cannot </span><em><span>read</span></em><span> or </span><em><span>write</span></em></td>
+</tr>
+<tr>
+<td><code>shared</code></td>
+<td><span>Cannot </span><em><span>write</span></em></td>
+</tr>
+<tr>
+<td><code>uncontended</code></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.
-Mode Crossing: When Modes and Types Work Together
-let gensym_n n =
- List.init n ~f:(fun _ -> genysm ())
+</code></pre>
+</div>
+<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 gensym_n n =
+ List.init n ~f:(fun _ -> genysm ())
let print_hd (ls @ contended) =
let gsym :: _ = ls in
@@ -2359,169 +2397,162 @@
ls is contended because multiple domains hold a reference to it. One domain may have uncontended access to ls, a potential write!
... wait, string list is an immutable type, nobody can write to it ...
We say that values of type string list mode cross along the contention axis
If a type upholds the properties of a mode axis, values of that type mode cross
- -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>
+<p><code>ls</code><span> is contended because multiple domains hold a reference to it. One domain may have uncontended access to </span><code>ls</code><span>, </span><em><span>a potential write!</span></em></p>
+<div pause></div>
+<p><span>... wait, </span><code>string list</code><span> is an immutable type, nobody can write to it ...</span></p>
+<div pause></div>
+<p><span>We say that values of type </span><code>string list</code><span> </span><em><span>mode cross</span></em><span> along the contention axis</span></p>
+<div pause></div>
+<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>
+<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)
-Because Atomic.t provides synchronization, it crosses portability and contention
What if fetch_and_add didn’t exist?
let gensym @ portable =
+ "gsym_" ^ (Int.to_string n)
+</code></pre>
+<div pause></div>
+<p><span>Because </span><code>Atomic.t</code><span> provides synchronization, it crosses portability and contention</span></p>
+<div 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 encapsulated data *)
- let counter = Capsule.Data.create (fun () -> ref 0) in
-
- let (P key) = Capsule.create () in (* 2. Create capsule and get key *)
+ "gsym_" ^ (Int.to_string n)
+</code></pre>
+<div center-at-unpause 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!
-Visit
-
-
-
-and complete a short activity on OxCaml modes! This will help with the live programming in the next half
- -OxCaml Summary 
-
-
-Session resumes at 1600: program in OxCaml and ask the experts anything!
OxCaml “office hours” daily: XXXX-XXXX @ 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_andexclave_) provide control over memory
- -
-
Modes provide the safety: for memory and parallelism
-
-
-
+</code></pre>
+</div>
+</div>
+</div>
+</div>
+</div>
- 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>Visit</span></p>
+<div style="display: grid; place-items: center;">
+<p><a href=""><span>TODO</span></a></p>
+</div>
+<p><span>and complete a short activity on OxCaml modes! This will help with the live programming in the next half</span></p>
+<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><strong><span>Session resumes at 1600:</span></strong><span> </span><em><span>program in OxCaml and ask the experts anything!</span></em><br/></p>
+<p><strong><span>OxCaml “office hours” daily:</span></strong><span> XXXX-XXXX @ 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
...
-
-
- ←
- ⇱
- →
- 0
-