src/Pure/ML-Systems/multithreading.ML
2009-09-30 wenzelm 2009-09-30 tuned whitespace;
2009-09-30 wenzelm 2009-09-30 more uniform treatment of structure Unsynchronized in ML bootstrap phase;
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-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-03-20 wenzelm 2009-03-20 future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
2009-01-19 wenzelm 2009-01-19 removed Ids;
2008-10-09 wenzelm 2008-10-09 added enabled;
2008-10-02 wenzelm 2008-10-02 max_threads_value always 1 for dummy version;
2008-09-09 wenzelm 2008-09-09 proper values of no_interrupts, regular_interrupts;
2008-09-08 wenzelm 2008-09-08 removed unused sync_interrupts;
2008-09-07 wenzelm 2008-09-07 added sync_interrupts, regular_interrupts;
2008-09-07 wenzelm 2008-09-07 added no_interrupts; moved dummy thread structures to dummy_thread.ML;
2008-09-04 wenzelm 2008-09-04 provide dummy thread structures, including proper Thread.getLocal/setLocal; moved task/schedule to Concurrent/schedule.ML;
2008-02-16 wenzelm 2008-02-16 removed managed_process (cf. General/shell_process.ML);
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 renamed ML-Systems/multithreading_dummy.ML to ML-Systems/multithreading.ML;