# HG changeset patch
# User wenzelm
# Date 1422541276 -3600
# Node ID fe665176064329aa4028b27744e8c4040cbf01b6
# Parent  58c4f3e1870fb5717e41bdef3d06122d0963edbb
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;

diff -r 58c4f3e1870f -r fe6651760643 etc/options
--- a/etc/options	Thu Jan 29 13:58:02 2015 +0100
+++ b/etc/options	Thu Jan 29 15:21:16 2015 +0100
@@ -66,6 +66,8 @@
   -- "maximum number of worker threads for prover process (0 = hardware max.)"
 option threads_trace : int = 0
   -- "level of tracing information for multithreading"
+option threads_stack_limit : real = 0.25
+  -- "maximum stack size for worker threads (in giga words, 0 = unlimited)"
 public option parallel_print : bool = true
   -- "parallel and asynchronous printing of results"
 public option parallel_proofs : int = 2
diff -r 58c4f3e1870f -r fe6651760643 src/HOL/Tools/Sledgehammer/async_manager.ML
--- a/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/HOL/Tools/Sledgehammer/async_manager.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -28,7 +28,7 @@
       Runtime.debugging NONE body () handle exn =>
         if Exn.is_interrupt exn then ()
         else writeln ("## INTERNAL ERROR ##\n" ^ Runtime.exn_message exn),
-      Simple_Thread.attributes interrupts);
+      Simple_Thread.attributes {stack_limit = NONE, interrupts = interrupts});
 
 val message_store_limit = 20
 val message_display_limit = 10
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/Concurrent/bash.ML
--- a/src/Pure/Concurrent/bash.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/Pure/Concurrent/bash.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -31,7 +31,7 @@
     val _ = cleanup_files ();
 
     val system_thread =
-      Simple_Thread.fork false (fn () =>
+      Simple_Thread.fork {stack_limit = NONE, interrupts = false} (fn () =>
         Multithreading.with_attributes Multithreading.private_interrupts (fn _ =>
           let
             val _ = File.write script_path script;
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/Concurrent/event_timer.ML
--- a/src/Pure/Concurrent/event_timer.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/Pure/Concurrent/event_timer.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -104,7 +104,7 @@
 
 fun manager_check manager =
   if is_some manager andalso Thread.isActive (the manager) then manager
-  else SOME (Simple_Thread.fork false manager_loop);
+  else SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} manager_loop);
 
 fun shutdown () =
   uninterruptible (fn restore_attributes => fn () =>
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/Concurrent/future.ML
--- a/src/Pure/Concurrent/future.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/Pure/Concurrent/future.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -258,12 +258,17 @@
   | SOME work => (worker_exec work; worker_loop name));
 
 fun worker_start name = (*requires SYNCHRONIZED*)
-  Unsynchronized.change workers (cons (Simple_Thread.fork false (fn () => worker_loop name),
-    Unsynchronized.ref Working))
+  let
+    val threads_stack_limit =
+      Real.floor (Options.default_real "threads_stack_limit" * 1024.0 * 1024.0 * 1024.0);
+    val stack_limit = if threads_stack_limit <= 0 then NONE else SOME threads_stack_limit;
+    val worker =
+      Simple_Thread.fork {stack_limit = stack_limit, interrupts = false}
+        (fn () => worker_loop name);
+  in Unsynchronized.change workers (cons (worker, Unsynchronized.ref Working)) end
   handle Fail msg => Multithreading.tracing 0 (fn () => "SCHEDULER: " ^ msg);
 
 
-
 (* scheduler *)
 
 fun scheduler_next () = (*requires SYNCHRONIZED*)
@@ -359,7 +364,8 @@
 fun scheduler_check () = (*requires SYNCHRONIZED*)
  (do_shutdown := false;
   if scheduler_active () then ()
-  else scheduler := SOME (Simple_Thread.fork false scheduler_loop));
+  else
+    scheduler := SOME (Simple_Thread.fork {stack_limit = NONE, interrupts = false} scheduler_loop));
 
 
 
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/Concurrent/simple_thread.ML
--- a/src/Pure/Concurrent/simple_thread.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/Pure/Concurrent/simple_thread.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -7,8 +7,9 @@
 signature SIMPLE_THREAD =
 sig
   val is_self: Thread.thread -> bool
