src/Pure/ML-Systems/multithreading_polyml.ML
Thu, 24 May 2012 15:01:17 +0200 wenzelm discontinued support for Poly/ML 5.2.1;
Mon, 11 Jul 2011 22:55:47 +0200 wenzelm tuned signature -- corresponding to Scala version;
Tue, 08 Feb 2011 14:09:24 +0100 wenzelm added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
Sat, 05 Feb 2011 18:09:57 +0100 wenzelm clarified bootstrapping of structure TimeLimit;
Sat, 27 Nov 2010 16:29:53 +0100 wenzelm removed bash from ML system bootstrap, and past the Secure ML barrier;
Tue, 02 Nov 2010 20:55:12 +0100 wenzelm simplified some time constants;
Wed, 22 Sep 2010 18:21:48 +0200 wenzelm renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
Wed, 22 Sep 2010 00:45:42 +0200 wenzelm more robust lib/scripts/process, with explicit script/no_script mode;
Mon, 20 Sep 2010 23:36:26 +0200 wenzelm refined ML/Scala bash wrapper, based on more general lib/scripts/process;
Thu, 09 Sep 2010 17:20:27 +0200 wenzelm more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
Sun, 07 Feb 2010 20:21:38 +0100 wenzelm modernized perl scripts: prefer standalone executables;
Sat, 06 Feb 2010 14:50:55 +0100 wenzelm renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
Tue, 27 Oct 2009 10:54:25 +0100 wenzelm max_threads_value: eliminated tested_platform -- Poly/ML 5.3 fully supports linux, darwin, solaris, cygwin;
Mon, 26 Oct 2009 11:36:23 +0100 wenzelm implicit default is 4 cores -- more cost-effective;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Sat, 01 Aug 2009 00:09:45 +0200 wenzelm renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
Thu, 30 Jul 2009 23:06:06 +0200 wenzelm added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
Mon, 27 Jul 2009 17:36:30 +0200 wenzelm interruptible: Thread.testInterrupt before changing thread attributes;
Sat, 25 Jul 2009 00:53:47 +0200 wenzelm tuned tracing;
Sat, 25 Jul 2009 00:39:05 +0200 wenzelm added Multithreading.real_time;
Sat, 25 Jul 2009 00:13:39 +0200 wenzelm simplified/unified Multithreading.tracing_time;
Tue, 21 Jul 2009 23:42:29 +0200 wenzelm future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
Tue, 30 Jun 2009 22:12:46 +0200 wenzelm default to maximum max_threads;
Sun, 14 Jun 2009 23:18:32 +0200 wenzelm back to default -M max, with more robust interpretation of corresponding max_threads value;
Sun, 31 May 2009 14:46:44 +0200 wenzelm more precise version information;
Fri, 20 Mar 2009 20:20:09 +0100 wenzelm future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
Fri, 20 Mar 2009 11:08:59 +0100 wenzelm with_attributes: canonical capture/release scheme (potentially iron out race condition);
Mon, 19 Jan 2009 19:38:03 +0100 wenzelm removed Ids;
Sun, 18 Jan 2009 16:33:09 +0100 wenzelm with_attributes: make double sure that unsafe attributes are avoided;
Thu, 09 Oct 2008 20:53:24 +0200 wenzelm added enabled;
Thu, 02 Oct 2008 21:21:21 +0200 wenzelm with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
Thu, 02 Oct 2008 19:59:01 +0200 wenzelm tracing: ignore failure of any kind;
Wed, 01 Oct 2008 12:00:02 +0200 wenzelm more robust treatment of Interrupt (cf. exn.ML);
Mon, 29 Sep 2008 11:46:52 +0200 wenzelm tuned comments;
Tue, 16 Sep 2008 18:01:24 +0200 wenzelm multithreading for Poly/ML 5.1 is no longer supported;
Mon, 08 Sep 2008 20:33:29 +0200 wenzelm removed unused sync_interrupts;
Sun, 07 Sep 2008 22:20:15 +0200 wenzelm added sync_interrupts, regular_interrupts;
Sun, 07 Sep 2008 17:46:41 +0200 wenzelm added no_interrupts;
Thu, 04 Sep 2008 16:03:47 +0200 wenzelm moved Multithreading.task/schedule to Concurrent/schedule.ML;
Mon, 31 Mar 2008 23:08:55 +0200 wenzelm before close: Exn.capture/release;
Sat, 29 Mar 2008 19:14:15 +0100 wenzelm CRITICAL: further trace levels for 1000ms and 100ms;
Tue, 25 Mar 2008 12:14:17 +0100 wenzelm moved multithreaded "profile" to multithreading_polyml.ML;
Tue, 11 Mar 2008 20:30:46 +0100 wenzelm schedule main control: more robust interrupting of potentially running threads;
Thu, 06 Mar 2008 20:17:51 +0100 wenzelm system_out: threaded version does not work for 5.1;
Tue, 19 Feb 2008 20:34:30 +0100 wenzelm added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
Sat, 16 Feb 2008 16:44:02 +0100 wenzelm removed managed_process (cf. General/shell_process.ML);
Fri, 15 Feb 2008 23:22:02 +0100 wenzelm support for managed external processes;
Wed, 02 Jan 2008 16:32:53 +0100 wenzelm added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
Thu, 20 Dec 2007 21:12:02 +0100 wenzelm added get/put_data;
Tue, 18 Dec 2007 22:21:42 +0100 wenzelm signature BASIC_MULTITHREADING;
Mon, 24 Sep 2007 13:52:50 +0200 wenzelm replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
Fri, 21 Sep 2007 22:51:13 +0200 wenzelm tuned;
Thu, 20 Sep 2007 20:58:40 +0200 wenzelm added interrupt_timeout;
Thu, 16 Aug 2007 18:53:22 +0200 wenzelm improved treatment of global interrupts: Thread.EnableBroadcastInterrupt, redefine ignore/raise_interrupt;
Wed, 15 Aug 2007 22:21:13 +0200 wenzelm main: wait_timeout (1 second);
Fri, 10 Aug 2007 14:49:01 +0200 wenzelm (un)interruptible: pass-through original thread attributes;
Thu, 09 Aug 2007 23:53:50 +0200 wenzelm schedule: more precise task model;
Fri, 03 Aug 2007 16:28:23 +0200 wenzelm tuned tracing;
Wed, 01 Aug 2007 17:03:28 +0200 wenzelm tracing: level;
Wed, 01 Aug 2007 16:50:16 +0200 wenzelm oops -- fixed syntax;
less more (0) -60 tip