1 files changed, 98 insertions, 0 deletions
diff --git a/nixos/modules/programs/benchexec.nix b/nixos/modules/programs/benchexec.nix
new file mode 100644
index 0000000000000..652670c117ea3
--- /dev/null
+++ b/nixos/modules/programs/benchexec.nix
@@ -0,0 +1,98 @@
+{ lib
+, pkgs
+, config
+, options
+, ...
+}:
+let
+  cfg = config.programs.benchexec;
+  opt = options.programs.benchexec;
+
+  filterUsers = x:
+    if builtins.isString x then config.users.users ? ${x} else
+    if builtins.isInt    x then x                         else
+    throw "filterUsers expects string (username) or int (UID)";
+
+  uid = x:
+    if builtins.isString x then config.users.users.${x}.uid else
+    if builtins.isInt    x then x                           else
+    throw "uid expects string (username) or int (UID)";
+in
+{
+  options.programs.benchexec = {
+    enable = lib.mkEnableOption "BenchExec";
+    package = lib.options.mkPackageOption pkgs "benchexec" { };
+
+    users = lib.options.mkOption {
+      type = with lib.types; listOf (either str int);
+      description = ''
+        Users that intend to use BenchExec.
+        Provide usernames of users that are configured via {option}`${options.users.users}` as string,
+        and UIDs of "mutable users" as integers.
+        Control group delegation will be configured via systemd.
+        For more information, see <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#setting-up-cgroups>.
+      '';
+      default = [ ];
+      example = lib.literalExpression ''
+        [
+          "alice" # username of a user configured via ${options.users.users}
+          1007    # UID of a mutable user
+        ]
+      '';
+    };
+  };
+
+  config = lib.mkIf cfg.enable {
+    assertions = (map
+      (user: {
+        assertion = config.users.users ? ${user};
+        message = ''
+          The user '${user}' intends to use BenchExec (via `${opt.users}`), but is not configured via `${options.users.users}`.
+        '';
+      })
+      (builtins.filter builtins.isString cfg.users)
+    ) ++ (map
+      (id: {
+        assertion = config.users.mutableUsers;
+        message = ''
+          The user with UID '${id}' intends to use BenchExec (via `${opt.users}`), but mutable users are disabled via `${options.users.mutableUsers}`.
+        '';
+      })
+      (builtins.filter builtins.isInt cfg.users)
+    ) ++ [
+      {
+        assertion = config.systemd.enableUnifiedCgroupHierarchy == true;
+        message = ''
+          The BenchExec module `${opt.enable}` only supports control groups 2 (`${options.systemd.enableUnifiedCgroupHierarchy} = true`).
+        '';
+      }
+    ];
+
+    environment.systemPackages = [ cfg.package ];
+
+    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#setting-up-cgroups>.
+    systemd.services = builtins.listToAttrs (map
+      (user: {
+        name = "user@${builtins.toString (uid user)}";
+        value = {
+          serviceConfig.Delegate = "yes";
+          overrideStrategy = "asDropin";
+        };
+      })
+      (builtins.filter filterUsers cfg.users));
+
+    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#requirements>.
+    virtualisation.lxc.lxcfs.enable = lib.mkDefault true;
+
+    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#requirements>.
+    programs = {
+      cpu-energy-meter.enable = lib.mkDefault true;
+      pqos-wrapper.enable = lib.mkDefault true;
+    };
+
+    # See <https://github.com/sosy-lab/benchexec/blob/3.18/doc/INSTALL.md#kernel-requirements>.
+    security.unprivilegedUsernsClone = true;
+  };
+
+  meta.maintainers = with lib.maintainers; [ lorenzleutgeb ];
+}