src/Pure/Concurrent/future.ML
2016-04-06 wenzelm 2016-04-06 clarified modules; tuned signature;
2016-04-02 wenzelm 2016-04-02 prefer infix operations;
2016-04-02 wenzelm 2016-04-02 tuned signature;
2016-04-02 wenzelm 2016-04-02 careful export of type-dependent functions, without losing their special status;
2016-03-18 wenzelm 2016-03-18 clarified modules; tuned signature;
2016-03-03 wenzelm 2016-03-03 clarified modules; tuned signature;
2016-02-18 wenzelm 2016-02-18 unconditional Multithreading; clarified files;
2015-11-03 wenzelm 2015-11-03 clarified modules;
2015-09-01 wenzelm 2015-09-01 thread context for exceptions from forks, e.g. relevant when printing errors; tuned signature;
2015-08-12 wenzelm 2015-08-12 default ML context for forks, e.g. relevant for debugging and toplevel pretty-printing;
2015-07-21 wenzelm 2015-07-21 more explicit thread identification;
2015-06-29 wenzelm 2015-06-29 improved scheduling for urgent tasks, using farm of replacement threads (may lead to factor 2 overloading, but CPUs are usually hyperthreaded);
2015-01-29 wenzelm 2015-01-29 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 wenzelm 2015-01-29 unused;
2015-01-29 wenzelm 2015-01-29 clarified worker_wait; clarified join_next/join_loop, with proper thread attributes to allow interrupting of join (e.g. via Lazy.force);
2015-01-10 wenzelm 2015-01-10 explicit shutdown of scheduler and worker thread farm, assuming Session.shutdown() before saving heap image; discontinued spontaneous thread expiration from TTY age to avoid sporadic Simple_Thread.fork, which is potentially fragile in situations of resource shortage;
2015-01-10 wenzelm 2015-01-10 discontinued worker_trend: prefer constant number of active + reserve threads; tuned exceptional situations;
2015-01-09 wenzelm 2015-01-09 permissive worker_start: failure to fork thread is deferred to later attempt to provide missing threads, without crashing scheduler;
2014-12-22 wenzelm 2014-12-22 discontinued central critical sections: NAMED_CRITICAL / CRITICAL;
2014-11-26 wenzelm 2014-11-26 load simple_thread.ML later, such that it benefits from redefined print_exception_trace;
2014-06-23 wenzelm 2014-06-23 more on "Futures"; removed obsolete comments;
2014-03-31 wenzelm 2014-03-31 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 wenzelm 2013-12-05 merged, resolving obvious conflicts in NEWS and src/Pure/System/isabelle_process.ML;
2013-11-28 wenzelm 2013-11-28 more official task context via Task_Queue.enroll, which is required to participate in group cancellation (e.g. to terminate command exec); tuned signature;
2013-11-20 wenzelm 2013-11-20 register actual group of nested worker context -- relevant for insulated cancellation of exec_ids (see also 78693e46a237, e0169f13bd37); tuned signature;
2013-11-11 wenzelm 2013-11-11 tuned signature;
2013-11-06 wenzelm 2013-11-06 tuned signature;
2013-08-25 wenzelm 2013-08-25 simplified Goal.forked_proofs: status is determined via group instead of dummy future (see also Pure/PIDE/execution.ML); clarified Task_Queue.group_status; tuned;
2013-08-25 wenzelm 2013-08-25 discontinued parallel_subproofs_saturation and related internal counters (superseded by parallel_subproofs_threshold and timing information); simplified Goal.future_enabled;
2013-07-29 wenzelm 2013-07-29 keep memo_exec execution running, which is important to cancel goal forks eventually; run as nested worker task to keep main group valid, even after cancelation of removed subgroups; do not memoize interrupt, but absorb it silently in main execution; Goal.purge_futures: rough sanity check of group status;
2013-07-11 wenzelm 2013-07-11 tuned signature; unified exceptions for this module;
2013-07-08 wenzelm 2013-07-08 allow worker guest threads, which participate actively in future joins, but are outside thread accounting;
2013-05-14 wenzelm 2013-05-14 more uniform Markup.print_real;
2013-04-09 wenzelm 2013-04-09 clarified protocol_message undefinedness;
2013-04-08 wenzelm 2013-04-08 discontinued odd magic number, which was once used for performance measurements;
2013-03-05 wenzelm 2013-03-05 removed unused Future.flat, while leaving its influence of Future.map (see bcd6b1aa4db5);
2013-03-03 wenzelm 2013-03-03 more uniform Future.map: always internalize failure; added Future.flat as fast-path operation;
2013-02-26 wenzelm 2013-02-26 disallow shutdown from worker, which would lead to deadlock since the scheduler cannot terminate;
2013-02-26 wenzelm 2013-02-26 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 wenzelm 2013-02-26 less eventful shutdown: merely wait for scheduler to terminate;
2013-02-26 wenzelm 2013-02-26 tuned messages;
2013-01-24 wenzelm 2013-01-24 report status more frequently on demand;
2013-01-19 wenzelm 2013-01-19 tuned signature;
2013-01-18 wenzelm 2013-01-18 more systematic task statistics;
2013-01-18 wenzelm 2013-01-18 added "tasks_proof" statistics, via slighly odd global reference Future.forked_proofs (NB: Future.report_status is intertwined with scheduler thread);
2013-01-17 wenzelm 2013-01-17 clarified Future.error_msg: slightly more robust id check, actually suppress displaced messages;
2013-01-16 wenzelm 2013-01-16 proper runtime position (cf. fe4714886d92 and Toplevel.error_msg) -- to make error messages actually appear in the document;
2013-01-16 wenzelm 2013-01-16 identify future results more carefully, to avoid odd duplication of error messages, notably from forked goals;
2013-01-16 wenzelm 2013-01-16 more explicit treatment of (optional) exception properties, notably for "serial" -- avoid conflict with startPosition = offset;
2013-01-16 wenzelm 2013-01-16 tuned signature;
2013-01-02 wenzelm 2013-01-02 inline ML statistics into build log;
2013-01-01 wenzelm 2013-01-01 more robust report_status: tolerate ML_statistics even if ignored right now, e.g. in batch build;
2012-12-07 wenzelm 2012-12-07 final report_status within SYNCHRONIZED part of scheduler loop: required for sanity of data;
2012-11-29 wenzelm 2012-11-29 more uniform ML statistics;
2012-11-28 wenzelm 2012-11-28 some support for ML runtime statistics;
2012-10-19 wenzelm 2012-10-19 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 wenzelm 2012-10-18 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 wenzelm 2012-10-18 tuned comment;
2012-10-18 wenzelm 2012-10-18 more official Future.terminate; tuned signature;
2012-10-17 wenzelm 2012-10-17 more robust cancel_now: avoid shooting yourself in the foot;