KC Sivaramakrishnan, a researcher behind Multicore OCaml, writes about effect handlers, memory models, garbage collection and concurrency in OCaml.
HN commenters recommend it for effect handler tutorials and slides, and for his paper on bounding data races, which discusses language memory models.
Multicore OCaml works using a thread-safe generational garbage collector. Each domain (i.e. thread) gets its own minor heap, and the major heap is shared. Each heap is GCd independently. The domain-level minor heaps are restricted so different domains can't write to each other's minor heap. And the shared major heap is protected with more bookkeeping. More details in https://kcsrk.info/multicore/gc/2017/07/06/multicore-ocaml-gc/
Scala of course just uses the set of GCs that are available on the JVM. OCaml's GC has an advantage in that it's optimized for quickly creating and collecting many small objects–perfect for functional programming. But some advanced JVM GCs probably come close to that.
The new effect system is basically 'resumable exceptions'. An effect is declared somewhat similarly to an exception. When the effect is 'thrown', it is handled by the nearest effect handler up the callstack. The difference from an exception is that once (if) it is handled, it actually resumes at the exact position in the code where it left off, not in a continuation created by a closure which is effectively what Scala and every other userland effect system does.
> In Rust it's not even possible to write such code.
What does "such code" mean though? Rust won't let you say that your mutable variables are just shared between threads, because that's unsafe. But if you say OK, I want atomic data types (and so they lack tearing and other things you were bothered about) then you can clone an Arc of them, and write code to manipulate the atomics whose consequences are just as under specified. It's just that now you have to spell out that this is what you wanted, writing e.g. std::sync::atomic::Ordering::Relaxed
If you later complain to me that this code surprised you because the memory ordering wasn't what you expected, I will point at that symbol. If you wanted some specific ordering then "Relaxed" was wrong.
> My point is that the assumption that a == b is invalid if x is a global variable.
No it isn't? This is an important optimisation, which you would prefer to sacrifice rather than just writing what you mean in the first place.
> if you've any relevant references / descriptions of their memory model, let me know!
https://kcsrk.info/papers/pldi18-memory.pdf
> Not sure how that's the same as "doesn't see a reason to solve data races". I see lots of reasons. I just think it is possible to achieve the security goals without it.
If Carbon doesn't prevent data races, then how exactly will it achieve memory safety? Will it implement something like OCaml's "Bounding Data Races in Space and Time"? [0]
If we ignore compiler optimizations, the problem with data races is that it may make you observe tearing (incomplete writes) and thus it's almost impossible to maintain safety invariants with them. But the job of a safe low level language is to give tools for the programmer to guarantee correctness of the unsafe parts. In the presence of data races, this is infeasible. So even if you find a way to ensure that data races aren't technically UB, data races happening in a low level language surely lead to UB elsewhere.
Ultimately this may end up showing as CVEs related to memory safety so I don't think you can achieve your security goals without preventing data races.
[0] https://kcsrk.info/papers/pldi18-memory.pdf
The canonical way to do concurrency these days is with a monadic library like Lwt or Async, which is a mechanism akin to promises/deferreds. They have their own implementations of channels/events/streams/what-call-you-it.
There is some interesting work being done on an effects system [1] which would be another option for type-safe concurrency, hopefully it will land soon alongside the multicore work.
There is also the old fashioned way with the stdlib's Event module[2] (in conjunction with Thread), but that's not used as often, mostly because Lwt/Async offer richer, safer abstractions.
[1] http://kcsrk.info/ocaml/multicore/2015/05/20/effects-multicore/
[2] http://caml.inria.fr/pub/docs/manual-ocaml/libref/Event.html
Multicore is picking up pace, and there will be a paper on the formalised memory model at this year's OCaml Workshop in Oxford in September.
There are a series of milestones to hit: the runtime GC, the memory model, the low-level programming model using one-shot continuations, and how it affects libraries running over it (e.g. algebraic effects). Each of these have associated papers and talks (see the ocamllabs.ionews section), so it's not quite fair to compare it to Duke Nukem Forever :-)
Some quick links to recent papers:
- memory model: http://kcsrk.info/papers/memory_model_ocaml17.pdf
- programming model: http://kcsrk.info/papers/awkward_effects_ml17.pdf
Indeed, Irmin is a library to implement data stores which can be freely cloned, updated and merged along a model similar to git.
It separates the content from the actual store. So it can run as well on a file-system, on a git repository, in memory or in the browser (See for instance https://github.com/talex5/irmin-js).
As git, Irmin uses 3-way merge but applied to arbitrary values and not only files. As described here http://gazagnaire.org/pub/FGM15.pdf and generalized here
https://kcsrk.info/papers/oopsla19-mrdt.pdf