1/*  Title:      Pure/System/numa.scala
2    Author:     Makarius
3
4Support for Non-Uniform Memory Access of separate CPU nodes.
5*/
6
7package isabelle
8
9
10object NUMA
11{
12  /* available nodes */
13
14  def nodes(): List[Int] =
15  {
16    val numa_nodes_linux = Path.explode("/sys/devices/system/node/online")
17
18    val Single = """^(\d+)$""".r
19    val Multiple = """^(\d+)-(\d+)$""".r
20
21    def read(s: String): List[Int] =
22      s match {
23        case Single(Value.Int(i)) => List(i)
24        case Multiple(Value.Int(i), Value.Int(j)) => (i to j).toList
25        case _ => error("Cannot parse CPU node specification: " + quote(s))
26      }
27
28    if (numa_nodes_linux.is_file) {
29      space_explode(',', File.read(numa_nodes_linux).trim).flatMap(read(_))
30    }
31    else Nil
32  }
33
34
35  /* CPU policy via numactl tool */
36
37  lazy val numactl_available: Boolean = Isabelle_System.bash("numactl -m0 -N0 true").ok
38
39  def policy(node: Int): String =
40    if (numactl_available) "numactl -m" + node + " -N" + node else ""
41
42  def policy_options(options: Options, numa_node: Option[Int] = Some(0)): Options =
43    numa_node match {
44      case None => options
45      case Some(n) => options.string("ML_process_policy") = policy(n)
46    }
47
48
49  /* shuffling of CPU nodes */
50
51  def enabled: Boolean =
52    try { nodes().length >= 2 && numactl_available }
53    catch { case ERROR(_) => false }
54
55  def enabled_warning(progress: Progress, enabled: Boolean): Boolean =
56  {
57    def warning =
58      if (nodes().length < 2) Some("no NUMA nodes available")
59      else if (!numactl_available) Some("bad numactl tool")
60      else None
61
62    enabled &&
63      (warning match {
64        case Some(s) => progress.echo_warning("Shuffling of CPU nodes is disabled: " + s); false
65        case _ => true
66      })
67  }
68
69  class Nodes(enabled: Boolean = true)
70  {
71    private val available = nodes().zipWithIndex
72    private var next_index = 0
73
74    def next(used: Int => Boolean = _ => false): Option[Int] = synchronized {
75      if (!enabled || available.isEmpty) None
76      else {
77        val candidates = available.drop(next_index) ::: available.take(next_index)
78        val (n, i) =
79          candidates.find({ case (n, i) => i == next_index && !used(n) }) orElse
80            candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
81        next_index = (i + 1) % available.length
82        Some(n)
83      }
84    }
85  }
86}
87