src/Pure/Concurrent/future.ML
Wed, 06 Jan 2010 18:22:43 +0100 wenzelm more robust cancelation, notably of passive futures without scheduler running;
Wed, 06 Jan 2010 18:14:16 +0100 wenzelm 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);
Wed, 06 Jan 2010 15:07:56 +0100 wenzelm tasks of canceled groups are considered "ready" -- enables to purge the queue from tasks depending on unfinished promises (also improves general reactivity);
Tue, 05 Jan 2010 23:38:10 +0100 wenzelm added Future.promise/fulfill -- promised futures that are fulfilled by external means;
Thu, 05 Nov 2009 13:16:22 +0100 wenzelm scheduler: clarified interrupt attributes and handling;
Thu, 05 Nov 2009 13:01:11 +0100 wenzelm worker_next: plain signalling via work_available only, not scheduler_event;
Wed, 04 Nov 2009 21:22:35 +0100 wenzelm avoid broadcast work_available, use daisy-chained signal instead;
Wed, 04 Nov 2009 20:31:36 +0100 wenzelm worker_next: treat wait for work_available as Sleeping, not Waiting;
Wed, 04 Nov 2009 11:58:29 +0100 wenzelm worker activity: distinguish between waiting (formerly active) and sleeping;
Wed, 04 Nov 2009 11:37:06 +0100 wenzelm tuned;
Wed, 04 Nov 2009 11:30:22 +0100 wenzelm tuned thread data;
Wed, 04 Nov 2009 00:29:58 +0100 wenzelm worker_next: ensure that work_available is passed on before sleeping (was occasionally lost when worker configuration changed, causing scheduler deadlock);
Tue, 03 Nov 2009 19:52:09 +0100 wenzelm slightly leaner and more direct control of worker activity etc.;
Thu, 22 Oct 2009 15:21:01 +0200 wenzelm use Synchronized.assign to achieve actual immutable results;
Thu, 01 Oct 2009 16:27:13 +0200 wenzelm added Task_Queue.depend (again) -- light-weight version for transitive graph;
Tue, 29 Sep 2009 11:49:22 +0200 wenzelm explicit indication of Unsynchronized.ref;
Mon, 28 Sep 2009 12:09:18 +0200 wenzelm added fork_deps_pri;
Tue, 22 Sep 2009 20:25:31 +0200 wenzelm full reserve of worker threads -- for improved CPU utilization;
Sun, 20 Sep 2009 19:17:33 +0200 wenzelm tuned tracing;
Sun, 20 Sep 2009 18:37:55 +0200 wenzelm scheduler backdoor: 9999 means 1 worker;
Wed, 16 Sep 2009 22:46:10 +0200 wenzelm Synchronized.value does not require locking, since assigments are atomic;
Thu, 27 Aug 2009 17:00:03 +0200 wenzelm tuned tracing;
Sat, 01 Aug 2009 00:17:03 +0200 wenzelm future scheduler: uninterruptible cancelation;
Sat, 01 Aug 2009 00:09:45 +0200 wenzelm renamed Multithreading.regular_interrupts to Multithreading.public_interrupts;
Thu, 30 Jul 2009 23:37:53 +0200 wenzelm tuned tracing;
Thu, 30 Jul 2009 23:06:06 +0200 wenzelm added Multithreading.sync_wait, which turns enabled interrupts to sync ones, to ensure that wait will reaquire its lock when interrupted;
Tue, 28 Jul 2009 16:30:23 +0200 wenzelm eliminated separate Future.enabled -- let Future.join fail explicitly in critical section, instead of entering sequential mode silently;
Tue, 28 Jul 2009 15:10:15 +0200 wenzelm future result: Synchronized.var;
Tue, 28 Jul 2009 14:35:27 +0200 wenzelm Task_Queue.dequeue: explicit thread;
Tue, 28 Jul 2009 14:29:25 +0200 wenzelm more precise treatment of scheduler_event: continous pulse (50ms) instead of flooding, which was burning many CPU cycles in spare threads;
Tue, 28 Jul 2009 14:11:15 +0200 wenzelm interruptible_task: unified treatment of Multithreading.with_attributes (cf. 9f6461b1c9cc);
Tue, 28 Jul 2009 14:04:33 +0200 wenzelm misc tuning;
Mon, 27 Jul 2009 17:36:30 +0200 wenzelm interruptible: Thread.testInterrupt before changing thread attributes;
Mon, 27 Jul 2009 17:12:19 +0200 wenzelm wait: absorb spurious interrupts;
Mon, 27 Jul 2009 16:53:28 +0200 wenzelm scheduler: shutdown spontaneously (after some delay) if queue is empty;
Mon, 27 Jul 2009 16:08:41 +0200 wenzelm join_next: do not yield, even if overloaded, to minimize "running" tasks;
Mon, 27 Jul 2009 15:53:43 +0200 wenzelm tuned tracing;
Mon, 27 Jul 2009 15:30:21 +0200 wenzelm cancel: improved reactivity due to more careful broadcasting;
Mon, 27 Jul 2009 15:06:33 +0200 wenzelm dequeue_towards: always return active tasks;
Mon, 27 Jul 2009 13:32:23 +0200 wenzelm removed unused low-level interrupts;
Mon, 27 Jul 2009 12:16:58 +0200 wenzelm tuned;
Mon, 27 Jul 2009 12:11:18 +0200 wenzelm more specific conditions: scheduler_event, work_available, work_finished -- considereably reduces overhead with many threads;
Sat, 25 Jul 2009 00:53:47 +0200 wenzelm tuned tracing;
Wed, 22 Jul 2009 10:46:35 +0200 wenzelm future_job: more robust Exn.capture outside thread attribute change;
Tue, 21 Jul 2009 23:42:29 +0200 wenzelm future_job: tight scope for interrupts, to prevent shooting ourselves in the foot via cancel_group;
Tue, 21 Jul 2009 20:37:31 +0200 wenzelm added worker_group;
Tue, 21 Jul 2009 15:25:22 +0200 wenzelm propagate exceptions within future groups;
Tue, 21 Jul 2009 13:42:48 +0200 wenzelm tuned;
Tue, 21 Jul 2009 11:30:12 +0200 wenzelm tuned tracing;
Sun, 19 Jul 2009 18:02:40 +0200 wenzelm more abstract Future.is_worker;
Sun, 19 Jul 2009 14:14:25 +0200 wenzelm recovered a version of dequeue_towards (cf. bb7b5a5942c7);
Sat, 18 Jul 2009 22:52:31 +0200 wenzelm scheduler: tuned tracing (status);
Sun, 14 Jun 2009 23:24:38 +0200 wenzelm simplified join: do not record dependencies (which are slow, but were only required for dequeue_towards);
Sun, 14 Jun 2009 02:21:46 +0200 wenzelm tuned join: produce less garbage while waiting;
Sat, 13 Jun 2009 19:40:37 +0200 wenzelm 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);
Mon, 23 Mar 2009 11:20:46 +0100 wenzelm future scheduler: reduced wait timeout if tasks need to be canceled -- to improve reactivity of interrupts;
Sat, 21 Mar 2009 13:11:12 +0100 wenzelm restricted interrupts for tasks running as future worker thread -- attempt to prevent interrupt race conditions;
Fri, 20 Mar 2009 20:20:09 +0100 wenzelm future_job: do not inherit attributes, but enforce restricted interrupts -- attempt to prevent interrupt race conditions;
Sun, 18 Jan 2009 16:42:43 +0100 wenzelm join_results: when dependencies are resulved (but not finished yet),
Sat, 10 Jan 2009 16:53:12 +0100 wenzelm added cancel_group;
less more (0) -100 -60 tip