src/Pure/Concurrent/future.ML
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;
2008-10-03 wenzelm 2008-10-03 tuned tracing;
2008-10-03 wenzelm 2008-10-03 slower heartbeat;
2008-10-02 wenzelm 2008-10-02 added simple heartbeat thread;
2008-10-02 wenzelm 2008-10-02 more tuning of tracing messages;
2008-10-02 wenzelm 2008-10-02 tuned SYNCHRONIZED: outermost Exn.release; tuned tracing;
2008-10-01 wenzelm 2008-10-01 removed release_results (cf. Exn.release_all, Exn.release_first);
2008-09-30 wenzelm 2008-09-30 renamed Future.fork_irrelevant to Future.fork_background; tuned;
2008-09-29 wenzelm 2008-09-29 added str_of;
2008-09-28 wenzelm 2008-09-28 proper setmp_thread_data for nested execute (cf. join_loop);
2008-09-28 wenzelm 2008-09-28 thread_data: include thread name, export access; more tracing;
2008-09-27 wenzelm 2008-09-27 added release_results (formerly in par_list.ML); more informative trace_active; join_results: avoid deadlock via nested SYNCHRONOIZED, more robust active join, less rechecking of tasks;
2008-09-27 wenzelm 2008-09-27 more tracing;
2008-09-23 wenzelm 2008-09-23 join_results: special case for empty list, works without multithreading;
2008-09-22 wenzelm 2008-09-22 added is_finished;
2008-09-19 wenzelm 2008-09-19 future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-17 wenzelm 2008-09-17 shutdown only if Multithreading.available;
2008-09-16 wenzelm 2008-09-16 SimpleThread.fork;
2008-09-11 wenzelm 2008-09-11 cancel, shutdown: notify_all;
2008-09-11 wenzelm 2008-09-11 eliminated requests, use global state variables uniformly; more robust shutdown;
2008-09-11 wenzelm 2008-09-11 shutdown: global join-and-shutdown operation; reduced trace_active; scheduler_fork: always notify; tracing for thread exit; unique ids for workers;
2008-09-11 wenzelm 2008-09-11 added focus, which indicates a particular collection of high-priority tasks; tuned;
2008-09-11 wenzelm 2008-09-11 some general notes on future values;
2008-09-10 wenzelm 2008-09-10 added interrupt_task (external id); tuned signature;
2008-09-10 wenzelm 2008-09-10 replaced join_all by join_results, which returns Exn.results; join: disallow Multithreading.self_critical, which is prone to deadlocks due to context change via fork;
2008-09-10 wenzelm 2008-09-10 workers: explicit activity flag; SYNCHRONIZED: optional tracing;
2008-09-10 wenzelm 2008-09-10 future: allow explicit group; cancel: invalidate group identifier for all future members; tuned comments; tuned;
2008-09-09 wenzelm 2008-09-09 cancel: check_scheduler; adapted to simplified TaskQueue.cancel; improved join/join_all: actively work towards results, i.e. do not yield unnecessarily; misc tuning;
2008-09-09 wenzelm 2008-09-09 inherit group from running thread, or create a new one -- make it harder to re-use canceled groups; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;
2008-09-08 wenzelm 2008-09-08 tuned Mailbox.send;