src/Pure/System/host.scala

clarified database content: store actual value instead of index;

/*  Title:      Pure/System/host.scala
    Author:     Makarius

Information about compute hosts, including NUMA: Non-Uniform Memory Access of
separate CPU nodes.

See also https://www.open-mpi.org/projects/hwloc --- notably "lstopo" or
"hwloc-ls" (e.g. via Ubuntu package "hwloc").
*/

package isabelle


object Host {
  /* allocated resources */

  object Node_Info { def none: Node_Info = Node_Info("", None) }

  sealed case class Node_Info(hostname: String, numa_node: Option[Int])


  /* available NUMA nodes */

  private val numa_info_linux: Path = Path.explode("/sys/devices/system/node/online")

  def numa_nodes(enabled: Boolean = true, ssh: SSH.System = SSH.Local): List[Int] = {
    val Single = """^(\d+)$""".r
    val Multiple = """^(\d+)-(\d+)$""".r

    def parse(s: String): List[Int] =
      s match {
        case Single(Value.Int(i)) => List(i)
        case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
        case _ => error("Cannot parse CPU NUMA node specification: " + quote(s))
      }

    val numa_info = if (ssh.isabelle_platform.is_linux) Some(numa_info_linux) else None
    for {
      path <- numa_info.toList
      if enabled && ssh.is_file(path)
      s <- space_explode(',', ssh.read(path).trim)
      n <- parse(s)
    } yield n
  }


  /* process policy via numactl tool */

  def numactl(node: Int): String = "numactl -m" + node + " -N" + node
  def numactl_ok(node: Int): Boolean = Isabelle_System.bash(numactl(node) + " true").ok

  def process_policy(node: Int): String = if (numactl_ok(node)) numactl(node) else ""

  def process_policy_options(options: Options, numa_node: Option[Int]): Options =
    numa_node match {
      case None => options
      case Some(n) => options.string("process_policy") = process_policy(n)
    }

  def perhaps_process_policy_options(options: Options): Options = {
    val numa_node =
      try {
        numa_nodes() match {
          case ns if ns.length >= 2 && numactl_ok(ns.head) => Some(ns.head)
          case _ => None
        }
      }
      catch { case ERROR(_) => None }
    process_policy_options(options, numa_node)
  }


  /* shuffling of NUMA nodes */

  def numa_check(progress: Progress, enabled: Boolean): Boolean = {
    def warning =
      numa_nodes() match {
        case ns if ns.length < 2 => Some("no NUMA nodes available")
        case ns if !numactl_ok(ns.head) => Some("bad numactl tool")
        case _ => None
      }

    enabled &&
      (warning match {
        case Some(s) =>
          progress.echo_warning("Shuffling of NUMA CPU nodes is disabled: " + s)
          false
        case _ => true
      })
  }


  /* SQL data model */

  object Data {
    def make_table(name: String, columns: List[SQL.Column], body: String = ""): SQL.Table =
      SQL.Table("isabelle_host" + if_proper(name, "_" + name), columns, body = body)

    object Node_Info {
      val hostname = SQL.Column.string("hostname").make_primary_key
      val numa_next = SQL.Column.int("numa_next")

      val table = make_table("node_info", List(hostname, numa_next))
    }

    def read_numa_next(db: SQL.Database, hostname: String): Int =
      db.using_statement(
        Node_Info.table.select(List(Node_Info.numa_next),
          sql = Node_Info.hostname.where_equal(hostname))
      )(stmt => stmt.execute_query().iterator(_.int(Node_Info.numa_next)).nextOption.getOrElse(0))

    def update_numa_next(db: SQL.Database, hostname: String, numa_next: Int): Boolean =
      if (read_numa_next(db, hostname) != numa_next) {
        db.using_statement(
          Node_Info.table.delete(sql = Node_Info.hostname.where_equal(hostname))
        )(_.execute())
        db.using_statement(Node_Info.table.insert()) { stmt =>
          stmt.string(1) = hostname
          stmt.int(2) = numa_next
          stmt.execute()
        }
        true
      }
      else false
  }
}