author | wenzelm |
Tue, 27 Jun 2023 10:24:32 +0200 | |
changeset 78213 | fd0430a7b7a4 |
parent 78204 | 0aa5360fa88b |
child 78266 | d8c99a497502 |
permissions | -rw-r--r-- |
76991 | 1 |
/* Title: Pure/ML/ml_heap.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
ML heap operations. |
|
5 |
*/ |
|
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
10 |
import java.nio.ByteBuffer |
|
11 |
import java.nio.channels.FileChannel |
|
12 |
import java.nio.file.StandardOpenOption |
|
13 |
||
14 |
||
15 |
object ML_Heap { |
|
16 |
/** heap file with SHA1 digest **/ |
|
17 |
||
18 |
private val sha1_prefix = "SHA1:" |
|
19 |
||
78182 | 20 |
def read_file_digest(heap: Path): Option[SHA1.Digest] = { |
76991 | 21 |
if (heap.is_file) { |
77711
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
22 |
val l = sha1_prefix.length |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
23 |
val m = l + SHA1.digest_length |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
24 |
val n = heap.file.length |
77718 | 25 |
val bs = Bytes.read_file(heap.file, offset = n - m) |
77711
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
26 |
if (bs.length == m) { |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
27 |
val s = bs.text |
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
28 |
if (s.startsWith(sha1_prefix)) Some(SHA1.fake_digest(s.substring(l))) |
76991 | 29 |
else None |
30 |
} |
|
77711
25fd62cba347
clarified signature: more general operation Bytes.read_slice;
wenzelm
parents:
77206
diff
changeset
|
31 |
else None |
76991 | 32 |
} |
33 |
else None |
|
34 |
} |
|
35 |
||
78182 | 36 |
def write_file_digest(heap: Path): SHA1.Digest = |
37 |
read_file_digest(heap) getOrElse { |
|
77206 | 38 |
val digest = SHA1.digest(heap) |
39 |
File.append(heap, sha1_prefix + digest.toString) |
|
40 |
digest |
|
76991 | 41 |
} |
77720 | 42 |
|
43 |
||
44 |
/* SQL data model */ |
|
45 |
||
78187
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
46 |
object Data extends SQL.Data("isabelle_heaps") { |
2df0f3604a67
clarified signature: more explicit class SQL.Data;
wenzelm
parents:
78186
diff
changeset
|
47 |
override lazy val tables = SQL.Tables(Base.table, Slices.table) |
78183 | 48 |
|
49 |
object Generic { |
|
50 |
val name = SQL.Column.string("name").make_primary_key |
|
51 |
} |
|
52 |
||
53 |
object Base { |
|
54 |
val name = Generic.name |
|
55 |
val size = SQL.Column.long("size") |
|
56 |
val digest = SQL.Column.string("digest") |
|
57 |
||
58 |
val table = make_table("", List(name, size, digest)) |
|
59 |
} |
|
60 |
||
61 |
object Slices { |
|
62 |
val name = Generic.name |
|
63 |
val slice = SQL.Column.int("slice").make_primary_key |
|
64 |
val content = SQL.Column.bytes("content") |
|
65 |
||
66 |
val table = make_table("slices", List(name, slice, content)) |
|
67 |
} |
|
68 |
||
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
69 |
def get_entry(db: SQL.Database, name: String): Option[SHA1.Digest] = |
78183 | 70 |
db.execute_query_statementO[String]( |
71 |
Base.table.select(List(Base.digest), sql = Generic.name.where_equal(name)), |
|
72 |
_.string(Base.digest) |
|
73 |
).flatMap(proper_string).map(SHA1.fake_digest) |
|
74 |
||
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
75 |
def read_entry(db: SQL.Database, name: String): List[Bytes] = |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
76 |
db.execute_query_statement( |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
77 |
Slices.table.select(List(Slices.content), |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
78 |
sql = Generic.name.where_equal(name) + SQL.order_by(List(Slices.slice))), |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
79 |
List.from[Bytes], _.bytes(Slices.content)) |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
80 |
|
78183 | 81 |
def clean_entry(db: SQL.Database, name: String): Unit = { |
82 |
for (table <- List(Base.table, Slices.table)) { |
|
83 |
db.execute_statement(table.delete(sql = Base.name.where_equal(name))) |
|
84 |
} |
|
85 |
} |
|
86 |
||
87 |
def prepare_entry(db: SQL.Database, name: String): Unit = |
|
88 |
db.execute_statement(Base.table.insert(), body = |
|
89 |
{ stmt => |
|
90 |
stmt.string(1) = name |
|
91 |
stmt.long(2) = None |
|
92 |
stmt.string(3) = None |
|
93 |
}) |
|
94 |
||
95 |
def write_entry(db: SQL.Database, name: String, slice: Int, content: Bytes): Unit = |
|
96 |
db.execute_statement(Slices.table.insert(), body = |
|
97 |
{ stmt => |
|
98 |
stmt.string(1) = name |
|
99 |
stmt.int(2) = slice |
|
100 |
stmt.bytes(3) = content |
|
101 |
}) |
|
102 |
||
103 |
def finish_entry(db: SQL.Database, name: String, size: Long, digest: SHA1.Digest): Unit = |
|
104 |
db.execute_statement( |
|
105 |
Base.table.update(List(Base.size, Base.digest), sql = Base.name.where_equal(name)), |
|
106 |
body = |
|
107 |
{ stmt => |
|
108 |
stmt.long(1) = size |
|
109 |
stmt.string(2) = digest.toString |
|
110 |
}) |
|
111 |
} |
|
112 |
||
78204 | 113 |
def clean_entry(db: SQL.Database, session_name: String): Unit = |
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
114 |
Data.transaction_lock(db, create = true, synchronized = true) { |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
115 |
Data.clean_entry(db, session_name) |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
116 |
} |
78186 | 117 |
|
78204 | 118 |
def get_entry(db: SQL.Database, session_name: String): Option[SHA1.Digest] = |
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
119 |
Data.transaction_lock(db, create = true, synchronized = true) { |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
120 |
Data.get_entry(db, session_name) |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
121 |
} |
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
122 |
|
78191 | 123 |
def store( |
78183 | 124 |
database: Option[SQL.Database], |
78204 | 125 |
session_name: String, |
78183 | 126 |
heap: Path, |
78188 | 127 |
slice: Long, |
78193 | 128 |
cache: Compress.Cache = Compress.Cache.none |
78183 | 129 |
): SHA1.Digest = { |
130 |
val digest = write_file_digest(heap) |
|
131 |
database match { |
|
78204 | 132 |
case None => |
78183 | 133 |
case Some(db) => |
134 |
val size = File.space(heap).bytes - sha1_prefix.length - SHA1.digest_length |
|
135 |
||
78188 | 136 |
val slices = (size.toDouble / slice.toDouble).ceil.toInt |
78183 | 137 |
val step = (size.toDouble / slices.toDouble).ceil.toLong |
138 |
||
139 |
try { |
|
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
140 |
Data.transaction_lock(db, create = true, synchronized = true) { |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
141 |
Data.prepare_entry(db, session_name) |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
142 |
} |
78183 | 143 |
|
144 |
for (i <- 0 until slices) { |
|
145 |
val j = i + 1 |
|
146 |
val offset = step * i |
|
147 |
val limit = if (j < slices) step * j else size |
|
148 |
val content = |
|
149 |
Bytes.read_file(heap.file, offset = offset, limit = limit) |
|
150 |
.compress(cache = cache) |
|
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
151 |
Data.transaction_lock(db, synchronized = true) { |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
152 |
Data.write_entry(db, session_name, i, content) |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
153 |
} |
78183 | 154 |
} |
155 |
||
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
156 |
Data.transaction_lock(db, synchronized = true) { |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
157 |
Data.finish_entry(db, session_name, size, digest) |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
158 |
} |
78183 | 159 |
} |
160 |
catch { case exn: Throwable => |
|
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
161 |
Data.transaction_lock(db, create = true, synchronized = true) { |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
162 |
Data.clean_entry(db, session_name) |
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
163 |
} |
78183 | 164 |
throw exn |
165 |
} |
|
166 |
} |
|
167 |
digest |
|
168 |
} |
|
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
169 |
|
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
170 |
def restore( |
78204 | 171 |
database: Option[SQL.Database], |
172 |
session_name: String, |
|
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
173 |
heap: Path, |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
174 |
cache: Compress.Cache = Compress.Cache.none |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
175 |
): Unit = { |
78204 | 176 |
database match { |
177 |
case None => |
|
178 |
case Some(db) => |
|
78213
fd0430a7b7a4
avoid repeated open_database_server: synchronized transaction_lock;
wenzelm
parents:
78204
diff
changeset
|
179 |
Data.transaction_lock(db, create = true, synchronized = true) { |
78204 | 180 |
val db_digest = Data.get_entry(db, session_name) |
181 |
val file_digest = read_file_digest(heap) |
|
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
182 |
|
78204 | 183 |
if (db_digest.isDefined && db_digest != file_digest) { |
184 |
Isabelle_System.make_directory(heap.expand.dir) |
|
185 |
Bytes.write(heap, Bytes.empty) |
|
186 |
for (slice <- Data.read_entry(db, session_name)) { |
|
187 |
Bytes.append(heap, slice.uncompress(cache = cache)) |
|
188 |
} |
|
189 |
val digest = write_file_digest(heap) |
|
190 |
if (db_digest.get != digest) error("Incoherent content for file " + heap) |
|
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
191 |
} |
78204 | 192 |
} |
78196
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
193 |
} |
140a6f2e3728
restore heaps from database, which takes precedence over file-system;
wenzelm
parents:
78193
diff
changeset
|
194 |
} |
76991 | 195 |
} |