--- a/NEWS Fri Dec 12 10:58:40 2014 +0100
+++ b/NEWS Fri Dec 12 14:42:37 2014 +0100
@@ -235,6 +235,9 @@
* Renamed "pairself" to "apply2", in accordance to @{apply 2}.
INCOMPATIBILITY.
+* Synchronized.value (ML) is actually synchronized (as in Scala):
+subtle change of semantics with minimal potential for INCOMPATIBILITY.
+
*** System ***
--- a/etc/settings Fri Dec 12 10:58:40 2014 +0100
+++ b/etc/settings Fri Dec 12 14:42:37 2014 +0100
@@ -14,7 +14,7 @@
ISABELLE_SCALA_BUILD_OPTIONS="-encoding UTF-8 -nowarn -target:jvm-1.7 -Xmax-classfile-name 130"
-ISABELLE_JAVA_SYSTEM_OPTIONS="-Dfile.encoding=UTF-8 -server"
+ISABELLE_JAVA_SYSTEM_OPTIONS="-server -Dfile.encoding=UTF-8 -Disabelle.threads=0"
classpath "$ISABELLE_HOME/lib/classes/Pure.jar"
--- a/src/Doc/Implementation/ML.thy Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Doc/Implementation/ML.thy Fri Dec 12 14:42:37 2014 +0100
@@ -2019,8 +2019,8 @@
individual exceptions by conventional @{verbatim "handle"} of ML.
\item @{ML Par_Exn.release_first} is similar to @{ML
- Par_Exn.release_all}, but only the first exception that has occurred
- in the original evaluation process is raised again, the others are
+ Par_Exn.release_all}, but only the first (meaningful) exception that has
+ occurred in the original evaluation process is raised again, the others are
ignored. That single exception may get handled by conventional
means in ML.
--- a/src/HOL/ex/Cartouche_Examples.thy Fri Dec 12 10:58:40 2014 +0100
+++ b/src/HOL/ex/Cartouche_Examples.thy Fri Dec 12 14:42:37 2014 +0100
@@ -265,7 +265,7 @@
text \<open>Input source with position information:\<close>
ML \<open>
- val s: Input.source = \<open>abc\<close>;
+ val s: Input.source = \<open>abc123def456\<close>;
writeln (Markup.markup Markup.information ("Look here!" ^ Position.here (Input.pos_of s)));
\<open>abc123def456\<close> |> Input.source_explode |> List.app (fn (s, pos) =>
@@ -282,6 +282,4 @@
val thms = [a, b, c];
\<close>
-ML \<open>\<close>
-
end
--- a/src/Pure/Concurrent/par_list.ML Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Concurrent/par_list.ML Fri Dec 12 14:42:37 2014 +0100
@@ -56,21 +56,19 @@
fun get_some f xs =
let
- exception FOUND of 'b option;
- fun found (Exn.Exn (FOUND some)) = some
- | found _ = NONE;
+ exception FOUND of 'b;
val results =
managed_results "Par_List.get_some"
- (fn x => (case f x of NONE => () | some => raise FOUND some)) xs;
+ (fn x => (case f x of NONE => () | SOME y => raise FOUND y)) xs;
in
- (case get_first found results of
- SOME y => SOME y
- | NONE => (Par_Exn.release_first results; NONE))
+ (case get_first (fn Exn.Exn (FOUND res) => SOME res | _ => NONE) results of
+ NONE => (Par_Exn.release_first results; NONE)
+ | some => some)
end;
fun find_some P = get_some (fn x => if P x then SOME x else NONE);
-fun exists P = is_some o get_some (fn x => if P x then SOME () else NONE);
+fun exists P = is_some o find_some P;
fun forall P = not o exists (not o P);
end;
--- /dev/null Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/Concurrent/par_list.scala Fri Dec 12 14:42:37 2014 +0100
@@ -0,0 +1,68 @@
+/* Title: Pure/Concurrent/par_list.scala
+ Author: Makarius
+
+Parallel list combinators.
+*/
+
+
+package isabelle
+
+
+import java.util.concurrent.{Future => JFuture, CancellationException}
+
+
+object Par_List
+{
+ def managed_results[A, B](f: A => B, xs: List[A]): List[Exn.Result[B]] =
+ if (xs.isEmpty || xs.tail.isEmpty) xs.map(x => Exn.capture { f(x) })
+ else {
+ val state = Synchronized((List.empty[JFuture[Exn.Result[B]]], false))
+
+ def cancel_other(self: Int = -1): Unit =
+ state.change { case (tasks, canceled) =>
+ if (!canceled) {
+ for ((task, i) <- tasks.iterator.zipWithIndex if i != self)
+ task.cancel(true)
+ }
+ (tasks, true)
+ }
+
+ try {
+ state.change(_ =>
+ (xs.iterator.zipWithIndex.map({ case (x, self) =>
+ Simple_Thread.submit_task {
+ val result = Exn.capture { f(x) }
+ result match { case Exn.Exn(_) => cancel_other(self) case _ => }
+ result
+ }
+ }).toList, false))
+
+ state.value._1.map(future =>
+ try { future.get }
+ catch { case _: CancellationException => Exn.Exn(Exn.Interrupt()): Exn.Result[B] })
+ }
+ finally { cancel_other() }
+ }
+
+ def map[A, B](f: A => B, xs: List[A]): List[B] =
+ Exn.release_first(managed_results(f, xs))
+
+ def get_some[A, B](f: A => Option[B], xs: List[A]): Option[B] =
+ {
+ class Found(val res: B) extends Exception
+ val results =
+ managed_results(
+ (x: A) => f(x) match { case None => () case Some(y) => throw new Found(y) }, xs)
+ results.collectFirst({ case Exn.Exn(found: Found) => found.res }) match {
+ case None => Exn.release_first(results); None
+ case some => some
+ }
+ }
+
+ def find_some[A](P: A => Boolean, xs: List[A]): Option[A] =
+ get_some((x: A) => if (P(x)) Some(x) else None, xs)
+
+ def exists[A](P: A => Boolean, xs: List[A]): Boolean = find_some(P, xs).isDefined
+ def forall[A](P: A => Boolean, xs: List[A]): Boolean = !exists((x: A) => !P(x), xs)
+}
+
--- a/src/Pure/Concurrent/simple_thread.scala Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Concurrent/simple_thread.scala Fri Dec 12 14:42:37 2014 +0100
@@ -9,9 +9,8 @@
import java.lang.Thread
-import java.util.concurrent.{Callable, Future => JFuture}
-
-import scala.collection.parallel.ForkJoinTasks
+import java.util.concurrent.{Callable, Future => JFuture, ThreadPoolExecutor,
+ TimeUnit, LinkedBlockingQueue}
object Simple_Thread
@@ -41,7 +40,12 @@
/* thread pool */
- lazy val default_pool = ForkJoinTasks.defaultForkJoinPool
+ lazy val default_pool =
+ {
+ val m = Properties.Value.Int.unapply(System.getProperty("isabelle.threads", "0")) getOrElse 0
+ val n = if (m > 0) m else (Runtime.getRuntime.availableProcessors max 1) min 8
+ new ThreadPoolExecutor(n, n, 2500L, TimeUnit.MILLISECONDS, new LinkedBlockingQueue[Runnable])
+ }
def submit_task[A](body: => A): JFuture[A] =
default_pool.submit(new Callable[A] { def call = body })
--- a/src/Pure/Concurrent/synchronized.ML Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Concurrent/synchronized.ML Fri Dec 12 14:42:37 2014 +0100
@@ -33,7 +33,8 @@
cond = ConditionVar.conditionVar (),
var = Unsynchronized.ref x};
-fun value (Var {var, ...}) = ! var;
+fun value (Var {name, lock, var, ...}) =
+ Multithreading.synchronized name lock (fn () => ! var);
(* synchronized access *)
--- a/src/Pure/General/exn.scala Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/General/exn.scala Fri Dec 12 14:42:37 2014 +0100
@@ -26,6 +26,12 @@
case Exn(exn) => throw exn
}
+ def release_first[A](results: List[Result[A]]): List[A] =
+ results.find({ case Exn(exn) => !is_interrupt(exn) case _ => false }) match {
+ case Some(Exn(exn)) => throw exn
+ case _ => results.map(release(_))
+ }
+
/* interrupts */
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Fri Dec 12 14:42:37 2014 +0100
@@ -80,8 +80,7 @@
val available = true;
fun max_threads_result m =
- if m > 0 then m
- else Int.min (Int.max (Thread.numProcessors (), 1), 8);
+ if m > 0 then m else Int.min (Int.max (Thread.numProcessors (), 1), 8);
val max_threads = ref 1;
--- a/src/Pure/Thy/thy_info.scala Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Thy/thy_info.scala Fri Dec 12 14:42:37 2014 +0100
@@ -85,13 +85,11 @@
def loaded_files: List[Path] =
{
val dep_files =
- rev_deps.par.map(dep =>
- Exn.capture {
- dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a))
- }).toList
- ((Nil: List[Path]) /: dep_files) {
- case (acc_files, files) => Exn.release(files) ::: acc_files
- }
+ Par_List.map(
+ (dep: Dep) =>
+ dep.loaded_files(syntax).map(a => Path.explode(dep.name.master_dir) + Path.explode(a)),
+ rev_deps)
+ ((Nil: List[Path]) /: dep_files) { case (acc_files, files) => files ::: acc_files }
}
}
--- a/src/Pure/Tools/build.scala Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/Tools/build.scala Fri Dec 12 14:42:37 2014 +0100
@@ -345,9 +345,7 @@
val graph = tree.graph
val sessions = graph.keys
- val timings =
- sessions.par.map((name: String) =>
- Exn.capture { (name, load_timings(name)) }).toList.map(Exn.release(_))
+ val timings = Par_List.map((name: String) => (name, load_timings(name)), sessions)
val command_timings =
Map(timings.map({ case (name, (ts, _)) => (name, ts) }): _*).withDefaultValue(Nil)
val session_timing =
--- a/src/Pure/build-jars Fri Dec 12 10:58:40 2014 +0100
+++ b/src/Pure/build-jars Fri Dec 12 14:42:37 2014 +0100
@@ -14,6 +14,7 @@
Concurrent/event_timer.scala
Concurrent/future.scala
Concurrent/mailbox.scala
+ Concurrent/par_list.scala
Concurrent/simple_thread.scala
Concurrent/synchronized.scala
GUI/color_value.scala