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