Adding SLURM-compatibility to Benchexec

README.md

@@ -98,6 +98,7 @@ Maintainer: [Philipp Wendler](https://www.philippwendler.de)
 
 Contributors:
 - [Aditya Arora](https://github.com/alohamora)
+- [Levente Bajczi](https://github.com/leventeBajczi)
 - [Dirk Beyer](https://www.sosy-lab.org/people/beyer/)
 - [Laura Bschor](https://github.com/laurabschor)
 - [Thomas Bunk](https://github.com/TBunk)

contrib/README.md

@@ -16,6 +16,7 @@ Content:
 - `create_yaml_files.py`: Script for creating task-definition files from old input files that have expected verdicts encoded in the file name
 - [`p4-benchmark.py`](p4): BenchExec extension for [P4](https://p4.org/) programs for programmable switches
 - [`plots`](plots): Scripts and examples for generating plots from BenchExec results using Gnuplot or PGFPlots for LaTeX
+- [`slurm-benchmark.py`](slurm): BenchExec extension for execution benchmark runs via [SLURM](https://slurm.schedmd.com/documentation.html)
 - `serveFileFromZIP.php`: Script for letting a web server serve files from a ZIP archive as if the archive would have been expanded. This is useful for hosting HTML tables with results and links to log files in ZIP archives.
 - `vcloud-benchmark.py`: BenchExec extension for executing benchmark runs on the VerifierCloud service
 

contrib/slurm-benchmark.py

@@ -0,0 +1,75 @@
+#!/usr/bin/env python3
+
+# This file is part of BenchExec, a framework for reliable benchmarking:
+# https://github.com/sosy-lab/benchexec
+#
+# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
+# SPDX-FileCopyrightText: 2024 Levente Bajczi
+# SPDX-FileCopyrightText: Critical Systems Research Group
+# SPDX-FileCopyrightText: Budapest University of Technology and Economics <https://www.ftsrg.mit.bme.hu>
+#
+# SPDX-License-Identifier: Apache-2.0
+
+import logging
+import os
+import sys
+
+import benchexec.benchexec
+import benchexec.tools
+import benchexec.util
+
+sys.dont_write_bytecode = True  # prevent creation of .pyc files
+
+# Add ./benchmark/tools to __path__ of benchexec.tools package
+# such that additional tool-wrapper modules can be placed in this directory.
+benchexec.tools.__path__ = [
+    os.path.join(os.path.dirname(__file__), "benchmark", "tools")
+] + benchexec.tools.__path__
+
+
+class Benchmark(benchexec.benchexec.BenchExec):
+    """
+    An extension of BenchExec to execute benchmarks using SLURM,
+    optionally via Singularity.
+    """
+
+    def create_argument_parser(self):
+        parser = super(Benchmark, self).create_argument_parser()
+
+        slurm_args = parser.add_argument_group("Options for using SLURM")
+        slurm_args.add_argument(
+            "--slurm",
+            dest="slurm",
+            action="store_true",
+            help="Use SLURM to execute benchmarks.",
+        )
+        slurm_args.add_argument(
+            "--singularity",
+            dest="singularity",
+            type=str,
+            help="The path to the singularity .sif file to use. Will bind $PWD to $HOME when run.",
+        )
+        slurm_args.add_argument(
+            "--scratchdir",
+            dest="scratchdir",
+            type=str,
+            default="./",
+            help="The directory where temporary directories can be created for use within singularity.",
+        )
+
+        return parser
+
+    def load_executor(self):
+        if self.config.slurm:
+            from slurm import slurmexecutor as executor
+        else:
+            logging.warning(
+                "SLURM flag was not specified. Benchexec will be executed only on the local machine."
+            )
+            executor = super(Benchmark, self).load_executor()
+
+        return executor
+
+
+if __name__ == "__main__":
+    benchexec.benchexec.main(Benchmark())

contrib/slurm/README.md

@@ -0,0 +1,87 @@
+<!--
+This file is part of BenchExec, a framework for reliable benchmarking:
+https://github.com/sosy-lab/benchexec
+
+SPDX-FileCopyrightText: 2021 Dirk Beyer <https://www.sosy-lab.org>
+SPDX-FileCopyrightText: 2024 Levente Bajczi
+SPDX-FileCopyrightText: Critical Systems Research Group
+SPDX-FileCopyrightText: Budapest University of Technology and Economics <https://www.ftsrg.mit.bme.hu>
+
+SPDX-License-Identifier: Apache-2.0
+-->
+# BenchExec Extension for Benchmarking via SLURM
+
+This Python script extends BenchExec, a benchmarking framework, to facilitate benchmarking via SLURM, optionally using a Singularity container.
+
+In case of problems, please tag in an [issue](https://github.com/sosy-lab/benchexec/issues/new/choose): [Levente Bajczi](https://github.com/leventeBajczi) (@leventeBajczi).
+
+## Preliminaries
+
+* [SLURM](https://slurm.schedmd.com/documentation.html) is an open-source job scheduling and workload management system used primarily in high-performance computing (HPC) environments.
+* [Singularity](https://docs.sylabs.io/guides/latest/user-guide/) is a containerization platform designed for scientific and high-performance computing (HPC) workloads, providing users with a reproducible and portable environment for running applications and workflows.
+
+## Requirements
+
+* SLURM, tested with `slurm 22.05.7`, should work within `22.x.x`
+* Singularity (optional), tested with `singularity-ce version 4.0.1`, should work within `4.x.x`
+
+## Usage
+1. Run the script with Python 3:
+   ```
+   python3 $BENCHEXEC_FOLDER/contrib/slurm-benchmark.py [options]
+   ```
+   Options:
+   - `--slurm`: Use SLURM to execute benchmarks. Will revert to regular (local) benchexec if not given. 
+   - `--singularity <path_to_sif>`: Specify the path to the Singularity .sif file to use. See usage later.
+   - `--scratchdir <path>`: Specify the directory for temporary files. The script will use this parameter to create temporary directories for file storage per-run, which get discarded later. By default, this is the CWD, which might result in temporary files being generated by the thousands in the working directory. On some systems, this must be on the same mount, or even under the same hierarchy as the current directory. Must exist, be writable, and be a directory.
+   - `-N <N>`: Specify the factor of parallelism, i.e., how many instances to start at a time. Tested with up to `1000`, probably works with much higher values as well.
+
+## Overview of the Workflow
+
+This works similarly to BenchExec, however, instead of delegating each run to `runexec`, it delegates to `srun` from SLURM.
+
+1. If the `--singularity` option is given, the script wraps the command to run in a container. This is useful for dependency management (in most HPC environments, arbitrary package installations are frowned upon). For a simple container, use the following: 
+
+    ```singularity
+    BootStrap: docker
+    From: ubuntu:22.04
+
+    %post
+    apt -y update
+    apt -y install openjdk-17-jre-headless libgomp1 libmpfr-dev fuse-overlayfs
+    ```
+
+    Use `singularity build [--remote / --fakeroot] --fix-perms <name>.sif <name>.def` to build the container.
+
+    Notice the `fuse-overlayfs` package. That is mandatory for the overlay filesystem to work properly.
+
+    The script parameterizes `singularity exec` with the following params:
+    * `-B $PWD:/lower`: Bind the working directory to `/lower` (could be read-only)
+    * `--no-home`: Do not bind the home directory
+    * `-B {tempdir}:/overlay`: Bind the temporary directory to `/overlay` (must be writeable)
+    * `--fusemount  "container:fuse-overlayfs -o lowerdir=/lower -o upperdir=/overlay/upper -o workdir=/overlay/work $HOME"`: mount an overlay filesystem at $HOME, where modifications go in the temp dir but files can be read from the current dir
+
+2. Currently, the following parameters are passed to `srun` (calculated from the benchmark's parameters):
+   * `-t <hh:mm:ss>` CPU timelimit (generally, SLURM will round up to nearest minute)
+   * `-c <cpus>` number of cpus 
+   * `--threads-per-core=1` only use one thread per core
+   * `--mem-per-cpu <mem/cpus>` memory allocaiton in MBs per cpu
+   * `--ntasks=1` number of tasks per node
+
+3. The script parses the resulting job ID, and after the job finishes, runs `seff` to gather resource usage data:
+   * Exit code
+   * CPU time [s]
+   * Wall time [s]
+   * Memory [MB]
+
+## Limitations
+
+Currently, there are the following limitations compared to local benchexec:
+
+1. No advanced resource constraining / monitoring: only CPU time, CPU core and memory limits are handled, and only CPU time, wall time, and memory usage are monitored.
+2. No exotic paths in the command are handled: only the current working directory and its children are visible in the container
+3. The  user on the host and the container should not differ (due to using $HOME in the commands).
+4. Without singularity, no constraint is placed on the resulting files of the runs: this will populate the current directory with all the output files of all the runs.
+5. For timed-out runs, where SLURM terminated the run, no CPU time values are available.
+6. The executor only works with hyperthreading disabled, due to the inability to query nodes about the number of threads per core. Assuming it's always 2 is risky, as it may not hold true universally. Consequently, because we can only request whole cores from SLURM instead of threads, we must divide the requested number of threads by the threads-per-core value, which is unknown if hyperthreading could be enabled.
+7. Cancelling a benchmark run (by sending SIGINT) could be delayed up to a few minutes depending on the SLURM configuration.  

contrib/slurm/__init__.py

@@ -0,0 +1,9 @@
+# This file is part of BenchExec, a framework for reliable benchmarking:
+# https://github.com/sosy-lab/benchexec
+#
+# SPDX-FileCopyrightText: 2007-2020 Dirk Beyer <https://www.sosy-lab.org>
+# SPDX-FileCopyrightText: 2024 Levente Bajczi
+# SPDX-FileCopyrightText: Critical Systems Research Group
+# SPDX-FileCopyrightText: Budapest University of Technology and Economics <https://www.ftsrg.mit.bme.hu>
+#
+# SPDX-License-Identifier: Apache-2.0