src/Pure/Concurrent/future.ML
Fri, 19 Aug 2011 12:51:14 +0200 wenzelm more focused use of Multithreading.interrupted: retain interrupts within task group boundary, without loss of information;
Fri, 19 Aug 2011 12:03:44 +0200 wenzelm clarified Future.cond_forks: more uniform handling of exceptional situations;
Thu, 18 Aug 2011 16:07:58 +0200 wenzelm tuned comments;
Wed, 17 Aug 2011 23:37:23 +0200 wenzelm identify parallel exceptions where they emerge first -- to achieve unique results within evaluation graph;
Wed, 17 Aug 2011 22:14:22 +0200 wenzelm more systematic handling of parallel exceptions;
Mon, 15 Aug 2011 19:27:55 +0200 wenzelm explicit check of finished evaluation;
Sat, 13 Aug 2011 00:34:54 +0200 wenzelm immediate fork of initial workers -- avoid 5 ticks (250ms) for adaptive scheme (a07558eb5029);
Wed, 10 Aug 2011 16:26:05 +0200 wenzelm tuned signature;
Wed, 10 Aug 2011 16:05:14 +0200 wenzelm future_job: explicit indication of interrupts;
Wed, 10 Aug 2011 14:28:55 +0200 wenzelm synchronized cancel and flushing of Multithreading.interrupted state, to ensure that interrupts stay within task boundaries;
Wed, 10 Aug 2011 14:04:45 +0200 wenzelm tuned source structure;
Sat, 23 Jul 2011 22:22:21 +0200 wenzelm make double-sure that interrupts are flushed before executing new work (cf. 22f8c2483bd2);
Sat, 23 Jul 2011 21:29:56 +0200 wenzelm more detailed tracing;
Mon, 11 Jul 2011 22:55:47 +0200 wenzelm tuned signature -- corresponding to Scala version;
Tue, 05 Jul 2011 11:16:37 +0200 wenzelm tuned signature;
Thu, 23 Jun 2011 23:12:00 +0200 wenzelm more robust join_results: join_work needs to be uninterruptible, otherwise the task being dequeued by join_next might be never executed/finished!
Sat, 26 Mar 2011 21:28:04 +0100 wenzelm added Future.cond_forks convenience;
Fri, 18 Feb 2011 16:11:58 +0100 wenzelm less verbose tracing;
Wed, 09 Feb 2011 15:48:43 +0100 wenzelm tuned scope of Multithreading.interrupted vs. Multithreading.with_attributes;
Tue, 08 Feb 2011 16:11:52 +0100 wenzelm explicit Multithreading.interrupted to ensure that interrupts stay within the boundaries of managed evaluation blocks;
Fri, 04 Feb 2011 20:40:25 +0100 wenzelm tuned signature;
Wed, 02 Feb 2011 20:32:50 +0100 wenzelm eliminated slightly odd abstract type Task_Queue.deps;
Wed, 02 Feb 2011 15:04:09 +0100 wenzelm maintain Task_Queue.group within Task_Queue.task;
Wed, 02 Feb 2011 13:38:09 +0100 wenzelm Future.join_results: discontinued post-hoc recording of dynamic dependencies;
Tue, 01 Feb 2011 22:24:28 +0100 wenzelm more informative task timing: some dependency tracking;
Tue, 01 Feb 2011 21:05:22 +0100 wenzelm refined task timing: joining vs. waiting;
Mon, 31 Jan 2011 23:02:53 +0100 wenzelm tuned signature;
Mon, 31 Jan 2011 22:57:01 +0100 wenzelm support named tasks, for improved tracing;
Mon, 31 Jan 2011 21:54:49 +0100 wenzelm more direct Future.bulk, which potentially reduces overhead for Par_List;
Mon, 31 Jan 2011 16:34:10 +0100 wenzelm added basic task timing;
less more (0) -100 -50 -30 tip