src/Pure/ML-Systems/multithreading_polyml.ML
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;
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).