src/HOL/Tools/Sledgehammer/async_manager.ML
author blanchet
Sun May 01 18:37:24 2011 +0200 (2011-05-01)
changeset 42546 8591fcc56c34
parent 41042 8275f52ac991
child 43005 c96f06bffd90
permissions -rw-r--r--
make sure typing fact names are unique (needed e.g. by SNARK)
blanchet@41042
     1
(*  Title:      HOL/Tools/Sledgehammer/async_manager.ML
blanchet@37583
     2
    Author:     Fabian Immler, TU Muenchen
blanchet@37583
     3
    Author:     Makarius
blanchet@37583
     4
    Author:     Jasmin Blanchette, TU Muenchen
blanchet@37583
     5
blanchet@37583
     6
Central manager for asynchronous diagnosis tool threads.
blanchet@37583
     7
*)
blanchet@37583
     8
blanchet@37583
     9
signature ASYNC_MANAGER =
blanchet@37583
    10
sig
blanchet@39369
    11
  val break_into_chunks : string list -> string list
blanchet@37584
    12
  val launch :
blanchet@39006
    13
    string -> Time.time -> Time.time -> string -> (unit -> string) -> unit
blanchet@37585
    14
  val kill_threads : string -> string -> unit
blanchet@37585
    15
  val running_threads : string -> string -> unit
blanchet@37585
    16
  val thread_messages : string -> string -> int option -> unit
blanchet@37583
    17
end;
blanchet@37583
    18
blanchet@37583
    19
structure Async_Manager : ASYNC_MANAGER =
blanchet@37583
    20
struct
blanchet@37583
    21
blanchet@37583
    22
(** preferences **)
blanchet@37583
    23
blanchet@37583
    24
val message_store_limit = 20;
blanchet@37583
    25
val message_display_limit = 5;
blanchet@37583
    26
blanchet@37583
    27
blanchet@37583
    28
(** thread management **)
blanchet@37583
    29
blanchet@37583
    30
(* data structures over threads *)
blanchet@37583
    31
blanchet@37583
    32
structure Thread_Heap = Heap
blanchet@37583
    33
(
blanchet@37583
    34
  type elem = Time.time * Thread.thread;
blanchet@37583
    35
  fun ord ((a, _), (b, _)) = Time.compare (a, b);
blanchet@37583
    36
);
blanchet@37583
    37
blanchet@37583
    38
fun lookup_thread xs = AList.lookup Thread.equal xs;
blanchet@37583
    39
fun delete_thread xs = AList.delete Thread.equal xs;
blanchet@37583
    40
fun update_thread xs = AList.update Thread.equal xs;
blanchet@37583
    41
blanchet@37583
    42
blanchet@37583
    43
(* state of thread manager *)
blanchet@37583
    44
blanchet@37583
    45
type state =
blanchet@37585
    46
  {manager: Thread.thread option,
blanchet@37585
    47
   timeout_heap: Thread_Heap.T,
blanchet@37585
    48
   active: (Thread.thread * (string * Time.time * Time.time * string)) list,
blanchet@37585
    49
   canceling: (Thread.thread * (string * Time.time * string)) list,
blanchet@37585
    50
   messages: (string * string) list,
blanchet@37585
    51
   store: (string * string) list}
blanchet@37583
    52
blanchet@37583
    53
fun make_state manager timeout_heap active canceling messages store : state =
blanchet@37583
    54
  {manager = manager, timeout_heap = timeout_heap, active = active,
blanchet@37583
    55
   canceling = canceling, messages = messages, store = store}
blanchet@37583
    56
blanchet@37583
    57
val global_state = Synchronized.var "async_manager"
blanchet@37583
    58
  (make_state NONE Thread_Heap.empty [] [] [] []);
blanchet@37583
    59
blanchet@37583
    60
blanchet@37583
    61
(* unregister thread *)
blanchet@37583
    62
blanchet@39006
    63
fun unregister message thread =
blanchet@37583
    64
  Synchronized.change global_state
blanchet@37583
    65
  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583
    66
    (case lookup_thread active thread of
blanchet@39376
    67
      SOME (tool, _, _, desc) =>
blanchet@37583
    68
        let
blanchet@37583
    69
          val active' = delete_thread thread active;
blanchet@37583
    70
          val now = Time.now ()
blanchet@37585
    71
          val canceling' = (thread, (tool, now, desc)) :: canceling
blanchet@39006
    72
          val message' = desc ^ "\n" ^ message
blanchet@37585
    73
          val messages' = (tool, message') :: messages;
blanchet@37585
    74
          val store' = (tool, message') ::
blanchet@37583
    75
            (if length store <= message_store_limit then store
blanchet@37583
    76
             else #1 (chop message_store_limit store));
blanchet@37583
    77
        in make_state manager timeout_heap active' canceling' messages' store' end
blanchet@37583
    78
    | NONE => state));
blanchet@37583
    79
blanchet@37583
    80
blanchet@37583
    81
