author | wenzelm |
Thu, 05 Jan 2017 22:57:59 +0100 | |
changeset 64810 | 05b29c8f0add |
parent 64370 | 865b39487b5d |
child 71681 | 3622eea18e39 |
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 |
|
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
10 |
import java.lang.Thread |
62056
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
11 |
import java.util.concurrent.{ThreadPoolExecutor, TimeUnit, LinkedBlockingQueue, ThreadFactory} |
61563 | 12 |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
13 |
|
61556 | 14 |
object Standard_Thread |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
15 |
{ |
61563 | 16 |
/* fork */ |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
17 |
|
39577 | 18 |
def fork(name: String = "", daemon: Boolean = false)(body: => Unit): Thread = |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
19 |
{ |
39577 | 20 |
val thread = |
21 |
if (name == null || name == "") new Thread() { override def run = body } |
|
22 |
else new Thread(name) { override def run = body } |
|
38638 | 23 |
thread.setDaemon(daemon) |
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
24 |
thread.start |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
25 |
thread |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
26 |
} |
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
27 |
|
39579 | 28 |
|
61563 | 29 |
/* pool */ |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
30 |
|
61559
313eca3fa847
more direct task future implementation, with proper cancel operation;
wenzelm
parents:
61556
diff
changeset
|
31 |
lazy val pool: ThreadPoolExecutor = |
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
56860
diff
changeset
|
32 |
{ |
63805 | 33 |
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
|
34 |
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
|
35 |
val executor = |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
36 |
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
|
37 |
val old_thread_factory = executor.getThreadFactory |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
38 |
executor.setThreadFactory( |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
39 |
new ThreadFactory { |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
40 |
def newThread(r: Runnable) = |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
41 |
{ |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
42 |
val thread = old_thread_factory.newThread(r) |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
43 |
thread.setDaemon(true) |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
44 |
thread |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
45 |
} |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
46 |
}) |
6dbeafce6318
ensure that thread pool creates daemon threads, to increase chances that the JVM terminates spontaneously;
wenzelm
parents:
61563
diff
changeset
|
47 |
executor |
59136
c2b23cb8a677
added Par_List in Scala, in accordance to ML version;
wenzelm
parents:
56860
diff
changeset
|
48 |
} |
56730
e723f041b6d0
tuned signature -- separate pool for JFuture tasks, which can be canceled;
wenzelm
parents:
56707
diff
changeset
|
49 |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
50 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
51 |
/* delayed events */ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
52 |
|
64810 | 53 |
final class Delay private[Standard_Thread]( |
54 |
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
|
55 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
56 |
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
|
57 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
58 |
private def run: Unit = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
59 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
60 |
val do_run = synchronized { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
61 |
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
|
62 |
} |
64810 | 63 |
if (do_run) { |
64 |
try { event } |
|
65 |
catch { case exn: Throwable if !Exn.is_interrupt(exn) => log(Exn.message(exn)); throw exn } |
|
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 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
69 |
def invoke(): Unit = synchronized |
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 |
val new_run = |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
72 |
running match { |
62263 | 73 |
case Some(request) => if (first) false else { request.cancel; true } |
74 |
case None => true |
|
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
75 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
76 |
if (new_run) |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
77 |
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
|
78 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
79 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
80 |
def revoke(): Unit = synchronized |
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 |
running match { |
62263 | 83 |
case Some(request) => request.cancel; running = None |
84 |
case None => |
|
56770
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 |
} |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
87 |
|
61194 | 88 |
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
|
89 |
{ |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
90 |
running match { |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
91 |
case Some(request) => |
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
92 |
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
|
93 |
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
|
94 |
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
|
95 |
} |
62263 | 96 |
case None => |
56770
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
97 |
} |
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 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
101 |
// delayed event after first invocation |
64810 | 102 |
def delay_first(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = |
103 |
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
|
104 |
|
e160ae47db94
mane delayed events outside of Swing thread -- triggers no longer require Swing_Thread.later;
wenzelm
parents:
56730
diff
changeset
|
105 |
// delayed event after last invocation |
64810 | 106 |
def delay_last(delay: => Time, log: Logger = No_Logger)(event: => Unit): Delay = |
107 |
new Delay(false, delay, log, event) |
|
38636
b7647ca7de5a
module for simplified thread operations (Scala version);
wenzelm
parents:
diff
changeset
|
108 |
} |