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