SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
CondorBackend.h
Go to the documentation of this file.
1 /**
2  * @file CondorBackend.h
3  * @author Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
4  */
5 
6 #pragma once
7 
8 #include <atomic>
9 #include <cstdlib>
10 #include <fstream>
11 #include <future>
12 
13 #include "Backend.h"
14 
15 #include "../logging.h"
16 
17 namespace benchmax {
18 
19 /**
20  * Backend for the HTCondor batch system.
21  * Currently submits all jobs individually and asynchronously waits for them to finish.
22  */
23 class CondorBackend: public Backend {
24 protected:
25  /// No-op version of execute.
26  virtual void execute(const Tool*, const fs::path&) {}
27 private:
28  /// List of processes that are currently running.
29  std::list<std::atomic<bool>> processes;
30 
31  /// Generate a submit file for the given job.
32  std::string generateSubmitFile(std::size_t ID, const Tool& tool, const BenchmarkSet& b) {
33  std::ofstream wrapper(".wrapper_" + std::to_string(ID));
34  wrapper << "#!/bin/sh" << std::endl;
35  wrapper << "ulimit -S -t " << std::chrono::seconds(settings_benchmarks().limit_time).count() << std::endl;
36  wrapper << "ulimit -S -v " << settings_benchmarks().limit_memory.kibi() << std::endl;
37  wrapper << "date +\"Start: %s%3N\"" << std::endl;
38  wrapper << tool.getCommandline("$*") << std::endl;
39  wrapper << "date +\"End: %s%3N\"" << std::endl;
40  wrapper.close();
41 
42  std::ofstream out(".jobs." + std::to_string(ID));
43  out << "executable = .wrapper_" << ID << std::endl;
44  out << "output = out/out." << ID << ".$(cluster).$(process)" << std::endl;
45  out << "error = out/err." << ID << ".$(cluster).$(process)" << std::endl;
46  out << "log = out/log." << ID << std::endl;
47  out << "periodic_hold = (time() - JobCurrentStartExecutingDate) > " << std::chrono::seconds(settings_benchmarks().limit_time).count() << std::endl;
48 
49  for (const auto& file: b) {
50  if (!tool.canHandle(file)) continue;
51  out << "transfer_input_files = " << file.native() << ", " << tool.binary().native() << std::endl;
52  out << "arguments = " << file.filename().native() << std::endl;
53  out << "queue" << std::endl;
54  }
55  out.close();
56  return ".jobs." + std::to_string(ID);
57  }
58 
59  /// Collect job results for the given id.
60  void collectResults(std::size_t ID) {
61  typedef fs::directory_iterator dirIt;
62 
63  for (dirIt it("out/"), end; it != end; ++it) {
64  std::string name = it->path().native();
65  if (name.find("out/out." + std::to_string(ID)) != std::string::npos) {
66 
67  }
68  }
69  }
70 
71  /// Run the given job and wait for its results.
72  void runAndWait(std::size_t ID, const std::string& submitFile, std::atomic<bool>& it) {
73  BENCHMAX_LOG_INFO("benchmax.condor", "Queueing batch " << ID << "...");
74  std::system(("condor_submit " + submitFile).c_str());
75  BENCHMAX_LOG_INFO("benchmax.condor", "Waiting for batch " << ID << "...");
76  std::system(("condor_wait out/log." + std::to_string(ID)).c_str());
77  BENCHMAX_LOG_INFO("benchmax.condor", "Collecting statistics for batch " << ID << "...");
78  collectResults(ID);
79  BENCHMAX_LOG_INFO("benchmax.condor", "Finished batch " << ID << ".");
80  it = true;
81  }
82 
83 public:
84  /// Run all tools on all benchmarks.
85  void run(const Jobs& /*jobs*/, bool /*wait_for_termination*/) {
86  BENCHMAX_LOG_INFO("benchmax.condor", "Generating submit files...");
87 
88  //for (const auto& tool: tools) {
89  // std::size_t ID = processes.size() + 1;
90  // std::string submitFile = generateSubmitFile(ID, *tool.get(), benchmarks);
91  // processes.emplace_back(false);
92  // std::async(&CondorBackend::runAndWait, this, ID, std::ref(submitFile), std::ref(processes.back()));
93  //}
94  //while (!processes.empty()) {
95  // while (!processes.front()) usleep(1000000);
96  // assert(processes.front());
97  // processes.pop_front();
98  //}
99  }
100 };
101 
102 }
#define BENCHMAX_LOG_INFO(channel, msg)
Log informational messages.
Definition: logging.h:53
Base class for all backends.
Definition: Backend.h:23
A set of benchmarks from some common base directory.
Definition: BenchmarkSet.h:12
Backend for the HTCondor batch system.
Definition: CondorBackend.h:23
void collectResults(std::size_t ID)
Collect job results for the given id.
Definition: CondorBackend.h:60
void run(const Jobs &, bool)
Run all tools on all benchmarks.
Definition: CondorBackend.h:85
virtual void execute(const Tool *, const fs::path &)
No-op version of execute.
Definition: CondorBackend.h:26
void runAndWait(std::size_t ID, const std::string &submitFile, std::atomic< bool > &it)
Run the given job and wait for its results.
Definition: CondorBackend.h:72
std::string generateSubmitFile(std::size_t ID, const Tool &tool, const BenchmarkSet &b)
Generate a submit file for the given job.
Definition: CondorBackend.h:32
std::list< std::atomic< bool > > processes
List of processes that are currently running.
Definition: CondorBackend.h:29
Represents a set of jobs, constructed as the cartesian product of a set of tools and a set of benchma...
Definition: Jobs.h:70
Base class for any tool.
Definition: Tool.h:38
virtual bool canHandle(const fs::path &) const
Checks whether this cool can handle this file type.
Definition: Tool.h:142
virtual std::string getCommandline(const std::string &file) const
Compose commandline for this tool and the given input file.
Definition: Tool.h:122
fs::path binary() const
Full path to the binary.
Definition: Tool.h:67
const auto & settings_benchmarks()
Return the benchmark settings.
Definition: benchmarks.h:41