forked from leanprover/lean4
-
Notifications
You must be signed in to change notification settings - Fork 0
/
time_task.cpp
90 lines (80 loc) · 2.83 KB
/
time_task.cpp
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
/*
Copyright (c) 2018 Microsoft Corporation. All rights reserved.
Released under Apache 2.0 license as described in the file LICENSE.
Author: Sebastian Ullrich
*/
#include <string>
#include <map>
#include "library/time_task.h"
#include "library/trace.h"
namespace lean {
static std::map<std::string, second_duration> * g_cum_times;
static mutex * g_cum_times_mutex;
LEAN_THREAD_PTR(time_task, g_current_time_task);
void report_profiling_time(std::string const & category, second_duration time) {
lock_guard<mutex> _(*g_cum_times_mutex);
(*g_cum_times)[category] += time;
}
void display_cumulative_profiling_times(std::ostream & out) {
if (g_cum_times->empty())
return;
sstream ss;
ss << "cumulative profiling times:\n";
for (auto const & p : *g_cum_times)
ss << "\t" << p.first << " " << display_profiling_time{p.second} << "\n";
// output atomically, like IO.print
out << ss.str();
}
void initialize_time_task() {
g_cum_times_mutex = new mutex;
g_cum_times = new std::map<std::string, second_duration>;
}
void finalize_time_task() {
delete g_cum_times;
delete g_cum_times_mutex;
}
time_task::time_task(std::string const & category, options const & opts, name decl) :
m_category(category) {
if (!m_category.size()) {
// ignore given block in timings of surrounding task, if any
if (g_current_time_task) {
m_timeit = optional<xtimeit>([](prof_clock::duration _) {});
m_parent_task = g_current_time_task;
g_current_time_task = this;
}
} else if (get_profiler(opts)) {
m_timeit = optional<xtimeit>(get_profiling_threshold(opts), [=](prof_clock::duration duration) mutable {
sstream ss;
ss << m_category;
if (decl)
ss << " of " << decl;
ss << " took " << display_profiling_time{duration} << "\n";
// output atomically, like IO.print
tout() << ss.str();
});
m_parent_task = g_current_time_task;
g_current_time_task = this;
}
}
time_task::~time_task() {
if (m_timeit) {
g_current_time_task = m_parent_task;
if (m_category.size()) {
report_profiling_time(m_category, m_timeit->get_elapsed());
if (m_parent_task)
// report exclusive times
m_parent_task->m_timeit->exclude_duration(m_timeit->get_elapsed_inclusive());
} else {
if (m_parent_task) {
m_parent_task->m_timeit->ignore(*m_timeit);
}
}
}
}
/* profileit {α : Type} (category : String) (opts : Options) (fn : Unit → α) : α */
extern "C" LEAN_EXPORT obj_res lean_profileit(b_obj_arg category, b_obj_arg opts, obj_arg fn) {
time_task t(string_to_std(category),
TO_REF(options, opts));
return apply_1(fn, box(0));
}
}