# HG changeset patch
# User wenzelm
# Date 1678309728 -3600
# Node ID edc96be6b939f743e7f6f1676160d5ed4831ae40
# Parent  46a033c4701bdc8ef6014a0c51459cf33c9d74ce
explicit locking for PostgreSQL --- neither available nor required for SQLite;

diff -r 46a033c4701b -r edc96be6b939 src/Pure/General/sql.scala
--- a/src/Pure/General/sql.scala	Wed Mar 08 20:19:05 2023 +0100
+++ b/src/Pure/General/sql.scala	Wed Mar 08 22:08:48 2023 +0100
@@ -369,6 +369,8 @@
       finally { connection.setAutoCommit(auto_commit) }
     }
 
+    def lock_tables(tables: List[Table]): Unit = {}  // PostgreSQL only
+
 
     /* statements and results */
 
@@ -550,6 +552,14 @@
       table.insert_cmd(sql = if_proper(sql, sql + " ") + "ON CONFLICT DO NOTHING")
 
 
+    /* explicit locking: only applicable to PostgreSQL within transaction context */
+    // see https://www.postgresql.org/docs/current/sql-lock.html
+    // see https://www.postgresql.org/docs/current/explicit-locking.html
+
+    override def lock_tables(tables: List[SQL.Table]): Unit =
+      execute_statement("LOCK TABLE " + tables.mkString(", ") + " IN ACCESS EXCLUSIVE MODE")
+
+
     /* notifications: IPC via database server */
     // see https://www.postgresql.org/docs/current/sql-notify.html
 
diff -r 46a033c4701b -r edc96be6b939 src/Pure/Tools/build_process.scala
--- a/src/Pure/Tools/build_process.scala	Wed Mar 08 20:19:05 2023 +0100
+++ b/src/Pure/Tools/build_process.scala	Wed Mar 08 22:08:48 2023 +0100
@@ -134,6 +134,7 @@
       using_option(open_database()) { db =>
         db.transaction {
           for (table <- Data.all_tables) db.create_table(table)
+          db.lock_tables(Data.all_tables)
           Data.clean_build(db)
         }
         db.rebuild()
@@ -753,6 +754,15 @@
       stamp_worker(db, worker_uuid, serial)
       state.set_serial(serial).set_workers(read_workers(db))
     }
+
+
+    /* transaction_lock */
+
+    def transaction_lock[A](db: SQL.Database, body: => A): A =
+      db.transaction {
+        db.lock_tables(Build_Process.Data.all_tables)
+        body
+      }
   }
 }
 
@@ -786,7 +796,7 @@
     synchronized {
       _database match {
         case None => body
-        case Some(db) => db.transaction { body }
+        case Some(db) => Build_Process.Data.transaction_lock(db, body)
       }
     }