From: Stefano Zacchiroli 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 +(* + (* *) + 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 + (* *) +*) 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 +(* + (* *) + 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 + (* *) +*) 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 +(* + (* *) + 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 + (* *) +*) 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 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