src/Pure/Concurrent/future.ML
2010-11-02 wenzelm 2010-11-02 simplified some time constants;
2010-09-10 wenzelm 2010-09-10 Future.promise: more robust treatment of concurrent abort vs. fulfill (amending 047c96f41455);
2010-09-09 wenzelm 2010-09-09 more abstract treatment of interrupts in structure Exn -- hardly ever need to mention Interrupt literally;
2010-08-08 wenzelm 2010-08-08 explicitly distinguish Output.status (essential feedback) vs. Output.report (useful markup);
2010-07-22 wenzelm 2010-07-22 tuned comments;
2010-07-21 wenzelm 2010-07-21 clarified/exported Future.worker_subgroup, which is already the default for Future.fork;
2010-07-20 wenzelm 2010-07-20 back to more strict dependencies, even for canceled groups (reverting parts of 02936e77a07c); cancel passive tasks more actively via Exn.Interrupt, by treating them like ragular jobs here; attempts to re-assign canceled futures/promises raise Exn.Interrupt; tuned;
2010-07-20 wenzelm 2010-07-20 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; tuned some error messages;
2010-07-04 wenzelm 2010-07-04 general Future.report -- also for Toplevel.async_state;
2010-07-02 wenzelm 2010-07-02 tuned white space;
2010-05-31 wenzelm 2010-05-31 modernized some structure names, keeping a few legacy aliases;
2010-05-29 wenzelm 2010-05-29 future result: retain plain Interrupt for vacuous group exceptions;
2010-05-21 wenzelm 2010-05-21 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 wenzelm 2010-02-06 result: Single_Assignment.var;
2010-01-06 wenzelm 2010-01-06 more robust cancelation, notably of passive futures without scheduler running;
2010-01-06 wenzelm 2010-01-06 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 wenzelm 2010-01-06 tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity); shutdown: back to synchronous wait, which means no asynchronous interrupts within the loop;
2010-01-05 wenzelm 2010-01-05 added Future.promise/fulfill -- promised futures that are fulfilled by external means; Future.value: official result assignment -- produces immutable ref; Future.shutdown: raw_wait keeps raw task attributes, e.g. asynchronous interrupts of toplevel; Task_Queue: passive tasks track dependencies, but lack any evaluation process; tuned;
2009-11-05 wenzelm 2009-11-05 scheduler: clarified interrupt attributes and handling;
2009-11-05 wenzelm 2009-11-05 worker_next: plain signalling via work_available only, not scheduler_event; scheduler: tuned worker pool adjustments;
2009-11-04 wenzelm 2009-11-04 avoid broadcast work_available, use daisy-chained signal instead; max_threads: allow as much as 4 * m, after extra delay;
2009-11-04 wenzelm 2009-11-04 worker_next: treat wait for work_available as Sleeping, not Waiting; max_threads: simple adaptive scheme between m and 2 * m;
2009-11-04 wenzelm 2009-11-04 worker activity: distinguish between waiting (formerly active) and sleeping; tuned;
2009-11-04 wenzelm 2009-11-04 tuned;
2009-11-04 wenzelm 2009-11-04 tuned thread data;
2009-11-04 wenzelm 2009-11-04 worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock); worker_start: back to non-self version; scheduler: status output based on ticks;
2009-11-03 wenzelm 2009-11-03 slightly leaner and more direct control of worker activity etc.;
2009-10-22 wenzelm 2009-10-22 use Synchronized.assign to achieve actual immutable results;
2009-10-01 wenzelm 2009-10-01 added Task_Queue.depend (again) -- light-weight version for transitive graph; Future.join_results: record explicit dependency, detect direct task-task join cycles; Future.join_results: no change of interruptibility, allows to interrupt wait; added Future.worker_task; ThyInfo.schedule_futures: uninterruptible outer join;
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;