(* main manager thread -- only one may exist *)
blanchet@37583
    82
wenzelm@40301
    83
val min_wait_time = seconds 0.3;
wenzelm@40301
    84
val max_wait_time = seconds 10.0;
blanchet@37583
    85
blanchet@37583
    86
fun replace_all bef aft =
blanchet@37583
    87
  let
blanchet@37583
    88
    fun aux seen "" = String.implode (rev seen)
blanchet@37583
    89
      | aux seen s =
blanchet@37583
    90
        if String.isPrefix bef s then
blanchet@37583
    91
          aux seen "" ^ aft ^ aux [] (unprefix bef s)
blanchet@37583
    92
        else
blanchet@37583
    93
          aux (String.sub (s, 0) :: seen) (String.extract (s, 1, NONE))
blanchet@37583
    94
  in aux [] end
blanchet@37583
    95
blanchet@37583
    96
(* This is a workaround for Proof General's off-by-a-few sendback display bug,
blanchet@37583
    97
   whereby "pr" in "proof" is not highlighted. *)
blanchet@39369
    98
val break_into_chunks = maps (space_explode "\000" o replace_all "\n\n" "\000")
blanchet@37583
    99
blanchet@37585
   100
fun print_new_messages () =
blanchet@37583
   101
  case Synchronized.change_result global_state
