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