author | wenzelm |
Thu, 09 Nov 2023 14:22:19 +0100 | |
changeset 78926 | 35d42112301a |
parent 78925 | b33a7c6b99c5 |
child 78943 | bc89bdc65f29 |
permissions | -rw-r--r-- |
78398 | 1 |
/* Title: Pure/Tools/build_cluster.scala |
2 |
Author: Makarius |
|
3 |
||
4 |
Management of build cluster: independent ssh hosts with access to shared |
|
5 |
PostgreSQL server. |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
6 |
|
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
7 |
NB: extensible classes allow quite different implementations in user-space, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
8 |
via the service class Build.Engine and overridable methods |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
9 |
Build.Engine.open_build_process(), Build_Process.open_build_cluster(). |
78398 | 10 |
*/ |
11 |
||
12 |
package isabelle |
|
13 |
||
14 |
||
15 |
object Build_Cluster { |
|
78413 | 16 |
/* host specifications */ |
17 |
||
78399 | 18 |
object Host { |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
19 |
private val rfc822_specials = """()<>@,;:\"[]""" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
20 |
|
78925 | 21 |
private val HOSTNAME = "hostname" |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
22 |
private val USER = "user" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
23 |
private val PORT = "port" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
24 |
private val JOBS = "jobs" |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
25 |
private val NUMA = "numa" |
78580 | 26 |
private val DIRS = "dirs" |
78567 | 27 |
private val SHARED = "shared" |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
28 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
29 |
val parameters: Options = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
30 |
Options.inline(""" |
78925 | 31 |
option hostname : string = "" -- "explicit SSH hostname" |
32 |
option user : string = "" -- "explicit SSH user" |
|
33 |
option port : int = 0 -- "explicit SSH port" |
|
34 |
option jobs : int = 1 -- "maximum number of parallel jobs" |
|
35 |
option numa : bool = false -- "cyclic shuffling of NUMA CPU nodes" |
|
36 |
option dirs : string = "" -- "additional session directories (separated by colon)" |
|
37 |
option shared : bool = false -- "shared directory: omit sync + init" |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
38 |
""") |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
39 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
40 |
def is_parameter(spec: Options.Spec): Boolean = parameters.defined(spec.name) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
41 |
|
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
42 |
lazy val test_options: Options = Options.init0() |
78399 | 43 |
|
44 |
def apply( |
|
78416 | 45 |
name: String = "", |
78925 | 46 |
hostname: String = parameters.string(HOSTNAME), |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
47 |
user: String = parameters.string(USER), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
48 |
port: Int = parameters.int(PORT), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
49 |
jobs: Int = parameters.int(JOBS), |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
50 |
numa: Boolean = parameters.bool(NUMA), |
78580 | 51 |
dirs: String = parameters.string(DIRS), |
78567 | 52 |
shared: Boolean = parameters.bool(SHARED), |
78399 | 53 |
options: List[Options.Spec] = Nil |
78580 | 54 |
): Host = { |
55 |
Path.split(dirs) // check |
|
78925 | 56 |
new Host(name, hostname, user, port, jobs, numa, dirs, shared, options) |
78580 | 57 |
} |
78401 | 58 |
|
78578 | 59 |
def parse(str: String): List[Host] = { |
60 |
val names = str.takeWhile(c => !rfc822_specials.contains(c) || c == ',') |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
61 |
val (params, options) = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
62 |
try { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
63 |
val rest = { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
64 |
val n = str.length |
78578 | 65 |
val m = names.length |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
66 |
val l = |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
67 |
if (m == n) n |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
68 |
else if (str(m) == ':') m + 1 |
78423 | 69 |
else error("Missing \":\" after host name") |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
70 |
str.substring(l) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
71 |
} |
78911 | 72 |
val (specs1, specs2) = Options.Spec.parse(rest).partition(is_parameter) |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
73 |
(parameters ++ specs1, { test_options ++ specs2; specs2 }) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
74 |
} |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
75 |
catch { |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
76 |
case ERROR(msg) => |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
77 |
cat_error(msg, "The error(s) above occurred in host specification " + quote(str)) |
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
78 |
} |
78578 | 79 |
for (name <- space_explode(',', names)) yield { |
80 |
apply(name = name, |
|
78925 | 81 |
hostname = params.string(HOSTNAME), |
78578 | 82 |
user = params.string(USER), |
83 |
port = params.int(PORT), |
|
84 |
jobs = params.int(JOBS), |
|
85 |
numa = params.bool(NUMA), |
|
78580 | 86 |
dirs = params.string(DIRS), |
78578 | 87 |
shared = params.bool(SHARED), |
88 |
options = options) |
|
89 |
} |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
90 |
} |
78399 | 91 |
} |
92 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
93 |
class Host( |
78427 | 94 |
val name: String, |
78925 | 95 |
val hostname: String, |
78427 | 96 |
val user: String, |
97 |
val port: Int, |
|
98 |
val jobs: Int, |
|
99 |
val numa: Boolean, |
|
78580 | 100 |
val dirs: String, |
78567 | 101 |
val shared: Boolean, |
78427 | 102 |
val options: List[Options.Spec] |
78399 | 103 |
) { |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
104 |
host => |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
105 |
|
78925 | 106 |
def ssh_host: String = proper_string(hostname) getOrElse name |
107 |
def is_local: Boolean = SSH.is_local(ssh_host) |
|
78413 | 108 |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
109 |
override def toString: String = print |
78399 | 110 |
|
111 |
def print: String = { |
|
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
112 |
val params = |
78399 | 113 |
List( |
78925 | 114 |
if (host.hostname.isEmpty) "" else Options.Spec.print(Host.HOSTNAME, host.hostname), |
78560 | 115 |
if (host.user.isEmpty) "" else Options.Spec.print(Host.USER, host.user), |
116 |
if (host.port == 0) "" else Options.Spec.print(Host.PORT, host.port.toString), |
|
117 |
if (host.jobs == 1) "" else Options.Spec.print(Host.JOBS, host.jobs.toString), |
|
78567 | 118 |
if_proper(host.numa, Host.NUMA), |
78580 | 119 |
if_proper(dirs, Options.Spec.print(Host.DIRS, host.dirs)), |
78567 | 120 |
if_proper(host.shared, Host.SHARED) |
78399 | 121 |
).filter(_.nonEmpty) |
78560 | 122 |
val rest = (params ::: host.options.map(_.print)).mkString(",") |
78408
092f1e435b3a
proper Build_Cluster.Host.parse for parameters and system options;
wenzelm
parents:
78401
diff
changeset
|
123 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
124 |
SSH.print_local(host.name) + if_proper(rest, ":" + rest) |
78399 | 125 |
} |
126 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
127 |
def message(msg: String): String = "Host " + quote(host.name) + if_proper(msg, ": " + msg) |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
128 |
|
78926 | 129 |
def open_ssh(options: Options): SSH.System = |
130 |
SSH.open_system(options ++ host.options, ssh_host, port = host.port, user = host.user) |
|
131 |
||
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
132 |
def open_session(build_context: Build.Context, progress: Progress = new Progress): Session = { |
78926 | 133 |
val ssh_options = build_context.build_options ++ host.options |
134 |
val ssh = open_ssh(build_context.build_options) |
|
135 |
new Session(build_context, host, ssh_options, ssh, progress) |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
136 |
} |
78399 | 137 |
} |
78413 | 138 |
|
139 |
||
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
140 |
/* SSH sessions */ |
78413 | 141 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
142 |
class Session( |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
143 |
val build_context: Build.Context, |
78433 | 144 |
val host: Host, |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
145 |
val options: Options, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
146 |
val ssh: SSH.System, |
78433 | 147 |
val progress: Progress |
148 |
) extends AutoCloseable { |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
149 |
override def toString: String = ssh.toString |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
150 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
151 |
val remote_identifier: String = options.string("build_cluster_identifier") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
152 |
val remote_root: Path = Path.explode(options.string("build_cluster_root")) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
153 |
val remote_isabelle_home: Path = remote_root + Path.explode("isabelle") |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
154 |
val remote_afp_root: Option[Path] = |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
155 |
if (build_context.afp_root.isEmpty) None |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
156 |
else Some(remote_isabelle_home + Path.explode("AFP")) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
157 |
|
78443 | 158 |
lazy val remote_isabelle: Other_Isabelle = |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
159 |
Other_Isabelle(remote_isabelle_home, isabelle_identifier = remote_identifier, ssh = ssh) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
160 |
|
78443 | 161 |
def sync(): Other_Isabelle = { |
162 |
Sync.sync(options, Rsync.Context(ssh = ssh), remote_isabelle_home, |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
163 |
afp_root = build_context.afp_root, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
164 |
purge_heaps = true, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
165 |
preserve_jars = true) |
78443 | 166 |
remote_isabelle |
167 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
168 |
|
78443 | 169 |
def init(): Unit = remote_isabelle.init() |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
170 |
|
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
171 |
def benchmark(): Unit = { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
172 |
val script = |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
173 |
Benchmark.benchmark_command(host, ssh = ssh, isabelle_home = remote_isabelle_home) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
174 |
remote_isabelle.bash(script).check |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
175 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
176 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
177 |
def start(): Process_Result = { |
78572 | 178 |
val remote_ml_platform = remote_isabelle.getenv("ML_PLATFORM") |
179 |
if (remote_ml_platform != build_context.ml_platform) { |
|
180 |
error("Bad ML_PLATFORM: found " + remote_ml_platform + |
|
181 |
", but expected " + build_context.ml_platform) |
|
182 |
} |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
183 |
val script = |
78558 | 184 |
Build.build_worker_command(host, |
78556 | 185 |
ssh = ssh, |
78559 | 186 |
build_options = List(options.spec("build_database_server")), |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
187 |
build_id = build_context.build_uuid, |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
188 |
isabelle_home = remote_isabelle_home, |
78580 | 189 |
afp_root = remote_afp_root, |
78638
28a2c55648d5
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
wenzelm
parents:
78584
diff
changeset
|
190 |
dirs = Path.split(host.dirs).map(remote_isabelle.expand_path), |
28a2c55648d5
prefer quiet mode: potentially more robust ssh connection, e.g. when master closes;
wenzelm
parents:
78584
diff
changeset
|
191 |
quiet = true) |
78584
92ef737f412c
removed junk (following ab07d4cb7d1c, amending 8cd399b25dac);
wenzelm
parents:
78582
diff
changeset
|
192 |
remote_isabelle.bash(script).check |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
193 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
194 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
195 |
override def close(): Unit = ssh.close() |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
196 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
197 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
198 |
class Result(val host: Host, val process_result: Exn.Result[Process_Result]) { |
78443 | 199 |
def rc: Int = Process_Result.RC(process_result) |
200 |
def ok: Boolean = rc == Process_Result.RC.ok |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
201 |
} |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
202 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
203 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
204 |
/* build clusters */ |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
205 |
|
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
206 |
object none extends Build_Cluster { |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
207 |
override def toString: String = "Build_Cluster.none" |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
208 |
} |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
209 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
210 |
def make(build_context: Build.Context, progress: Progress = new Progress): Build_Cluster = { |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
211 |
val remote_hosts = build_context.build_hosts.filterNot(_.is_local) |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
212 |
if (remote_hosts.isEmpty) none |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
213 |
else new Remote_Build_Cluster(build_context, remote_hosts, progress = progress) |
78413 | 214 |
} |
78398 | 215 |
} |
78413 | 216 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
217 |
// NB: extensible via Build.Engine.build_process() and Build_Process.init_cluster() |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
218 |
trait Build_Cluster extends AutoCloseable { |
78443 | 219 |
def rc: Int = Process_Result.RC.ok |
220 |
def ok: Boolean = rc == Process_Result.RC.ok |
|
221 |
def return_code(rc: Int): Unit = () |
|
222 |
def return_code(res: Process_Result): Unit = return_code(res.rc) |
|
223 |
def return_code(exn: Throwable): Unit = return_code(Process_Result.RC(exn)) |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
224 |
def open(): Unit = () |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
225 |
def init(): Unit = () |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
226 |
def benchmark(): Unit = () |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
227 |
def start(): Unit = () |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
228 |
def active(): Boolean = false |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
229 |
def join: List[Build_Cluster.Result] = Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
230 |
def stop(): Unit = { join; close() } |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
231 |
override def close(): Unit = () |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
232 |
} |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
233 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
234 |
class Remote_Build_Cluster( |
78436
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
235 |
val build_context: Build.Context, |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
236 |
val remote_hosts: List[Build_Cluster.Host], |
5f5f909206bb
clarified signature: more "object-oriented" style;
wenzelm
parents:
78434
diff
changeset
|
237 |
val progress: Progress = new Progress |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
238 |
) extends Build_Cluster { |
78424 | 239 |
require(remote_hosts.nonEmpty && !remote_hosts.exists(_.is_local), "remote hosts required") |
78413 | 240 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
241 |
override def toString: String = |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
242 |
remote_hosts.iterator.map(_.name).mkString("Build_Cluster(", ", ", ")") |
78413 | 243 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
244 |
|
78443 | 245 |
/* cumulative return code */ |
246 |
||
78581 | 247 |
private val _rc = Synchronized(Process_Result.RC.ok) |
78443 | 248 |
|
78581 | 249 |
override def rc: Int = _rc.value |
78499
a7dab3b8ebfe
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;
wenzelm
parents:
78447
diff
changeset
|
250 |
|
a7dab3b8ebfe
clarified synchronized regions: avoid deadlock of Build_Cluster operations on other thread vs. return_code(), notably via capture() error handling;
wenzelm
parents:
78447
diff
changeset
|
251 |
override def return_code(rc: Int): Unit = |
78581 | 252 |
_rc.change(rc0 => Process_Result.RC.merge(rc0, rc)) |
78443 | 253 |
|
254 |
def capture[A](host: Build_Cluster.Host, op: String)( |
|
255 |
e: => A, |
|
256 |
msg: String = host.message(op + " ..."), |
|
78506 | 257 |
err: Throwable => String = { exn => |
258 |
return_code(exn) |
|
259 |
host.message("failed to " + op + "\n" + Exn.print(exn)) |
|
260 |
} |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
261 |
): Exn.Result[A] = { |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
262 |
progress.capture(e, msg = msg, err = err) |
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
263 |
} |
78443 | 264 |
|
265 |
||
266 |
/* open remote sessions */ |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
267 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
268 |
private var _sessions = List.empty[Build_Cluster.Session] |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
269 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
270 |
override def open(): Unit = synchronized { |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
271 |
require(_sessions.isEmpty, "build cluster already open") |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
272 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
273 |
val attempts = |
78433 | 274 |
Par_List.map((host: Build_Cluster.Host) => |
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
275 |
capture(host, "open") { host.open_session(build_context, progress = progress) }, |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
276 |
remote_hosts, thread = true) |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
277 |
|
78674 | 278 |
if (attempts.forall(Exn.is_res)) { |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
279 |
_sessions = attempts.map(Exn.the_res) |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
280 |
_sessions |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
281 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
282 |
else { |
78592 | 283 |
for (case Exn.Res(session) <- attempts) session.close() |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
284 |
error("Failed to connect build cluster") |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
285 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
286 |
} |
78413 | 287 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
288 |
|
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
289 |
/* init and benchmark remote Isabelle distributions */ |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
290 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
291 |
private var _init = List.empty[Future[Unit]] |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
292 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
293 |
override def init(): Unit = synchronized { |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
294 |
require(_sessions.nonEmpty, "build cluster not yet open") |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
295 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
296 |
if (_init.isEmpty) { |
78443 | 297 |
_init = |
78567 | 298 |
for (session <- _sessions if !session.host.shared) yield { |
78443 | 299 |
Future.thread(session.host.message("session")) { |
300 |
capture(session.host, "sync") { session.sync() } |
|
301 |
capture(session.host, "init") { session.init() } |
|
302 |
} |
|
303 |
} |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
304 |
} |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
305 |
} |
78840
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
306 |
|
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
307 |
override def benchmark(): Unit = synchronized { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
308 |
_init.foreach(_.join) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
309 |
_init = |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
310 |
for (session <- _sessions if !session.host.shared) yield { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
311 |
Future.thread(session.host.message("session")) { |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
312 |
capture(session.host, "benchmark") { session.benchmark() } |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
313 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
314 |
} |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
315 |
_init.foreach(_.join) |
4b528ca25573
added initial version of benchmark module, e.g., to compare performance of different hosts;
Fabian Huch <huch@in.tum.de>
parents:
78674
diff
changeset
|
316 |
} |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
317 |
|
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
318 |
|
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
319 |
/* workers */ |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
320 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
321 |
private var _workers = List.empty[Future[Process_Result]] |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
322 |
|
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
323 |
override def active(): Boolean = synchronized { _workers.nonEmpty } |
78413 | 324 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
325 |
override def start(): Unit = synchronized { |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
326 |
require(_sessions.nonEmpty, "build cluster not yet open") |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
327 |
require(_workers.isEmpty, "build cluster already active") |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
328 |
|
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
329 |
init() |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
330 |
_init.foreach(_.join) |
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
331 |
|
78443 | 332 |
_workers = |
333 |
for (session <- _sessions) yield { |
|
78582 | 334 |
Future.thread(session.host.message("work")) { |
335 |
Exn.release(capture(session.host, "work") { session.start() }) |
|
78444
3d1746a716fa
clarified signature: Build_Cluster.Session.build_context;
wenzelm
parents:
78443
diff
changeset
|
336 |
} |
78443 | 337 |
} |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
338 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
339 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
340 |
override def join: List[Build_Cluster.Result] = synchronized { |
78443 | 341 |
_init.foreach(_.join) |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
342 |
if (_workers.isEmpty) Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
343 |
else { |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
344 |
assert(_sessions.length == _workers.length) |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
345 |
for ((session, worker) <- _sessions zip _workers) |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
346 |
yield Build_Cluster.Result(session.host, worker.join_result) |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
347 |
} |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
348 |
} |
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
349 |
|
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
350 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
351 |
/* close */ |
78430
0461fc9d43e8
more build_cluster management: open SSH connections in parallel, but synchronously;
wenzelm
parents:
78427
diff
changeset
|
352 |
|
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
353 |
override def close(): Unit = synchronized { |
78441 | 354 |
_init.foreach(_.join) |
78639
ca56952b7322
proper stop of build_process shutdown, despite errors on workers;
wenzelm
parents:
78638
diff
changeset
|
355 |
_workers.foreach(_.join_result) |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
356 |
_sessions.foreach(_.close()) |
78440
126a12483c67
support for Build_Cluster.Session.init (rsync + Admin/init);
wenzelm
parents:
78436
diff
changeset
|
357 |
|
78443 | 358 |
_init = Nil |
78434
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
359 |
_workers = Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
360 |
_sessions = Nil |
b4ec7ea073da
clarified signature: delegate policies to Build_Cluster implementation, potentially provided by Build.Engine via Build_Process.open_build_cluster;
wenzelm
parents:
78433
diff
changeset
|
361 |
} |
78413 | 362 |
} |