author | wenzelm |
Sun, 05 Apr 2020 13:05:40 +0200 | |
changeset 71692 | f8e52c0152fe |
parent 71691 | src/Pure/Concurrent/standard_thread.scala@d682b4000a77 |
child 71693 | f249b5c0fea2 |
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 |
{ |
71682 | 15 |
/* fork */ |
16 |
||
17 |
private val counter = Counter.make() |
|
18 |
||
71683 | 19 |
def make_name(name: String = "", base: String = "thread"): String = |
71682 | 20 |
proper_string(name).getOrElse(base + counter()) |
21 |
||
71683 | 22 |
def current_thread_group: ThreadGroup = Thread.currentThread.getThreadGroup |
23 |
||
71685 | 24 |
def fork( |
25 |
name: String = "", |
|
26 |
group: ThreadGroup = current_thread_group, |
|
27 |
pri: Int = Thread.NORM_PRIORITY, |
|
28 |
daemon: Boolean = false, |
|
71690 | 29 |
inherit_locals: Boolean = false, |
71692 | 30 |
uninterruptible: Boolean = false)(body: => Unit): Isabelle_Thread = |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
31 |
{ |
71690 | 32 |
val main = |
71692 | 33 |
if (uninterruptible) new Runnable { override def run { Isabelle_Thread.uninterruptible { body } } } |
71691 | 34 |
else new Runnable { override def run { body } } |
71685 | 35 |
val thread = |
71692 | 36 |
new Isabelle_Thread(main, name = make_name(name = name), group = group, |
71685 | 37 |
pri = pri, daemon = daemon, inherit_locals = inherit_locals) |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
38 |
thread.start |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
39 |
thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
40 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
41 |
|
71682 | 42 |
|
43 |
/* self */ |
|
44 |
||
71692 | 45 |
def self: Isabelle_Thread = |
71682 | 46 |
Thread.currentThread match { |
71692 | 47 |
case thread: Isabelle_Thread => thread |
71685 | 48 |
case _ => error("Expected to run on Isabelle/Scala standard thread") |
71682 | 49 |
} |
50 |
||
71685 | 51 |
def uninterruptible[A](body: => A): A = self.uninterruptible(body) |
71681 | 52 |
|
39579 | 53 |
|
61563 | 54 |
/* pool */ |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
55 |
|
61559
313eca3fa847
more direct task future implementation, with proper cancel operation;
wenzelm
parents:
61556
diff
changeset
|
56 |
lazy val pool: ThreadPoolExecutor = |
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
56860
diff
changeset
|
57 |
{ |
63805 | 58 |
val m = Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0 |
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
56860
diff
changeset
|
59 |
val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8 |
62056
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
60 |
val executor = |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
61 |
new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable]) |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
62 |
executor.setThreadFactory( |
71692 | 63 |
new Isabelle_Thread(_, name = make_name(base = "worker"), group = current_thread_group)) |
62056
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
64 |
executor |
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
56860
diff
changeset
|
65 |
} |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
66 |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
67 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
68 |
/* delayed events */ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
69 |
|
71692 | 70 |
final class Delay private[Isabelle_Thread]( |
64810 | 71 |
first: Boolean, delay: => Time, log: Logger, event: => Unit) |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
72 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
73 |
private var running: Option[Event_Timer.Request] = None |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
74 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
75 |
private def run: Unit = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
76 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
77 |
val do_run = synchronized { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
78 |
if (running.isDefined) { running = None; true } else false |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
79 |
} |
64810 | 80 |
if (do_run) { |
81 |
try { event } |
|
82 |
catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn } |
|
83 |
} |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
84 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
85 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
86 |
def invoke(): Unit = synchronized |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
87 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
88 |
val new_run = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
89 |
running match { |
62263 | 90 |
case Some(request) => if (first) false else { request.cancel; true } |
91 |
case None => true |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
92 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
93 |
if (new_run) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
94 |
running = Some(Event_Timer.request(Time.now() + delay)(run)) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
95 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
96 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
97 |
def revoke(): Unit = synchronized |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
98 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
99 |
running match { |
62263 | 100 |
case Some(request) => request.cancel; running = None |
101 |
case None => |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
102 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
103 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
104 |
|
61194 | 105 |
def postpone(alt_delay: Time): Unit = synchronized |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
106 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
107 |
running match { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
108 |
case Some(request) => |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
109 |
val alt_time = Time.now() + alt_delay |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
110 |
if (request.time < alt_time && request.cancel) { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
111 |
running = Some(Event_Timer.request(alt_time)(run)) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
112 |
} |
62263 | 113 |
case None => |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
114 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
115 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
116 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
117 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
118 |
// delayed event after first invocation |
64810 | 119 |
def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = |
120 |
new Delay(true, delay, log, event) |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
121 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
122 |
// delayed event after last invocation |
64810 | 123 |
def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = |
124 |
new Delay(false, delay, log, event) |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
125 |
} |
71681 | 126 |
|
71692 | 127 |
class Isabelle_Thread private( |
71685 | 128 |
main: Runnable, |
129 |
name: String = "", |
|
130 |
group: ThreadGroup = null, |
|
131 |
pri: Int = Thread.NORM_PRIORITY, |
|
132 |
daemon: Boolean = false, |
|
133 |
inherit_locals: Boolean = false) |
|
134 |
extends Thread(group, null, name, 0L, inherit_locals) |
|
71681 | 135 |
{ |
136 |
thread => |
|
137 |
||
71685 | 138 |
thread.setPriority(pri) |
71681 | 139 |
thread.setDaemon(daemon) |
140 |
||
71682 | 141 |
override def run { main.run() } |
71681 | 142 |
|
143 |
private var interruptible: Boolean = true |
|
144 |
private var interrupt_pending: Boolean = false |
|
145 |
||
146 |
override def interrupt: Unit = synchronized |
|
147 |
{ |
|
148 |
if (interruptible) super.interrupt() |
|
149 |
else { interrupt_pending = true } |
|
150 |
} |
|
151 |
||
71682 | 152 |
def uninterruptible[A](body: => A): A = |
71681 | 153 |
{ |
71682 | 154 |
require(Thread.currentThread == thread) |
155 |
||
71681 | 156 |
val interruptible0 = synchronized { val b = interruptible; interruptible = false; b } |
157 |
try { body } |
|
158 |
finally { |
|
159 |
synchronized { |
|
160 |
interruptible = interruptible0 |
|
161 |
if (interruptible && interrupt_pending) { |
|
162 |
interrupt_pending = false |
|
163 |
super.interrupt() |
|
164 |
} |
|
165 |
} |
|
71688 | 166 |
Exn.Interrupt.expose() |
71681 | 167 |
} |
168 |
} |
|
169 |
} |