# HG changeset patch # User wenzelm # Date 1708788625 -3600 # Node ID deb3056ed823b695e8303c1a016aa736b96912be # Parent 8544f10451231a9c669e089ee04f0be53f497501 minor performance tuning: just 1 transaction for slices <= 1; diff -r 8544f1045123 -r deb3056ed823 src/Pure/ML/ml_heap.scala --- a/src/Pure/ML/ml_heap.scala Sat Feb 24 15:10:50 2024 +0100 +++ b/src/Pure/ML/ml_heap.scala Sat Feb 24 16:30:25 2024 +0100 @@ -135,7 +135,13 @@ } } - def init_entry(db: SQL.Database, name: String, log_db: Option[Log_DB] = None): Unit = { + def init_entry( + db: SQL.Database, + name: String, + heap_size: Long, + heap_digest: Option[SHA1.Digest], + log_db: Option[Log_DB] + ): Unit = { clean_entry(db, name) for (table <- List(Size.table, Slices_Size.table)) { db.create_view(table) @@ -143,14 +149,14 @@ db.execute_statement(Base.table.insert(), body = { stmt => stmt.string(1) = name - stmt.long(2) = None - stmt.string(3) = None + stmt.long(2) = heap_size + stmt.string(3) = heap_digest.map(_.toString) stmt.string(4) = log_db.map(_.uuid) stmt.bytes(5) = log_db.map(_.content) }) } - def finish_entry( + def update_entry( db: SQL.Database, name: String, heap_size: Long, @@ -215,15 +221,25 @@ } try { - if (slices == 0 && log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...") + if (slices > 0) progress.echo("Storing " + session.name + " ...") - private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") { - private_data.init_entry(db, session.name, log_db = if (slices == 0) log_db else None) + // init entry: slice 0 + initial log_db + { + val (heap_size0, heap_digest0) = if (slices > 1) (0L, None) else (heap_size, heap_digest) + val log_db0 = if (slices <= 1) log_db else None + val content0 = if (slices > 0) Some(slice_content(0)) else None + + if (log_db0.isDefined) progress.echo("Storing " + session.log_db_name + " ...") + + private_data.transaction_lock(db, create = true, label = "ML_Heap.store1") { + private_data.init_entry(db, session.name, heap_size0, heap_digest0, log_db0) + for (content <- content0) private_data.write_slice(db, session.name, 0, content) + } } - if (slices > 0) { - progress.echo("Storing " + session.name + " ...") - for (i <- 0 until slices) { + // update entry: slice 1 ... + final log_db + if (slices > 1) { + for (i <- 1 until slices) { val content = slice_content(i) private_data.transaction_lock(db, label = "ML_Heap.store2") { private_data.write_slice(db, session.name, i, content) @@ -233,7 +249,7 @@ if (log_db.isDefined) progress.echo("Storing " + session.log_db_name + " ...") private_data.transaction_lock(db, label = "ML_Heap.store3") { - private_data.finish_entry(db, session.name, heap_size, heap_digest, log_db) + private_data.update_entry(db, session.name, heap_size, heap_digest, log_db) } } }