]> matita.cs.unibo.it Git - helm.git/blobdiff - helm/hbugs/tutors/hbugs_tutors_common.ml
added support for slaves killing
[helm.git] / helm / hbugs / tutors / hbugs_tutors_common.ml
index f00b17bc014998cdfa558699206df0686a4826d7..ca3de9fed48335036e6b384796e3ea414de817a1 100644 (file)
@@ -171,24 +171,41 @@ module BuildTutor (Dsc: HbugsTutorDescription) : HbugsTutor =
         (sprintf "Bye, I've completed my duties (success = %b)" success)
 
     let hbugs_callback =
+        (* hashtbl mapping musings ids to PID of threads doing the related (dirty)
+        work *)
+      let slaves = Hashtbl.create 17 in
       let forbidden () =
         prerr_endline "ignoring request from unauthorized broker";
         Exception ("forbidden", "")
       in
-      function
+      function  (* _the_ callback *)
       | Start_musing (broker_id, state) ->
           if is_authenticated broker_id then begin
             prerr_endline "received Start_musing";
             let new_musing_id = Hbugs_id_generator.new_musing_id () in
             prerr_endline
               (sprintf "starting a new musing (id = %s)" new_musing_id);
-            ignore (Thread.create slave (state, new_musing_id));
+(*             let slave_thread = Thread.create slave (state, new_musing_id) in *)
+            let slave_thread =
+              Hbugs_deity.create slave (state, new_musing_id)
+            in
+            Hashtbl.add slaves new_musing_id slave_thread;
             Musing_started (my_own_id, new_musing_id)
           end else  (* broker unauthorized *)
             forbidden ();
       | Abort_musing (broker_id, musing_id) ->
           if is_authenticated broker_id then begin
-            prerr_endline "Ignoring 'Abort_musing' message ...";
+            (try  (* kill thread responsible for "musing_id" *)
+              let slave_thread = Hashtbl.find slaves musing_id in
+              Hbugs_deity.kill slave_thread;
+              Hashtbl.remove slaves musing_id
+            with
+            | Hbugs_deity.Can_t_kill (pid, reason) ->
+              prerr_endline (sprintf "Unable to kill slave %d: %s" pid reason)
+            | Not_found ->
+                prerr_endline (sprintf
+                  "Can't find slave corresponding to musing %s, can't kill it"
+                  musing_id));
             Musing_aborted (my_own_id, musing_id)
           end else (* broker unauthorized *)
             forbidden ();