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