From: Stefano Zacchiroli <zack@upsilon.cc>
Date: Wed, 19 Feb 2003 13:48:35 +0000 (+0000)
Subject: - bugfix: musings table is now consistent!
X-Git-Tag: V_0_0_4_1~34
X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=commitdiff_plain;h=e404d33b583660bee61656308ddd20df79ad1eba;p=helm.git

- bugfix: musings table is now consistent!
- changed data structures used to hold musings: now explicitely use
  lists instead of relying on Hashtbl multiple bindings
- added isActive method on musings class
---

diff --git a/helm/hbugs/broker/hbugs_broker_registry.ml b/helm/hbugs/broker/hbugs_broker_registry.ml
index 644f0c53f..879d746ac 100644
--- a/helm/hbugs/broker/hbugs_broker_registry.ml
+++ b/helm/hbugs/broker/hbugs_broker_registry.ml
@@ -49,6 +49,13 @@ class clients =
   object (self)
 
     inherit ThreadSafe.threadSafe
+(*
+    (* <DEBUGGING> *)
+    method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    (* </DEBUGGING> *)
+*)
 
     val timetable: (client_id, float) Hashtbl.t = Hashtbl.create 17
     val urls: (client_id, string) Hashtbl.t = Hashtbl.create 17
@@ -129,6 +136,13 @@ class tutors =
   object (self)
 
     inherit ThreadSafe.threadSafe
+(*
+    (* <DEBUGGING> *)
+    method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    (* </DEBUGGING> *)
+*)
 
     val timetable: (tutor_id, float) Hashtbl.t = Hashtbl.create 17
     val tbl: (tutor_id, string * hint_type * string) Hashtbl.t =
@@ -203,45 +217,79 @@ class musings =
   object (self)
 
     inherit ThreadSafe.threadSafe
+(*
+    (* <DEBUGGING> *)
+    method private doCritical: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    method private doWriter: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    method private doReader: 'a. 'a lazy_t -> 'a = fun act -> Lazy.force act
+    (* </DEBUGGING> *)
+*)
 
     val timetable: (musing_id, float) Hashtbl.t = Hashtbl.create 17
     val musings: (musing_id, client_id * tutor_id) Hashtbl.t = Hashtbl.create 17
-    val clients: (client_id, musing_id) Hashtbl.t = Hashtbl.create 17
-    val tutors: (tutor_id, musing_id) Hashtbl.t = Hashtbl.create 17
+    val clients: (client_id, musing_id list) Hashtbl.t = Hashtbl.create 17
+    val tutors: (tutor_id, musing_id list) Hashtbl.t = Hashtbl.create 17
 
       (** INVARIANT: each registered musing <musing_id, client_id, tutor_id> has
-      an entry in 'musings' table, an entry in 'clients' table and an entry in
-      'tutors' table *)
+      an entry in 'musings' table, an entry in 'clients' (i.e. one of the
+      musings for client_id is musing_id) table, an entry in 'tutors' table
+      (i.e. one of the musings for tutor_id is musing_id) and an entry in
+      'timetable' table *)
+
 
     method register musing_id client_id tutor_id = self#doWriter (lazy (
       if Hashtbl.mem musings musing_id then
         raise (Musing_already_in musing_id)
       else begin
         Hashtbl.add musings musing_id (client_id, tutor_id);
-        Hashtbl.add clients client_id musing_id;
-        Hashtbl.add tutors tutor_id musing_id;
+          (* now add this musing as the first one of musings list for client and
+          tutor *)
+        Hashtbl.replace clients client_id
+          (musing_id ::
+            (try Hashtbl.find clients client_id with Not_found -> []));
+        Hashtbl.replace tutors tutor_id
+          (musing_id ::
+            (try Hashtbl.find tutors tutor_id with Not_found -> []));
         Hashtbl.add timetable musing_id (Unix.time ())
       end
     ))
     method private remove id =
+        (* ASSUMPTION: this method is invoked under a 'writer' lock *)
+      let (client_id, tutor_id) = self#getByMusingId' id in
       Hashtbl.remove musings id;
-      hashtbl_remove_all clients id;
-      hashtbl_remove_all tutors id;
+        (* now remove this musing from the list of musings for client and tutor
+        *)
+      Hashtbl.replace clients client_id
+        (List.filter ((<>) id)
+          (try Hashtbl.find clients client_id with Not_found -> []));
+      Hashtbl.replace tutors tutor_id
+        (List.filter ((<>) id)
+          (try Hashtbl.find tutors tutor_id with Not_found -> []));
       Hashtbl.remove timetable id
     method unregister id = self#doWriter (lazy (
       if Hashtbl.mem musings id then
         self#remove id
     ))
-    method getByMusingId id = self#doReader (lazy (
+    method private getByMusingId' id =
+      (* ASSUMPTION: this method is invoked under a 'reader' lock *)
       try
         Hashtbl.find musings id
       with Not_found -> raise (Musing_not_found id)
+    method getByMusingId id = self#doReader (lazy (
+      self#getByMusingId' id
     ))
     method getByClientId id = self#doReader (lazy (
-      Hashtbl.find_all clients id
+      try
+        Hashtbl.find clients id
+      with Not_found -> []
     ))
     method getByTutorId id = self#doReader (lazy (
-      Hashtbl.find_all tutors id
+      try
+        Hashtbl.find tutors id
+      with Not_found -> []
+    ))
+    method isActive id = self#doReader (lazy (
+      Hashtbl.mem musings id
     ))
 
     method dump = self#doReader (lazy (
diff --git a/helm/hbugs/broker/hbugs_broker_registry.mli b/helm/hbugs/broker/hbugs_broker_registry.mli
index ad0c694e1..ece9e07cf 100644
--- a/helm/hbugs/broker/hbugs_broker_registry.mli
+++ b/helm/hbugs/broker/hbugs_broker_registry.mli
@@ -79,6 +79,7 @@ class musings:
     method getByMusingId: musing_id -> client_id * tutor_id
     method getByClientId: client_id -> musing_id list
     method getByTutorId: tutor_id -> musing_id list
+    method isActive: musing_id -> bool
 
     method dump: string
     method purge: unit