diff --git a/cms/grading/Sandbox.py b/cms/grading/Sandbox.py index 75c2d8db94..7867006902 100644 --- a/cms/grading/Sandbox.py +++ b/cms/grading/Sandbox.py @@ -217,7 +217,7 @@ def __init__( # TODO: move all other common properties here. self.box_id: int = 0 self.fsize: int | None = None - self.dirs: list[tuple[str, str, str | None]] = [] + self.dirs: list[tuple[str | None, str, str | None]] = [] self.preserve_env: bool = False self.inherit_env: list[str] = [] self.set_env: dict[str, str] = {} @@ -966,6 +966,10 @@ def __init__(self, file_cacher, name=None, temp_dir=None): self.add_mapped_directory( self._home, dest=self._home_dest, options="rw") + # Create temporary directory on /dev/shm to prevent communication + # between sandboxes. + self.dirs.append((None, "/dev/shm", "tmp")) + # Set common environment variables. # Specifically needed by Python, that searches the home for # packages. @@ -1132,7 +1136,9 @@ def build_box_options(self) -> list[str]: if self.chdir is not None: res += ["--chdir=%s" % self.chdir] for src, dest, options in self.dirs: - s = dest + "=" + src + s = dest + if src is not None: + s += "=" + src if options is not None: s += ":" + options res += ["--dir=%s" % s]