author wenzelm Fri, 06 Jul 2018 15:35:48 +0200 changeset 68597 afa7c5a239e6 parent 68596 81086e6f5429 child 68598 d465b396ef85
more frugal assignment of lazy value: fewer mutexes, condvars; cannot use RunCall.clearMutableBit due to spurious crashes;
 src/Pure/Concurrent/lazy.ML file | annotate | diff | comparison | revisions src/Pure/Concurrent/synchronized.ML file | annotate | diff | comparison | revisions
```--- a/src/Pure/Concurrent/lazy.ML	Fri Jul 06 10:44:45 2018 +0100
+++ b/src/Pure/Concurrent/lazy.ML	Fri Jul 06 15:35:48 2018 +0200
@@ -89,7 +89,11 @@
(fn Expr (name, e) =>
let val x = Future.promise_name name I
in ((SOME (name, e), x), Result x) end
-                    | Result x => ((NONE, x), Result x));
+                    | Result x => ((NONE, x), Result x))
+                  handle exn as Fail _ =>
+                    (case Synchronized.value var of
+                      Expr _ => Exn.reraise exn
+                    | Result x => (NONE, x));
in
(case expr of
SOME (name, e) =>
@@ -102,7 +106,7 @@
val _ =
if Exn.is_interrupt_exn res
then Synchronized.change var (fn _ => Expr (name, e))
-                      else Synchronized.change var (fn _ => Result (Future.value_result res));
+                      else Synchronized.assign var (Result (Future.value_result res));
in res end
| NONE => Exn.capture (restore_attributes (fn () => Future.join x)) ())
end) ());```
```--- a/src/Pure/Concurrent/synchronized.ML	Fri Jul 06 10:44:45 2018 +0100
+++ b/src/Pure/Concurrent/synchronized.ML	Fri Jul 06 15:35:48 2018 +0200
@@ -9,6 +9,7 @@
type 'a var
val var: string -> 'a -> 'a var
val value: 'a var -> 'a
+  val assign: 'a var -> 'a -> unit
val timed_access: 'a var -> ('a -> Time.time option) -> ('a -> ('b * 'a) option) -> 'b option
val guarded_access: 'a var -> ('a -> ('b * 'a) option) -> 'b
val change_result: 'a var -> ('a -> 'b * 'a) -> 'b
@@ -20,41 +21,66 @@

(* state variable *)

-abstype 'a var = Var of
- {name: string,
-  lock: Mutex.mutex,
-  cond: ConditionVar.conditionVar,
-  var: 'a Unsynchronized.ref}
+datatype 'a state =
+    Immutable of 'a
+  | Mutable of {lock: Mutex.mutex, cond: ConditionVar.conditionVar, content: 'a};
+
+fun init_state x =
+  Mutable {lock = Mutex.mutex (), cond = ConditionVar.conditionVar (), content = x};
+
+fun immutable_fail name = raise Fail ("Illegal access to immutable value " ^ name);
+
+abstype 'a var = Var of {name: string, state: 'a state Unsynchronized.ref}
with

-fun var name x = Var
- {name = name,
-  lock = Mutex.mutex (),
-  cond = ConditionVar.conditionVar (),
-  var = Unsynchronized.ref x};
+fun var name x =
+  Var {name = name, state = Unsynchronized.ref (init_state x)};
+
+fun value (Var {name, state}) =
+  (case ! state of
+    Immutable x => x
+  | Mutable {lock, ...} =>
+      Multithreading.synchronized name lock (fn () =>
+        (case ! state of
+          Immutable x => x
+        | Mutable {content, ...} => content)));

-fun value (Var {name, lock, var, ...}) =
-  Multithreading.synchronized name lock (fn () => ! var);
+fun assign (Var {name, state}) x =
+  (case ! state of
+    Immutable _ => immutable_fail name
+  | Mutable {lock, cond, ...} =>
+      Multithreading.synchronized name lock (fn () =>
+        (case ! state of
+          Immutable _ => immutable_fail name
+        | Mutable _ =>
+            Thread_Attributes.uninterruptible (fn _ => fn () =>
+             (state := Immutable x; (* FIXME RunCall.clearMutableBit state; *)

(* synchronized access *)

-fun timed_access (Var {name, lock, cond, var}) time_limit f =
-  Multithreading.synchronized name lock (fn () =>
-    let
-      fun try_change () =
-        let val x = ! var in
-          (case f x of
-            NONE =>
-              (case Multithreading.sync_wait (time_limit x) cond lock of
-                Exn.Res true => try_change ()
-              | Exn.Res false => NONE
-              | Exn.Exn exn => Exn.reraise exn)
-          | SOME (y, x') =>
-              Thread_Attributes.uninterruptible (fn _ => fn () =>
-                (var := x'; ConditionVar.broadcast cond; SOME y)) ())
-        end;
-    in try_change () end);
+fun timed_access (Var {name, state}) time_limit f =
+  (case ! state of
+    Immutable _ => immutable_fail name
+  | Mutable {lock, cond, ...} =>
+      Multithreading.synchronized name lock (fn () =>
+        let
+          fun try_change () =
+            (case ! state of
+              Immutable _ => immutable_fail name
+            | Mutable {content = x, ...} =>
+                (case f x of
+                  NONE =>
+                    (case Multithreading.sync_wait (time_limit x) cond lock of
+                      Exn.Res true => try_change ()
+                    | Exn.Res false => NONE
+                    | Exn.Exn exn => Exn.reraise exn)
+                | SOME (y, x') =>
+                    Thread_Attributes.uninterruptible (fn _ => fn () =>
+                      (state := Mutable {lock = lock, cond = cond, content = x'};
+                        ConditionVar.broadcast cond; SOME y)) ()));
+        in try_change () end));

fun guarded_access var f = the (timed_access var (fn _ => NONE) f);
```
{"ft_lang_label":"__label__en","ft_lang_prob":0.53116107,"math_prob":0.9599115,"size":4236,"snap":"2022-40-2023-06","text_gpt3_token_len":1303,"char_repetition_ratio":0.13492438,"word_repetition_ratio":0.2351387,"special_character_ratio":0.39187914,"punctuation_ratio":0.23483871,"nsfw_num_words":0,"has_unicode_error":false,"math_prob_llama3":0.95107144,"pos_list":[0],"im_url_duplicate_count":[null],"WARC_HEADER":"{\"WARC-Type\":\"response\",\"WARC-Date\":\"2023-01-27T18:15:43Z\",\"WARC-Record-ID\":\"<urn:uuid:ed0ac94d-6b4a-4cea-a957-162585c799b9>\",\"Content-Length\":\"18302\",\"Content-Type\":\"application/http; msgtype=response\",\"WARC-Warcinfo-ID\":\"<urn:uuid:da9cfabd-31a3-4ce8-9e80-b9d0ac4cfd21>\",\"WARC-Concurrent-To\":\"<urn:uuid:1b0cc3b4-2dc8-4762-bc2e-ad6c9187c494>\",\"WARC-IP-Address\":\"131.159.46.82\",\"WARC-Target-URI\":\"https://isabelle.in.tum.de/repos/isabelle/rev/afa7c5a239e6\",\"WARC-Payload-Digest\":\"sha1:MOG7ADDVYBXMWMXMJSXPCBQEV55PPBIE\",\"WARC-Block-Digest\":\"sha1:SYXH4O2QZV4P47A7VHHNJ2HQEI3SLQX4\",\"WARC-Identified-Payload-Type\":\"application/xhtml+xml\",\"warc_filename\":\"/cc_download/warc_2023/CC-MAIN-2023-06/CC-MAIN-2023-06_segments_1674764495001.99_warc_CC-MAIN-20230127164242-20230127194242-00545.warc.gz\"}"}