author | wenzelm |
Wed, 06 Apr 2016 16:33:33 +0200 | |
changeset 62889 | 99c7f31615c2 |
parent 62505 | 9e2a65912111 |
child 62923 | 3a122e1e352a |
permissions | -rw-r--r-- |
61556 | 1 |
(* Title: Pure/Concurrent/standard_thread.ML |
28241 | 2 |
Author: Makarius |
3 |
||
61556 | 4 |
Standard thread operations. |
28241 | 5 |
*) |
6 |
||
61556 | 7 |
signature STANDARD_THREAD = |
28241 | 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 | 10 |
val get_name: unit -> string option |
11 |
val the_name: unit -> string |
|
60764 | 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 | 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 | 17 |
end; |
18 |
||
61556 | 19 |
structure Standard_Thread: STANDARD_THREAD = |
28241 | 20 |
struct |
21 |
||
60764 | 22 |
(* self *) |
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 | 26 |
|
60829 | 27 |
(* unique name *) |
60764 | 28 |
|
29 |
local |
|
62889 | 30 |
val name_var = Thread_Data.var () : string Thread_Data.var; |
60764 | 31 |
val count = Counter.make (); |
32 |
in |
|
33 |
||
62889 | 34 |
fun get_name () = Thread_Data.get name_var; |
60830 | 35 |
|
36 |
fun the_name () = |
|
37 |
(case get_name () of |
|
38 |
NONE => raise Fail "Unknown thread name" |
|
39 |
| SOME name => name); |
|
40 |
||
41 |
fun set_name base = |
|
62889 | 42 |
Thread_Data.put name_var (SOME (base ^ "/" ^ string_of_int (count ()))); |
60764 | 43 |
|
44 |
end; |
|
45 |
||
46 |
||
47 |
(* fork *) |
|
48 |
||
49 |
type params = {name: string, stack_limit: int option, interrupts: bool}; |
|
50 |
||
51 |
fun attributes ({stack_limit, interrupts, ...}: params) = |
|
62501 | 52 |
Thread.MaximumMLStack stack_limit :: |
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
|
53 |
(if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts); |
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
|
54 |
|
60764 | 55 |
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
|
56 |
Thread.fork (fn () => |
62505 | 57 |
Exn.trace General.exnMessage tracing (fn () => |
60829 | 58 |
(set_name (#name params); body ()) |
62505 | 59 |
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
|
60 |
attributes params); |
28241 | 61 |
|
60764 | 62 |
|
63 |
(* join *) |
|
64 |
||
52583 | 65 |
fun join thread = |
66 |
while Thread.isActive thread |
|
67 |
do OS.Process.sleep (seconds 0.1); |
|
68 |
||
60764 | 69 |
|
70 |
(* interrupt *) |
|
71 |
||
72 |
fun interrupt_unsynchronized thread = |
|
73 |
Thread.interrupt thread handle Thread _ => (); |
|
28550 | 74 |
|
28241 | 75 |
end; |