-
Notifications
You must be signed in to change notification settings - Fork 225
Description
Currently, there are two ways how BenchExec can handle file storage of a run (i.e., what happens to those files that a tool writes in directories with overlay or hidden mode, like /tmp by default):
- The default mode is "tmpfs": All written files remain in memory and are counted as part of the run's memory limit.
- The alternative is
--no-tmpfs: All files are written to a standard temporary directory, i.e., typically to disk (as they would be if written to a temporary directory outside of the container).
The tmpfs mode has the advantage of reproducible performance and that a tool cannot write arbitrary amounts of files. However, in some cases (like SAT-COMP) tools need to be able to write out large (100 GB) files that should not count against the memory limit. The problem is that in the no-tmpfs mode, we cannot reliably prevent a tool from writing out larger numbers of larger sizes of files than desired or prevent it from completely filling the disk. runexec has --filesCountLimit and --filesSizeLimit, but they are enforced only periodically through sampling, and for each sample we need to iterate through all files produced by the tool and sum ump their sizes. This is not as reliable as all other limits that BenchExec provides.
One way around this might be the following suggestion by @arminbiere: BenchExec could create a (potentially sparse) file on disk with a given size, create a file system in it, and then loop-mount that into the container for all temporary storage. This would guarantee that the tool cannot write more than the desired amount of data, we do not need any sampling or iteration over files, and if the tool attempts to exceed its storage quota it would get the usual ENOSPC error instead of being killed with out-of-memory (as in the tmpfs case).
The problem is that currently we cannot do this because the kernel does not allow us to mount regular file systems like ext4 in the container. Only special file systems like tmps and overlayfs are allowed without having root permissions on the system.
There might be some ways out of that:
- We could use Fuse and a project like
fuse2fsto mount the image in the container. This should work right now, but it might be slow on reads and writes. This could be a problem in particular for those use cases with large files (that would want to use this mode). In the long term, projects on speeding up Fuse could help. - Maybe the kernel eventually gets some simple file system that it allows to be mounted from image files in containers?
- Maybe we can have some privileged helper that creates and mounts the image for us and hands it over to us. That would need setup by the system administrators, but for many cases (like competitions) this might be acceptable. Writing such a helper securely could be difficult, but maybe there are already existing tools that do something like that, for example as part of existing container solutions? At least conceptually, as long as the helper creates the fresh file system and makes sure the underlying file is not accessible to anything except itself, meaning that all unprivileged processes can only access the mounted file system but not mess with the underlying storage, it should be a secure and fast solution.