# HG changeset patch
# User wenzelm
# Date 1530887387 -7200
# Node ID d465b396ef85075d3469a041357b7c9d9cd33004
# Parent  afa7c5a239e6a2ed34715705eed707f8b642da99
just one global lock for group status: avoid proliferation of mutexes, condvars;

diff -r afa7c5a239e6 -r d465b396ef85 src/Pure/Concurrent/task_queue.ML
--- a/src/Pure/Concurrent/task_queue.ML	Fri Jul 06 15:35:48 2018 +0200
+++ b/src/Pure/Concurrent/task_queue.ML	Fri Jul 06 16:29:47 2018 +0200
@@ -62,12 +62,13 @@
 abstype group = Group of
  {parent: group option,
   id: int,
-  status: exn option Synchronized.var}
+  status: exn option Unsynchronized.ref}
 with
 
 fun make_group (parent, id, status) = Group {parent = parent, id = id, status = status};
 
-fun new_group parent = make_group (parent, new_id (), Synchronized.var "group_status" NONE);
+fun new_group parent =
+  make_group (parent, new_id (), Unsynchronized.ref NONE);
 
 fun group_id (Group {id, ...}) = id;
 fun eq_group (group1, group2) = group_id group1 = group_id group2;
@@ -78,17 +79,32 @@
 
 (* group status *)
 
-fun cancel_group (Group {status, ...}) exn =
-  Synchronized.change status
-    (fn exns => SOME (Par_Exn.make (exn :: the_list exns)));
+local
+
+fun is_canceled_unsynchronized (Group {parent, status, ...}) =
+  is_some (! status) orelse
+    (case parent of NONE => false | SOME group => is_canceled_unsynchronized group);
+
+fun group_status_unsynchronized (Group {parent, status, ...}) =
+  the_list (! status) @
+    (case parent of NONE => [] | SOME group => group_status_unsynchronized group);
+
+val lock = Mutex.mutex ();
+fun SYNCHRONIZED e = Multithreading.synchronized "group_status" lock e;
 
-fun is_canceled (Group {parent, status, ...}) =
-  is_some (Synchronized.value status) orelse
-    (case parent of NONE => false | SOME group => is_canceled group);
+in
+
+fun cancel_group (Group {status, ...}) exn =
+  SYNCHRONIZED (fn () =>
+    Unsynchronized.change status (fn exns => SOME (Par_Exn.make (exn :: the_list exns))));
 
-fun group_status (Group {parent, status, ...}) =
-  the_list (Synchronized.value status) @
-    (case parent of NONE => [] | SOME group => group_status group);
+fun is_canceled group =
+  SYNCHRONIZED (fn () => is_canceled_unsynchronized group);
+
+fun group_status group =
+  SYNCHRONIZED (fn () => group_status_unsynchronized group);
+
+end;
 
 fun str_of_group group =
   (is_canceled group ? enclose "(" ")") (string_of_int (group_id group));