more explicit thread identification;
authorwenzelm
Tue Jul 21 14:12:45 2015 +0200 (2015-07-21)
changeset 60764b610ba36e02c
parent 60763 b8170925c848
child 60765 e43e71a75838
more explicit thread identification;
src/HOL/Tools/Sledgehammer/async_manager_legacy.ML
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/event_timer.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/simple_thread.ML
src/Pure/System/message_channel.ML
     1.1 --- a/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Jul 21 14:07:06 2015 +0200
     1.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager_legacy.ML	Tue Jul 21 14:12:45 2015 +0200
     1.3 @@ -28,7 +28,8 @@
     1.4        Runtime.debugging NONE body () handle exn =>
     1.5          if Exn.is_interrupt exn then ()
     1.6          else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
     1.7 -      Simple_Thread.attributes {stack_limit = NONE, interrupts = interrupts});
     1.8 +      Simple_Thread.attributes
     1.9 +        {name = "async_manager", stack_limit = NONE, interrupts = interrupts});
    1.10  
    1.11  val message_store_limit = 20
    1.12  val message_display_limit = 10
     2.1 --- a/src/Pure/Concurrent/bash.ML	Tue Jul 21 14:07:06 2015 +0200
     2.2 +++ b/src/Pure/Concurrent/bash.ML	Tue Jul 21 14:12:45 2015 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4      val _ = cleanup_files ();
     2.5  
     2.6      val system_thread =
     2.7 -      Simple_Thread.fork {stack_limit = NONE, interrupts = false} (fn () =>
     2.8 +      Simple_Thread.fork {name = "bash", stack_limit = NONE, interrupts = false} (fn () =>
     2.9          Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    2.10            let
    2.11              val _ = File.write script_path script;
     3.1 --- a/src/Pure/Concurrent/event_timer.ML	Tue Jul 21 14:07:06 2015 +0200
     3.2 +++ b/src/Pure/Concurrent/event_timer.ML	Tue Jul 21 14:12:45 2015 +0200
     3.3 @@ -104,7 +104,9 @@
     3.4  
     3.5  fun manager_check manager =
     3.6    if is_some manager andalso Thread.isActive (the manager) then manager
     3.7 -  else SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} manager_loop);
     3.8 +  else
     3.9 +    SOME (Simple_Thread.fork {name = "event_timer", stack_limit = NONE, interrupts = false}
    3.10 +      manager_loop);
    3.11  
    3.12  fun shutdown () =
    3.13    uninterruptible (fn restore_attributes => fn () =>
     4.1 --- a/src/Pure/Concurrent/future.ML	Tue Jul 21 14:07:06 2015 +0200
     4.2 +++ b/src/Pure/Concurrent/future.ML	Tue Jul 21 14:12:45 2015 +0200
     4.3 @@ -264,7 +264,7 @@
     4.4        Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
     4.5      val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
     4.6      val worker =
     4.7 -      Simple_Thread.fork {stack_limit = stack_limit, interrupts = false}
     4.8 +      Simple_Thread.fork {name = "worker", stack_limit = stack_limit, interrupts = false}
     4.9          (fn () => worker_loop name);
    4.10    in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
    4.11    handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
    4.12 @@ -366,7 +366,9 @@
    4.13   (do_shutdown := false;
    4.14    if scheduler_active () then ()
    4.15    else
    4.16 -    scheduler := SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} scheduler_loop));
    4.17 +    scheduler :=
    4.18 +      SOME (Simple_Thread.fork {name = "scheduler", stack_limit = NONE, interrupts = false}
    4.19 +        scheduler_loop));
    4.20  
    4.21  
    4.22  
     5.1 --- a/src/Pure/Concurrent/simple_thread.ML	Tue Jul 21 14:07:06 2015 +0200
     5.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Tue Jul 21 14:12:45 2015 +0200
     5.3 @@ -7,7 +7,8 @@
     5.4  signature SIMPLE_THREAD =
     5.5  sig
     5.6    val is_self: Thread.thread -> bool
     5.7 -  type params = {stack_limit: int option, interrupts: bool}
     5.8 +  val identification: unit -> string option
     5.9 +  type params = {name: string, stack_limit: int option, interrupts: bool}
    5.10    val attributes: params -> Thread.threadAttribute list
    5.11    val fork: params -> (unit -> unit) -> Thread.thread
    5.12    val join: Thread.thread -> unit
    5.13 @@ -17,24 +18,52 @@
    5.14  structure Simple_Thread: SIMPLE_THREAD =
    5.15  struct
    5.16  
    5.17 +(* self *)
    5.18 +
    5.19  fun is_self thread = Thread.equal (Thread.self (), thread);
    5.20  
    5.21 -type params = {stack_limit: int option, interrupts: bool};
    5.22 +
    5.23 +(* identification *)
    5.24 +
    5.25 +local
    5.26 +  val tag = Universal.tag () : string Universal.tag;
    5.27 +  val count = Counter.make ();
    5.28 +in
    5.29 +
    5.30 +fun identification () = Thread.getLocal tag;
    5.31  
    5.32 -fun attributes {stack_limit, interrupts} =
    5.33 +fun set_identification name =
    5.34 +  Thread.setLocal (tag, name ^ ":" ^ string_of_int (count ()));
    5.35 +
    5.36 +end;
    5.37 +
    5.38 +
    5.39 +(* fork *)
    5.40 +
    5.41 +type params = {name: string, stack_limit: int option, interrupts: bool};
    5.42 +
    5.43 +fun attributes ({stack_limit, interrupts, ...}: params) =
    5.44    maximum_ml_stack stack_limit @
    5.45    (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
    5.46  
    5.47 -fun fork params body =
    5.48 +fun fork (params: params) body =
    5.49    Thread.fork (fn () =>
    5.50      print_exception_trace General.exnMessage tracing (fn () =>
    5.51 -      body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
    5.52 +      (set_identification (#name params); body ())
    5.53 +        handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
    5.54      attributes params);
    5.55  
    5.56 +
    5.57 +(* join *)
    5.58 +
    5.59  fun join thread =
    5.60    while Thread.isActive thread
    5.61    do OS.Process.sleep (seconds 0.1);
    5.62  
    5.63 -fun interrupt_unsynchronized thread = Thread.interrupt thread handle Thread _ => ();
    5.64 +
    5.65 +(* interrupt *)
    5.66 +
    5.67 +fun interrupt_unsynchronized thread =
    5.68 +  Thread.interrupt thread handle Thread _ => ();
    5.69  
    5.70  end;
     6.1 --- a/src/Pure/System/message_channel.ML	Tue Jul 21 14:07:06 2015 +0200
     6.2 +++ b/src/Pure/System/message_channel.ML	Tue Jul 21 14:12:45 2015 +0200
     6.3 @@ -60,7 +60,8 @@
     6.4      let
     6.5        val mbox = Mailbox.create ();
     6.6        val thread =
     6.7 -        Simple_Thread.fork {stack_limit = NONE, interrupts = false} (message_output mbox channel);
     6.8 +        Simple_Thread.fork {name = "channel", stack_limit = NONE, interrupts = false}
     6.9 +          (message_output mbox channel);
    6.10        fun send msg = Mailbox.send mbox (SOME msg);
    6.11        fun shutdown () =
    6.12          (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);