src/Pure/Concurrent/future.ML
2010-09-09 ago more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-08 ago explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-07-22 ago tuned comments;
2010-07-21 ago clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
2010-07-20 ago back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c);
2010-07-20 ago eliminated old-style sys_error/SYS_ERROR in favour of exception Fail -- after careful checking that there is no overlap with existing handling of that;
2010-07-04 ago general Future.report -- also for Toplevel.async_state;
2010-07-02 ago tuned white space;
2010-05-31 ago modernized some structure names, keeping a few legacy aliases;
2010-05-29 ago future result: retain plain Interrupt for vacuous group exceptions;
2010-05-21 ago future_job: propagate current Position.thread_data to the forked job -- this is important to provide a default position, e.g. for parallelizied Goal.prove within a package (proper command transactions are wrapped via Toplevel.setmp_thread_position);
2010-02-06 ago result: Single_Assignment.var;
2010-01-06 ago more robust cancelation, notably of passive futures without scheduler running;
2010-01-06 ago eliminated cache, which complicates the code without making a real difference (NB: deque_towards often disrupts caching, and daisy-chaining of workers already reduces queue overhead);
2010-01-06 ago tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
2010-01-05 ago added Future.promise/fulfill -- promised futures that are fulfilled by external means;
2009-11-05 ago scheduler: clarified interrupt attributes and handling;
2009-11-05 ago worker_next: plain signalling via work_available only, not scheduler_event;
2009-11-04 ago avoid broadcast work_available, use daisy-chained signal instead;
2009-11-04 ago worker_next: treat wait for work_available as Sleeping, not Waiting;
2009-11-04 ago worker activity: distinguish between waiting (formerly active) and sleeping;
2009-11-04 ago tuned;
2009-11-04 ago tuned thread data;
2009-11-04 ago worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
2009-11-03 ago slightly leaner and more direct control of worker activity etc.;
2009-10-22 ago use Synchronized.assign to achieve actual immutable results;
2009-10-01 ago added Task_Queue.depend (again) -- light-weight version for transitive graph;
2009-09-29 ago explicit indication of Unsynchronized.ref;
2009-09-28 ago added fork_deps_pri;
2009-09-22 ago full reserve of worker threads -- for improved CPU utilization;
2009-09-20 ago tuned tracing;
2009-09-20 ago scheduler backdoor: 9999 means 1 worker;
2009-09-16 ago Synchronized.value does not require locking, since assigments are atomic;
2009-08-27 ago tuned tracing;
2009-08-01 ago future scheduler: uninterruptible cancelation;
2009-08-01 ago renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
2009-07-30 ago tuned tracing;
2009-07-30 ago added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
2009-07-28 ago eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
2009-07-28 ago future result: Synchronized.var;
2009-07-28 ago Task_Queue.dequeue: explicit thread;
2009-07-28 ago more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
2009-07-28 ago interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
2009-07-28 ago misc tuning;
2009-07-27 ago interruptible: Thread.testInterrupt before changing thread attributes;
2009-07-27 ago wait: absorb spurious interrupts;
2009-07-27 ago scheduler: shutdown spontaneously (after some delay) if queue is empty;
2009-07-27 ago join_next: do not yield, even if overloaded, to minimize "running" tasks;
2009-07-27 ago tuned tracing;
2009-07-27 ago cancel: improved reactivity due to more careful broadcasting;
2009-07-27 ago dequeue_towards: always return active tasks;
2009-07-27 ago removed unused low-level interrupts;
2009-07-27 ago tuned;
2009-07-27 ago more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
2009-07-25 ago tuned tracing;
2009-07-22 ago future_job: more robust Exn.capture outside thread attribute change;
2009-07-21 ago future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
2009-07-21 ago added worker_group;
2009-07-21 ago propagate exceptions within future groups;
2009-07-21 ago tuned;