blanchet@37583
   102
         (fn {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583
   103
             (messages, make_state manager timeout_heap active canceling []
blanchet@37583
   104
                                   store)) of
blanchet@37583
   105
    [] => ()
blanchet@37585
   106
  | msgs as (tool, _) :: _ =>
blanchet@39369
   107
    let val ss = break_into_chunks (map snd msgs) in
wenzelm@40132
   108
      List.app Output.urgent_message (tool ^ ": " ^ hd ss :: tl ss)
blanchet@37585
   109
    end
blanchet@37583
   110
blanchet@39006
   111
fun check_thread_manager () = Synchronized.change global_state
blanchet@37583
   112
  (fn state as {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583
   113
    if (case manager of SOME thread => Thread.isActive thread | NONE => false) then state
blanchet@37583
   114
    else let val manager = SOME (Toplevel.thread false (fn () =>
blanchet@37583
   115
      let
blanchet@37583
   116
        fun time_limit timeout_heap =
blanchet@37583
   117
          (case try Thread_Heap.min timeout_heap of
blanchet@37583
   118
            NONE => Time.+ (Time.now (), max_wait_time)
blanchet@37583
   119
          | SOME (time, _) => time);
blanchet@37583
   120
blanchet@37583
   121
        (*action: find threads whose timeout is reached, and interrupt canceling threads*)
blanchet@37583
   122
        fun action {manager, timeout_heap, active, canceling, messages, store} =
blanchet@37583
   123
          let val (timeout_threads, timeout_heap') =
blanchet@37583
   124
            Thread_Heap.upto (Time.now (), Thread.self ()) timeout_heap;
blanchet@37583
   125
          in
blanchet@37585
   126
            if null timeout_threads andalso null canceling then
blanchet@37585
   127
              NONE
blanchet@37583
   128
            else
blanchet@37583
   129
              let
blanchet@37583
   130
                val _ = List.app (Simple_Thread.interrupt o #1) canceling
blanchet@37583
   131
                val canceling' = filter (Thread.isActive o #1) canceling
blanchet@37583
   132
                val state' = make_state manager timeout_heap' active canceling' messages store;
blanchet@37583
   133
              in SOME (map #2 timeout_threads, state') end
blanchet@37583
   134
          end;
blanchet@37583
   135
      in
blanchet@37583
   136
        while Synchronized.change_result global_state
blanchet@37583
   137
          (fn state as {timeout_heap, active, canceling, messages, store, ...} =>
blanchet@37583
   138
            if null active andalso null canceling andalso null messages
blanchet@37583
   139
            then (false, make_state NONE timeout_heap active canceling messages store)
blanchet@37583
   140
            else (true, state))
blanchet@37583
   141
        do
blanchet@37583
   142
          (Synchronized.timed_access global_state (SOME o time_limit o #timeout_heap) action
blanchet@37583
   143
            |> these
blanchet@39006
   144
            |> List.app (unregister "Timed out.\n");
blanchet@37585
   145
            print_new_messages ();
blanchet@37583
   146
            (*give threads some time to respond to interrupt*)
blanchet@37583
   147
            OS.Process.sleep min_wait_time)
blanchet@37583
   148
      end))
blanchet@37583
   149
    in make_state manager timeout_heap active canceling messages store end)
blanchet@37583
   150
blanchet@37583
   151
blanchet@37583
   152
(* register thread *)
blanchet@37583
   153
blanchet@39006
   154
fun register tool birth_time death_time desc thread =
blanchet@37583
   155
 (Synchronized.change global_state
blanchet@37583
   156
    (fn {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583
   157
      let
blanchet@37583
   158
        val timeout_heap' = Thread_Heap.insert (death_time, thread) timeout_heap;
blanchet@37585
   159
        val active' = update_thread (thread, (tool, birth_time, death_time, desc)) active;
blanchet@37583
   160
        val state' = make_state manager timeout_heap' active' canceling messages store;
blanchet@37583
   161
      in state' end);
blanchet@39006
   162
  check_thread_manager ())
blanchet@37583
   163
blanchet@37583
   164
blanchet@39006
   165
fun launch tool birth_time death_time desc f =
blanchet@37584
   166
  (Toplevel.thread true
blanchet@37584
   167
       (fn () =>
blanchet@37584
   168
           let
blanchet@37584
   169
             val self = Thread.self ()
blanchet@39006
   170
             val _ = register tool birth_time death_time desc self
blanchet@37584
   171
             val message = f ()
blanchet@39006
   172
           in unregister message self end);
blanchet@37584
   173
   ())
blanchet@37584
   174
blanchet@37583
   175
blanchet@37583
   176
(** user commands **)
blanchet@37583
   177
blanchet@37583
   178
(* kill threads *)
blanchet@37583
   179
blanchet@37585
   180
fun kill_threads tool workers = Synchronized.change global_state
blanchet@37583
   181
  (fn {manager, timeout_heap, active, canceling, messages, store} =>
blanchet@37583
   182
    let
blanchet@37585
   183
      val killing =
blanchet@37585
   184
        map_filter (fn (th, (tool', _, _, desc)) =>
blanchet@37585
   185
                       if tool' = tool then SOME (th, (tool', Time.now (), desc))
blanchet@37585
   186
                       else NONE) active
blanchet@37583
   187
      val state' = make_state manager timeout_heap [] (killing @ canceling) messages store;
wenzelm@40132
   188
      val _ = if null killing then () else Output.urgent_message ("Killed active " ^ workers ^ ".")
blanchet@37583
   189
    in state' end);
blanchet@37583
   190
blanchet@37583
   191
blanchet@37583
   192
(* running threads *)
blanchet@37583
   193
blanchet@37585
   194
fun seconds time = string_of_int (Time.toSeconds time) ^ " s"
blanchet@37583
   195
blanchet@37585
   196
fun running_threads tool workers =
blanchet@37583
   197
  let
blanchet@37583
   198
    val {active, canceling, ...} = Synchronized.value global_state;
blanchet@37583
   199
blanchet@37583
   200
    val now = Time.now ();
blanchet@37585
   201
    fun running_info (_, (tool', birth_time, death_time, desc)) =
blanchet@37585
   202
      if tool' = tool then
blanchet@37585
   203
        SOME ("Running: " ^ seconds (Time.- (now, birth_time)) ^ " -- " ^
blanchet@37585
   204
              seconds (Time.- (death_time, now)) ^ " to live:\n" ^ desc)
blanchet@37585
   205
      else
blanchet@37585
   206
        NONE
blanchet@37585
   207
    fun canceling_info (_, (tool', death_time, desc)) =
blanchet@37585
   208
      if tool' = tool then
blanchet@37585
   209
        SOME ("Trying to interrupt thread since " ^
blanchet@37585
   210
              seconds (Time.- (now, death_time)) ^ ":\n" ^ desc)
blanchet@37585
   211
      else
blanchet@37585
   212
        NONE
blanchet@37583
   213
    val running =
blanchet@37585
   214
      case map_filter running_info active of
blanchet@37585
   215
        [] => ["No " ^ workers ^ " running."]
blanchet@37585
   216
      | ss => "Running " ^ workers ^ ":" :: ss
blanchet@37583
   217
    val interrupting =
blanchet@37585
   218
      case map_filter canceling_info canceling of
blanchet@37583
   219
        [] => []
blanchet@37585
   220
      | ss => "Trying to interrupt the following " ^ workers ^ ":" :: ss
wenzelm@40132
   221
  in Output.urgent_message (space_implode "\n\n" (running @ interrupting)) end
blanchet@37583
   222
blanchet@37585
   223
fun thread_messages tool worker opt_limit =
blanchet@37583
   224
  let
blanchet@37583
   225
    val limit = the_default message_display_limit opt_limit;
blanchet@37585
   226
    val tool_store = Synchronized.value global_state
blanchet@37585
   227
                     |> #store |> filter (curry (op =) tool o fst)
blanchet@37583
   228
    val header =
blanchet@37585
   229
      "Recent " ^ worker ^ " messages" ^
blanchet@37585
   230
        (if length tool_store <= limit then ":"
blanchet@37585
   231
         else " (" ^ string_of_int limit ^ " displayed):");
blanchet@39369
   232
  in
wenzelm@40132
   233
    List.app Output.urgent_message (header :: break_into_chunks
blanchet@39369
   234
                                     (map snd (#1 (chop limit tool_store))))
blanchet@39369
   235
  end
blanchet@37583
   236
blanchet@37583
   237
end;