# HG changeset patch # User wenzelm # Date 1419277237 -3600 # Node ID c0fa3b3bdabd621a7b614ac6aeeb60315c6fc4c8 # Parent cad8a0012a126ea895c2d355520e90989fa72331 discontinued central critical sections: NAMED_CRITICAL / CRITICAL; diff -r cad8a0012a12 -r c0fa3b3bdabd NEWS --- 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). diff -r cad8a0012a12 -r c0fa3b3bdabd src/Doc/Implementation/ML.thy --- 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} \ @@ -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 \Explicit synchronization\ -text \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! -\ +text \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!\ text %mlref \ \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 \The following example implements a counter that produces positive integers that are unique over the runtime of the Isabelle - process: -\ + process:\ ML \ local diff -r cad8a0012a12 -r c0fa3b3bdabd src/Pure/Concurrent/future.ML --- 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; diff -r cad8a0012a12 -r c0fa3b3bdabd src/Pure/Concurrent/par_list.ML --- 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 () => diff -r cad8a0012a12 -r c0fa3b3bdabd src/Pure/ML-Systems/multithreading.ML --- 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; diff -r cad8a0012a12 -r c0fa3b3bdabd src/Pure/ML-Systems/multithreading_polyml.ML --- 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; + diff -r cad8a0012a12 -r c0fa3b3bdabd src/Pure/Thy/thy_info.ML --- 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;