src/Pure/System/message_channel.ML
author wenzelm
Fri, 31 Oct 2014 22:48:00 +0100
changeset 58857 b0ccc7e1e7f3
parent 57417 29fe9bac501b
child 59058 a78612c67ec0
permissions -rw-r--r--
tuned;
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     1
(*  Title:      Pure/System/message_channel.ML
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     2
    Author:     Makarius
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     3
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     4
Preferably asynchronous channel for Isabelle messages.
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     5
*)
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     6
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     7
signature MESSAGE_CHANNEL =
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
     8
sig
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
     9
  type message
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 52800
diff changeset
    10
  val message: string -> Properties.T -> string list -> message
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    11
  type T
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    12
  val send: T -> message -> unit
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    13
  val shutdown: T -> unit
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    14
  val make: System_Channel.T -> T
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    15
end;
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    16
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    17
structure Message_Channel: MESSAGE_CHANNEL =
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    18
struct
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    19
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    20
(* message *)
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    21
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    22
datatype message = Message of string list;
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    23
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 52800
diff changeset
    24
fun chunk ss =
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 52800
diff changeset
    25
  string_of_int (fold (Integer.add o size) ss 0) :: "\n" :: ss;
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    26
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    27
fun message name raw_props body =
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    28
  let
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    29
    val robust_props = map (pairself YXML.embed_controls) raw_props;
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    30
    val header = YXML.string_of (XML.Elem ((name, robust_props), []));
56333
38f1422ef473 support bulk messages consisting of small string segments, which are more healthy to the Poly/ML RTS and might prevent spurious GC crashes such as MTGCProcessMarkPointers::ScanAddressesInObject;
wenzelm
parents: 52800
diff changeset
    31
  in Message (chunk [header] @ chunk body) end;
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    32
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    33
fun output_message channel (Message ss) =
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    34
  List.app (System_Channel.output channel) ss;
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    35
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    36
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    37
(* channel *)
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    38
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    39
datatype T = Message_Channel of {send: message -> unit, shutdown: unit -> unit};
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    40
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    41
fun send (Message_Channel {send, ...}) = send;
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    42
fun shutdown (Message_Channel {shutdown, ...}) = shutdown ();
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    43
56733
f7700146678d manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
wenzelm
parents: 56333
diff changeset
    44
fun flush channel = ignore (try System_Channel.flush channel);
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    45
val flush_timeout = SOME (seconds 0.02);
56733
f7700146678d manager is direct receiver of prover output -- discontinued old performance tuning (329320fc88df, 1baa5d19ac44);
wenzelm
parents: 56333
diff changeset
    46
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    47
fun message_output mbox channel =
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    48
  let
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    49
    fun continue timeout =
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    50
      (case Mailbox.receive timeout mbox of
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    51
        [] => (flush channel; continue NONE)
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    52
      | msgs => received timeout msgs)
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    53
    and received _ (NONE :: _) = flush channel
58857
wenzelm
parents: 57417
diff changeset
    54
      | received _ (SOME msg :: rest) = (output_message channel msg; received flush_timeout rest)
57417
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    55
      | received timeout [] = continue timeout;
29fe9bac501b more tight Mailbox: single list is sufficient for single receiver, reverse outside critical section;
wenzelm
parents: 56733
diff changeset
    56
  in fn () => continue NONE end;
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    57
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    58
fun make channel =
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    59
  if Multithreading.available then
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    60
    let
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    61
      val mbox = Mailbox.create ();
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    62
      val thread = Simple_Thread.fork false (message_output mbox channel);
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    63
      fun send msg = Mailbox.send mbox (SOME msg);
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    64
      fun shutdown () =
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    65
        (Mailbox.send mbox NONE; Mailbox.await_empty mbox; Simple_Thread.join thread);
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    66
    in Message_Channel {send = send, shutdown = shutdown} end
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    67
  else
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    68
    let
52800
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    69
      fun send msg = (output_message channel msg; flush channel);
1baa5d19ac44 less aggressive flushing: cope with massive amounts of protocol messages, e.g. from threads_trace;
wenzelm
parents: 52584
diff changeset
    70
    in Message_Channel {send = send, shutdown = fn () => ()} end;
52584
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    71
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    72
end;
5cad4a5f5615 more abstract message channel;
wenzelm
parents:
diff changeset
    73