From 901b50c303590e0fd12543f49a804e370f30b777 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Wed, 29 May 2024 08:23:49 +0200 Subject: [PATCH 1/8] Polish documentation for using BenchExec in a container We want to provide a full usable command line in the main installation docs and not have the information split on two documentation pages. Using the container mode of BenchExec is not so rare anymore that we document it separately. And because people misunderstand what to do for Docker, also copy the instructions for Docker into the main documentation. --- doc/INSTALL.md | 24 ++++++++++++++++++------ doc/container.md | 2 +- 2 files changed, 19 insertions(+), 7 deletions(-) diff --git a/doc/INSTALL.md b/doc/INSTALL.md index b5c90ce26..cb1816876 100644 --- a/doc/INSTALL.md +++ b/doc/INSTALL.md @@ -334,20 +334,32 @@ If you want to run BenchExec inside a container, we recommend Podman and systems with cgroups v2. Then use the following command-line arguments: - podman run --security-opt unmask=/sys/fs/cgroup --cgroups=split ... - -This will work if BenchExec is the main process inside the container, -otherwise you need to create an appropriate cgroup hierarchy inside the container, + podman run --security-opt unmask=/sys/fs/cgroup --cgroups=split --security-opt unmask=/proc/* --security-opt seccomp=unconfined ... + +This allows BenchExec to use cgroups and create its own containers inside the Podman container. + +Using Docker is also possible, but only using the `--privileged` argument. +However, this gives your Docker container *full root access* to the host, +so please also add the `--cap-drop=all` flag, +make sure to use this only with trusted images, +and configure your Docker container such that everything in it +is executed under a different user account, not as root. +BenchExec is not designed to run as root and does not provide +any safety guarantees regarding its container under this circumstances. + +For both Podman and Docker this will work +if BenchExec is the main process inside the container, +otherwise you need to manually create an appropriate cgroup hierarchy inside the container, i.e., one where BenchExec has its own separate cgroup. -For other cases, e.g., with cgroups v1, +For systems with cgroups v1, please use the following command line argument to mount the cgroup hierarchy within the container when starting it (same for Podman): docker run -v /sys/fs/cgroup:/sys/fs/cgroup:rw ... -Note that you additionally need some flags for container mode, +Note that you need some additional flags for container mode, which are explained in the [container documentation](container.md#using-benchexec-in-a-dockerpodman-container). ### Testing Cgroups Setup and Known Problems diff --git a/doc/container.md b/doc/container.md index a01b40b27..72772799e 100644 --- a/doc/container.md +++ b/doc/container.md @@ -185,7 +185,7 @@ because it provides "rootless" containers To use BenchExec within Podman, start it as a regular user (not root) and use the following arguments: ``` -podman run --security-opt unmask=/proc/* --security-opt unmask=/sys/fs/cgroup --security-opt seccomp=unconfined ... +podman run --security-opt unmask=/proc/* --security-opt seccomp=unconfined ... ``` You may additionally need the arguments documented for [cgroup usage](INSTALL.md#setting-up-cgroups-in-a-dockerpodman-container). From f00645e069ae05907f9cc854eec7ac1d8bc30e49 Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Wed, 29 May 2024 16:50:49 +0200 Subject: [PATCH 2/8] Update information in Btor2C's tool-info module --- benchexec/tools/btor2c.py | 8 ++++---- 1 file changed, 4 insertions(+), 4 deletions(-) diff --git a/benchexec/tools/btor2c.py b/benchexec/tools/btor2c.py index 51c7f93f0..0fe716a39 100644 --- a/benchexec/tools/btor2c.py +++ b/benchexec/tools/btor2c.py @@ -12,14 +12,14 @@ class Tool(benchexec.tools.template.BaseTool2): """ - Tool info for BTOR2C: A Converter from BTOR2 models to C programs + Tool info for Btor2C: A translator from Btor2 circuits to C programs """ def executable(self, tool_locator): - return tool_locator.find_executable("btor2code", subdir="build") + return tool_locator.find_executable("btor2c", subdir="build") def name(self): - return "BTOR2C" + return "Btor2C" def project_url(self): return "https://gitlab.com/sosy-lab/software/btor2c" @@ -30,7 +30,7 @@ def cmdline(self, executable, options, task, rlimits): def get_value_from_output(self, output, identifier): # search for the text in output and get its value, # search the first line, that starts with the searched text - # warn if there are more lines (multiple statistics from sequential analysis?) + # warn if there are more lines match = None for line in output: if line.lstrip().startswith(identifier): From e401d0d58b8ff1478505ac0d48bc94633d997e8d Mon Sep 17 00:00:00 2001 From: Po-Chun Chien Date: Wed, 29 May 2024 16:54:13 +0200 Subject: [PATCH 3/8] Extract Btor2C's version --- benchexec/tools/btor2c.py | 3 +++ 1 file changed, 3 insertions(+) diff --git a/benchexec/tools/btor2c.py b/benchexec/tools/btor2c.py index 0fe716a39..36d29f455 100644 --- a/benchexec/tools/btor2c.py +++ b/benchexec/tools/btor2c.py @@ -24,6 +24,9 @@ def name(self): def project_url(self): return "https://gitlab.com/sosy-lab/software/btor2c" + def version(self, executable): + return self._version_from_tool(executable, line_prefix="Btor2C version") + def cmdline(self, executable, options, task, rlimits): return [executable] + options + [task.single_input_file] From a89a9c6a8355897b23b12a6e0b4cc0947dfa91db Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 3 Jun 2024 13:38:28 +0200 Subject: [PATCH 4/8] Handle invalid cgroup setup more gracefully for cgroups v2 Inside a container with an invalid cgroups setup, such as cgroupns but using the host's cgroup filesystem, it can happen that our cgroup is shown by the kernel as "/../foo". This is an unusable cgroup. So far BenchExec would crash due to this, now we at least handle it like a cgroup without permissions. Fixes #1047. --- benchexec/cgroupsv2.py | 11 ++++++++++- 1 file changed, 10 insertions(+), 1 deletion(-) diff --git a/benchexec/cgroupsv2.py b/benchexec/cgroupsv2.py index 258d0cce7..67422151c 100644 --- a/benchexec/cgroupsv2.py +++ b/benchexec/cgroupsv2.py @@ -102,7 +102,7 @@ def initialize(): cgroup = CgroupsV2.from_system() - if list(cgroup.get_all_tasks()) == [os.getpid()]: + if cgroup.path and list(cgroup.get_all_tasks()) == [os.getpid()]: # If we are the only process, somebody prepared a cgroup for us. Use it. # We might be able to relax this check and for example allow child processes, # but then we would also have to move them to another cgroup, @@ -229,6 +229,12 @@ def _parse_proc_pid_cgroup(cgroup_file): mountpoint = _find_cgroup_mount() for line in cgroup_file: own_cgroup = line.strip().split(":")[2][1:] + if own_cgroup.startswith("../"): + # Our cgroup is outside the root cgroup! + # Happens inside containers with a cgroup namespace + # and an inappropriate cgroup config, such as bind-mounting the host cgroup. + logging.debug("Process is in unusable out-of-tree cgroup '%s'", own_cgroup) + return None path = mountpoint / own_cgroup return path @@ -308,6 +314,9 @@ def from_system(cls, cgroup_procinfo=None): else: cgroup_path = _parse_proc_pid_cgroup(cgroup_procinfo) + if not cgroup_path: + return cls({}) + try: with open(cgroup_path / "cgroup.controllers") as subsystems_file: subsystems = set(subsystems_file.readline().strip().split()) From 324bbc777855eb0afd87cadf9012119c66f6c89b Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 3 Jun 2024 17:07:04 +0200 Subject: [PATCH 5/8] Move log message to specific case because otherwise it is misleading --- benchexec/cgroupsv2.py | 6 +++--- 1 file changed, 3 insertions(+), 3 deletions(-) diff --git a/benchexec/cgroupsv2.py b/benchexec/cgroupsv2.py index 67422151c..9e6c164fb 100644 --- a/benchexec/cgroupsv2.py +++ b/benchexec/cgroupsv2.py @@ -306,10 +306,10 @@ def __init__(self, subsystems): @classmethod def from_system(cls, cgroup_procinfo=None): - logging.debug( - "Analyzing /proc/mounts and /proc/self/cgroup to determine cgroups." - ) if cgroup_procinfo is None: + logging.debug( + "Analyzing /proc/mounts and /proc/self/cgroup to determine cgroups." + ) cgroup_path = _find_own_cgroups() else: cgroup_path = _parse_proc_pid_cgroup(cgroup_procinfo) From 29480b32914356e182b598bf174e4c5ed2e63acc Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Mon, 3 Jun 2024 17:39:25 +0200 Subject: [PATCH 6/8] Add a fallback logic for locating a usable cgroup for cgroups v2 For cgroups v1 we already use /system.slice/benchexec-cgroup.service as a fallback cgroup if it exists and we cannot use our current cgroup. For cgroups v2 we do not yet have such a fallback. However, implementing this makes it much easier for people on systems without systemd (e.g., in a container) to setup and configure cgroups for BenchExec, so let's do this. Background discussion is in #1048, from which also the suggested commands in the documentation are taken. Thanks to @incaseoftrouble for reviewing the design of this. --- benchexec/cgroupsv2.py | 32 +++++++++++++++++++++++++++++--- doc/INSTALL.md | 17 +++++++++++++++++ 2 files changed, 46 insertions(+), 3 deletions(-) diff --git a/benchexec/cgroupsv2.py b/benchexec/cgroupsv2.py index 9e6c164fb..79dd14148 100644 --- a/benchexec/cgroupsv2.py +++ b/benchexec/cgroupsv2.py @@ -109,9 +109,9 @@ def initialize(): # which might not be a good idea. logging.debug("BenchExec was started in its own cgroup: %s", cgroup) - elif _create_systemd_scope_for_us(): - # If we can create a systemd scope for us and move ourselves in it, - # we have a usable cgroup afterwards. + elif _create_systemd_scope_for_us() or _try_fallback_cgroup(): + # If we can create a systemd scope for us or find a usable fallback cgroup + # and move ourselves in it, we have a usable cgroup afterwards. cgroup = CgroupsV2.from_system() else: @@ -192,6 +192,32 @@ def _create_systemd_scope_for_us(): return False +def _try_fallback_cgroup(): + """ + Attempt to locate a usable fallback cgroup. + If it is found this process is moved into it. + + @return: a boolean indicating whether this succeeded + """ + # Attempt to use /benchexec cgroup. + # If it exists, some deliberately created it for us to use. + # The following does this by just faking a /proc/self/cgroup for this case. + cgroup = CgroupsV2.from_system(["0::/benchexec"]) + if cgroup.path and not list(cgroup.get_all_tasks()): + logging.debug("Found existing cgroup /benchexec, using it as fallback.") + + # Create cgroup for this execution of BenchExec. + cgroup = cgroup.create_fresh_child_cgroup( + cgroup.subsystems.keys(), prefix="benchexec_" + ) + # Move ourselves to it such that for the rest of the code this looks as usual. + cgroup.add_task(os.getpid()) + + return True + + return False + + def _find_cgroup_mount(): """ Return the mountpoint of the cgroupv2 unified hierarchy. diff --git a/doc/INSTALL.md b/doc/INSTALL.md index cb1816876..3eabb5869 100644 --- a/doc/INSTALL.md +++ b/doc/INSTALL.md @@ -351,6 +351,23 @@ For both Podman and Docker this will work if BenchExec is the main process inside the container, otherwise you need to manually create an appropriate cgroup hierarchy inside the container, i.e., one where BenchExec has its own separate cgroup. +You can either start BenchExec as the only process in a fresh cgroup +or create an empty cgroup named `/benchexec`, +which BenchExec will then automatically use. +This cgroup should have as many controllers enabled and delegated to sub-cgroups as possible, +for example like this: +``` +mkdir -p /sys/fs/cgroup/benchexec +for controller in $(cat /sys/fs/cgroup/cgroup.controllers); do + echo "+$controller" > /sys/fs/cgroup/cgroup.subtree_control +done +for controller in $(cat /sys/fs/cgroup/benchexec/cgroup.controllers); do + echo "+$controller" > /sys/fs/cgroup/benchexec/cgroup.subtree_control +done +``` +Note that if no other cgroups exist, +you first need to create a different child cgroup +for all existing processes in the container. For systems with cgroups v1, please use the following command line argument From 618c2ba8befd72534d8562558a17af39821123d3 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Tue, 4 Jun 2024 07:46:01 +0200 Subject: [PATCH 7/8] Fix crash in fallback logic if /benchexec cgroup does not exist It is not nice to have to double-check this here but CgroupsV2.from_system() is also used for other cases and we cannot easily change it to return only a dummy cgroup if the cgroup does not exist. Once we get rid of cgroups v1 we might be able to refactor and clean up a lot of this. --- benchexec/cgroupsv2.py | 2 +- 1 file changed, 1 insertion(+), 1 deletion(-) diff --git a/benchexec/cgroupsv2.py b/benchexec/cgroupsv2.py index 79dd14148..11aefcc41 100644 --- a/benchexec/cgroupsv2.py +++ b/benchexec/cgroupsv2.py @@ -203,7 +203,7 @@ def _try_fallback_cgroup(): # If it exists, some deliberately created it for us to use. # The following does this by just faking a /proc/self/cgroup for this case. cgroup = CgroupsV2.from_system(["0::/benchexec"]) - if cgroup.path and not list(cgroup.get_all_tasks()): + if cgroup.path and os.path.isdir(cgroup.path) and not list(cgroup.get_all_tasks()): logging.debug("Found existing cgroup /benchexec, using it as fallback.") # Create cgroup for this execution of BenchExec. From 9997760a495853458f8cbcc9b56ac8a8b3f9cf05 Mon Sep 17 00:00:00 2001 From: Philipp Wendler Date: Fri, 7 Jun 2024 07:55:55 +0200 Subject: [PATCH 8/8] Fix stdin handling when getting version number from benchmarked tool In the function that most tool-info modules use for getting the version number from the tool, we did not specify what stdin of the tool should be. The unfortunate default for this is the same as stdin of the calling tool, i.e., BenchExec. This means that if a tool would read from stdin while we call it to get its version, it would either hang due to no input or even read from what the user attempted to pass to BenchExec. Both is not good and this happened in #1045. Now we explicitly specify /dev/null as stdin, such that when attempting to read the tool just gets EOF. We also use /dev/null for stdin by default for the actual tool execution since 564f18f (BenchExec 0.5), so I do not expect any problems. Tools who do not read from stdin are not affected, and for tools who do read it is just an improvement that they get EOF instead of waiting for input. --- benchexec/tools/template.py | 1 + 1 file changed, 1 insertion(+) diff --git a/benchexec/tools/template.py b/benchexec/tools/template.py index 2309f95dd..35d7de2b2 100644 --- a/benchexec/tools/template.py +++ b/benchexec/tools/template.py @@ -155,6 +155,7 @@ def _version_from_tool( [executable, arg], stdout=subprocess.PIPE, stderr=subprocess.PIPE, + stdin=subprocess.DEVNULL, universal_newlines=True, ) except OSError as e: