author | wenzelm |
Fri, 24 Nov 2023 21:32:32 +0100 | |
changeset 79055 | c83cdd300848 |
parent 79053 | badb3da19ac6 |
child 79056 | 1f34f6394383 |
permissions | -rw-r--r-- |
45027 | 1 |
/* Title: Pure/System/system_channel.scala |
2 |
Author: Makarius |
|
3 |
||
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
59341
diff
changeset
|
4 |
Socket-based system channel for inter-process communication. |
45027 | 5 |
*/ |
6 |
||
7 |
package isabelle |
|
8 |
||
9 |
||
59350
acba5d6fdb2f
discontinued fifo channel, always use portable socket;
wenzelm
parents:
59341
diff
changeset
|
10 |
import java.io.{InputStream, OutputStream} |
79055 | 11 |
import java.net.{InetAddress, InetSocketAddress, ProtocolFamily, ServerSocket, SocketAddress, |
12 |
StandardProtocolFamily, UnixDomainSocketAddress, StandardSocketOptions} |
|
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
13 |
import java.nio.channels.{ServerSocketChannel, Channels} |
45027 | 14 |
|
15 |
||
75393 | 16 |
object System_Channel { |
79053
badb3da19ac6
disable unix_domain for now: somewhat unstable, e.g. "isabelle build -b HOL-Analysis" on arm64_32-darwin (studio1);
wenzelm
parents:
79049
diff
changeset
|
17 |
def apply(unix_domain: Boolean = false): System_Channel = |
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
18 |
if (unix_domain) new Unix else new Inet |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
19 |
|
79055 | 20 |
val buffer_size: Integer = Integer.valueOf(131072) |
21 |
||
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
22 |
class Inet extends System_Channel(StandardProtocolFamily.INET) { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
23 |
server.bind(new InetSocketAddress(Server.localhost, 0), 50) |
79055 | 24 |
server.setOption(StandardSocketOptions.SO_RCVBUF, buffer_size) |
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
25 |
|
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
26 |
override def address: String = |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
27 |
Server.print_address(server.getLocalAddress.asInstanceOf[InetSocketAddress].getPort) |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
28 |
} |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
29 |
|
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
30 |
class Unix extends System_Channel(StandardProtocolFamily.UNIX) { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
31 |
private val socket_file = Isabelle_System.tmp_file("socket", initialized = false) |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
32 |
private val socket_file_name = socket_file.getPath |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
33 |
|
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
34 |
server.bind(UnixDomainSocketAddress.of(socket_file_name)) |
79055 | 35 |
server.setOption(StandardSocketOptions.SO_RCVBUF, buffer_size) |
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
36 |
|
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
37 |
override def address: String = socket_file_name |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
38 |
override def shutdown(): Unit = { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
39 |
super.shutdown() |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
40 |
socket_file.delete |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
41 |
} |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
42 |
} |
45027 | 43 |
} |
44 |
||
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
45 |
abstract class System_Channel private(protocol_family: ProtocolFamily) { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
46 |
protected val server: ServerSocketChannel = ServerSocketChannel.open(protocol_family) |
45028 | 47 |
|
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
48 |
def address: String |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
49 |
lazy val password: String = UUID.random().toString |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
50 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
51 |
override def toString: String = address |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
52 |
|
73367 | 53 |
def shutdown(): Unit = server.close() |
45028 | 54 |
|
75393 | 55 |
def rendezvous(): (OutputStream, InputStream) = { |
45028 | 56 |
val socket = server.accept |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
57 |
try { |
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
58 |
val out_stream = Channels.newOutputStream(socket) |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
59 |
val in_stream = Channels.newInputStream(socket) |
45028 | 60 |
|
79048 | 61 |
Byte_Message.read_line(in_stream) match { |
62 |
case Some(bs) if bs.text == password => (out_stream, in_stream) |
|
63 |
case _ => |
|
64 |
out_stream.close() |
|
65 |
in_stream.close() |
|
66 |
error("Failed to connect system channel: bad password") |
|
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
67 |
} |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
68 |
} |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
69 |
finally { shutdown() } |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
70 |
} |
45028 | 71 |
} |