SMT-RAT
24.02
Toolbox for Strategic and Parallel Satisfiability-Modulo-Theories Solving
|
Backend for the Slurm workload manager. More...
#include <SlurmBackend.h>
Public Member Functions | |
bool | suspendable () const |
void | run (const Jobs &jobs, bool wait_for_termination) |
Run all tools on all benchmarks using Slurm. More... | |
void | process_results (const Jobs &jobs, bool check_finished) |
void | addResult (const Tool *tool, const fs::path &file, BenchmarkResult &&result) |
Add a result. More... | |
Protected Member Functions | |
virtual void | startTool (const Tool *) |
Hook for every tool at the beginning. More... | |
virtual void | finalize () |
Hook to allow for asynchronous backends to wait for jobs to terminate. More... | |
virtual void | execute (const Tool *, const fs::path &) |
Execute a single pair of tool and benchmark. More... | |
void | madeProgress (std::size_t files=1) |
Can be called to give information about the current progress, if available. More... | |
void | sanitize_results (const Jobs &jobs) const |
void | write_results (const Jobs &jobs) const |
Protected Attributes | |
std::size_t | mExpectedJobs |
Number of jobs that should be run. More... | |
std::atomic< std::size_t > | mFinishedJobs |
Number of jobs that are finished. More... | |
std::atomic< std::size_t > | mLastPercent |
Percentage of finished jobs when madeProgress() was last called. More... | |
Private Types | |
using | JobData = std::tuple< const Tool *, std::filesystem::path, BenchmarkResult > |
A job consists of a tool, an input file, a base dir and results. More... | |
Private Member Functions | |
void | parse_result_file (const Jobs &jobs, const std::filesystem::path &file, std::map< size_t, JobData > &results) |
Parse the content of an output file. More... | |
std::pair< std::size_t, std::size_t > | get_job_range (std::size_t n, std::size_t numJobs) const |
void | store_job_id (int jobid) |
std::vector< int > | load_job_ids () |
void | remove_job_ids () |
void | run_job_async (std::size_t n, const std::vector< JobData > &results, bool wait_for_termination) |
bool | collect_results (const Jobs &jobs, bool check_finished) override |
Private Attributes | |
std::mutex | mSubmissionMutex |
Mutex for submission delay. More... | |
std::mutex | mSlurmjobMutex |
Mutex for slurmjobs file. More... | |
Results | mResults |
Results of already completed jobs. More... | |
Backend for the Slurm workload manager.
The execution model is as follows: We create multiple jobs that each consists of multiple array jobs that each execute one slice of the task list. One array job executes Settings::slice_size entries of the task list. One job consists of Settings::array_size array jobs. We start as many jobs as necessary.
Definition at line 29 of file SlurmBackend.h.
|
private |
A job consists of a tool, an input file, a base dir and results.
Definition at line 32 of file SlurmBackend.h.
|
inlineinherited |
|
inlineoverrideprivatevirtual |
Reimplemented from benchmax::Backend.
Definition at line 177 of file SlurmBackend.h.
|
inlineprotectedvirtualinherited |
Execute a single pair of tool and benchmark.
Reimplemented in benchmax::LocalBackend, and benchmax::CondorBackend.
Definition at line 49 of file Backend.h.
|
inlineprotectedvirtualinherited |
|
inlineprivate |
Definition at line 97 of file SlurmBackend.h.
|
inlineprivate |
Definition at line 113 of file SlurmBackend.h.
|
inlineprotectedinherited |
|
inlineprivate |
Parse the content of an output file.
Definition at line 44 of file SlurmBackend.h.
|
inlineinherited |
|
inlineprivate |
Definition at line 127 of file SlurmBackend.h.
|
inline |
Run all tools on all benchmarks using Slurm.
Definition at line 222 of file SlurmBackend.h.
|
inlineprivate |
Definition at line 133 of file SlurmBackend.h.
|
inlineprotectedinherited |
|
inlineprotectedvirtualinherited |
|
inlineprivate |
Definition at line 105 of file SlurmBackend.h.
|
inline |
Definition at line 218 of file SlurmBackend.h.
|
inlineprotectedinherited |
|
protectedinherited |
|
protectedinherited |
|
protectedinherited |
Percentage of finished jobs when madeProgress() was last called.
|
privateinherited |
|
private |
Mutex for slurmjobs file.
Definition at line 41 of file SlurmBackend.h.
|
private |
Mutex for submission delay.
Definition at line 39 of file SlurmBackend.h.