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