src/Pure/Concurrent/task_queue.ML
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-30 wenzelm 2009-09-30 eliminated redundant bindings;
2009-07-28 wenzelm 2009-07-28 group status: Synchronized.var;
2009-07-28 wenzelm 2009-07-28 tuned;
2009-07-28 wenzelm 2009-07-28 Task_Queue.dequeue: explicit thread;
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 signature;
2009-07-27 wenzelm 2009-07-27 enqueue/finish: return minimal/maximal state of this task;
2009-07-25 wenzelm 2009-07-25 dequeue_towards: need to try imm_preds as well;
2009-07-25 wenzelm 2009-07-25 enqueue: maintain transitive closure, which simplifies dequeue_towards;
2009-07-21 wenzelm 2009-07-21 support for nested groups -- cancellation is propagated to peers and subgroups; added is_canceled; tuned;
2009-07-21 wenzelm 2009-07-21 propagate exceptions within future groups; Future.map: inherit group;
2009-07-21 wenzelm 2009-07-21 tuned dequeu_towards: try immediate tasks before expensive all_preds;
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 added group_id; added status;
2009-07-09 wenzelm 2009-07-09 renamed functor TableFun to Table, and GraphFun to Graph;
2009-06-14 wenzelm 2009-06-14 removed obsolete depend, add_job_acyclic; enqueue, finished: more careful update of cache;
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-01-06 wenzelm 2009-01-06 added is_valid; added extend: support bulk jobs; tuned;
2009-01-04 wenzelm 2009-01-04 cancel: unique threads;
2009-01-03 wenzelm 2009-01-03 added eq_group; opaque signature match prevents accidental task/group equality; added cancel_all;
2008-12-16 wenzelm 2008-12-16 renamed structure TaskQueue to Task_Queue; tasks are ordered according to priority, which has been generalized from bool to int; removed unused focus; tuned dequeue: single pass due to proper priority order; tuned dequeue_towards;
2008-12-16 wenzelm 2008-12-16 tuned enqueue: plain add_edge, acyclic not required here;
2008-12-06 wenzelm 2008-12-06 added new_task;
2008-10-09 wenzelm 2008-10-09 added invalidate_group; SimpleThread.interrupt;
2008-09-27 wenzelm 2008-09-27 dequeue_towards: return bound for unfinished tasks;
2008-09-23 wenzelm 2008-09-23 IntGraph.del_node;
2008-09-19 wenzelm 2008-09-19 future tasks: support boolean priorities (true = high, false = low/irrelevant);
2008-09-11 wenzelm 2008-09-11 added is_empty;
2008-09-11 wenzelm 2008-09-11 added focus, which indicates a particular collection of high-priority tasks; tuned;
2008-09-10 wenzelm 2008-09-10 tuned;
2008-09-10 wenzelm 2008-09-10 cancel: invalidate group implicitly, via bool ref; job: moved ok flag into group; added interrupt, interrupt_external for tasks;
2008-09-09 wenzelm 2008-09-09 simplified dequeue: provide Thread.self internally; simplified cancel: interrupt running threads internally; added depend; added dequeue_towards; misc tuning;
2008-09-09 wenzelm 2008-09-09 eliminated cache, access queue efficiently via IntGraph.get_first;
2008-09-09 wenzelm 2008-09-09 human-readable printing of TaskQueue.task/group;
2008-09-09 wenzelm 2008-09-09 job: explicit 'ok' status -- false for canceled jobs; group is now non-optional; tuned signature; replaced low-level interrupts by group cancel operation; misc tuning;
2008-09-08 wenzelm 2008-09-08 proper signature constraint;
2008-09-08 wenzelm 2008-09-08 moved thread data to future.ML (again); dequeue: include group; more interrupt operations; misc tuning;
2008-09-08 wenzelm 2008-09-08 Ordered queue of grouped tasks. formerly in future.ML; added thread data; added group; more robust dequeue: change into running here; misc tuning;