@@ -54,18 +54,28 @@ let time_phase phase_name f =
5454
5555let report () =
5656 if ! enabled then (
57- let cmt_total = times.file_loading +. times.result_collection in
57+ (* NOTE about semantics:
58+ - [file_loading] is treated as the WALL-CLOCK time for the overall
59+ "CMT processing" phase (including per-file processing and any
60+ synchronization).
61+ - [result_collection] is an AGGREGATE metric across domains: time spent
62+ in (and waiting on) the mutex-protected result merge/collection
63+ section, summed across all worker domains. This may exceed wall-clock
64+ time in parallel runs.
65+ We do NOT add them together, otherwise we'd double-count. *)
66+ let cmt_total = times.file_loading in
5867 let analysis_total = times.merging +. times.solving in
5968 let total = cmt_total +. analysis_total +. times.reporting in
6069 Printf. eprintf " \n === Timing ===\n " ;
6170 Printf. eprintf " CMT processing: %.3fs (%.1f%%)\n " cmt_total
6271 (100.0 *. cmt_total /. total);
63- Printf. eprintf " - File loading: %.3fs\n " times.file_loading;
64- Printf. eprintf " - Result collection: %.3fs\n " times.result_collection;
72+ Printf. eprintf " - Wall clock: %.3fs\n " times.file_loading;
73+ Printf. eprintf " - Result collection: %.3fms (aggregate)\n "
74+ (1000.0 *. times.result_collection);
6575 Printf. eprintf " Analysis: %.3fs (%.1f%%)\n " analysis_total
6676 (100.0 *. analysis_total /. total);
67- Printf. eprintf " - Merging: %.3fs \n " times.merging;
68- Printf. eprintf " - Solving: %.3fs \n " times.solving;
77+ Printf. eprintf " - Merging: %.3fms \n " ( 1000.0 *. times.merging) ;
78+ Printf. eprintf " - Solving: %.3fms \n " ( 1000.0 *. times.solving) ;
6979 Printf. eprintf " Reporting: %.3fs (%.1f%%)\n " times.reporting
7080 (100.0 *. times.reporting /. total);
7181 Printf. eprintf " Total: %.3fs\n " total)
0 commit comments