author | wenzelm |
Sat, 10 Jan 2015 16:35:07 +0100 | |
changeset 59341 | a74eb8e0907a |
parent 58639 | 1df53737c59b |
child 59350 | acba5d6fdb2f |
permissions | -rw-r--r-- |
45027 | 1 |
/* Title: Pure/System/system_channel.scala |
2 |
Author: Makarius |
|
3 |
||
45028 | 4 |
Portable system channel for inter-process communication, based on |
5 |
named pipes or sockets. |
|
45027 | 6 |
*/ |
7 |
||
8 |
package isabelle |
|
9 |
||
10 |
||
48409 | 11 |
import java.io.{InputStream, OutputStream, File => JFile, FileInputStream, |
12 |
FileOutputStream, IOException} |
|
45028 | 13 |
import java.net.{ServerSocket, InetAddress} |
45027 | 14 |
|
15 |
||
16 |
object System_Channel |
|
17 |
{ |
|
59341
a74eb8e0907a
always use socket to test performance and stability;
wenzelm
parents:
58639
diff
changeset
|
18 |
def apply(): System_Channel = new Socket_Channel |
a74eb8e0907a
always use socket to test performance and stability;
wenzelm
parents:
58639
diff
changeset
|
19 |
// FIXME if (Platform.is_windows) new Socket_Channel else new Fifo_Channel |
45027 | 20 |
} |
21 |
||
22 |
abstract class System_Channel |
|
23 |
{ |
|
54005
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52537
diff
changeset
|
24 |
def params: List[String] |
57915
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
54344
diff
changeset
|
25 |
def prover_args: List[String] |
45027 | 26 |
def rendezvous(): (OutputStream, InputStream) |
27 |
def accepted(): Unit |
|
28 |
} |
|
29 |
||
30 |
||
45028 | 31 |
/** named pipes **/ |
32 |
||
45251 | 33 |
private object Fifo_Channel |
45027 | 34 |
{ |
52537 | 35 |
private val next_fifo = Counter.make() |
45027 | 36 |
} |
37 |
||
45251 | 38 |
private class Fifo_Channel extends System_Channel |
45027 | 39 |
{ |
49695 | 40 |
require(!Platform.is_windows) |
41 |
||
45027 | 42 |
private def mk_fifo(): String = |
43 |
{ |
|
44 |
val i = Fifo_Channel.next_fifo() |
|
45 |
val script = |
|
58639
1df53737c59b
prefer Unix standard-conformant $TMPDIR over hard-wired /tmp;
wenzelm
parents:
57915
diff
changeset
|
46 |
"FIFO=\"${TMPDIR:-/tmp}/isabelle-fifo-${PPID}-$$" + i + "\"\n" + |
45027 | 47 |
"echo -n \"$FIFO\"\n" + |
48 |
"mkfifo -m 600 \"$FIFO\"\n" |
|
50845 | 49 |
val result = Isabelle_System.bash(script) |
50 |
if (result.rc == 0) result.out else error(result.err) |
|
45027 | 51 |
} |
52 |
||
49695 | 53 |
private def rm_fifo(fifo: String): Boolean = (new JFile(fifo)).delete |
45027 | 54 |
|
49695 | 55 |
private def fifo_input_stream(fifo: String): InputStream = new FileInputStream(fifo) |
56 |
private def fifo_output_stream(fifo: String): OutputStream = new FileOutputStream(fifo) |
|
45027 | 57 |
|
58 |
private val fifo1 = mk_fifo() |
|
59 |
private val fifo2 = mk_fifo() |
|
60 |
||
54005
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52537
diff
changeset
|
61 |
def params: List[String] = List(fifo1, fifo2) |
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52537
diff
changeset
|
62 |
|
57915
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
54344
diff
changeset
|
63 |
val prover_args: List[String] = List ("-W", fifo1 + ":" + fifo2) |
45027 | 64 |
|
65 |
def rendezvous(): (OutputStream, InputStream) = |
|
66 |
{ |
|
67 |
val output_stream = fifo_output_stream(fifo1) |
|
68 |
val input_stream = fifo_input_stream(fifo2) |
|
69 |
(output_stream, input_stream) |
|
70 |
} |
|
71 |
||
72 |
def accepted() { rm_fifo(fifo1); rm_fifo(fifo2) } |
|
73 |
} |
|
45028 | 74 |
|
75 |
||
76 |
/** sockets **/ |
|
77 |
||
45251 | 78 |
private class Socket_Channel extends System_Channel |
45028 | 79 |
{ |
80 |
private val server = new ServerSocket(0, 2, InetAddress.getByName("127.0.0.1")) |
|
81 |
||
54005
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52537
diff
changeset
|
82 |
def params: List[String] = List("127.0.0.1", server.getLocalPort.toString) |
132640f4c453
tuned signature -- facilitate experimentation with other processes;
wenzelm
parents:
52537
diff
changeset
|
83 |
|
57915
448325de6e4f
more abstract Prover.System_Process, which allows to bypass Isabelle_System.Managed_Process;
wenzelm
parents:
54344
diff
changeset
|
84 |
def prover_args: List[String] = List("-T", "127.0.0.1:" + server.getLocalPort) |
45028 | 85 |
|
86 |
def rendezvous(): (OutputStream, InputStream) = |
|
87 |
{ |
|
88 |
val socket = server.accept |
|
54340
18c621069bf8
prefer TCP_NODELAY -- avoid extra buffering due to Nagle's algorithm;
wenzelm
parents:
54005
diff
changeset
|
89 |
socket.setTcpNoDelay(true) |
45028 | 90 |
(socket.getOutputStream, socket.getInputStream) |
91 |
} |
|
92 |
||
93 |
def accepted() { server.close } |
|
94 |
} |