src/Pure/ML-Systems/multithreading_polyml.ML
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;
2007-08-03 wenzelm 2007-08-03 tuned tracing;
2007-08-01 wenzelm 2007-08-01 tracing: level;
2007-08-01 wenzelm 2007-08-01 oops -- fixed syntax;
2007-08-01 wenzelm 2007-08-01 "running": PROTECTED wakeup; "cont": actually invoke wakeup!!
2007-07-30 wenzelm 2007-07-30 dequeue: wait loop while PROTECTED -- avoids race condition;
2007-07-29 wenzelm 2007-07-29 tuned msgs; tuned;
2007-07-29 wenzelm 2007-07-29 more informative tracing; tuned;
2007-07-29 wenzelm 2007-07-29 more informative tracing;
2007-07-29 wenzelm 2007-07-29 critical: improved diagostics; schedule: proper broadcast on wakeup condition;
2007-07-25 wenzelm 2007-07-25 renamed CRITICAL' to NAMED_CRITICAL; tuned messages;
2007-07-25 wenzelm 2007-07-25 added trace flag, official tracing operation; added named CRITICAL'; schedule: tuned signature, actually observe dependencies on running tasks;
2007-07-24 wenzelm 2007-07-24 renamed number_of_threads to max_threads; added schedule operator;
2007-07-24 wenzelm 2007-07-24 Multithreading in Poly/ML (version 5.1).