explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
authorwenzelm
Thu Jan 29 15:21:16 2015 +0100 (2015-01-29)
changeset 59468fe6651760643
parent 59467 58c4f3e1870f
child 59469 fb393ecde29d
explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
etc/options
src/HOL/Tools/Sledgehammer/async_manager.ML
src/Pure/Concurrent/bash.ML
src/Pure/Concurrent/event_timer.ML
src/Pure/Concurrent/future.ML
src/Pure/Concurrent/simple_thread.ML
src/Pure/ML-Systems/maximum_ml_stack_dummy.ML
src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
src/Pure/ML-Systems/polyml.ML
src/Pure/ML-Systems/smlnj.ML
src/Pure/System/message_channel.ML
     1.1 --- a/etc/options	Thu Jan 29 13:58:02 2015 +0100
     1.2 +++ b/etc/options	Thu Jan 29 15:21:16 2015 +0100
     1.3 @@ -66,6 +66,8 @@
     1.4    -- "maximum number of worker threads for prover process (0 = hardware max.)"
     1.5  option threads_trace : int = 0
     1.6    -- "level of tracing information for multithreading"
     1.7 +option threads_stack_limit : real = 0.25
     1.8 +  -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
     1.9  public option parallel_print : bool = true
    1.10    -- "parallel and asynchronous printing of results"
    1.11  public option parallel_proofs : int = 2
     2.1 --- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Jan 29 13:58:02 2015 +0100
     2.2 +++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Jan 29 15:21:16 2015 +0100
     2.3 @@ -28,7 +28,7 @@
     2.4        Runtime.debugging NONE body () handle exn =>
     2.5          if Exn.is_interrupt exn then ()
     2.6          else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
     2.7 -      Simple_Thread.attributes interrupts);
     2.8 +      Simple_Thread.attributes {stack_limit = NONE, interrupts = interrupts});
     2.9  
    2.10  val message_store_limit = 20
    2.11  val message_display_limit = 10
     3.1 --- a/src/Pure/Concurrent/bash.ML	Thu Jan 29 13:58:02 2015 +0100
     3.2 +++ b/src/Pure/Concurrent/bash.ML	Thu Jan 29 15:21:16 2015 +0100
     3.3 @@ -31,7 +31,7 @@
     3.4      val _ = cleanup_files ();
     3.5  
     3.6      val system_thread =
     3.7 -      Simple_Thread.fork false (fn () =>
     3.8 +      Simple_Thread.fork {stack_limit = NONE, interrupts = false} (fn () =>
     3.9          Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
    3.10            let
    3.11              val _ = File.write script_path script;
     4.1 --- a/src/Pure/Concurrent/event_timer.ML	Thu Jan 29 13:58:02 2015 +0100
     4.2 +++ b/src/Pure/Concurrent/event_timer.ML	Thu Jan 29 15:21:16 2015 +0100
     4.3 @@ -104,7 +104,7 @@
     4.4  
     4.5  fun manager_check manager =
     4.6    if is_some manager andalso Thread.isActive (the manager) then manager
     4.7 -  else SOME (Simple_Thread.fork false manager_loop);
     4.8 +  else SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} manager_loop);
     4.9  
    4.10  fun shutdown () =
    4.11    uninterruptible (fn restore_attributes => fn () =>
     5.1 --- a/src/Pure/Concurrent/future.ML	Thu Jan 29 13:58:02 2015 +0100
     5.2 +++ b/src/Pure/Concurrent/future.ML	Thu Jan 29 15:21:16 2015 +0100
     5.3 @@ -258,12 +258,17 @@
     5.4    | SOME work => (worker_exec work; worker_loop name));
     5.5  
     5.6  fun worker_start name = (*requires SYNCHRONIZED*)
     5.7 -  Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
     5.8 -    Unsynchronized.ref Working))
     5.9 +  let
    5.10 +    val threads_stack_limit =
    5.11 +      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
    5.12 +    val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
    5.13 +    val worker =
    5.14 +      Simple_Thread.fork {stack_limit = stack_limit, interrupts = false}
    5.15 +        (fn () => worker_loop name);
    5.16 +  in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
    5.17    handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
    5.18  
    5.19  
    5.20 -
    5.21  (* scheduler *)
    5.22  
    5.23  fun scheduler_next () = (*requires SYNCHRONIZED*)
    5.24 @@ -359,7 +364,8 @@
    5.25  fun scheduler_check () = (*requires SYNCHRONIZED*)
    5.26   (do_shutdown := false;
    5.27    if scheduler_active () then ()
    5.28 -  else scheduler := SOME (Simple_Thread.fork false scheduler_loop));
    5.29 +  else
    5.30 +    scheduler := SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} scheduler_loop));
    5.31  
    5.32  
    5.33  
     6.1 --- a/src/Pure/Concurrent/simple_thread.ML	Thu Jan 29 13:58:02 2015 +0100
     6.2 +++ b/src/Pure/Concurrent/simple_thread.ML	Thu Jan 29 15:21:16 2015 +0100
     6.3 @@ -7,8 +7,9 @@
     6.4  signature SIMPLE_THREAD =
     6.5  sig
     6.6    val is_self: Thread.thread -> bool
     6.7 -  val attributes: bool -> Thread.threadAttribute list
     6.8 -  val fork: bool -> (unit -> unit) -> Thread.thread
     6.9 +  type params = {stack_limit: int option, interrupts: bool}
    6.10 +  val attributes: params -> Thread.threadAttribute list
    6.11 +  val fork: params -> (unit -> unit) -> Thread.thread
    6.12    val join: Thread.thread -> unit
    6.13    val interrupt_unsynchronized: Thread.thread -> unit
    6.14  end;
    6.15 @@ -18,14 +19,17 @@
    6.16  
    6.17  fun is_self thread = Thread.equal (Thread.self (), thread);
    6.18  
    6.19 -fun attributes interrupts =
    6.20 -  if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
    6.21 +type params = {stack_limit: int option, interrupts: bool};
    6.22  
    6.23 -fun fork interrupts body =
    6.24 +fun attributes {stack_limit, interrupts} =
    6.25 +  maximum_ml_stack stack_limit @
    6.26 +  (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
    6.27 +
    6.28 +fun fork params body =
    6.29    Thread.fork (fn () =>
    6.30      print_exception_trace General.exnMessage tracing (fn () =>
    6.31        body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
    6.32 -    attributes interrupts);
    6.33 +    attributes params);
    6.34  
    6.35  fun join thread =
    6.36    while Thread.isActive thread
     7.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     7.2 +++ b/src/Pure/ML-Systems/maximum_ml_stack_dummy.ML	Thu Jan 29 15:21:16 2015 +0100
     7.3 @@ -0,0 +1,7 @@
     7.4 +(*  Title:      Pure/ML-Systems/maximum_ml_stack_dummy.ML
     7.5 +
     7.6 +Maximum stack size (in words) for ML threads -- dummy version.
     7.7 +*)
     7.8 +
     7.9 +fun maximum_ml_stack (_: int option) : Thread.threadAttribute list = [];
    7.10 +
     8.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     8.2 +++ b/src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML	Thu Jan 29 15:21:16 2015 +0100
     8.3 @@ -0,0 +1,7 @@
     8.4 +(*  Title:      Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
     8.5 +
     8.6 +Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, or later.
     8.7 +*)
     8.8 +
     8.9 +fun maximum_ml_stack limit = [Thread.MaximumMLStack limit];
    8.10 +
     9.1 --- a/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 13:58:02 2015 +0100
     9.2 +++ b/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 15:21:16 2015 +0100
     9.3 @@ -66,6 +66,10 @@
     9.4  use "ML-Systems/multithreading.ML";
     9.5  use "ML-Systems/multithreading_polyml.ML";
     9.6  
     9.7 +if ML_System.name = "polyml-5.5.3"
     9.8 +then use "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
     9.9 +else use "ML-Systems/maximum_ml_stack_dummy.ML";
    9.10 +
    9.11  use "ML-Systems/unsynchronized.ML";
    9.12  val _ = PolyML.Compiler.forgetValue "ref";
    9.13  val _ = PolyML.Compiler.forgetType "ref";
    10.1 --- a/src/Pure/ML-Systems/smlnj.ML	Thu Jan 29 13:58:02 2015 +0100
    10.2 +++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jan 29 15:21:16 2015 +0100
    10.3 @@ -18,6 +18,7 @@
    10.4  use "ML-Systems/universal.ML";
    10.5  use "ML-Systems/thread_dummy.ML";
    10.6  use "ML-Systems/multithreading.ML";
    10.7 +use "ML-Systems/maximum_ml_stack_dummy.ML";
    10.8  use "ML-Systems/ml_name_space.ML";
    10.9  use "ML-Systems/ml_pretty.ML";
   10.10  structure PolyML = struct end;
    11.1 --- a/src/Pure/System/message_channel.ML	Thu Jan 29 13:58:02 2015 +0100
    11.2 +++ b/src/Pure/System/message_channel.ML	Thu Jan 29 15:21:16 2015 +0100
    11.3 @@ -59,7 +59,8 @@
    11.4    if Multithreading.available then
    11.5      let
    11.6        val mbox = Mailbox.create ();
    11.7 -      val thread = Simple_Thread.fork false (message_output mbox channel);
    11.8 +      val thread =
    11.9 +        Simple_Thread.fork {stack_limit = NONE, interrupts = false} (message_output mbox channel);
   11.10        fun send msg = Mailbox.send mbox (SOME msg);
   11.11        fun shutdown () =
   11.12          (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);