Adding SLURM-compatibility to Benchexec

README.md

@@ -122,6 +122,7 @@ Contributors:
 - [Thomas Stieglmaier](https://stieglmaier.me/)
 - [Martin Yankov](https://github.com/marto97)
 - [Ilja Zakharov](https://github.com/IljaZakharov)
+- [Levente Bajczi](https://github.com/leventeBajczi)
 - and [lots of more people who integrated tools into BenchExec](https://github.com/sosy-lab/benchexec/graphs/contributors)
 
 ### Users of BenchExec

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 for use with CPAchecker
+    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 path to the singularity .sif file to use. Will bind $PWD to $HOME when run.",
+        )
+
+        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,86 @@
+<!--
+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, contact / tag in an issue: [Levente Bajczi](https://github.com/leventeBajczi)
+
+## Preliminaries
+
+* *SLURM* is an open-source job scheduling and workload management system used primarily in high-performance computing (HPC) environments.
+* *Singularity* 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
+
+* Singularity (optional), tested with `singularity-ce version 4.0.1`
+* SLURM, tested with `slurm 22.05.7` on `Red Hat Enterprise Linux 8.6 (Ootpa)`, kernel version `4.18.0-372.9.1.el8.x86_64`
+
+## 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
+
+The workflow is based on `localexecution.py`, and uses the same general layout. However, instead of delegating to `runexec`, it delegates to `srun`.
+
+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
+
+    Modifications to the script are necessary if the user on the host and the container differ (due to using $HOME). Also, files not under the current directory will not be visible.
+
+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. 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.
+4. For timed-out runs, where SLURM terminated the run, no CPU time values are available.

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