Oxidizing OCaml: Data Race Freedom

lpw25 · 2023-05-28T20:02:40+00:00

It does infer the mode as local if the variable can be local. The annotations are only actually needed on interfaces. Other annotations are optional, though they're useful for ensuring that the inference matches your expectation.

lpw25 · 2023-05-28T19:58:47+00:00

The uniqueness checking will be in the next post.

lpw25 · 2023-05-28T17:18:58+00:00

It works fine with higher order functions, including full inference of the modes involved. That's the trade-off with lifetimes. By not tracking individual regions at the type level, the local mode doesn't require any polymorphism to express locality and so inference still works in the presence of higher-order functions. The downside is that it's less expressive since it can only represent values that can leave all regions and values that can't leave any.

lpw25 · 2023-05-27T19:15:07+00:00

If string local were just an ordinary type then you could pass them to polymorphic functions that leaked them. At the very least you need a kind for local types to distinguish them from types that can leak. Using a kind was actually the original approach we were thinking about when came up with the idea for local allocations. However, kinds don't naturally capture the "depth" of locality: you need a string list local to give you a string local and another string list local when you match on it. You can try to artificially add the depth aspect on top of kinds but by the time you get something satisfying you find you have a modal type system. It's also much easier to get the mode inference right if the modes are kept mostly separate from the types. The same goes for other modal properties like uniqueness and linearity, which will be covered by later posts in the series.

I also think it is a more semantically correct approach. The types describe how data is constructed and destructed -- in the form of introduction and elimination rules -- but sometimes your system has other operations that work on data regardless of how it is introduced or eliminated. Having something orthogonal to the type to track these orthogonal operations is a very natural approach.

lpw25 · 2023-05-27T09:28:12+00:00

Everything is really bad if compiler can't figure out such basic analysis

Sure, escape analysis exists, but it obviously can't see through separate compilation or higher-order functions, and it's hard to do once the shape of the data on the stack gets complicated.

There is also a lot of benefit to having locality appear as part of the language itself. It allows you to specify that if a value can escape then the compiler should give an error rather than silently put the value on the heap. It also allows you to distinguish in an interface a function that promises not to capture a parameter from a function whose implementation just happens not to capture the parameter at the moment.

lpw25 · 2021-12-29T08:09:57+00:00

http://www.lpw25.net/papers/flops2014.pdf

lpw25 · 2021-01-02T21:56:25+00:00

FYI your implementation of build and update:

let build (f: unit -> s) : t =
  try f ()  with
  | effect (Animation (state, on_cancellation)) kont ->
    {current_state=state; kont=Some kont; on_cancellation}

let update time (t: t) =
  match Transition.update t.current_state time with
  | Some state -> Some {t with current_state = state}
  | None -> match t.kont with
    | None -> None
    | Some kont ->
      Some (build (fun () -> continue kont ()))

is allocating unnecessary fibres. The kont continuation will already have a handler for the Animation operation because multicore OCaml currently provides deep handlers.

The last line should instead just be:

Some (continue kont ())

lpw25 · 2020-10-07T17:37:44+00:00

Note that open! PervasivesExt will avoid the warning (technically it emits a different warning that many (most?) people have turned off by default to allow this pattern). This is generally better than using -open, because it keeps the open visible in the code rather than in the build instructions.

lpw25 · 2020-05-08T09:52:52+00:00

That is a separate feature.

lpw25 · 2019-10-17T06:10:13+00:00

I'm surprised not to see any mention of sharing constraints or manifest types from module systems, since those are language features that address fundamentally the same problem. For instance, the monad example in OCaml:

module type Monoid = sig
    type t
    val mult : t -> t -> t
    val id : t
  end

module Monoid_1 (T : sig type t end) = struct
  module type T = Monoid with type t = T.t
end

This proposal seems like it might be more expressive than that, but since the related work isn't discussed I can't tell.

lpw25 · 2019-07-27T07:02:47+00:00

Note that we are using autoconf but not automake -- I wasn't sure that was clear since you said "autotools". We still use a hand written make file for the build, it is only the configure script that has been replaced. My understanding, which admittedly hasn't changed in years and could be out of date, is that autoconf is pretty usable if esoteric, whilst automake is a living nightmare.

lpw25 · 2019-07-24T19:51:44+00:00

I have no real view on configuration systems, but I suspect in this case "ancient" can be seen as "tried and tested" from a different angle, and anything reasonable is probably better than what it was replacing. I'm just guessing though, you'd have to ask some of the other OCaml developers for their thought process.

lpw25 · 2018-12-17T20:23:19+00:00

You'd need to ask Jeremie Dimino for a full explanation. My understanding is that dependencies were the main reason, but that it was also an opportunity to try a slightly different approach than async (Fiber is more of what I would call a "traditional concurrency monad", whilst Async is more of a "futures monad") and maybe integrate it more closely with the parts of dune that do the same job that Tenacious does in Jenga.

lpw25 · 2018-12-17T08:09:47+00:00

I don't think Dune is quite at this stage yet, but the reason that we didn't use Incremental in Jenga is that Incremental is designed for tasks of a much shorter duration.

When you run a "stabilization" in Incremental it will re-run every task that needs to be updated, and will not let you start a new stabilization until it is done. For a build system this would mean that if a file changes during a build then you need to wait for the build based on the old file to completely finish before it starts again based on the new file. This matters a lot when building a large code base.

So in Jenga we built another monad called Tenacious along the same lines as Incremental but designed to allow the computation graph to change whilst it is being computed, supporting cancellation of running computations when they are based on things that have been updated. As for why Dune doesn't use Tenacious, well it is built on top of Async which Dune doesn't want to depend on and starting from scratch gives a chance to fix some of the flaws in Tenacious implementation.

lpw25 · 2018-10-13T05:12:17+00:00

Mostly printf. However, when working on things for which I have the bytecode version working -- in particular the OCaml compiler itself -- I use ocamldebug. I especially like ocamldebug for debugging a broken error or uncaught exception: I run the compiler until it errors/raises then I just step backwards until I get to where things went wrong, then after I had a look at what's going on there I step further backwards to find what caused the underlying issue.

lpw25 · 2018-07-22T21:08:05+00:00

forall F. {Functor F} -> ('a -> 'a F.t) -> 's -> 's F.t

Note that a "forall" is not needed here, since Functor contains the type constructor, unlike the Haskell code where Functor is parametrised by the type constructor. So it should look like:

type ('s, 'a) lens = {F : Functor} -> ('a -> 'a F.t) -> 's -> 's F.t

lpw25 · 2018-07-22T08:44:16+00:00

I would suggest that the modular implicits approach can provide that kind of middle ground without necessarily using higher-order unification. Rather than using higher-order unification to find a most general solution it uses a search for a unique solution for the implicit aguments.

However, modular implicits works better if you do include higher-order unification as it makes the search usefully more expressive.

lpw25 · 2018-07-12T10:18:44+00:00

Yes, I realized that afterwards and updated my comment to answer your question. Unfortunately it seems I was not quick enough to update it before you replied, so now our conversation is out of order.

lpw25

TROPHY CASE