-  val attributes: bool -> Thread.threadAttribute list
-  val fork: bool -> (unit -> unit) -> Thread.thread
+  type params = {stack_limit: int option, interrupts: bool}
+  val attributes: params -> Thread.threadAttribute list
+  val fork: params -> (unit -> unit) -> Thread.thread
   val join: Thread.thread -> unit
   val interrupt_unsynchronized: Thread.thread -> unit
 end;
@@ -18,14 +19,17 @@
 
 fun is_self thread = Thread.equal (Thread.self (), thread);
 
-fun attributes interrupts =
-  if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts;
+type params = {stack_limit: int option, interrupts: bool};
 
-fun fork interrupts body =
+fun attributes {stack_limit, interrupts} =
+  maximum_ml_stack stack_limit @
+  (if interrupts then Multithreading.public_interrupts else Multithreading.no_interrupts);
+
+fun fork params body =
   Thread.fork (fn () =>
     print_exception_trace General.exnMessage tracing (fn () =>
       body () handle exn => if Exn.is_interrupt exn then () (*sic!*) else reraise exn),
-    attributes interrupts);
+    attributes params);
 
 fun join thread =
   while Thread.isActive thread
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/ML-Systems/maximum_ml_stack_dummy.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/maximum_ml_stack_dummy.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -0,0 +1,7 @@
+(*  Title:      Pure/ML-Systems/maximum_ml_stack_dummy.ML
+
+Maximum stack size (in words) for ML threads -- dummy version.
+*)
+
+fun maximum_ml_stack (_: int option) : Thread.threadAttribute list = [];
+
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -0,0 +1,7 @@
+(*  Title:      Pure/ML-Systems/maximum_ml_stack_polyml-5.5.3.ML
+
+Maximum stack size (in words) for ML threads -- Poly/ML 5.5.3, or later.
+*)
+
+fun maximum_ml_stack limit = [Thread.MaximumMLStack limit];
+
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/ML-Systems/polyml.ML
--- a/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/Pure/ML-Systems/polyml.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -66,6 +66,10 @@
 use "ML-Systems/multithreading.ML";
 use "ML-Systems/multithreading_polyml.ML";
 
+if ML_System.name = "polyml-5.5.3"
+then use "ML-Systems/maximum_ml_stack_polyml-5.5.3.ML"
+else use "ML-Systems/maximum_ml_stack_dummy.ML";
+
 use "ML-Systems/unsynchronized.ML";
 val _ = PolyML.Compiler.forgetValue "ref";
 val _ = PolyML.Compiler.forgetType "ref";
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/ML-Systems/smlnj.ML
--- a/src/Pure/ML-Systems/smlnj.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/Pure/ML-Systems/smlnj.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -18,6 +18,7 @@
 use "ML-Systems/universal.ML";
 use "ML-Systems/thread_dummy.ML";
 use "ML-Systems/multithreading.ML";
+use "ML-Systems/maximum_ml_stack_dummy.ML";
 use "ML-Systems/ml_name_space.ML";
 use "ML-Systems/ml_pretty.ML";
 structure PolyML = struct end;
diff -r 58c4f3e1870f -r fe6651760643 src/Pure/System/message_channel.ML
--- a/src/Pure/System/message_channel.ML	Thu Jan 29 13:58:02 2015 +0100
+++ b/src/Pure/System/message_channel.ML	Thu Jan 29 15:21:16 2015 +0100
@@ -59,7 +59,8 @@
   if Multithreading.available then
     let
       val mbox = Mailbox.create ();
-      val thread = Simple_Thread.fork false (message_output mbox channel);
+      val thread =
+        Simple_Thread.fork {stack_limit = NONE, interrupts = false} (message_output mbox channel);
       fun send msg = Mailbox.send mbox (SOME msg);
       fun shutdown () =
         (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);