src/Pure/Concurrent/isabelle_thread.ML
author wenzelm
Sun, 05 Apr 2020 13:05:40 +0200
changeset 71692 f8e52c0152fe
parent 64557 src/Pure/Concurrent/standard_thread.ML@37074e22e8be
child 71693 f249b5c0fea2
permissions -rw-r--r--
clarified names;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
71692
f8e52c0152fe clarified names;
wenzelm
parents: 64557
diff changeset
     1
(*  Title:      Pure/Concurrent/isabelle_thread.ML
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     3
71692
f8e52c0152fe clarified names;
wenzelm
parents: 64557
diff changeset
     4
Isabelle-specific thread management.
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     5
*)
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     6
71692
f8e52c0152fe clarified names;
wenzelm
parents: 64557
diff changeset
     7
signature ISABELLE_THREAD =
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
     8
sig
49894
69bfd86cc711 more robust cancel_now: avoid shooting yourself in the foot;
wenzelm
parents: 44112
diff changeset
     9
  val is_self: Thread.thread -> bool
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    10
  val get_name: unit -> string option
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    11
  val the_name: unit -> string
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    12
  type params = {name: string, stack_limit: int option, interrupts: bool}
59468
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents: 59055
diff changeset
    13
  val attributes: params -> Thread.threadAttribute list
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents: 59055
diff changeset
    14
  val fork: params -> (unit -> unit) -> Thread.thread
52583
0a7240d88e09 explicit shutdown of message output thread;
wenzelm
parents: 49894
diff changeset
    15
  val join: Thread.thread -> unit
44112
ef876972fdc1 more explicit Simple_Thread.interrupt_unsynchronized, to emphasize its meaning;
wenzelm
parents: 40232
diff changeset
    16
  val interrupt_unsynchronized: Thread.thread -> unit
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    17
end;
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    18
71692
f8e52c0152fe clarified names;
wenzelm
parents: 64557
diff changeset
    19
structure Isabelle_Thread: ISABELLE_THREAD =
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    20
struct
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    21
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    22
(* self *)
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    23
49894
69bfd86cc711 more robust cancel_now: avoid shooting yourself in the foot;
wenzelm
parents: 44112
diff changeset
    24
fun is_self thread = Thread.equal (Thread.self (), thread);
69bfd86cc711 more robust cancel_now: avoid shooting yourself in the foot;
wenzelm
parents: 44112
diff changeset
    25
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    26
60829
4b16b778ce0d clarified thread name;
wenzelm
parents: 60764
diff changeset
    27
(* unique name *)
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    28
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    29
local
62889
99c7f31615c2 clarified modules;
wenzelm
parents: 62505
diff changeset
    30
  val name_var = Thread_Data.var () : string Thread_Data.var;
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    31
  val count = Counter.make ();
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    32
in
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    33
62889
99c7f31615c2 clarified modules;
wenzelm
parents: 62505
diff changeset
    34
fun get_name () = Thread_Data.get name_var;
60830
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    35
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    36
fun the_name () =
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    37
  (case get_name () of
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    38
    NONE => raise Fail "Unknown thread name"
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    39
  | SOME name => name);
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    40
f56e189350b2 separate channel for debugger output;
wenzelm
parents: 60829
diff changeset
    41
fun set_name base =
62889
99c7f31615c2 clarified modules;
wenzelm
parents: 62505
diff changeset
    42
  Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ())));
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    43
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    44
end;
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    45
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    46
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    47
(* fork *)
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    48
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    49
type params = {name: string, stack_limit: int option, interrupts: bool};
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    50
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    51
fun attributes ({stack_limit, interrupts, ...}: params) =
62501
98fa1f9a292f discontinued polyml-5.3.0;
wenzelm
parents: 61556
diff changeset
    52
  Thread.MaximumMLStack stack_limit ::
64557
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 62923
diff changeset
    53
  Thread_Attributes.convert_attributes
37074e22e8be more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents: 62923
diff changeset
    54
    (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
59468
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents: 59055
diff changeset
    55
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    56
fun fork (params: params) body =
39232
69c6d3e87660 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
wenzelm
parents: 37216
diff changeset
    57
  Thread.fork (fn () =>
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62501
diff changeset
    58
    Exn.trace General.exnMessage tracing (fn () =>
60829
4b16b778ce0d clarified thread name;
wenzelm
parents: 60764
diff changeset
    59
      (set_name (#name params); body ())
62505
9e2a65912111 clarified modules;
wenzelm
parents: 62501
diff changeset
    60
        handle exn => if Exn.is_interrupt exn then () (*sic!*) else Exn.reraise exn),
59468
fe6651760643 explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
wenzelm
parents: 59055
diff changeset
    61
    attributes params);
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    62
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    63
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    64
(* join *)
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    65
52583
0a7240d88e09 explicit shutdown of message output thread;
wenzelm
parents: 49894
diff changeset
    66
fun join thread =
0a7240d88e09 explicit shutdown of message output thread;
wenzelm
parents: 49894
diff changeset
    67
  while Thread.isActive thread
0a7240d88e09 explicit shutdown of message output thread;
wenzelm
parents: 49894
diff changeset
    68
  do OS.Process.sleep (seconds 0.1);
0a7240d88e09 explicit shutdown of message output thread;
wenzelm
parents: 49894
diff changeset
    69
60764
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    70
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    71
(* interrupt *)
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    72
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    73
fun interrupt_unsynchronized thread =
b610ba36e02c more explicit thread identification;
wenzelm
parents: 59468
diff changeset
    74
  Thread.interrupt thread handle Thread _ => ();
28550
422e9bd169ac added fail-safe interrupt;
wenzelm
parents: 28241
diff changeset
    75
28241
de20fccf6509 Simplified thread fork interface.
wenzelm
parents:
diff changeset
    76
end;