Nicollet.Net

A nice thing about pure functional programming is that it’s inherently thread-safe. Since your code never actually modifies anything, atomicity of operations ceases to be an issue. At the hardware level, every modification operation is performed by a single thread (since it happens while a value is created, but before the high-level semantics can manipulate it) so no error can arise from multiple threads. Every value is basically written by one thread then read by everyone else until it dies.

Except that isn’t always the case. I’ve recently stumbled upon a nasty interaction between Objective Caml threads and pure functional lazy evaluation.

Lazy evaluation is the process of delaying the evaluation of an expression until it’s needed (so that, if it’s never needed, no time is wasted evaluating it). This can be done in Objective Caml through the use of the “lazy” keyword:

let text = lazy (String.concat "," values)

This example delays a costly operation (concatenating a list of strings) until it’s required. Evaluating it requires applying a specific evaluation function:

print_string (Lazy.force text)

The first time a lazy value is forced, it is evaluated. Subsequent reads merely return the already evaluated value. While the semantics of this operation are fairly simple and involve no side-effects, the implementation of it does involve side-effects. Which is why I was very cautious of whether such a mechanism could be used in a thread-safe manner.

Imagine that two threads are provided with an un-evaluated lazy value. Both threads evaluate it at the same time (either on different processors, or on the same processor with time-sharing). Can the evaluation process result in anything other than the evaluation returning the correct value in both threads? It can. There’s a situation where the evaluation can raise an “Undefined” exception (which is quite likely if the evaluation takes a long time) and a less likely situation where the evaluation can cause a segmentation fault or even constitute a security flaw by executing arbitrary code.

The Implementation

The code that handles lazy evaluation looks like this (this is a direct excerpt from the codebase of Objective Caml 3.11.0, any copyrights apply):

let force_lazy_block (blk : 'arg lazy_t) =
  let closure = (Obj.obj (Obj.field (Obj.repr blk) 0) : unit -> 'arg) in
  Obj.set_field (Obj.repr blk) 0 raise_undefined;
  try
    let result = closure () in
    Obj.set_field (Obj.repr blk) 0 (Obj.repr result);  (* do set_field BEFORE set_tag *)
    Obj.set_tag (Obj.repr blk) Obj.forward_tag;
    result
  with e ->
    Obj.set_field (Obj.repr blk) 0 (Obj.repr (fun () -> raise e));
    raise e
;;

Lazy.force inlines a piece of machine code that tests whether the lazy object is already evaluated (its tag is Obj.forward_tag) and, if it isn’t, calls force_lazy_block. The latter (shown above) extracts the evaluation closure, calls it to get the result, and turns the lazy expression into an evaluated object (setting its zeroth field to the result and its tag to Obj.forward_tag). If the expression raises an exception, it remains un-evaluated but turns into a function that throws the exception, so that side-effects are not repeated.

Two race conditions appear here.

First Race Condition

The first is caused when a thread forces the evaluation of a lazy value while another thread is already evaluating it. In order:

• Thread A forces the evaluation.
• Thread A sets field 0 of the lazy block to raise_undefined.
• Thread A starts running closure ().
• Context switch!
• Thread B forces the evaluation.
• Thread B runs closure (), which is now raise_undefined.
• Thread B gets Lazy.Undefined.

This behavior can be readily achieved with a three-line test:

let expr = lazy (Thread.delay 1.0)

let _ =
  let thread = Thread.create (fun () -> Lazy.force expr) () in
  Lazy.force expr; Thread.join thread

The evaluation of the lazy expression explicitly forces a context switch, which causes the second thread to die with the Undefined exception. The same would happen if the runtime forces a context switch during the evaluation of the closure (which is usually a long computation that might warrant it).

Second Race Condition

This one is harder to illustrate due to the nature of context switching in the middle of  a standard library function. It happens if a context switch occurs between the instruction that sets the zeroth field to the evaluated result and the instruction that sets the tag to Obj.forward_tag. Such a switch results in a normal lazy block, which has an arbitrary value as its zeroth field. If another thread attempts to force the value, the runtime will treat that arbitrary value as a closure and execute it. This, in most situations, means death of the program, or perhaps the execution of arbitrary intruder-chosen code if the lazy value is chosen appropriately.