src/Pure/System/numa.scala
author wenzelm
Sun, 16 Oct 2016 20:19:10 +0200
changeset 64264 42138702d6ec
child 64265 8eb6365f5916
permissions -rw-r--r--
support for Non-Uniform Memory Access of separate CPU nodes;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
64264
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     1
/*  Title:      Pure/System/numa.scala
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     3
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     4
Support for Non-Uniform Memory Access of separate CPU nodes.
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     5
*/
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     6
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     7
package isabelle
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     8
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
     9
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    10
object NUMA
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    11
{
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    12
  /* available nodes */
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    13
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    14
  def nodes(): List[Int] =
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    15
  {
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    16
    val numa_nodes_linux = Path.explode("/sys/devices/system/node/online")
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    17
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    18
    val Single = """^(\d+)$""".r
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    19
    val Multiple = """^(\d+)-(\d+)$""".r
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    20
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    21
    def read(s: String): List[Int] =
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    22
      s match {
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    23
        case Single(Value.Int(i)) => List(i)
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    24
        case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    25
        case _ => error("Cannot parse CPU node specification: " + quote(s))
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    26
      }
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    27
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    28
    if (numa_nodes_linux.is_file) {
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    29
      Library.space_explode(',', Library.trim_line(File.read(numa_nodes_linux))).flatMap(read(_))
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    30
    }
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    31
    else Nil
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    32
  }
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    33
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    34
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    35
  /* CPU policy via numactl tool */
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    36
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    37
  lazy val numactl_available: Boolean = Isabelle_System.bash("numactl --hardware").ok
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    38
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    39
  def policy(node: Int): String =
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    40
    if (numactl_available) "numactl -m" + node + " -N" + node else ""
42138702d6ec support for Non-Uniform Memory Access of separate CPU nodes;
wenzelm
parents:
diff changeset
    41
}