author | wenzelm |
Wed, 11 Oct 2023 11:27:01 +0200 | |
changeset 78757 | a094bf81a496 |
parent 78755 | 42e48ad59cda |
child 78762 | 89202852e52c |
permissions | -rw-r--r-- |
71692 | 1 |
(* Title: Pure/Concurrent/isabelle_thread.ML |
28241 | 2 |
Author: Makarius |
3 |
||
71692 | 4 |
Isabelle-specific thread management. |
28241 | 5 |
*) |
6 |
||
71692 | 7 |
signature ISABELLE_THREAD = |
28241 | 8 |
sig |
78648 | 9 |
type T |
78650
47d0c333d155
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
wenzelm
parents:
78648
diff
changeset
|
10 |
val get_thread: T -> Thread.Thread.thread |
78648 | 11 |
val get_name: T -> string |
12 |
val get_id: T -> int |
|
13 |
val equal: T * T -> bool |
|
14 |
val print: T -> string |
|
15 |
val self: unit -> T |
|
16 |
val is_self: T -> bool |
|
78711
3a3a70d4d422
clarified order of modules: early access to interrupt management of Isabelle_Threads;
wenzelm
parents:
78704
diff
changeset
|
17 |
val threads_stack_limit: real Unsynchronized.ref |
78753 | 18 |
val default_stack_limit: unit -> int option |
19 |
type params |
|
20 |
val params: string -> params |
|
21 |
val stack_limit: int -> params -> params |
|
22 |
val interrupts: params -> params |
|
78650
47d0c333d155
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
wenzelm
parents:
78648
diff
changeset
|
23 |
val attributes: params -> Thread.Thread.threadAttribute list |
78648 | 24 |
val fork: params -> (unit -> unit) -> T |
25 |
val is_active: T -> bool |
|
26 |
val join: T -> unit |
|
78681 | 27 |
val interrupt: exn |
28 |
val interrupt_exn: 'a Exn.result |
|
29 |
val interrupt_self: unit -> 'a |
|
30 |
val interrupt_other: T -> unit |
|
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
31 |
structure Exn: EXN |
78714 | 32 |
val expose_interrupt_result: unit -> unit Exn.result |
78740
45ff003d337c
discontinue obsolete "Interrupt" constructor (NB: catch-all pattern produces ML compiler error);
wenzelm
parents:
78720
diff
changeset
|
33 |
val expose_interrupt: unit -> unit (*exception Exn.is_interrupt*) |
78701 | 34 |
val try_catch: (unit -> 'a) -> (exn -> 'a) -> 'a |
35 |
val try_finally: (unit -> 'a) -> (unit -> unit) -> 'a |
|
78688 | 36 |
val try: (unit -> 'a) -> 'a option |
37 |
val can: (unit -> 'a) -> bool |
|
28241 | 38 |
end; |
39 |
||
71692 | 40 |
structure Isabelle_Thread: ISABELLE_THREAD = |
28241 | 41 |
struct |
42 |
||
78648 | 43 |
(* abstract type *) |
44 |
||
78650
47d0c333d155
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
wenzelm
parents:
78648
diff
changeset
|
45 |
abstype T = T of {thread: Thread.Thread.thread, name: string, id: int} |
78648 | 46 |
with |
47 |
val make = T; |
|
48 |
fun dest (T args) = args; |
|
49 |
end; |
|
50 |
||
51 |
val get_thread = #thread o dest; |
|
52 |
val get_name = #name o dest; |
|
53 |
val get_id = #id o dest; |
|
54 |
||
78711
3a3a70d4d422
clarified order of modules: early access to interrupt management of Isabelle_Threads;
wenzelm
parents:
78704
diff
changeset
|
55 |
fun equal (t1, t2) = Thread.Thread.equal (get_thread t1, get_thread t2); |
78648 | 56 |
|
57 |
fun print t = |
|
58 |
(case get_name t of "" => "ML" | a => "Isabelle." ^ a) ^ |
|
78711
3a3a70d4d422
clarified order of modules: early access to interrupt management of Isabelle_Threads;
wenzelm
parents:
78704
diff
changeset
|
59 |
"-" ^ Int.toString (get_id t); |
78648 | 60 |
|
61 |
||
60764 | 62 |
(* self *) |
63 |
||
78648 | 64 |
val make_id = Counter.make (); |
60764 | 65 |
|
66 |
local |
|
78648 | 67 |
val self_var = Thread_Data.var () : T Thread_Data.var; |
60764 | 68 |
in |
69 |
||
78678 | 70 |
fun init_self args = |
71 |
let val t = make args in Thread_Data.put self_var (SOME t); t end; |
|
60830 | 72 |
|
78648 | 73 |
fun self () = |
74 |
(case Thread_Data.get self_var of |
|
75 |
SOME t => t |
|
78678 | 76 |
| NONE => init_self {thread = Thread.Thread.self (), name = "", id = make_id ()}); |
78648 | 77 |
|
78 |
fun is_self t = equal (t, self ()); |
|
60764 | 79 |
|
80 |
end; |
|
81 |
||
82 |
||
83 |
(* fork *) |
|
84 |
||
78711
3a3a70d4d422
clarified order of modules: early access to interrupt management of Isabelle_Threads;
wenzelm
parents:
78704
diff
changeset
|
85 |
val threads_stack_limit = Unsynchronized.ref 0.25; |
3a3a70d4d422
clarified order of modules: early access to interrupt management of Isabelle_Threads;
wenzelm
parents:
78704
diff
changeset
|
86 |
|
78753 | 87 |
fun default_stack_limit () = |
71883 | 88 |
let |
78711
3a3a70d4d422
clarified order of modules: early access to interrupt management of Isabelle_Threads;
wenzelm
parents:
78704
diff
changeset
|
89 |
val limit = Real.floor (! threads_stack_limit * 1024.0 * 1024.0 * 1024.0); |
3a3a70d4d422
clarified order of modules: early access to interrupt management of Isabelle_Threads;
wenzelm
parents:
78704
diff
changeset
|
90 |
in if limit <= 0 then NONE else SOME limit end; |
71883 | 91 |
|
78753 | 92 |
abstype params = Params of {name: string, stack_limit: int option, interrupts: bool} |
93 |
with |
|
94 |
||
95 |
fun make_params (name, stack_limit, interrupts) = |
|
96 |
Params {name = name, stack_limit = stack_limit, interrupts = interrupts}; |
|
97 |
||
98 |
fun params name = make_params (name, default_stack_limit (), false); |
|
99 |
fun stack_limit limit (Params {name, interrupts, ...}) = make_params (name, SOME limit, interrupts); |
|
100 |
fun interrupts (Params {name, stack_limit, ...}) = make_params (name, stack_limit, true); |
|
60764 | 101 |
|
78753 | 102 |
fun params_name (Params {name, ...}) = name; |
103 |
fun params_stack_limit (Params {stack_limit, ...}) = stack_limit; |
|
104 |
fun params_interrupts (Params {interrupts, ...}) = interrupts; |
|
105 |
||
106 |
end; |
|
107 |
||
108 |
fun attributes params = |
|
109 |
Thread.Thread.MaximumMLStack (params_stack_limit params) :: |
|
64557
37074e22e8be
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
wenzelm
parents:
62923
diff
changeset
|
110 |
Thread_Attributes.convert_attributes |
78753 | 111 |
(if params_interrupts params |
112 |
then Thread_Attributes.public_interrupts |
|
113 |
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
|
114 |
|
78753 | 115 |
fun fork params body = |
78648 | 116 |
let |
78677 | 117 |
val self = Single_Assignment.var "self"; |
118 |
fun main () = |
|
119 |
let |
|
78753 | 120 |
val name = params_name params; |
121 |
val t = init_self {thread = Thread.Thread.self (), name = name, id = make_id ()}; |
|
78677 | 122 |
val _ = Single_Assignment.assign self t; |
123 |
in body () end; |
|
124 |
val _ = Thread.Thread.fork (main, attributes params); |
|
125 |
in Single_Assignment.await self end; |
|
28241 | 126 |
|
60764 | 127 |
|
128 |
(* join *) |
|
129 |
||
78650
47d0c333d155
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
wenzelm
parents:
78648
diff
changeset
|
130 |
val is_active = Thread.Thread.isActive o get_thread; |
78648 | 131 |
|
132 |
fun join t = |
|
133 |
while is_active t |
|
52583 | 134 |
do OS.Process.sleep (seconds 0.1); |
135 |
||
60764 | 136 |
|
78681 | 137 |
(* interrupts *) |
60764 | 138 |
|
78681 | 139 |
val interrupt = Thread.Thread.Interrupt; |
140 |
val interrupt_exn = Exn.Exn interrupt; |
|
141 |
||
142 |
fun interrupt_self () = raise interrupt; |
|
143 |
||
144 |
fun interrupt_other t = |
|
78650
47d0c333d155
clarified signature: retain original Poly/ML names Thread.Thread, Thread.Mutex, Thread.ConditionVar and de-emphasize them for Isabelle/ML;
wenzelm
parents:
78648
diff
changeset
|
145 |
Thread.Thread.interrupt (get_thread t) handle Thread.Thread _ => (); |
28550 | 146 |
|
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
147 |
structure Exn: EXN = |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
148 |
struct |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
149 |
open Exn; |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
150 |
val capture = capture0; |
78757 | 151 |
fun capture_body e = capture e (); |
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
152 |
end; |
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
153 |
|
78714 | 154 |
fun expose_interrupt_result () = |
78713 | 155 |
let |
156 |
val orig_atts = Thread_Attributes.safe_interrupts (Thread_Attributes.get_attributes ()); |
|
78755 | 157 |
fun main () = |
158 |
(Thread_Attributes.set_attributes Thread_Attributes.test_interrupts; |
|
159 |
Thread.Thread.testInterrupt ()); |
|
78757 | 160 |
val test = Exn.capture_body main; |
78713 | 161 |
val _ = Thread_Attributes.set_attributes orig_atts; |
78714 | 162 |
in test end; |
163 |
||
164 |
val expose_interrupt = Exn.release o expose_interrupt_result; |
|
78713 | 165 |
|
78701 | 166 |
fun try_catch e f = |
78720 | 167 |
Thread_Attributes.uninterruptible_body (fn run => |
168 |
run e () handle exn => if Exn.is_interrupt exn then Exn.reraise exn else f exn); |
|
78701 | 169 |
|
170 |
fun try_finally e f = |
|
78720 | 171 |
Thread_Attributes.uninterruptible_body (fn run => |
78757 | 172 |
Exn.release (Exn.capture_body (run e) before f ())); |
78701 | 173 |
|
78688 | 174 |
fun try e = Basics.try e (); |
175 |
fun can e = Basics.can e (); |
|
176 |
||
28241 | 177 |
end; |
78715
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
178 |
|
9506b852ebdf
clarified signature: distinction of unmanaged vs. managed interrupts (not implemented yet);
wenzelm
parents:
78714
diff
changeset
|
179 |
structure Exn = Isabelle_Thread.Exn; |