SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
Backend.h
Go to the documentation of this file.
1 /**
2  * @file Backend.h
3  * @author Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
4  */
5 
6 #pragma once
7 
8 #include "../results/Results.h"
9 #include "../settings/Settings.h"
10 #include "Jobs.h"
11 
12 #include <atomic>
13 
14 namespace benchmax {
15 
16 /**
17  * Base class for all backends.
18  * Offers appropriate hooks to model the whole workflow for backends where each job is executed individually.
19  * The run() method is called from ourside which first calls startTool() for every tool and then runs execute() for every pair of tool and benchmark.
20  * It also offers addResult() to store results and madeProgress() to provide a progress indication to the user.
21  * If a benchmark requires a completely different workflow, for example for a batch job, it should override the run() method.
22  */
23 class Backend {
24 private:
25  /// Results of already completed jobs.
27 protected:
28  /// Number of jobs that should be run.
29  std::size_t mExpectedJobs;
30  /// Number of jobs that are finished.
31  std::atomic<std::size_t> mFinishedJobs;
32  /// Percentage of finished jobs when madeProgress() was last called.
33  std::atomic<std::size_t> mLastPercent;
34 
36 
37  /**
38  * Hook for every tool at the beginning.
39  * Can be used to upload the tool to some remote system.
40  */
41  virtual void startTool(const Tool*) {}
42  /**
43  * Hook to allow for asynchronous backends to wait for jobs to terminate.
44  */
45  virtual void finalize() {};
46  /**
47  * Execute a single pair of tool and benchmark.
48  */
49  virtual void execute(const Tool*, const fs::path&) {}
50  /// Can be called to give information about the current progress, if available.
51  void madeProgress(std::size_t files = 1) {
52  mFinishedJobs += files;
53  std::size_t newPercent = mFinishedJobs * 100 / mExpectedJobs;
54  if (newPercent > mLastPercent) {
55  mLastPercent = newPercent;
56  BENCHMAX_LOG_INFO("benchmax", "Progress: " << mLastPercent << "% (" << mFinishedJobs << " / " << mExpectedJobs << ")");
57  }
58  }
59 
60  virtual bool collect_results(const Jobs& /*jobs*/, bool /*check_finished*/) { return true; }
61  void sanitize_results(const Jobs& jobs) const {
62  for (const auto& j: jobs) {
63  auto res = mResults.get(j.first, j.second);
64  if (!res && j.first->canHandle(j.second)) {
65  BENCHMAX_LOG_WARN("benchmax", "Missing result for " << j.first->name() << " on " << j.second);
66  BENCHMAX_LOG_WARN("benchmax", "Chances are that something went wrong, please check this!");
67  }
68  }
69  }
70  void write_results(const Jobs& jobs) const {
71  if (settings_benchmarks().output_file_xml != "") {
72  BENCHMAX_LOG_INFO("benchmax", "Writing results to " << settings_benchmarks().output_file_xml);
73  XMLWriter xml(settings_benchmarks().output_file_xml);
74  mResults.store(xml, jobs);
75  } else if (settings_benchmarks().output_file_csv != "") {
76  BENCHMAX_LOG_INFO("benchmax", "Writing results to " << settings_benchmarks().output_file_csv);
77  CSVWriter csv(settings_benchmarks().output_file_csv);
78  mResults.store(csv, jobs);
79  } else {
80  BENCHMAX_LOG_WARN("benchmax", "No output file specified, writing no results!");
81  }
82  }
83 
84 public:
85  bool suspendable() const {
86  return false;
87  }
88  void process_results(const Jobs& jobs, bool check_finished) {
89  if (collect_results(jobs, check_finished)) {
90  sanitize_results(jobs);
91  write_results(jobs);
92  } else {
93  BENCHMAX_LOG_WARN("benchmax", "Aborted.");
94  }
95  }
96  /// Add a result.
97  void addResult(const Tool* tool, const fs::path& file, BenchmarkResult&& result) {
98  tool->additionalResults(file, result);
99  if (result.answer == "segfault" && result.peak_memory_kbytes > settings_benchmarks().limit_memory.kibi()) {
100  result.answer = "memout";
101  }
102  result.additional.emplace("peak_memory_kbytes", std::to_string(result.peak_memory_kbytes)); // lazy hack
103  if (result.time > settings_benchmarks().limit_time + 2*settings_benchmarks().grace_time) {
104  BENCHMAX_LOG_WARN("benchmax", "Computation took longer than it should: " << carl::settings::duration(result.time) << " > " << settings_benchmarks().limit_time << " + " << settings_benchmarks().grace_time);
105  BENCHMAX_LOG_WARN("benchmax", "Offending command: " << tool->name() << " " << file);
106  }
107  result.cleanup(settings_benchmarks().limit_time);
108  mResults.addResult(tool, file, std::move(result));
109  }
110  /// Run the list of tools against the list of benchmarks.
111  void run(const Jobs& jobs, bool wait_for_termination) {
112  mExpectedJobs = jobs.size();
113  BENCHMAX_LOG_INFO("benchmax", "Running " << mExpectedJobs << " now.");
114  if (!wait_for_termination) {
115  BENCHMAX_LOG_INFO("benchmax", "Running jobs synchronously.");
116  }
117 
118  for (const auto& tool: jobs.tools()) {
119  this->startTool(tool.get());
120  }
121  for (const auto& [tool, file]: jobs.randomized()) {
122  this->execute(tool, file);
123  }
124  this->finalize();
125  }
126 };
127 
128 }
#define BENCHMAX_LOG_WARN(channel, msg)
Log warnings.
Definition: logging.h:51
#define BENCHMAX_LOG_INFO(channel, msg)
Log informational messages.
Definition: logging.h:53
Base class for all backends.
Definition: Backend.h:23
void madeProgress(std::size_t files=1)
Can be called to give information about the current progress, if available.
Definition: Backend.h:51
void addResult(const Tool *tool, const fs::path &file, BenchmarkResult &&result)
Add a result.
Definition: Backend.h:97
void write_results(const Jobs &jobs) const
Definition: Backend.h:70
std::atomic< std::size_t > mLastPercent
Percentage of finished jobs when madeProgress() was last called.
Definition: Backend.h:33
void run(const Jobs &jobs, bool wait_for_termination)
Run the list of tools against the list of benchmarks.
Definition: Backend.h:111
virtual void finalize()
Hook to allow for asynchronous backends to wait for jobs to terminate.
Definition: Backend.h:45
void sanitize_results(const Jobs &jobs) const
Definition: Backend.h:61
std::atomic< std::size_t > mFinishedJobs
Number of jobs that are finished.
Definition: Backend.h:31
void process_results(const Jobs &jobs, bool check_finished)
Definition: Backend.h:88
virtual void execute(const Tool *, const fs::path &)
Execute a single pair of tool and benchmark.
Definition: Backend.h:49
virtual bool collect_results(const Jobs &, bool)
Definition: Backend.h:60
std::size_t mExpectedJobs
Number of jobs that should be run.
Definition: Backend.h:29
Results mResults
Results of already completed jobs.
Definition: Backend.h:26
bool suspendable() const
Definition: Backend.h:85
virtual void startTool(const Tool *)
Hook for every tool at the beginning.
Definition: Backend.h:41
Writes results to a csv file.
Definition: CSVWriter.h:18
Represents a set of jobs, constructed as the cartesian product of a set of tools and a set of benchma...
Definition: Jobs.h:70
auto size() const
Returns the overall number of jobs.
Definition: Jobs.h:96
const auto & tools() const
Returns the set of tools.
Definition: Jobs.h:88
auto randomized() const
Returns all jobs in a pseudo-randomized order.
Definition: Jobs.h:109
Stores results for for whole benchmax run.
Definition: Results.h:33
void store(Database &db)
Store all results to some database.
Definition: Results.h:69
std::optional< std::reference_wrapper< const BenchmarkResult > > get(const Tool *tool, const fs::path &file) const
Definition: Results.h:41
void addResult(const Tool *tool, const fs::path &file, BenchmarkResult &&results)
Add a new result.
Definition: Results.h:54
Base class for any tool.
Definition: Tool.h:38
std::string name() const
Common name of this tool.
Definition: Tool.h:62
virtual void additionalResults(const fs::path &, BenchmarkResult &) const
Recover additional results from the tool output.
Definition: Tool.h:152
Writes results to a xml file.
Definition: XMLWriter.h:18
const auto & settings_benchmarks()
Return the benchmark settings.
Definition: benchmarks.h:41
Results for a single benchmark run.