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