more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
authorwenzelm
Tue Dec 13 23:29:54 2016 +0100 (2016-12-13)
changeset 6455737074e22e8be
parent 64556 851ae0e7b09c
child 64558 63c76802ab5e
child 64562 e154ec4e3eac
more tight thread attributes, based in internal word arithmetic instead of symbolic datatypes: measurable performance improvement;
src/Pure/Concurrent/multithreading.ML
src/Pure/Concurrent/standard_thread.ML
src/Pure/Concurrent/thread_attributes.ML
src/Pure/Tools/ml_process.scala
     1.1 --- a/src/Pure/Concurrent/multithreading.ML	Tue Dec 13 11:51:42 2016 +0100
     1.2 +++ b/src/Pure/Concurrent/multithreading.ML	Tue Dec 13 23:29:54 2016 +0100
     1.3 @@ -48,7 +48,7 @@
     1.4  
     1.5  fun sync_wait time cond lock =
     1.6    Thread_Attributes.with_attributes
     1.7 -    (Thread_Attributes.sync_interrupts (Thread.getAttributes ()))
     1.8 +    (Thread_Attributes.sync_interrupts (Thread_Attributes.get_attributes ()))
     1.9      (fn _ =>
    1.10        (case time of
    1.11          SOME t => Exn.Res (ConditionVar.waitUntil (cond, lock, t))
     2.1 --- a/src/Pure/Concurrent/standard_thread.ML	Tue Dec 13 11:51:42 2016 +0100
     2.2 +++ b/src/Pure/Concurrent/standard_thread.ML	Tue Dec 13 23:29:54 2016 +0100
     2.3 @@ -50,7 +50,8 @@
     2.4  
     2.5  fun attributes ({stack_limit, interrupts, ...}: params) =
     2.6    Thread.MaximumMLStack stack_limit ::
     2.7 -  (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
     2.8 +  Thread_Attributes.convert_attributes
     2.9 +    (if interrupts then Thread_Attributes.public_interrupts else Thread_Attributes.no_interrupts);
    2.10  
    2.11  fun fork (params: params) body =
    2.12    Thread.fork (fn () =>
     3.1 --- a/src/Pure/Concurrent/thread_attributes.ML	Tue Dec 13 11:51:42 2016 +0100
     3.2 +++ b/src/Pure/Concurrent/thread_attributes.ML	Tue Dec 13 23:29:54 2016 +0100
     3.3 @@ -6,7 +6,10 @@
     3.4  
     3.5  signature THREAD_ATTRIBUTES =
     3.6  sig
     3.7 -  type attributes = Thread.Thread.threadAttribute list
     3.8 +  type attributes
     3.9 +  val get_attributes: unit -> attributes
    3.10 +  val set_attributes: attributes -> unit
    3.11 +  val convert_attributes: attributes -> Thread.Thread.threadAttribute list
    3.12    val no_interrupts: attributes
    3.13    val test_interrupts: attributes
    3.14    val public_interrupts: attributes
    3.15 @@ -21,40 +24,77 @@
    3.16  structure Thread_Attributes: THREAD_ATTRIBUTES =
    3.17  struct
    3.18  
    3.19 -type attributes = Thread.Thread.threadAttribute list;
    3.20 +abstype attributes = Attributes of Word.word
    3.21 +with
    3.22  
    3.23 -val no_interrupts =
    3.24 -  [Thread.Thread.EnableBroadcastInterrupt false,
    3.25 -    Thread.Thread.InterruptState Thread.Thread.InterruptDefer];
    3.26 +(* thread attributes *)
    3.27 +
    3.28 +val thread_attributes = 0w7;
    3.29 +
    3.30 +val broadcast = 0w1;
    3.31  
    3.32 -val test_interrupts =
    3.33 -  [Thread.Thread.EnableBroadcastInterrupt false,
    3.34 -    Thread.Thread.InterruptState Thread.Thread.InterruptSynch];
    3.35 +val interrupt_state = 0w6;
    3.36 +val interrupt_defer = 0w0;
    3.37 +val interrupt_synch = 0w2;
    3.38 +val interrupt_asynch = 0w4;
    3.39 +val interrupt_asynch_once = 0w6;
    3.40 +
    3.41  
    3.42 -val public_interrupts =
    3.43 -  [Thread.Thread.EnableBroadcastInterrupt true,
    3.44 -    Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
    3.45 +(* access thread flags *)
    3.46 +
    3.47 +val thread_flags = 0w1;
    3.48 +
    3.49 +fun load_word () : word =
    3.50 +  RunCall.loadWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags);
    3.51 +
    3.52 +fun get_attributes () = Attributes (Word.andb (load_word (), thread_attributes));
    3.53  
    3.54 -val private_interrupts =
    3.55 -  [Thread.Thread.EnableBroadcastInterrupt false,
    3.56 -    Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce];
    3.57 +fun set_attributes (Attributes w) =
    3.58 +  let
    3.59 +    val w' = Word.orb (Word.andb (load_word (), Word.notb thread_attributes), w);
    3.60 +    val _ = RunCall.storeWord (RunCall.unsafeCast (Thread.Thread.self ()), thread_flags, w');
    3.61 +  in
    3.62 +    if Word.andb (w', interrupt_asynch) = interrupt_asynch
    3.63 +    then Thread.Thread.testInterrupt () else ()
    3.64 +  end;
    3.65 +
    3.66 +fun convert_attributes (Attributes w) =
    3.67 +  [Thread.Thread.EnableBroadcastInterrupt (Word.andb (w, broadcast) = broadcast),
    3.68 +   Thread.Thread.InterruptState
    3.69 +      let val w' = Word.andb (w, interrupt_state) in
    3.70 +        if w' = interrupt_defer then Thread.Thread.InterruptDefer
    3.71 +        else if w' = interrupt_synch then Thread.Thread.InterruptSynch
    3.72 +        else if w' = interrupt_asynch then Thread.Thread.InterruptAsynch
    3.73 +        else Thread.Thread.InterruptAsynchOnce
    3.74 +      end];
    3.75 +
    3.76  
    3.77 -val sync_interrupts = map
    3.78 -  (fn x as Thread.Thread.InterruptState Thread.Thread.InterruptDefer => x
    3.79 -    | Thread.Thread.InterruptState _ => Thread.Thread.InterruptState Thread.Thread.InterruptSynch
    3.80 -    | x => x);
    3.81 +(* common configurations *)
    3.82 +
    3.83 +val no_interrupts = Attributes interrupt_defer;
    3.84 +val test_interrupts = Attributes interrupt_synch;
    3.85 +val public_interrupts = Attributes (Word.orb (broadcast, interrupt_asynch_once));
    3.86 +val private_interrupts = Attributes interrupt_asynch_once;
    3.87  
    3.88 -val safe_interrupts = map
    3.89 -  (fn Thread.Thread.InterruptState Thread.Thread.InterruptAsynch =>
    3.90 -      Thread.Thread.InterruptState Thread.Thread.InterruptAsynchOnce
    3.91 -    | x => x);
    3.92 +fun sync_interrupts (Attributes w) =
    3.93 +  let
    3.94 +    val w' = Word.andb (w, interrupt_state);
    3.95 +    val w'' = Word.andb (w, Word.notb interrupt_state);
    3.96 +  in Attributes (if w' = interrupt_defer then w else Word.orb (w'', interrupt_synch)) end;
    3.97 +
    3.98 +fun safe_interrupts (Attributes w) =
    3.99 +  let
   3.100 +    val w' = Word.andb (w, interrupt_state);
   3.101 +    val w'' = Word.andb (w, Word.notb interrupt_state);
   3.102 +  in Attributes (if w' = interrupt_asynch then Word.orb (w'', interrupt_asynch_once) else w) end;
   3.103 +
   3.104 +end;
   3.105  
   3.106  fun with_attributes new_atts e =
   3.107    let
   3.108 -    val orig_atts = safe_interrupts (Thread.Thread.getAttributes ());
   3.109 -    val result = Exn.capture (fn () =>
   3.110 -      (Thread.Thread.setAttributes (safe_interrupts new_atts); e orig_atts)) ();
   3.111 -    val _ = Thread.Thread.setAttributes orig_atts;
   3.112 +    val orig_atts = safe_interrupts (get_attributes ());
   3.113 +    val result = Exn.capture (fn () => (set_attributes (safe_interrupts new_atts); e orig_atts)) ();
   3.114 +    val _ = set_attributes orig_atts;
   3.115    in Exn.release result end;
   3.116  
   3.117  fun uninterruptible f x =
   3.118 @@ -63,10 +103,10 @@
   3.119  
   3.120  fun expose_interrupt () =
   3.121    let
   3.122 -    val orig_atts = safe_interrupts (Thread.Thread.getAttributes ());
   3.123 -    val _ = Thread.Thread.setAttributes test_interrupts;
   3.124 +    val orig_atts = safe_interrupts (get_attributes ());
   3.125 +    val _ = set_attributes test_interrupts;
   3.126      val test = Exn.capture Thread.Thread.testInterrupt ();
   3.127 -    val _ = Thread.Thread.setAttributes orig_atts;
   3.128 +    val _ = set_attributes orig_atts;
   3.129    in Exn.release test end;
   3.130  
   3.131  end;
     4.1 --- a/src/Pure/Tools/ml_process.scala	Tue Dec 13 11:51:42 2016 +0100
     4.2 +++ b/src/Pure/Tools/ml_process.scala	Tue Dec 13 23:29:54 2016 +0100
     4.3 @@ -48,7 +48,18 @@
     4.4            fun subparagraph (_: string) = ();
     4.5            val ML_file = PolyML.use;
     4.6            """,
     4.7 -          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6") "structure FixedInt = IntInf"
     4.8 +          if (Isabelle_System.getenv("ML_SYSTEM") == "polyml-5.6")
     4.9 +            """
    4.10 +              structure FixedInt = IntInf;
    4.11 +              structure RunCall =
    4.12 +              struct
    4.13 +                open RunCall
    4.14 +                val loadWord: word * word -> word =
    4.15 +                  run_call2 RuntimeCalls.POLY_SYS_load_word;
    4.16 +                val storeWord: word * word * word -> unit =
    4.17 +                  run_call3 RuntimeCalls.POLY_SYS_assign_word;
    4.18 +              end;
    4.19 +            """
    4.20            else "",
    4.21            if (Platform.is_windows)
    4.22              "fun exit 0 = OS.Process.exit OS.Process.success" +