src/Pure/Concurrent/future.ML
2009-09-29 wenzelm 2009-09-29 explicit indication of Unsynchronized.ref;
2009-09-28 wenzelm 2009-09-28 added fork_deps_pri;
2009-09-22 wenzelm 2009-09-22 full reserve of worker threads -- for improved CPU utilization;
2009-09-20 wenzelm 2009-09-20 tuned tracing;
2009-09-20 wenzelm 2009-09-20 scheduler backdoor: 9999 means 1 worker;
2009-09-16 wenzelm 2009-09-16 Synchronized.value does not require locking, since assigments are atomic; removed obsolete Synchronized.peek;
2009-08-27 wenzelm 2009-08-27 tuned tracing;
2009-08-01 wenzelm 2009-08-01 future scheduler: uninterruptible cancelation;
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 tuned tracing;
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-28 wenzelm 2009-07-28 eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-28 wenzelm 2009-07-28 future result: Synchronized.var;
2009-07-28 wenzelm 2009-07-28 Task_Queue.dequeue: explicit thread;
2009-07-28 wenzelm 2009-07-28 more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
2009-07-28 wenzelm 2009-07-28 interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
2009-07-28 wenzelm 2009-07-28 misc tuning;
2009-07-27 wenzelm 2009-07-27 interruptible: Thread.testInterrupt before changing thread attributes;
2009-07-27 wenzelm 2009-07-27 wait: absorb spurious interrupts; replaced wait_timeout by explicit wait_interruptible;
2009-07-27 wenzelm 2009-07-27 scheduler: shutdown spontaneously (after some delay) if queue is empty; scheduler_check: critical, only performed after fork/enqueue; shutdown: passively wait for termination;
2009-07-27 wenzelm 2009-07-27 join_next: do not yield, even if overloaded, to minimize "running" tasks;
2009-07-27 wenzelm 2009-07-27 tuned tracing;
2009-07-27 wenzelm 2009-07-27 cancel: improved reactivity due to more careful broadcasting; internal broadcast_all;
2009-07-27 wenzelm 2009-07-27 dequeue_towards: always return active tasks; join_work: imitate worker more closely, keep active if queue appears to be blocked for the moment -- it may become free again after some worker_finished event;
2009-07-27 wenzelm 2009-07-27 removed unused low-level interrupts;
2009-07-27 wenzelm 2009-07-27 tuned;
2009-07-27 wenzelm 2009-07-27 more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads; more specific signal vs. broadcast; execute/finish: more careful notification based on minimal/maximal status; tuned shutdown;
2009-07-25 wenzelm 2009-07-25 tuned tracing;
2009-07-22 wenzelm 2009-07-22 future_job: more robust Exn.capture outside thread attribute change;
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-07-21 wenzelm 2009-07-21 added worker_group; fork: default to subgroup of worker_group; removed obsolete fork_local; join/get_result: cumulative flattened exceptions; map: subgroup of worker_group;
2009-07-21 wenzelm 2009-07-21 propagate exceptions within future groups; Future.map: inherit group;
2009-07-21 wenzelm 2009-07-21 tuned;
2009-07-21 wenzelm 2009-07-21 tuned tracing; provide spare worker threads to saturate hardware while other workers wait during join;
2009-07-19 wenzelm 2009-07-19 more abstract Future.is_worker; Future.fork_local: inherit from worker (if available);
2009-07-19 wenzelm 2009-07-19 recovered a version of dequeue_towards (cf. bb7b5a5942c7); join_results: work only towards explicit dependencies -- otherwise could produce dynamic cycle (not recorded in queue);
2009-07-18 wenzelm 2009-07-18 scheduler: tuned tracing (status); join_wait: more robust is_finished check;
2009-06-14 wenzelm 2009-06-14 simplified join: do not record dependencies (which are slow, but were only required for dequeue_towards);
2009-06-14 wenzelm 2009-06-14 tuned join: produce less garbage while waiting;
2009-06-13 wenzelm 2009-06-13 simplified join_results: no longer work "towards" deps, which simplifies task queue management and maintains strict bottom up discipline (without "transfer of priority" to required futures); more efficient Task_Queue.dequeue, with internal cache (reduces wast of cycles with many idle workers); removed complicated/expensive Task_Queue.dequeue_towards;
2009-03-23 wenzelm 2009-03-23 future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
2009-03-21 wenzelm 2009-03-21 restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
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-18 wenzelm 2009-01-18 join_results: when dependencies are resulved (but not finished yet), always continue execution as worker thread -- improved parallelism at the cost of some reactivity;
2009-01-10 wenzelm 2009-01-10 added cancel_group;
2009-01-07 wenzelm 2009-01-07 more robust propagation of errors through bulk jobs;
2009-01-06 wenzelm 2009-01-06 tuned map: reduced overhead due to bulk jobs; tuned join_results: reduced overhead for finished futures; tuned;
2009-01-03 wenzelm 2009-01-03 more reactive scheduler: reduced loop timeout, propagate broadcast interrupt via TaskQueue.cancel_all;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue; generalized fork_background to fork_pri; reduced tracing; map: inherit task priority; removed unused focus;
2008-12-16 wenzelm 2008-12-16 removed old scheduler;
2008-12-06 wenzelm 2008-12-06 added constant value;
2008-12-04 wenzelm 2008-12-04 fork/map: no inheritance of group (structure is nested, not parallel); removed group thread_data; refined Future.fork interfaces, no longer export Future.future;
2008-12-04 wenzelm 2008-12-04 renamed type Future.T to future; added map combinator;
2008-10-21 wenzelm 2008-10-21 join_results: allow CRITICAL join of finished futures; added singleton join_result;
2008-10-21 wenzelm 2008-10-21 added Future.enabled check;
2008-10-13 wenzelm 2008-10-13 SimpleThread.synchronized;
2008-10-09 wenzelm 2008-10-09 replaced str_of by general peek;
2008-10-09 wenzelm 2008-10-09 future result: Interrupt invalidates group, but pretends success otherwise;
2008-10-08 wenzelm 2008-10-08 less tracing; removed heartbeat thread;
2008-10-08 wenzelm 2008-10-08 more careful handling of group interrupts; join control is uninterruptible; less tracing;