src/Pure/ML-Systems/multithreading_polyml.ML
2013-12-12 ago simplified polyml-5.5.2 setup -- implicit upgrade of Thread.numProcessors;
2013-12-11 ago support for polml-5.5.2;
2013-01-16 ago tuned comments;
2012-11-18 ago adjust max_threads_value to capabilities of Poly/ML 5.5 and current hardware;
2012-08-22 ago clarified bootstrapping of Pure;
2012-05-24 ago discontinued support for Poly/ML 5.2.1;
2011-07-11 ago tuned signature -- corresponding to Scala version;
2011-02-08 ago added Multithreading.interrupted (cf. java.lang.Thread.interrupted);
2011-02-05 ago clarified bootstrapping of structure TimeLimit;
2010-11-27 ago removed bash from ML system bootstrap, and past the Secure ML barrier;
2010-11-02 ago simplified some time constants;
2010-09-22 ago renamed setmp_noncritical to Unsynchronized.setmp to emphasize its meaning;
2010-09-22 ago more robust lib/scripts/process, with explicit script/no_script mode;
2010-09-20 ago refined ML/Scala bash wrapper, based on more general lib/scripts/process;
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-02-07 ago modernized perl scripts: prefer standalone executables;
2010-02-06 ago renamed system/system_out to bash/bash_output -- to emphasized that this is really GNU bash, not some undefined POSIX sh;
2009-10-27 ago max_threads_value: eliminated tested_platform -- Poly/ML 5.3 fully supports linux, darwin, solaris, cygwin;
2009-10-26 ago implicit default is 4 cores -- more cost-effective;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-08-01 ago renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
2009-07-30 ago added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
2009-07-27 ago interruptible: Thread.testInterrupt before changing thread attributes;
2009-07-25 ago tuned tracing;
2009-07-25 ago added Multithreading.real_time;
2009-07-25 ago simplified/unified Multithreading.tracing_time;
2009-07-21 ago future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
2009-06-30 ago default to maximum max_threads;
2009-06-14 ago back to default -M max, with more robust interpretation of corresponding max_threads value;
2009-05-31 ago more precise version information;
2009-03-20 ago future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
2009-03-20 ago with_attributes: canonical capture/release scheme (potentially iron out race condition);
2009-01-19 ago removed Ids;
2009-01-18 ago with_attributes: make double sure that unsafe attributes are avoided;
2008-10-09 ago added enabled;
2008-10-02 ago with_attributes: enforces InterruptAsynch => InterruptAsynchOnce to avoid race condition;
2008-10-02 ago tracing: ignore failure of any kind;
2008-10-01 ago more robust treatment of Interrupt (cf. exn.ML);
2008-09-29 ago tuned comments;
2008-09-16 ago multithreading for Poly/ML 5.1 is no longer supported;
2008-09-08 ago removed unused sync_interrupts;
2008-09-07 ago added sync_interrupts, regular_interrupts;
2008-09-07 ago added no_interrupts;
2008-09-04 ago moved Multithreading.task/schedule to Concurrent/schedule.ML;
2008-03-31 ago before close: Exn.capture/release;
2008-03-29 ago CRITICAL: further trace levels for 1000ms and 100ms;
2008-03-25 ago moved multithreaded "profile" to multithreading_polyml.ML;
2008-03-11 ago schedule main control: more robust interrupting of potentially running threads;
2008-03-06 ago system_out: threaded version does not work for 5.1;
2008-02-19 ago added system_out (back to multithreaded version -- still suffers from non-interruptible wait in Poly/ML 5.1);
2008-02-16 ago removed managed_process (cf. General/shell_process.ML);
2008-02-15 ago support for managed external processes;
2008-01-02 ago added Multithreading.max_threads_value, which maps a value of 0 to number of CPUs;
2007-12-20 ago added get/put_data;
2007-12-18 ago signature BASIC_MULTITHREADING;
2007-09-24 ago replaced interrupt_timeout by TimeLimit.timeLimit (available on SML/NJ and Poly/ML 5.1);
2007-09-21 ago tuned;
2007-09-20 ago added interrupt_timeout;
2007-08-16 ago improved treatment of global interrupts: Thread.EnableBroadcastInterrupt, redefine ignore/raise_interrupt;
2007-08-15 ago main: wait_timeout (1 second);