SMT-RAT  24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
SSHBackend.h
Go to the documentation of this file.
1 /**
2  * @file SSHBackend.h
3  * @author Gereon Kremer <gereon.kremer@cs.rwth-aachen.de>
4  */
5 
6 #pragma once
7 
8 #include "Backend.h"
9 #include "ssh/SSHSettings.h"
10 #include <benchmax/config.h>
11 
12 #ifdef BENCHMAX_SSH
13 
14 #include "ssh/SSHScheduler.h"
15 
16 #include <future>
17 #include <queue>
18 
19 namespace benchmax {
20 /**
21  * Backend using remote computation nodes via SSH.
22  * This backend connects to one or more remote computations nodes via SSH and runs all benchmarks concurrently.
23  * The queueing is performed manually by the SSHScheduler class.
24  *
25  * Additionally to simply connecting multiple times, SSH also allows for multiplexing within a single connection.
26  * As SSH limits both the number of concurrent connections and the number of channels within a single connection, we combine both mechanisms.
27  * The number of concurrent connections is specified by `connections` while the number of channels is specified by `cores` of a Node.
28  */
29 class SSHBackend: public Backend {
30 private:
31  std::queue<std::future<bool>> jobs;
32 
33  void waitAndPop() {
34  jobs.front().wait();
35  jobs.pop();
36  madeProgress();
37  }
38  ssh::SSHScheduler* scheduler;
39 
40 protected:
41  virtual void startTool(const Tool* tool) {
42  scheduler->uploadTool(tool);
43  }
44  virtual void finalize() {
45  while (!jobs.empty()) waitAndPop();
46  scheduler->cleanupTools();
47  }
48  virtual void execute(const Tool* tool, const fs::path& file) {
49  // Make sure enough jobs are active.
50  while (scheduler->runningJobs() > scheduler->workerCount() * 2) {
51  if (jobs.front().wait_for(std::chrono::milliseconds(1)) == std::future_status::ready) {
52  waitAndPop();
53  }
54  }
55  BENCHMAX_LOG_DEBUG("benchmax.backend", "Starting job.");
56  jobs.push(std::async(std::launch::async, &ssh::SSHScheduler::executeJob, scheduler, tool, file, this));
57  }
58 public:
59  SSHBackend(): Backend() {
60  scheduler = new ssh::SSHScheduler();
61  }
62 };
63 
64 }
65 
66 #else
67 
68 namespace benchmax {
69 class SSHBackend: public Backend {
70 public:
73  /// Dummy if SSH is disabled.
74  void run(const Jobs&, bool /*wait_for_termination*/) {
75  BENCHMAX_LOG_ERROR("benchmax", "This version of benchmax was compiled without support for SSH.");
76  }
77 };
78 
79 }
80 
81 #endif
#define BENCHMAX_LOG_DEBUG(channel, msg)
Log debug messages.
Definition: logging.h:55
#define BENCHMAX_LOG_ERROR(channel, msg)
Log errors.
Definition: logging.h:49
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
virtual void finalize()
Hook to allow for asynchronous backends to wait for jobs to terminate.
Definition: Backend.h:45
virtual void execute(const Tool *, const fs::path &)
Execute a single pair of tool and benchmark.
Definition: Backend.h:49
virtual void startTool(const Tool *)
Hook for every tool at the beginning.
Definition: Backend.h:41
Represents a set of jobs, constructed as the cartesian product of a set of tools and a set of benchma...
Definition: Jobs.h:70
void run(const Jobs &, bool)
Dummy if SSH is disabled.
Definition: SSHBackend.h:74