Re: [Caml-list] Threads and "transaction isolation" in OCaml

["Török Edwin" <edwin+ml-ocaml@etorok.net>]

[-- Attachment #1: Type: text/plain, Size: 1115 bytes --]

On 08/16/2013 12:57 AM, Markus Mottl wrote:
> Hi,
> 
> I just wondered how much we can rely on current OCaml-semantics where
> context-switches are impossible as long as there are no allocations.

I wrote a little test program and this is not true for bytecode -vmthread, but seems to work for bytecode -thread and native -thread:
$ ocamlfind ocamlc race.ml -package threads -vmthread -linkpkg -o race && ./race
started
Check OK
worker 2 OK
worker 3 OK
worker 4 OK
worker 5 OK
worker 7 OK
worker 8 OK
worker 9 OK
worker 10 OK
worker 11 OK
worker 12 OK
worker 13 OK
worker 14 OK
worker 0 OK
worker 1 OK
worker 6 OK
worker 15 OK
Array sum inconsistent: -33


> 
> Anyway, is it considered reasonably future-safe to write code of that
> sort?  I'd rather not have new compiler optimizations, etc., interfere
> with these assumptions in the near future.

I'd consider this very fragile as you'd need to know the implementation details of every function you call (or only calling your own safe functions). I was surprised to find out that even Array.fold_left creates a temporary ref for example.

Best regards,
--Edwin

[-- Attachment #2: race.ml --]
[-- Type: text/x-ocaml, Size: 1254 bytes --]

let n = 10000000
let global = Array.init n (fun i -> 0)
let cond = Condition.create ()
let mutex = Mutex.create ()

let rec check_consistent accum i =
  if i >= 0 then
    check_consistent (accum + global.(i)) (i-1)
  else if accum <> 0 then begin
    Printf.eprintf "Array sum inconsistent: %d\n" accum;
    flush stderr;
    exit 1
  end

let rec update_array x i =
  if i < n then begin
    if i mod 2 = 0 then
      global.(i) <- x
    else
      global.(i) <- -x;
    update_array x (i+1)
  end

let start = ref false

let barrier () =
  (* start all threads at same time *)
  Mutex.lock mutex;
  while !start = false do
    Condition.wait cond mutex
  done;
  Mutex.unlock mutex

let worker i =
  barrier ();
  while true; do
    (* the transaction *)
    update_array i 0;
    (* end of transaction *)
    Printf.printf "worker %d OK\n" i;
    flush stdout;
  done

let verifier () =
  barrier ();
  while true; do
    check_consistent 0 (n-1);
    Printf.printf "Check OK\n";
    flush stdout;
  done

let () =
  let a = Array.init 16 (fun i -> Thread.create worker i) in
  let t = Thread.create verifier () in
  start := true;
  Condition.broadcast cond;
  Printf.eprintf "started\n";
  flush stderr;
  Array.iter Thread.join a;
  Thread.join t