minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
authorwenzelm
Tue Oct 31 15:36:50 2017 +0100 (19 months ago)
changeset 6695886bc3f1ec97e
parent 66957 82d13ba817b2
child 66959 015d47486fc8
minor performance tuning: avoid mutable variable for plain value, e.g. relevant for GC;
src/Pure/Concurrent/future.ML
     1.1 --- a/src/Pure/Concurrent/future.ML	Tue Oct 31 15:15:02 2017 +0100
     1.2 +++ b/src/Pure/Concurrent/future.ML	Tue Oct 31 15:36:50 2017 +0100
     1.3 @@ -87,15 +87,19 @@
     1.4  
     1.5  type 'a result = 'a Exn.result Single_Assignment.var;
     1.6  
     1.7 -datatype 'a future = Future of
     1.8 - {promised: bool,
     1.9 -  task: task,
    1.10 -  result: 'a result};
    1.11 +datatype 'a future =
    1.12 +  Value of 'a Exn.result |
    1.13 +  Future of
    1.14 +   {promised: bool,
    1.15 +    task: task,
    1.16 +    result: 'a result};
    1.17  
    1.18 -fun task_of (Future {task, ...}) = task;
    1.19 -fun result_of (Future {result, ...}) = result;
    1.20 +fun task_of (Value _) = Task_Queue.dummy_task
    1.21 +  | task_of (Future {task, ...}) = task;
    1.22  
    1.23 -fun peek x = Single_Assignment.peek (result_of x);
    1.24 +fun peek (Value res) = SOME res
    1.25 +  | peek (Future {result, ...}) = Single_Assignment.peek result;
    1.26 +
    1.27  fun is_finished x = is_some (peek x);
    1.28  
    1.29  val _ =
    1.30 @@ -522,7 +526,10 @@
    1.31        else if is_some (worker_task ()) then
    1.32          Thread_Attributes.with_attributes Thread_Attributes.no_interrupts
    1.33            (fn orig_atts => join_loop orig_atts (map task_of xs))
    1.34 -      else List.app (ignore o Single_Assignment.await o result_of) xs;
    1.35 +      else
    1.36 +        xs |> List.app
    1.37 +          (fn Value _ => ()
    1.38 +            | Future {result, ...} => ignore (Single_Assignment.await result));
    1.39    in map get_result xs end;
    1.40  
    1.41  end;
    1.42 @@ -609,31 +616,30 @@
    1.43  
    1.44  fun promise abort = promise_name "passive" abort;
    1.45  
    1.46 -fun fulfill_result (Future {promised, task, result}) res =
    1.47 -  if not promised then raise Fail "Not a promised future"
    1.48 -  else
    1.49 -    let
    1.50 -      val group = Task_Queue.group_of_task task;
    1.51 -      val pos = Position.thread_data ();
    1.52 -      fun job ok =
    1.53 -        assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
    1.54 -      val _ =
    1.55 -        Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ =>
    1.56 -          let
    1.57 -            val passive_job =
    1.58 -              SYNCHRONIZED "fulfill_result" (fn () =>
    1.59 -                Unsynchronized.change_result queue
    1.60 -                  (Task_Queue.dequeue_passive (Thread.self ()) task));
    1.61 -          in
    1.62 -            (case passive_job of
    1.63 -              SOME true => worker_exec (task, [job])
    1.64 -            | SOME false => ()
    1.65 -            | NONE => ignore (job (not (Task_Queue.is_canceled group))))
    1.66 -          end);
    1.67 -      val _ =
    1.68 -        if is_some (Single_Assignment.peek result) then ()
    1.69 -        else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
    1.70 -    in () end;
    1.71 +fun fulfill_result (Future {promised = true, task, result}) res =
    1.72 +      let
    1.73 +        val group = Task_Queue.group_of_task task;
    1.74 +        val pos = Position.thread_data ();
    1.75 +        fun job ok =
    1.76 +          assign_result group result (if ok then identify_result pos res else Exn.interrupt_exn);
    1.77 +        val _ =
    1.78 +          Thread_Attributes.with_attributes Thread_Attributes.no_interrupts (fn _ =>
    1.79 +            let
    1.80 +              val passive_job =
    1.81 +                SYNCHRONIZED "fulfill_result" (fn () =>
    1.82 +                  Unsynchronized.change_result queue
    1.83 +                    (Task_Queue.dequeue_passive (Thread.self ()) task));
    1.84 +            in
    1.85 +              (case passive_job of
    1.86 +                SOME true => worker_exec (task, [job])
    1.87 +              | SOME false => ()
    1.88 +              | NONE => ignore (job (not (Task_Queue.is_canceled group))))
    1.89 +            end);
    1.90 +        val _ =
    1.91 +          if is_some (Single_Assignment.peek result) then ()
    1.92 +          else worker_waiting [task] (fn () => ignore (Single_Assignment.await result));
    1.93 +      in () end
    1.94 +  | fulfill_result _ _ = raise Fail "Not a promised future";
    1.95  
    1.96  fun fulfill x res = fulfill_result x (Exn.Res res);
    1.97