Skip to content

Parallelism tutorial #3886

New issue

Have a question about this project? Sign up for a free GitHub account to open an issue and contact its maintainers and the community.

By clicking “Sign up for GitHub”, you agree to our terms of service and privacy statement. We’ll occasionally send you account related emails.

Already on GitHub? Sign in to your account

Draft
wants to merge 17 commits into
base: main
Choose a base branch
from
Draft

Conversation

lukemaurer
Copy link
Contributor

@lukemaurer lukemaurer commented Apr 17, 2025

Basic introduction to data-race-free parallelism, focusing on fork/join parallelism and data parallelism provided by the parallel library as a way to introduce the portable and contended modes.

Currently pretty drafty:

  • Needs an introduction
  • Should probably be reorganized a bit—the section on portable and contended was supposed to be sort of an intermission but it's the biggest part
  • Possibly a bit too formal in places? I think having numbered rules for things is good but then I've written conference papers
  • Some of the example code could be more motivated: a Thing.t is just something with an immutable price and a mutable mood. (If nothing else, if my time at a trading firm has taught me anything, it's that prices are in fact mutable.)
  • Other not-quite-finished bits
Siteproxy
@lukemaurer lukemaurer added the documentation Improvements or additions to documentation label Apr 17, 2025
@mshinwell mshinwell added the drf Data race freedom label Apr 17, 2025
Copy link
Collaborator

@goldfirere goldfirere left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Nice tutorial. I enjoyed reading it.

I wondered in one of my inline comments about whether we want all the general portability/contention stuff in this tutorial. But after reflecting about this with @ccasin, I think it's good. We'll have general documentation for this stuff. But pointing readers to it in the middle of the tutorial is annoying, and the general documentation will inevitably have more detail than is needed at this point. So the stuff here might be duplicative, but I think on balance it's good duplication.

Happy to chat about anything here if you'd like.

unpredictable number of those changes. The only way to stop _that_ is to use
something more sophisticated like a lock over the whole tree, which grants a
function `uncontended` access while the lock is held. That's what the capsule
API is for, but it's beyond the scope of this tutorial.
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it's helpful to remind readers at this point that while our structures do not prevent non-deterministic or racy behavior, they do prevent memory corruption.

Copy link
Contributor

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I wouldn't say memory corruption exactly since the memory model already prevents undefined behavior. Maybe state corruption?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hmm. I'm learning that my belief in what DRF prevents was imprecise. I'll ask Stephen when he's in tomorrow

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Good point about memory corruption. I had been neglecting that fact about the memory model. Maybe our type system only prevents memory corruption in the presence of unboxed products like internal pointers? That is, a data race on a mutable unboxed product -- where one element in the product determines the validity of another -- can cause arbitrary memory corruption. But OCaml does not have such products natively. We're about to add them -- in the next week or two, according to @ccasin. So once we have such things, despite the guarantees the memory model gives us, then we'll have the possibility for memory corruption. And our type system prevents it. We both giveth and taketh away.

Neglecting this corner case (around dependent unboxed products), I'm honestly not sure what we gain with DRF.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Added a whole section to the beginning about this, having talked with Stephen. The headline is we get sequential consistency (but of course I have to explain what that is).

|> Option.value ~default:0
```

We first need to convert from `iarray` to `Parallel.Sequence.t`, a general
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Link to documentation?

requiring a definition of an unfolding state with an operation that splits it in
half.

**[I made a solution for this but unless there's something I missed that would
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Hard for me to see exactly where this is going, so I don't have much of an opinion here. I do like the idea of generalizing the initial example to something a little harder.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think folks reading this may also want to be able to observe the speedup. Though I don't think you should spend a lot of time explaining benchmarking or anything, I think it would be a valuable addition to show an actual executable that can be run to get timing measurements -- and then to show that parallelism can speed things up.

Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Might be nice to have a little summary at the end. This would include tips like "look at the Parallel library" or "benchmark after parallelizing". It could also maybe have all your Rules stated together in a little table.

Also use the word “domain,” not “thread”
Copy link
Collaborator

@goldfirere goldfirere left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Really happy with where this is going!

@@ -1,38 +1,162 @@
# Parallelism Tutorial
# Simple Parallelism Without Data Races
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Love the title


# Introduction

# Fork/join parallelism
OCaml 5 unleashed parallel programming for the OCaml ecosystem. As is often the
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
OCaml 5 unleashed parallel programming for the OCaml ecosystem. As is often the
OCaml 5 unleashed parallel programming on the OCaml ecosystem. As is often the

? Probably just kidding.

case when something is unleashed, this has quite a bit of potential to cause
chaos. **[Need to quit fussing with this so I'm leaving it as is for the moment,
but am I saying we're putting the leash back on? Leashes are good, actually? Or
maybe we're putting up a fence so the the multicore dog can run around without
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I kinda like the leash idea. Leashes keep dogs safe, but still allow them out to roam around.

One thing to check: ask around your office whether people know what "leash" means. The term of art in the UK, as I understand it, is "lead". But hopefully "leash" is commonly understood.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Decided in the end to keep the line but not extend the metaphor.


Suppose we're working with binary trees, and we want to take an average over all
the values in the tree. Here's a basic implementation:
OxCaml aims to provide an infrastructure for multicore OCaml programming that
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
OxCaml aims to provide an infrastructure for multicore OCaml programming that
OxCaml provides an infrastructure for multicore OCaml programming that

OxCaml aims to provide an infrastructure for multicore OCaml programming that
exploits the full power of parallelism while _guaranteeing_ freedom from an
especially pernicious threat, that of the _data race._ That infrastructure
includes many parts, from common primitives like atomics and locks to newer
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
includes many parts, from common primitives like atomics and locks to newer
includes many parts, from common primitives like atomics and locks to more exotic

? Modes aren't actually all that new, in the scheme of things. Just likely new to the reader.

We'll cover the details in the section on [mode crossing], but the short answer
is that since `float`s are immutable, no data race can arise from them, so the
compiler simply ignores `contended` and `uncontended` on `float`s (and you can
make use of this for your own immutable data as well).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Suggested change
make use of this for your own immutable data as well).
make use of this for your own deeply immutable data as well).

function around (in other words, the record could be a function [in a
trenchcoat]). So we have to forbid _all accesses_ of `nonportable` values from
other domains, not just function calls. The good news is that many types (in
fact, most types) obviously _can't_ cause a problem—you'll never make an `(int *
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Wrong kind of dash?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think an em dash is correct here? Used parenthetically?

other domains, not just function calls. The good news is that many types (in
fact, most types) obviously _can't_ cause a problem—you'll never make an `(int *
string option) list` that contains _any_ function, much less one that will cause
a data race—and if the compiler is aware that a type `t` can't have a function
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Other end of "wrong kind of dash?"

`mutable_data`, and `value`. Some kinds constrain what types they describe, and
in return types with those kinds get to cross certain modes. In summary (this
table isn't nearly exhaustive—in particular, there are many modes we haven't
covered, and `immutable_data` and `mutable_data` cross some of them as well):
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Link to the now-extant kinds documentation somewhere around here.

Comment on lines 853 to 854
only reason it gets to return an `uncontended` `float` is that `float` crosses
contention (which is to say, it has kind `immutable_data`).
Copy link
Collaborator

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Groan. Very sadly, float : immutable_data no longer holds. The problem is that immutable_data expands to value mod ... non_float. So, yeah, not float.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

That's absolutely tragic.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Thought about hand-waving this a bit but I think it's easiest just to delete the parenthetical. There's already the blurb after the table that introduces the idea that some special types don't have these exact kinds but do cross those modes.

Copy link

@jonludlam jonludlam left a comment

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Generally really nice, I feel I've got a much better understanding of this now. I think mainly my comments are to ensure that anyone trying to follow along with a code editor doesn't get tripped up. In fact, if you want to encourage someone doing that, then a bit of detail at the start of how to set it up would be useful.

```ocaml
let test_add4 par = add4 par 1 10 100 1000

let%expect_test "add4 in parallel" =

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

It probably wouldn't hurt to avoid extra PPXs in the examples - it's introducing more variations from 'stock' OCaml and makes actually building the examples harder.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, good point. Probably fine to just use a top-level printf here and put the result of execution in the next text box?


```
The value Thing.price is nonportable, so cannot be used inside a function that
is portable.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I got a slightly different error:

File "test.ml", line 73, characters 22-27:
73 |           (fun par -> total par l)
                           ^^^^^
Error: The value total is nonportable, so cannot be used inside a function that is portable.

which doesn't make it quite as obvious to fix as the text suggests!

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Whoops, yeah I lost track that I'd already added a @ portable in my test code


type t =
{ price : float
; mutable mood : Mood.t

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

When I did this the compiler grumbled at me that mood was never mutated - I know it's mutated later in the tutorial, but for someone following along it's a stumbling block.

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Ah, thanks—we seem to have that warning turned off

If you modify our test code to run `average_par_things` on a test tree like

```ocaml
let test_tree =

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it'd be useful to move this up a little - I'd made my own test_tree before I got here!

```

```
Error: This value is contended but expected to be uncontended.

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I didn't get this, I got

88 |     Parallel.fork_join2 par (fun _par -> Thing.cheer_up t) (fun _par -> Thing.bum_out t)
                                              ^^^^^^^^^^^^^^
Error: The value Thing.cheer_up is nonportable, so cannot be used inside a function that is portable.

though I had to modify things slightly, so I'm not entirely sure it's not possible to get the 'contended' error

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Oh! I never did say to add @@ portable to those functions, so that makes sense.

<a id="rule-contended-submode"></a>
> **Rule 3.** An `uncontended` value may be used as though it is `contended`.

This is entirely consistent with rules 1 and 2: having an `uncontended` value

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I suspect these two audiences are quite different, e.g. relative familiarity with the ppxs that I mentioned above. I imagine that writing for the non-JS audience won't cause the JS audience to get too annoyed though, though you'll definitely have a better sense of that than me!

missing information on `price`:

```ocaml
val price : t @ contended -> float @@ portable

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

I think it might be worth mentioning explicitly the scoping rules here, that the @ contended applies to t but the @@ portable applies to price

| | `contended` | `portable` |
|--------|-------------|------------|
| Rule 1 | No parallel `uncontended` accesses | Only `portable` values may cross domains |
| Rule 2 | No accessing `contended` `mutable` state | A `portable` function only sees `portable` `contended` values |

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Are there deep symmetries here, or have you just numbered the rules so that they match well? 3 and 4 are obviously related, but are 1 and 2?

Copy link
Contributor Author

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

The only analogy really is that rule 1 is a global soundness property and rule 2 is a typing rule. I wasn't sure there's a good way to get that across without straying into POPL territory, though


The three most important kinds for data-race freedom are `immutable_data`,
`mutable_data`, and `value`. Some kinds constrain what types they describe, and
in return types with those kinds get to cross certain modes. In summary (this

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

'crossing' hasn't been defined yet


So for example, we can take this .mli:

```ocaml

Choose a reason for hiding this comment

The reason will be displayed to describe this comment to others. Learn more.

Perhaps explicitly use thing.mli here, as you mention below that we take out the @@portable

Sign up for free to join this conversation on GitHub. Already have an account? Sign in to comment
Labels
documentation Improvements or additions to documentation drf Data race freedom
Projects
None yet
Development

Successfully merging this pull request may close these issues.

None yet

5 participants