author | wenzelm |
Fri, 01 Apr 2022 17:06:10 +0200 | |
changeset 75393 | 87ebf5a50283 |
parent 75380 | 2cb2606ce075 |
child 77409 | d2711c9ffa51 |
permissions | -rw-r--r-- |
71692 | 1 |
/* Title: Pure/Concurrent/isabelle_thread.scala |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
2 |
Author: Makarius |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
3 |
|
71692 | 4 |
Isabelle-specific thread management. |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
5 |
*/ |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
6 |
|
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
7 |
package isabelle |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
8 |
|
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
9 |
|
72192 | 10 |
import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue} |
61563 | 11 |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
12 |
|
75393 | 13 |
object Isabelle_Thread { |
71703 | 14 |
/* self-thread */ |
15 |
||
16 |
def self: Isabelle_Thread = |
|
17 |
Thread.currentThread match { |
|
18 |
case thread: Isabelle_Thread => thread |
|
71717 | 19 |
case thread => error("Isabelle-specific thread required: " + thread) |
71703 | 20 |
} |
21 |
||
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71711
diff
changeset
|
22 |
def check_self: Boolean = |
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71711
diff
changeset
|
23 |
Thread.currentThread.isInstanceOf[Isabelle_Thread] |
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71711
diff
changeset
|
24 |
|
71703 | 25 |
|
71711 | 26 |
/* create threads */ |
71682 | 27 |
|
28 |
private val counter = Counter.make() |
|
29 |
||
75393 | 30 |
def make_name(name: String = "", base: String = "thread"): String = { |
72334 | 31 |
val prefix = "Isabelle." |
32 |
val suffix = if (name.nonEmpty) name else base + counter() |
|
33 |
if (suffix.startsWith(prefix)) suffix else prefix + suffix |
|
34 |
} |
|
71682 | 35 |
|
71683 | 36 |
def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup |
37 |
||
72148 | 38 |
lazy val worker_thread_group: ThreadGroup = |
39 |
new ThreadGroup(current_thread_group, "Isabelle worker") |
|
40 |
||
71711 | 41 |
def create( |
42 |
main: Runnable, |
|
43 |
name: String = "", |
|
44 |
group: ThreadGroup = current_thread_group, |
|
45 |
pri: Int = Thread.NORM_PRIORITY, |
|
46 |
daemon: Boolean = false, |
|
75393 | 47 |
inherit_locals: Boolean = false |
48 |
): Isabelle_Thread = { |
|
71711 | 49 |
new Isabelle_Thread(main, name = make_name(name = name), group = group, |
50 |
pri = pri, daemon = daemon, inherit_locals = inherit_locals) |
|
51 |
} |
|
52 |
||
71685 | 53 |
def fork( |
54 |
name: String = "", |
|
55 |
group: ThreadGroup = current_thread_group, |
|
56 |
pri: Int = Thread.NORM_PRIORITY, |
|
57 |
daemon: Boolean = false, |
|
71690 | 58 |
inherit_locals: Boolean = false, |
75393 | 59 |
uninterruptible: Boolean = false)( |
60 |
body: => Unit |
|
61 |
): Isabelle_Thread = { |
|
71711 | 62 |
val main: Runnable = |
63 |
if (uninterruptible) { () => Isabelle_Thread.uninterruptible { body } } |
|
64 |
else { () => body } |
|
71685 | 65 |
val thread = |
71711 | 66 |
create(main, name = name, group = group, pri = pri, |
67 |
daemon = daemon, inherit_locals = inherit_locals) |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
68 |
thread.start |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
69 |
thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
70 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
71 |
|
71682 | 72 |
|
71703 | 73 |
/* thread pool */ |
71682 | 74 |
|
75393 | 75 |
def max_threads(): Int = { |
72192 | 76 |
val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 |
77 |
if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 |
|
78 |
} |
|
79 |
||
75393 | 80 |
lazy val pool: ThreadPoolExecutor = { |
72192 | 81 |
val n = max_threads() |
71703 | 82 |
val executor = |
83 |
new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) |
|
72148 | 84 |
executor.setThreadFactory( |
85 |
create(_, name = make_name(base = "worker"), group = worker_thread_group)) |
|
71703 | 86 |
executor |
87 |
} |
|
71682 | 88 |
|
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
89 |
|
71702 | 90 |
/* interrupt handlers */ |
91 |
||
75393 | 92 |
object Interrupt_Handler { |
71702 | 93 |
def apply(handle: Isabelle_Thread => Unit, name: String = "handler"): Interrupt_Handler = |
94 |
new Interrupt_Handler(handle, name) |
|
95 |
||
96 |
val interruptible: Interrupt_Handler = |
|
97 |
Interrupt_Handler(_.raise_interrupt, name = "interruptible") |
|
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
98 |
|
71702 | 99 |
val uninterruptible: Interrupt_Handler = |
100 |
Interrupt_Handler(_.postpone_interrupt, name = "uninterruptible") |
|
101 |
} |
|
102 |
||
103 |
class Interrupt_Handler private(handle: Isabelle_Thread => Unit, name: String) |
|
75393 | 104 |
extends Function[Isabelle_Thread, Unit] { |
73340 | 105 |
def apply(thread: Isabelle_Thread): Unit = handle(thread) |
71702 | 106 |
override def toString: String = name |
107 |
} |
|
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
108 |
|
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
109 |
def interrupt_handler[A](handler: Interrupt_Handler)(body: => A): A = |
71710 | 110 |
if (handler == null) body |
111 |
else self.interrupt_handler(handler)(body) |
|
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
112 |
|
71702 | 113 |
def interrupt_handler[A](handle: Isabelle_Thread => Unit)(body: => A): A = |
114 |
self.interrupt_handler(Interrupt_Handler(handle))(body) |
|
115 |
||
116 |
def interruptible[A](body: => A): A = |
|
117 |
interrupt_handler(Interrupt_Handler.interruptible)(body) |
|
118 |
||
119 |
def uninterruptible[A](body: => A): A = |
|
120 |
interrupt_handler(Interrupt_Handler.uninterruptible)(body) |
|
71712
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71711
diff
changeset
|
121 |
|
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71711
diff
changeset
|
122 |
def try_uninterruptible[A](body: => A): A = |
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71711
diff
changeset
|
123 |
if (check_self) interrupt_handler(Interrupt_Handler.uninterruptible)(body) |
c6b7f4da67b3
more robust kill: not always running on Isabelle_Thread (e.g. POSIX_Interrupt handler);
wenzelm
parents:
71711
diff
changeset
|
124 |
else body |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
125 |
} |
71681 | 126 |
|
71711 | 127 |
class Isabelle_Thread private(main: Runnable, name: String, group: ThreadGroup, |
128 |
pri: Int, daemon: Boolean, inherit_locals: Boolean) |
|
75393 | 129 |
extends Thread(group, null, name, 0L, inherit_locals) { |
71681 | 130 |
thread => |
131 |
||
71685 | 132 |
thread.setPriority(pri) |
71681 | 133 |
thread.setDaemon(daemon) |
134 |
||
73340 | 135 |
override def run: Unit = main.run() |
71681 | 136 |
|
71702 | 137 |
def is_self: Boolean = Thread.currentThread == thread |
138 |
||
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
139 |
|
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
140 |
/* interrupt state */ |
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
141 |
|
71702 | 142 |
// synchronized, with concurrent changes |
143 |
private var interrupt_postponed: Boolean = false |
|
144 |
||
75380 | 145 |
def clear_interrupt: Boolean = synchronized { |
71702 | 146 |
val was_interrupted = isInterrupted || interrupt_postponed |
147 |
Exn.Interrupt.dispose() |
|
148 |
interrupt_postponed = false |
|
149 |
was_interrupted |
|
150 |
} |
|
71681 | 151 |
|
75380 | 152 |
def raise_interrupt: Unit = synchronized { |
71702 | 153 |
interrupt_postponed = false |
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
154 |
super.interrupt() |
71681 | 155 |
} |
156 |
||
75380 | 157 |
def postpone_interrupt: Unit = synchronized { |
71702 | 158 |
interrupt_postponed = true |
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
159 |
Exn.Interrupt.dispose() |
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
160 |
} |
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
161 |
|
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
162 |
|
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
163 |
/* interrupt handler */ |
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
164 |
|
71702 | 165 |
// non-synchronized, only changed on self-thread |
166 |
@volatile private var handler = Isabelle_Thread.Interrupt_Handler.interruptible |
|
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
167 |
|
73367 | 168 |
override def interrupt(): Unit = handler(thread) |
71701
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
169 |
|
ca926ef898eb
more general interrupt_handler, with some cascading;
wenzelm
parents:
71694
diff
changeset
|
170 |
def interrupt_handler[A](new_handler: Isabelle_Thread.Interrupt_Handler)(body: => A): A = |
71710 | 171 |
if (new_handler == null) body |
172 |
else { |
|
73120
c3589f2dff31
more informative errors: simplify diagnosis of spurious failures reported by users;
wenzelm
parents:
72334
diff
changeset
|
173 |
require(is_self, "interrupt handler on other thread") |
71682 | 174 |
|
71710 | 175 |
val old_handler = handler |
176 |
handler = new_handler |
|
177 |
try { |
|
73367 | 178 |
if (clear_interrupt) interrupt() |
71710 | 179 |
body |
180 |
} |
|
181 |
finally { |
|
182 |
handler = old_handler |
|
73367 | 183 |
if (clear_interrupt) interrupt() |
71710 | 184 |
} |
71702 | 185 |
} |
71681 | 186 |
} |