... but the shared array should still be atomic

(otherwise Array.map can race with Array.get)
This commit is contained in:
Gabriel Scherer 2020-04-06 21:40:56 +02:00
parent d1e7a3a691
commit 7c7a1b327c
1 changed files with 7 additions and 3 deletions

View File

@ -36,7 +36,7 @@ let schedule (job : 'a -> 'b) (tasks : 'a array) : 'b array =
(* shared communication of jobs and results *)
let work_queue = Chan.make max_int in
let results = Array.map (fun _ -> None) tasks in
let results = Atomic.make (Array.map (fun _ -> None) tasks) in
(* worker loop *)
let exception Stop in
@ -49,7 +49,9 @@ let schedule (job : 'a -> 'b) (tasks : 'a array) : 'b array =
(* push all tasks *)
tasks |> Array.iteri (fun i input ->
Chan.send work_queue (fun () -> results.(i) <- Some (job input)));
Chan.send work_queue (fun () ->
let result = job input in
(Atomic.get results).(i) <- Some result));
(* schedule as many Stops as we will have workers *)
for _ = 1 to num_domains do
Chan.send work_queue (fun () -> raise Stop);
@ -61,7 +63,9 @@ let schedule (job : 'a -> 'b) (tasks : 'a array) : 'b array =
Array.iter Domain.join children;
(* at this point all workers are done *)
Array.mapi (fun i -> function None -> assert false | Some v -> v) results
Atomic.get results |> Array.map (function
| None -> assert false
| Some v -> v)
let do_depths min_depth =
let job d =