author | wenzelm |
Sat, 04 Apr 2020 20:16:25 +0200 | |
changeset 71688 | 220d19f3e074 |
parent 71685 | d5773922358d |
child 71690 | fef74c06cfac |
permissions | -rw-r--r-- |
61556 | 1 |
/* Title: Pure/Concurrent/standard_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 |
|
61556 | 4 |
Standard thread operations. |
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 |
|
61556 | 13 |
object Standard_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, |
|
29 |
inherit_locals: Boolean = false)(body: => Unit): Standard_Thread = |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
30 |
{ |
71682 | 31 |
val main = new Runnable { override def run { body } } |
71685 | 32 |
val thread = |
33 |
new Standard_Thread(main, name = make_name(name = name), group = group, |
|
34 |
pri = pri, daemon = daemon, inherit_locals = inherit_locals) |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
35 |
thread.start |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
36 |
thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
37 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
38 |
|
71682 | 39 |
|
40 |
/* self */ |
|
41 |
||
71685 | 42 |
def self: Standard_Thread = |
71682 | 43 |
Thread.currentThread match { |
71685 | 44 |
case thread: Standard_Thread => thread |
45 |
case _ => error("Expected to run on Isabelle/Scala standard thread") |
|
71682 | 46 |
} |
47 |
||
71685 | 48 |
def uninterruptible[A](body: => A): A = self.uninterruptible(body) |
71681 | 49 |
|
39579 | 50 |
|
61563 | 51 |
/* pool */ |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
52 |
|
61559
313eca3fa847
more direct task future implementation, with proper cancel operation;
wenzelm
parents:
61556
diff
changeset
|
53 |
lazy val pool: ThreadPoolExecutor = |
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
56860
diff
changeset
|
54 |
{ |
63805 | 55 |
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
|
56 |
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
|
57 |
val executor = |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
58 |
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
|
59 |
executor.setThreadFactory( |
71685 | 60 |
new Standard_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
|
61 |
executor |
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
56860
diff
changeset
|
62 |
} |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
63 |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
64 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
65 |
/* delayed events */ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
66 |
|
64810 | 67 |
final class Delay private[Standard_Thread]( |
68 |
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
|
69 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
70 |
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
|
71 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
72 |
private def run: Unit = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
73 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
74 |
val do_run = synchronized { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
75 |
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
|
76 |
} |
64810 | 77 |
if (do_run) { |
78 |
try { event } |
|
79 |
catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn } |
|
80 |
} |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
81 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
82 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
83 |
def invoke(): Unit = synchronized |
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 |
val new_run = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
86 |
running match { |
62263 | 87 |
case Some(request) => if (first) false else { request.cancel; true } |
88 |
case None => true |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
89 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
90 |
if (new_run) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
91 |
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
|
92 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
93 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
94 |
def revoke(): Unit = synchronized |
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 |
running match { |
62263 | 97 |
case Some(request) => request.cancel; running = None |
98 |
case None => |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
99 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
100 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
101 |
|
61194 | 102 |
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
|
103 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
104 |
running match { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
105 |
case Some(request) => |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
106 |
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
|
107 |
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
|
108 |
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
|
109 |
} |
62263 | 110 |
case None => |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
111 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
112 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
113 |
} |
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 |
// delayed event after first invocation |
64810 | 116 |
def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = |
117 |
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
|
118 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
119 |
// delayed event after last invocation |
64810 | 120 |
def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = |
121 |
new Delay(false, delay, log, event) |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
122 |
} |
71681 | 123 |
|
71685 | 124 |
class Standard_Thread private( |
125 |
main: Runnable, |
|
126 |
name: String = "", |
|
127 |
group: ThreadGroup = null, |
|
128 |
pri: Int = Thread.NORM_PRIORITY, |
|
129 |
daemon: Boolean = false, |
|
130 |
inherit_locals: Boolean = false) |
|
131 |
extends Thread(group, null, name, 0L, inherit_locals) |
|
71681 | 132 |
{ |
133 |
thread => |
|
134 |
||
71685 | 135 |
thread.setPriority(pri) |
71681 | 136 |
thread.setDaemon(daemon) |
137 |
||
71682 | 138 |
override def run { main.run() } |
71681 | 139 |
|
140 |
private var interruptible: Boolean = true |
|
141 |
private var interrupt_pending: Boolean = false |
|
142 |
||
143 |
override def interrupt: Unit = synchronized |
|
144 |
{ |
|
145 |
if (interruptible) super.interrupt() |
|
146 |
else { interrupt_pending = true } |
|
147 |
} |
|
148 |
||
71682 | 149 |
def uninterruptible[A](body: => A): A = |
71681 | 150 |
{ |
71682 | 151 |
require(Thread.currentThread == thread) |
152 |
||
71681 | 153 |
val interruptible0 = synchronized { val b = interruptible; interruptible = false; b } |
154 |
try { body } |
|
155 |
finally { |
|
156 |
synchronized { |
|
157 |
interruptible = interruptible0 |
|
158 |
if (interruptible && interrupt_pending) { |
|
159 |
interrupt_pending = false |
|
160 |
super.interrupt() |
|
161 |
} |
|
162 |
} |
|
71688 | 163 |
Exn.Interrupt.expose() |
71681 | 164 |
} |
165 |
} |
|
166 |
} |