Sandbox: Mount a temporary directory on /dev/shm (#1484)

Author: prandla

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]