--- a/NEWS Mon Dec 22 19:47:58 2014 +0100
+++ b/NEWS Mon Dec 22 20:40:37 2014 +0100
@@ -218,6 +218,13 @@
*** ML ***
+* Former combinators NAMED_CRITICAL and CRITICAL for central critical
+sections have been discontinued, in favour of the more elementary
+Multithreading.synchronized and its high-level derivative
+Synchronized.var (which is usually sufficient in applications). Subtle
+INCOMPATIBILITY: synchronized access needs to be atomic and cannot be
+nested.
+
* Cartouches within ML sources are turned into values of type
Input.source (with formal position information).
--- a/src/Doc/Implementation/ML.thy Mon Dec 22 19:47:58 2014 +0100
+++ b/src/Doc/Implementation/ML.thy Mon Dec 22 20:40:37 2014 +0100
@@ -1718,7 +1718,7 @@
\begin{warn}
Parallel computing resources are managed centrally by the
- Isabelle/ML infrastructure. User programs must not fork their own
+ Isabelle/ML infrastructure. User programs should not fork their own
ML threads to perform heavy computations.
\end{warn}
\<close>
@@ -1765,8 +1765,8 @@
Instead of poking initial values into (private) global references, a
new state record can be created on each invocation, and passed
through any auxiliary functions of the component. The state record
- may well contain mutable references, without requiring any special
- synchronizations, as long as each invocation gets its own copy, and the
+ contain mutable references in special situations, without requiring any
+ synchronization, as long as each invocation gets its own copy and the
tool itself is single-threaded.
\item Avoid raw output on @{text "stdout"} or @{text "stderr"}. The
@@ -1827,39 +1827,22 @@
subsection \<open>Explicit synchronization\<close>
-text \<open>Isabelle/ML also provides some explicit synchronization
- mechanisms, for the rare situations where mutable shared resources
- are really required. These are based on the synchronizations
- primitives of Poly/ML, which have been adapted to the specific
- assumptions of the concurrent Isabelle/ML environment. User code
- must not use the Poly/ML primitives directly!
-
- \medskip The most basic synchronization concept is a single
- \emph{critical section} (also called ``monitor'' in the literature).
- A thread that enters the critical section prevents all other threads
- from doing the same. A thread that is already within the critical
- section may re-enter it in an idempotent manner.
-
- Such centralized locking is convenient, because it prevents
- deadlocks by construction.
-
- \medskip More fine-grained locking works via \emph{synchronized
- variables}. An explicit state component is associated with
- mechanisms for locking and signaling. There are operations to
- await a condition, change the state, and signal the change to all
- other waiting threads.
-
- Here the synchronized access to the state variable is \emph{not}
- re-entrant: direct or indirect nesting within the same thread will
- cause a deadlock!
-\<close>
+text \<open>Isabelle/ML provides explicit synchronization for mutable variables over
+ immutable data, which may be updated atomically and exclusively. This
+ addresses the rare situations where mutable shared resources are really
+ required. Synchronization in Isabelle/ML is based on primitives of Poly/ML,
+ which have been adapted to the specific assumptions of the concurrent
+ Isabelle environment. User code should not break this abstraction, but stay
+ within the confines of concurrent Isabelle/ML.
+
+ A \emph{synchronized variable} is an explicit state component is associated
+ with mechanisms for locking and signaling. There are operations to await a
+ condition, change the state, and signal the change to all other waiting
+ threads. Synchronized access to the state variable is \emph{not} re-entrant:
+ direct or indirect nesting within the same thread will cause a deadlock!\<close>
text %mlref \<open>
\begin{mldecls}
- @{index_ML NAMED_CRITICAL: "string -> (unit -> 'a) -> 'a"} \\
- @{index_ML CRITICAL: "(unit -> 'a) -> 'a"} \\
- \end{mldecls}
- \begin{mldecls}
@{index_ML_type "'a Synchronized.var"} \\
@{index_ML Synchronized.var: "string -> 'a -> 'a Synchronized.var"} \\
@{index_ML Synchronized.guarded_access: "'a Synchronized.var ->
@@ -1868,19 +1851,6 @@
\begin{description}
- \item @{ML NAMED_CRITICAL}~@{text "name e"} evaluates @{text "e ()"}
- within the central critical section of Isabelle/ML. No other thread
- may do so at the same time, but non-critical parallel execution will
- continue. The @{text "name"} argument is used for tracing and might
- help to spot sources of congestion.
-
- Entering the critical section without contention is very fast. Each
- thread should stay within the critical section only very briefly,
- otherwise parallel performance may degrade.
-
- \item @{ML CRITICAL} is the same as @{ML NAMED_CRITICAL} with empty
- name argument.
-
\item Type @{ML_type "'a Synchronized.var"} represents synchronized
variables with state of type @{ML_type 'a}.
@@ -1907,8 +1877,7 @@
text %mlex \<open>The following example implements a counter that produces
positive integers that are unique over the runtime of the Isabelle
- process:
-\<close>
+ process:\<close>
ML \<open>
local
--- a/src/Pure/Concurrent/future.ML Mon Dec 22 19:47:58 2014 +0100
+++ b/src/Pure/Concurrent/future.ML Mon Dec 22 20:40:37 2014 +0100
@@ -522,8 +522,6 @@
let
val _ =
if forall is_finished xs then ()
- else if Multithreading.self_critical () then
- raise Fail "Cannot join future values within critical section"
else if is_some (worker_task ()) then join_work (map task_of xs)
else List.app (ignore o Single_Assignment.await o result_of) xs;
in map get_result xs end;
--- a/src/Pure/Concurrent/par_list.ML Mon Dec 22 19:47:58 2014 +0100
+++ b/src/Pure/Concurrent/par_list.ML Mon Dec 22 20:40:37 2014 +0100
@@ -30,8 +30,7 @@
struct
fun managed_results name f xs =
- if null xs orelse null (tl xs) orelse
- not (Multithreading.enabled ()) orelse Multithreading.self_critical ()
+ if null xs orelse null (tl xs) orelse not (Multithreading.enabled ())
then map (Exn.capture f) xs
else
uninterruptible (fn restore_attributes => fn () =>
--- a/src/Pure/ML-Systems/multithreading.ML Mon Dec 22 19:47:58 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading.ML Mon Dec 22 20:40:37 2014 +0100
@@ -4,15 +4,8 @@
Dummy implementation of multithreading setup.
*)
-signature BASIC_MULTITHREADING =
-sig
- val NAMED_CRITICAL: string -> (unit -> 'a) -> 'a
- val CRITICAL: (unit -> 'a) -> 'a
-end;
-
signature MULTITHREADING =
sig
- include BASIC_MULTITHREADING
val available: bool
val max_threads_value: unit -> int
val max_threads_update: int -> unit
@@ -30,7 +23,6 @@
val tracing: int -> (unit -> string) -> unit
val tracing_time: bool -> Time.time -> (unit -> string) -> unit
val real_time: ('a -> unit) -> 'a -> Time.time
- val self_critical: unit -> bool
val synchronized: string -> Mutex.mutex -> (unit -> 'a) -> 'a
val serial: unit -> int
end;
@@ -69,11 +61,7 @@
fun real_time f x = (f x; Time.zeroTime);
-(* critical section *)
-
-fun self_critical () = false;
-fun NAMED_CRITICAL _ e = e ();
-fun CRITICAL e = e ();
+(* synchronized evaluation *)
fun synchronized _ _ e = e ();
@@ -85,5 +73,3 @@
end;
-structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
-open Basic_Multithreading;
--- a/src/Pure/ML-Systems/multithreading_polyml.ML Mon Dec 22 19:47:58 2014 +0100
+++ b/src/Pure/ML-Systems/multithreading_polyml.ML Mon Dec 22 20:40:37 2014 +0100
@@ -4,22 +4,11 @@
Multithreading in Poly/ML (cf. polyml/basis/Thread.sml).
*)
-signature MULTITHREADING_POLYML =
-sig
- val interruptible: ('a -> 'b) -> 'a -> 'b
- val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
-end;
-
-signature BASIC_MULTITHREADING =
-sig
- include BASIC_MULTITHREADING
- include MULTITHREADING_POLYML
-end;
-
signature MULTITHREADING =
sig
include MULTITHREADING
- include MULTITHREADING_POLYML
+ val interruptible: ('a -> 'b) -> 'a -> 'b
+ val uninterruptible: ((('c -> 'd) -> 'c -> 'd) -> 'a -> 'b) -> 'a -> 'b
end;
structure Multithreading: MULTITHREADING =
@@ -138,50 +127,7 @@
in time end;
-(* critical section -- may be nested within the same thread *)
-
-local
-
-val critical_lock = Mutex.mutex ();
-val critical_thread = ref (NONE: Thread.thread option);
-val critical_name = ref "";
-
-fun show "" = "" | show name = " " ^ name;
-fun show' "" = "" | show' name = " [" ^ name ^ "]";
-
-in
-
-fun self_critical () =
- (case ! critical_thread of
- NONE => false
- | SOME t => Thread.equal (t, Thread.self ()));
-
-fun NAMED_CRITICAL name e =
- if self_critical () then e ()
- else
- Exn.release (uninterruptible (fn restore_attributes => fn () =>
- let
- val name' = ! critical_name;
- val _ =
- if Mutex.trylock critical_lock then ()
- else
- let
- val _ = tracing 5 (fn () => "CRITICAL" ^ show name ^ show' name' ^ ": waiting");
- val time = real_time Mutex.lock critical_lock;
- val _ = tracing_time true time (fn () =>
- "CRITICAL" ^ show name ^ show' name' ^ ": passed after " ^ Time.toString time);
- in () end;
- val _ = critical_thread := SOME (Thread.self ());
- val _ = critical_name := name;
- val result = Exn.capture (restore_attributes e) ();
- val _ = critical_name := "";
- val _ = critical_thread := NONE;
- val _ = Mutex.unlock critical_lock;
- in result end) ());
-
-fun CRITICAL e = NAMED_CRITICAL "" e;
-
-end;
+(* synchronized evaluation *)
fun synchronized name lock e =
Exn.release (uninterruptible (fn restore_attributes => fn () =>
@@ -221,5 +167,6 @@
end;
-structure Basic_Multithreading: BASIC_MULTITHREADING = Multithreading;
-open Basic_Multithreading;
+val interruptible = Multithreading.interruptible;
+val uninterruptible = Multithreading.uninterruptible;
+
--- a/src/Pure/Thy/thy_info.ML Mon Dec 22 19:47:58 2014 +0100
+++ b/src/Pure/Thy/thy_info.ML Mon Dec 22 20:40:37 2014 +0100
@@ -222,11 +222,7 @@
in
fun schedule_tasks tasks =
- if not (Multithreading.enabled ()) then schedule_seq tasks
- else if Multithreading.self_critical () then
- (warning "Theory loader: no multithreading within critical section";
- schedule_seq tasks)
- else schedule_futures tasks;
+ if Multithreading.enabled () then schedule_futures tasks else schedule_seq tasks;
end;