support for Non-Uniform Memory Access of separate CPU nodes;

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/Pure/System/numa.scala	Sun Oct 16 20:19:10 2016 +0200
@@ -0,0 +1,41 @@
+/*  Title:      Pure/System/numa.scala
+    Author:     Makarius
+
+Support for Non-Uniform Memory Access of separate CPU nodes.
+*/
+
+package isabelle
+
+
+object NUMA
+{
+  /* available nodes */
+
+  def nodes(): List[Int] =
+  {
+    val numa_nodes_linux = Path.explode("/sys/devices/system/node/online")
+
+    val Single = """^(\d+)$""".r
+    val Multiple = """^(\d+)-(\d+)$""".r
+
+    def read(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 node specification: " + quote(s))
+      }
+
+    if (numa_nodes_linux.is_file) {
+      Library.space_explode(',', Library.trim_line(File.read(numa_nodes_linux))).flatMap(read(_))
+    }
+    else Nil
+  }
+
+
+  /* CPU policy via numactl tool */
+
+  lazy val numactl_available: Boolean = Isabelle_System.bash("numactl --hardware").ok
+
+  def policy(node: Int): String =
+    if (numactl_available) "numactl -m" + node + " -N" + node else ""
+}

--- a/src/Pure/build-jars	Sun Oct 16 20:08:23 2016 +0200
+++ b/src/Pure/build-jars	Sun Oct 16 20:19:10 2016 +0200
@@ -104,6 +104,7 @@
   System/isabelle_process.scala
   System/isabelle_system.scala
   System/isabelle_tool.scala
+  System/numa.scala
   System/options.scala
   System/platform.scala
   System/posix_interrupt.scala