X-Git-Url: http://matita.cs.unibo.it/gitweb/?a=blobdiff_plain;f=helm%2Fhbugs%2Fbroker%2Fhbugs_broker_registry.ml;h=879d746ac1f6a22703c07e0bb2887d47b62edbad;hb=7cb90c67bc6f8113188a91ecc29f6db20db5aeb8;hp=adf8bc379f022c765aa932f7934dcd5a475f7eab;hpb=3c1a6c534877f7b7266809e4d92de02c7f1ee9d4;p=helm.git diff --git a/helm/hbugs/broker/hbugs_broker_registry.ml b/helm/hbugs/broker/hbugs_broker_registry.ml index adf8bc379..879d746ac 100644 --- a/helm/hbugs/broker/hbugs_broker_registry.ml +++ b/helm/hbugs/broker/hbugs_broker_registry.ml @@ -1,5 +1,7 @@ (* - * Copyright (C) 2003, HELM Team. + * Copyright (C) 2003: + * Stefano Zacchiroli + * for the HELM Team http://helm.cs.unibo.it/ * * This file is part of HELM, an Hypertextual, Electronic * Library of Mathematics, developed at the Computer Science @@ -21,11 +23,12 @@ * MA 02111-1307, USA. * * For details, see the HELM World-Wide-Web page, - * http://cs.unibo.it/helm/. + * http://helm.cs.unibo.it/ *) open Hbugs_misc;; open Hbugs_types;; +open Printf;; exception Client_already_in of client_id;; exception Client_not_found of client_id;; @@ -34,27 +37,51 @@ exception Musing_not_found of musing_id;; exception Tutor_already_in of tutor_id;; exception Tutor_not_found of tutor_id;; +class type registry = + object + method dump: string + method purge: unit + end + +let expire_time = 1800. (* 30 minutes *) + 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 val subscriptions: (client_id, tutor_id list) Hashtbl.t = Hashtbl.create 17 + (** INVARIANT: each client registered has an entry in 'urls' hash table + _and_ in 'subscriptions hash table even if it hasn't yet invoked + 'subscribe' method *) + method register id url = self#doWriter (lazy ( if Hashtbl.mem urls id then raise (Client_already_in id) else begin Hashtbl.add urls id url; - Hashtbl.add subscriptions id [] + Hashtbl.add subscriptions id []; + Hashtbl.add timetable id (Unix.time ()) end )) + method private remove id = + Hashtbl.remove urls id; + Hashtbl.remove subscriptions id; + Hashtbl.remove timetable id method unregister id = self#doWriter (lazy ( - if Hashtbl.mem urls id then begin - Hashtbl.remove urls id; - Hashtbl.remove subscriptions id - end else + if Hashtbl.mem urls id then + self#remove id + else raise (Client_not_found id) )) method isAuthenticated id = self#doReader (lazy ( @@ -79,25 +106,62 @@ class clients = raise (Client_not_found id) )) + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun id url dump -> + (dump ^ + (sprintf "\n" id url) ^ + "\n" ^ + (String.concat "\n" (* id's subscriptions *) + (List.map + (fun tutor_id -> sprintf "\n" tutor_id) + (Hashtbl.find subscriptions id))) ^ + "\n\n")) + urls "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + end 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 = Hashtbl.create 17 method register id url hint_type dsc = self#doWriter (lazy ( if Hashtbl.mem tbl id then raise (Tutor_already_in id) - else - Hashtbl.add tbl id (url, hint_type, dsc) + else begin + Hashtbl.add tbl id (url, hint_type, dsc); + Hashtbl.add timetable id (Unix.time ()) + end )) + method private remove id = + Hashtbl.remove tbl id; + Hashtbl.remove timetable id method unregister id = self#doWriter (lazy ( if Hashtbl.mem tbl id then - Hashtbl.remove tbl id + self#remove id else raise (Tutor_not_found id) )) @@ -127,43 +191,124 @@ class tutors = (fun id (url, hint_type, dsc) idx -> (id, dsc) :: idx) tbl [] )) + method dump = self#doReader (lazy ( + "\n" ^ + (Hashtbl.fold + (fun id (url, hint_type, dsc) dump -> + dump ^ + (sprintf +"\n%s\n%s\n" + id url hint_type dsc)) + tbl "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable + )) + end 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' (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; + (* 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 begin - Hashtbl.remove musings id; - hashtbl_remove_all clients id; - hashtbl_remove_all tutors id - end + 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 ( + "\n" ^ + (Hashtbl.fold + (fun mid (cid, tid) dump -> + dump ^ + (sprintf "\n" + mid cid tid)) + musings "") ^ + "" + )) + method purge = self#doWriter (lazy ( + let now = Unix.time () in + Hashtbl.iter + (fun id birthday -> + if now -. birthday > expire_time then + self#remove id) + timetable )) end