author | wenzelm |
Wed, 29 Jul 2015 13:34:04 +0200 | |
changeset 60830 | f56e189350b2 |
parent 60829 | 4b16b778ce0d |
child 60923 | 020becec359c |
permissions | -rw-r--r-- |
28241 | 1 |
(* Title: Pure/Concurrent/simple_thread.ML |
2 |
Author: Makarius |
|
3 |
||
28577
bd2456e0d944
added generic combinator for synchronized evaluation (formerly in future.ML);
wenzelm
parents:
28550
diff
changeset
|
4 |
Simplified thread operations. |
28241 | 5 |
*) |
6 |
||
7 |
signature SIMPLE_THREAD = |
|
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 |
||
37216
3165bc303f66
modernized some structure names, keeping a few legacy aliases;
wenzelm
parents:
33605
diff
changeset
|
19 |
structure Simple_Thread: SIMPLE_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 |
|
30 |
val tag = Universal.tag () : string Universal.tag; |
|
31 |
val count = Counter.make (); |
|
32 |
in |
|
33 |
||
60830 | 34 |
fun get_name () = Thread.getLocal tag; |
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 = |
|
42 |
Thread.setLocal (tag, 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) = |
|
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
|
52 |
maximum_ml_stack stack_limit @ |
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 () => |
59055
5a7157b8e870
more informative failure of protocol commands, with exception trace;
wenzelm
parents:
59054
diff
changeset
|
57 |
print_exception_trace General.exnMessage tracing (fn () => |
60829 | 58 |
(set_name (#name params); body ()) |
60764 | 59 |
handle exn => if Exn.is_interrupt exn then () (*sic!*) else 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; |