src/Pure/Concurrent/future.ML
2016-04-02 ago prefer infix operations;
2016-04-02 ago tuned signature;
2016-04-02 ago careful export of type-dependent functions, without losing their special status;
2016-03-18 ago clarified modules;
2016-03-03 ago clarified modules;
2016-02-18 ago unconditional Multithreading;
2015-11-03 ago clarified modules;
2015-09-01 ago thread context for exceptions from forks, e.g. relevant when printing errors;
2015-08-12 ago default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
2015-07-21 ago more explicit thread identification;
2015-06-29 ago improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-01-29 ago explicit threads_stack_limit (for recent Poly/ML SVN versions), which leads to soft interrupt instead of exhaustion of virtual memory, which is particularly relevant for the bigger address space of x86_64;
2015-01-29 ago unused;
2015-01-29 ago clarified worker_wait;
2015-01-10 ago explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image;
2015-01-10 ago discontinued worker_trend: prefer constant number of active + reserve threads;
2015-01-09 ago permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;
2014-12-22 ago discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
2014-11-26 ago load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
2014-06-23 ago more on "Futures";
2014-03-31 ago support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
2013-12-05 ago merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
2013-11-28 ago more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec);
2013-11-20 ago register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37);
2013-11-11 ago tuned signature;
2013-11-06 ago tuned signature;
2013-08-25 ago simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML);
2013-08-25 ago discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information);
2013-07-29 ago keep memo_exec execution running, which is important to cancel goal forks eventually;
2013-07-11 ago tuned signature;
2013-07-08 ago allow worker guest threads, which participate actively in future joins, but are outside thread accounting;
2013-05-14 ago more uniform Markup.print_real;
2013-04-09 ago clarified protocol_message undefinedness;
2013-04-08 ago discontinued odd magic number, which was once used for performance measurements;
2013-03-05 ago removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
2013-03-03 ago more uniform Future.map: always internalize failure;
2013-02-26 ago disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;
2013-02-26 ago signal work_available should be sufficient to initiate daisy-chained workers, and lead to separate broadcast work_finished eventually -- NB: broadcasting all worker threads tends to burn parallel CPU cycles;
2013-02-26 ago less eventful shutdown: merely wait for scheduler to terminate;
2013-02-26 ago tuned messages;
2013-01-24 ago report status more frequently on demand;
2013-01-19 ago tuned signature;
2013-01-18 ago more systematic task statistics;
2013-01-18 ago added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
2013-01-17 ago clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
2013-01-16 ago proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
2013-01-16 ago identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 ago more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-16 ago tuned signature;
2013-01-02 ago inline ML statistics into build log;
2013-01-01 ago more robust report_status: tolerate ML_statistics even if ignored right now, e.g. in batch build;
2012-12-07 ago final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;
2012-11-29 ago more uniform ML statistics;
2012-11-28 ago some support for ML runtime statistics;
2012-10-19 ago clarified Future.map (again): finished value is mapped in-place, which saves task structures and changes error behaviour slightly (tolerance against canceled group of old value etc.);
2012-10-18 ago more uniform group for map_future, which is relevant for cancel in worker_task vs. future_job -- prefer peer group despite 81d03a29980c;
2012-10-18 ago tuned comment;
2012-10-18 ago more official Future.terminate;
2012-10-17 ago more robust cancel_now: avoid shooting yourself in the foot;
2012-08-30 ago refined status of forked goals;