]> matita.cs.unibo.it Git - helm.git/blob - helm/http_getter/threadSafe.ml
removed ancient lablgtk, lablgtk_gtkmathview
[helm.git] / helm / http_getter / threadSafe.ml
1 (*
2  * Copyright (C) 2003:
3  *    Stefano Zacchiroli <zack@cs.unibo.it>
4  *    for the HELM Team http://helm.cs.unibo.it/
5  *
6  *  This file is part of HELM, an Hypertextual, Electronic
7  *  Library of Mathematics, developed at the Computer Science
8  *  Department, University of Bologna, Italy.
9  *
10  *  HELM is free software; you can redistribute it and/or
11  *  modify it under the terms of the GNU General Public License
12  *  as published by the Free Software Foundation; either version 2
13  *  of the License, or (at your option) any later version.
14  *
15  *  HELM is distributed in the hope that it will be useful,
16  *  but WITHOUT ANY WARRANTY; without even the implied warranty of
17  *  MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE.  See the
18  *  GNU General Public License for more details.
19  *
20  *  You should have received a copy of the GNU General Public License
21  *  along with HELM; if not, write to the Free Software
22  *  Foundation, Inc., 59 Temple Place - Suite 330, Boston,
23  *  MA  02111-1307, USA.
24  *
25  *  For details, see the HELM World-Wide-Web page,
26  *  http://helm.cs.unibo.it/
27  *)
28
29 open Http_getter_debugger;;
30 let debug_print _ = ();;  (* override debugger 'debug_print' *)
31
32 class threadSafe =
33   object (self)
34
35     val mutex = Mutex.create ()
36
37       (** condition variable: 'no readers is currently reading' *)
38     val noReaders = Condition.create ()
39
40       (** readers count *)
41     val mutable readersCount = 0
42
43     method private incrReadersCount = (* internal, not exported *)
44       self#doCritical (lazy (
45         readersCount <- readersCount + 1
46       ))
47
48     method private decrReadersCount = (* internal, not exported *)
49       self#doCritical (lazy (
50         if readersCount > 0 then readersCount <- readersCount - 1;
51       ))
52
53     method private signalNoReaders =  (* internal, not exported *)
54       self#doCritical (lazy (
55         if readersCount = 0 then Condition.signal noReaders
56       ))
57
58     method private doCritical: 'a. 'a lazy_t -> 'a =
59       fun action ->
60         debug_print "<doCritical>";
61         (try
62           Mutex.lock mutex;
63           let res = Lazy.force action in
64           Mutex.unlock mutex;
65           debug_print "</doCritical>";
66           res
67         with e ->
68           Mutex.unlock mutex;
69           raise e);
70
71     method private doReader: 'a. 'a lazy_t -> 'a =
72       fun action ->
73         debug_print "<doReader>";
74         let cleanup () =
75           self#decrReadersCount;
76           self#signalNoReaders
77         in
78         self#incrReadersCount;
79         let res = (try Lazy.force action with e -> (cleanup (); raise e)) in
80         cleanup ();
81         debug_print "</doReader>";
82         res
83
84       (* TODO may starve!!!! is what we want or not? *)
85     method private doWriter: 'a. 'a lazy_t -> 'a =
86       fun action ->
87         debug_print "<doWriter>";
88         self#doCritical (lazy (
89           while readersCount > 0 do
90             Condition.wait noReaders mutex
91           done;
92           let res = Lazy.force action in
93           debug_print "</doWriter>";
94           res
95         ))
96
97   end
98