diff -r 42138702d6ec -r 8eb6365f5916 src/Pure/Tools/build.scala
--- a/src/Pure/Tools/build.scala	Sun Oct 16 20:19:10 2016 +0200
+++ b/src/Pure/Tools/build.scala	Sun Oct 16 22:43:51 2016 +0200
@@ -236,7 +236,7 @@
   /* jobs */
 
   private class Job(progress: Progress, name: String, val info: Sessions.Info, tree: Sessions.Tree,
-    store: Sessions.Store, do_output: Boolean, verbose: Boolean,
+    store: Sessions.Store, do_output: Boolean, verbose: Boolean, val numa_node: Option[Int],
     session_graph: Graph_Display.Graph, command_timings: List[Properties.T])
   {
     val output = store.output_dir + Path.basic(name)
@@ -278,18 +278,25 @@
           "Build.build " + ML_Syntax.print_string0(File.standard_path(args_file)) +
           (if (do_output) "; ML_Heap.share_common_data (); " + output_save_state
            else "") + "));"
+
+        val process_options =
+          numa_node match {
+            case None => info.options
+            case Some(n) => info.options.string("ML_process_policy") = NUMA.policy(n)
+          }
         val process =
           if (Sessions.pure_name(name)) {
-            ML_Process(info.options, raw_ml_system = true, cwd = info.dir.file,
+            ML_Process(process_options, raw_ml_system = true, cwd = info.dir.file,
               args =
                 (for ((root, _) <- Thy_Header.ml_roots) yield List("--use", root)).flatten :::
                 List("--eval", eval),
               env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
           }
           else {
-            ML_Process(info.options, parent, List("--eval", eval), cwd = info.dir.file,
+            ML_Process(process_options, parent, List("--eval", eval), cwd = info.dir.file,
               env = env, tree = Some(tree), store = store, cleanup = () => args_file.delete)
           }
+
         process.result(
           progress_stdout = (line: String) =>
             Library.try_unprefix("\floading_theory = ", line) match {
@@ -396,6 +403,7 @@
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
+    numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
@@ -416,6 +424,7 @@
       clean_build = clean_build,
       dirs = dirs,
       select_dirs = select_dirs,
+      numa_shuffling = numa_shuffling,
       max_jobs = max_jobs,
       list_files = list_files,
       check_keywords = check_keywords,
@@ -434,6 +443,7 @@
     clean_build: Boolean = false,
     dirs: List[Path] = Nil,
     select_dirs: List[Path] = Nil,
+    numa_shuffling: Boolean = false,
     max_jobs: Int = 1,
     list_files: Boolean = false,
     check_keywords: Set[String] = Set.empty,
@@ -524,11 +534,17 @@
       catch { case Exn.Interrupt() => Exn.Interrupt.impose() }
     }
 
+    val numa_nodes = new NUMA.Nodes(numa_shuffling)
+
     @tailrec def loop(
       pending: Queue,
       running: Map[String, (List[String], Job)],
       results: Map[String, Result]): Map[String, Result] =
     {
+      def used_node(i: Int): Boolean =
+        running.iterator.exists(
+          { case (_, (_, job)) => job.numa_node.isDefined && job.numa_node.get == i })
+
       if (pending.is_empty) results
       else {
         if (progress.stopped)
@@ -621,10 +637,11 @@
                     results + (name -> Result(false, heap_stamp, Some(Process_Result(1)), info)))
                 }
                 else if (ancestor_results.forall(_.ok) && !progress.stopped) {
+                  val numa_node = numa_nodes.next(used_node(_))
                   progress.echo((if (do_output) "Building " else "Running ") + name + " ...")
                   val job =
                     new Job(progress, name, info, selected_tree, store, do_output, verbose,
-                      deps(name).session_graph, queue.command_timings(name))
+                      numa_node, deps(name).session_graph, queue.command_timings(name))
                   loop(pending, running + (name -> (ancestor_heaps, job)), results)
                 }
                 else {
@@ -650,7 +667,9 @@
       else loop(queue, Map.empty, Map.empty)
 
     val results =
-      new Results((for ((name, result) <- results0.iterator) yield (name, (result.process, result.info))).toMap)
+      new Results(
+        (for ((name, result) <- results0.iterator)
+          yield (name, (result.process, result.info))).toMap)
 
     if (results.rc != 0 && (verbose || !no_build)) {
       val unfinished =
@@ -691,6 +710,7 @@
     val build_options = Word.explode(Isabelle_System.getenv("ISABELLE_BUILD_OPTIONS"))
 
     var select_dirs: List[Path] = Nil
+    var numa_shuffling = false
     var requirements = false
     var exclude_session_groups: List[String] = Nil
     var all_sessions = false
@@ -712,6 +732,7 @@
 
   Options are:
     -D DIR       include session directory and select its sessions
+    -N           cyclic shuffling of NUMA CPU nodes (performance tuning)
     -R           operate on requirements of selected sessions
     -X NAME      exclude sessions from group NAME and all descendants
     -a           select all sessions
@@ -732,6 +753,7 @@
 
 """ + Library.prefix_lines("  ", Build_Log.Settings.show()),
       "D:" -> (arg => select_dirs = select_dirs ::: List(Path.explode(arg))),
+      "N" -> (_ => numa_shuffling = true),
       "R" -> (_ => requirements = true),
       "X:" -> (arg => exclude_session_groups = exclude_session_groups ::: List(arg)),
       "a" -> (_ => all_sessions = true),
@@ -768,6 +790,7 @@
           clean_build = clean_build,
           dirs = dirs,
           select_dirs = select_dirs,
+          numa_shuffling = NUMA.enabled_warning(numa_shuffling),
           max_jobs = max_jobs,
           list_files = list_files,
           check_keywords = check_keywords,