author | wenzelm |
Fri, 24 Nov 2023 15:58:24 +0100 | |
changeset 79049 | 10b6add456d0 |
parent 79048 | caddfe4949a8 |
child 79053 | badb3da19ac6 |
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} |
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
11 |
import java.net.{InetAddress, InetSocketAddress, ProtocolFamily, ServerSocket, SocketAddress, StandardProtocolFamily, UnixDomainSocketAddress} |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
12 |
import java.nio.channels.{ServerSocketChannel, Channels} |
45027 | 13 |
|
14 |
||
75393 | 15 |
object System_Channel { |
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
16 |
def apply(unix_domain: Boolean = Platform.is_unix): System_Channel = |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
17 |
if (unix_domain) new Unix else new Inet |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
18 |
|
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
19 |
class Inet extends System_Channel(StandardProtocolFamily.INET) { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
20 |
server.bind(new InetSocketAddress(Server.localhost, 0), 50) |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
21 |
|
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
22 |
override def address: String = |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
23 |
Server.print_address(server.getLocalAddress.asInstanceOf[InetSocketAddress].getPort) |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
24 |
} |
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 |
class Unix extends System_Channel(StandardProtocolFamily.UNIX) { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
27 |
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
|
28 |
private val socket_file_name = socket_file.getPath |
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 |
server.bind(UnixDomainSocketAddress.of(socket_file_name)) |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
31 |
|
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
32 |
override def address: String = socket_file_name |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
33 |
override def shutdown(): Unit = { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
34 |
super.shutdown() |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
35 |
socket_file.delete |
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 |
} |
45027 | 38 |
} |
39 |
||
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
40 |
abstract class System_Channel private(protocol_family: ProtocolFamily) { |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
41 |
protected val server: ServerSocketChannel = ServerSocketChannel.open(protocol_family) |
45028 | 42 |
|
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
43 |
def address: String |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
44 |
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
|
45 |
|
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
46 |
override def toString: String = address |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
47 |
|
73367 | 48 |
def shutdown(): Unit = server.close() |
45028 | 49 |
|
75393 | 50 |
def rendezvous(): (OutputStream, InputStream) = { |
45028 | 51 |
val socket = server.accept |
69572
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
52 |
try { |
79049
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
53 |
val out_stream = Channels.newOutputStream(socket) |
10b6add456d0
support for Unix-domain sockets, using java.nio.channels.ServerSocketChannel;
wenzelm
parents:
79048
diff
changeset
|
54 |
val in_stream = Channels.newInputStream(socket) |
45028 | 55 |
|
79048 | 56 |
Byte_Message.read_line(in_stream) match { |
57 |
case Some(bs) if bs.text == password => (out_stream, in_stream) |
|
58 |
case _ => |
|
59 |
out_stream.close() |
|
60 |
in_stream.close() |
|
61 |
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
|
62 |
} |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
63 |
} |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
64 |
finally { shutdown() } |
09a6a7c04b45
more robust system channel via options that are private to the user;
wenzelm
parents:
69463
diff
changeset
|
65 |
} |
45028 | 66 |
} |