--- a/src/Pure/General/json.scala Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/General/json.scala Wed Feb 22 21:40:32 2023 +0100
@@ -33,6 +33,9 @@
Some(m.asInstanceOf[Object.T])
case _ => None
}
+
+ def parse(s: S): Object.T =
+ unapply(JSON.parse(s)).getOrElse(error("Bad JSON object " + quote(s)))
}
--- a/src/Pure/General/sql.scala Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/General/sql.scala Wed Feb 22 21:40:32 2023 +0100
@@ -55,8 +55,12 @@
val join_inner: Source = " INNER JOIN "
def join(outer: Boolean): Source = if (outer) join_outer else join_inner
- def member(x: Source, set: Iterable[String]): Source =
+ def member(x: Source, set: Iterable[String]): Source = {
+ require(set.nonEmpty)
set.iterator.map(a => x + " = " + SQL.string(a)).mkString("(", " OR ", ")")
+ }
+
+ def where_member(x: Source, set: Iterable[String]): Source = " WHERE " + member(x, set)
/* types */
@@ -295,6 +299,8 @@
def is_server: Boolean
+ def rebuild(): Unit = ()
+
/* types */
@@ -407,6 +413,7 @@
class Database private[SQLite](name: String, val connection: Connection) extends SQL.Database {
override def toString: String = name
override def is_server: Boolean = false
+ override def rebuild(): Unit = using_statement("VACUUM")(_.execute())
def sql_type(T: SQL.Type.Value): SQL.Source = SQL.sql_type_sqlite(T)
@@ -419,8 +426,6 @@
def insert_permissive(table: SQL.Table, sql: SQL.Source = ""): SQL.Source =
table.insert_cmd("INSERT OR IGNORE", sql = sql)
-
- def rebuild(): Unit = using_statement("VACUUM")(_.execute())
}
}
--- a/src/Pure/General/uuid.scala Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/General/uuid.scala Wed Feb 22 21:40:32 2023 +0100
@@ -17,4 +17,7 @@
catch { case _: IllegalArgumentException => None }
def unapply(body: XML.Body): Option[T] = unapply(XML.content(body))
+
+ def make(s: String): T =
+ unapply(s).getOrElse(error("Bad UUID: " + quote(s)))
}
--- a/src/Pure/Tools/build_job.scala Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/Tools/build_job.scala Wed Feb 22 21:40:32 2023 +0100
@@ -12,15 +12,23 @@
trait Build_Job {
- def session_name: String
+ def job_name: String
def numa_node: Option[Int] = None
def start(): Unit = ()
def terminate(): Unit = ()
def is_finished: Boolean = false
def join: Process_Result = Process_Result.undefined
+ def make_abstract: Build_Job.Abstract = Build_Job.Abstract(job_name, numa_node)
}
object Build_Job {
+ case class Abstract(
+ override val job_name: String,
+ override val numa_node: Option[Int]
+ ) extends Build_Job {
+ override def make_abstract: Abstract = this
+ }
+
class Build_Session(progress: Progress,
session_background: Sessions.Background,
store: Sessions.Store,
@@ -31,6 +39,8 @@
override val numa_node: Option[Int]
) extends Build_Job {
def session_name: String = session_background.session_name
+ def job_name: String = session_name
+
val info: Sessions.Info = session_background.sessions_structure(session_name)
val options: Options = NUMA.policy_options(info.options, numa_node)
--- a/src/Pure/Tools/build_process.scala Tue Feb 21 16:47:03 2023 +0000
+++ b/src/Pure/Tools/build_process.scala Wed Feb 22 21:40:32 2023 +0100
@@ -152,7 +152,7 @@
/* dynamic state */
- case class Entry(name: String, deps: List[String]) {
+ case class Entry(name: String, deps: List[String], info: JSON.Object.T = JSON.Object.empty) {
def is_ready: Boolean = deps.isEmpty
def resolve(dep: String): Entry =
if (deps.contains(dep)) copy(deps = deps.filterNot(_ == dep)) else this
@@ -172,8 +172,17 @@
running: Map[String, Build_Job] = Map.empty,
results: Map[String, Build_Process.Result] = Map.empty
) {
- def get_numa: (Int, Set[Int]) = (numa_index, numa_running)
- def put_numa(i: Int): State = copy(numa_index = i)
+ def numa_next(numa_nodes: List[Int]): (Option[Int], State) =
+ if (numa_nodes.isEmpty) (None, this)
+ else {
+ val available = numa_nodes.zipWithIndex
+ val used = Set.from(for (job <- running.valuesIterator; i <- job.numa_node) yield i)
+ val candidates = available.drop(numa_index) ::: available.take(numa_index)
+ val (n, i) =
+ candidates.find({ case (n, i) => i == numa_index && !used(n) }) orElse
+ candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
+ (Some(n), copy(numa_index = (i + 1) % available.length))
+ }
def finished: Boolean = pending.isEmpty
@@ -183,9 +192,6 @@
def is_running(name: String): Boolean = running.isDefinedAt(name)
- def numa_running: Set[Int] =
- Set.from(for (job <- running.valuesIterator; i <- job.numa_node) yield i)
-
def stop_running(): Unit = running.valuesIterator.foreach(_.terminate())
def finished_running(): List[Build_Job.Build_Session] =
@@ -262,31 +268,12 @@
else None
}
- protected def next_numa_node(): Option[Int] = synchronized {
- val available = build_context.numa_nodes.zipWithIndex
- if (available.isEmpty) None
- else {
- val (index, used) = _state.get_numa
- val candidates = available.drop(index) ::: available.take(index)
- val (n, i) =
- candidates.find({ case (n, i) => i == index && !used(n) }) orElse
- candidates.find({ case (n, _) => !used(n) }) getOrElse candidates.head
- _state = _state.put_numa((i + 1) % available.length)
- Some(n)
- }
- }
-
protected def stop_running(): Unit = synchronized { _state.stop_running() }
protected def finished_running(): List[Build_Job.Build_Session] = synchronized {
_state.finished_running()
}
- protected def job_running(name: String, job: Build_Job): Build_Job = synchronized {
- _state = _state.add_running(name, job)
- job
- }
-
protected def finish_job(job: Build_Job.Build_Session): Unit = {
val session_name = job.session_name
val process_result = job.join
@@ -407,10 +394,12 @@
val job =
synchronized {
- val numa_node = next_numa_node()
- job_running(session_name,
+ val (numa_node, state1) = _state.numa_next(build_context.numa_nodes)
+ val job =
new Build_Job.Build_Session(progress, session_background, store, do_store,
- resources, build_context.session_setup, input_heaps, numa_node))
+ resources, build_context.session_setup, input_heaps, numa_node)
+ _state = state1.add_running(session_name, job)
+ job
}
job.start()
}