From 6fb7dd4ec420339578a69537387170a7c2fb288b Mon Sep 17 00:00:00 2001
From: fbesson <fbesson@85f007b7-540e-0410-9357-904b9bb8a0f7>
Date: Thu, 21 Apr 2011 12:53:15 +0000
Subject: bug fix: concurrent access of persistent_cache

git-svn-id: svn+ssh://scm.gforge.inria.fr/svn/coq/trunk@14037 85f007b7-540e-0410-9357-904b9bb8a0f7
---
 plugins/micromega/persistent_cache.ml | 77 +++++++++++++++++++++++------------
 1 file changed, 50 insertions(+), 27 deletions(-)

(limited to 'plugins')

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index cd045e425..ed9fdcead 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -6,9 +6,9 @@
 (*         *       GNU Lesser General Public License Version 2.1        *)
 (************************************************************************)
 (*                                                                      *)
-(* A persistent hashtable                                               *)
+(*  A persistent hashtable                                              *)
 (*                                                                      *)
-(*  Frédéric Besson (Inria Rennes) 2009                                 *)
+(*  Frédéric Besson (Inria Rennes) 2009-2011                            *)
 (*                                                                      *)
 (************************************************************************)
 
@@ -20,8 +20,7 @@ module type PHashtable =
 
     val create : int -> string -> 'a t
     (** [create i f] creates an empty persistent table
-	with initial size i
-	associated with file [f] *)
+	with initial size i associated with file [f] *)
 
 
     val open_in : string -> 'a t
@@ -40,7 +39,7 @@ module type PHashtable =
     val close : 'a t -> unit
     (** [close tbl] is closing the table.
 	Once closed, a table cannot be used.
-	i.e, copy, find,add will raise UnboundTable *)
+	i.e, find,add will raise UnboundTable *)
 
     val memo : string -> (key -> 'a) -> (key -> 'a)
       (** [memo cache f] returns a memo function for [f] using file [cache] as persistent table.
@@ -52,20 +51,17 @@ open Hashtbl
 
 module PHashtable(Key:HashedType) : PHashtable with type key = Key.t  =
 struct
+  open Unix
 
   type key = Key.t
 
   module Table = Hashtbl.Make(Key)
 
-
-
   exception InvalidTableFormat
   exception UnboundTable
 
-
   type mode = Closed | Open
 
-
   type 'a t =
       {
 	outch : out_channel ;
@@ -75,8 +71,9 @@ struct
 
 
 let create i f =
+  let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
   {
-    outch = open_out_bin f ;
+    outch = out_channel_of_descr (openfile f flags 0o666);
     status = Open ;
     htbl = Table.create i
   }
@@ -98,10 +95,20 @@ let read_key_elem inch =
     | End_of_file -> None
     |    _        -> raise InvalidTableFormat
 
+
+let unlock fd = 
+  try 
+    let pos = lseek fd 0 SEEK_CUR in
+    ignore (lseek fd 0 SEEK_SET) ; 
+    lockf fd F_ULOCK 0 ; 
+  ignore (lseek fd pos SEEK_SET)
+  with exc -> failwith (Printexc.to_string exc)
+
 let open_in f =
-  let flags = [Open_rdonly;Open_binary;Open_creat] in
-  let inch = open_in_gen flags 0o666 f in
-  let htbl = Table.create 10 in
+  let flags = [O_RDONLY ; O_CREAT] in
+  let finch = openfile f flags 0o666 in
+  let inch  = in_channel_of_descr finch in
+  let htbl = Table.create 100 in
 
   let rec xload () =
     match read_key_elem inch with
@@ -109,27 +116,38 @@ let open_in f =
       | Some (key,elem) ->
 	  Table.add htbl key elem ;
 	  xload () in
-
     try
-      finally (fun () -> xload () ) (fun () -> close_in inch) ;
+      (* Locking of the (whole) file while reading *)
+      lockf finch F_RLOCK 0 ; 
+      finally 
+	(fun () -> xload () ) 
+	(fun () -> 
+	   unlock finch ;
+	   close_in_noerr inch ; 
+	) ;
       {
-	outch = begin
-	  let flags = [Open_append;Open_binary;Open_creat] in
-	    open_out_gen flags 0o666 f
-	end ;
+	outch = out_channel_of_descr (openfile f [O_WRONLY;O_APPEND;O_CREAT] 0o666) ;
 	status = Open ;
 	htbl = htbl
       }
     with InvalidTableFormat ->
       (* Try to keep as many entries as possible *)
       begin
-	let flags = [Open_wronly; Open_trunc;Open_binary;Open_creat] in
-	let outch = open_out_gen flags 0o666 f in
-	  Table.iter (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
-	  { outch = outch ;
-	    status = Open ;
-	    htbl   = htbl
-	  }
+	let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
+	let out =  (openfile f flags 0o666) in
+	let outch = out_channel_of_descr out in
+	  lockf out F_LOCK 0 ; 
+	  (try 
+	    Table.iter 
+	      (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
+	    flush outch ; 
+	  with  _ -> () )
+	    ;
+	    unlock out ; 
+	    { outch = outch ;
+	      status = Open ;
+	      htbl   = htbl
+	    }
       end
 
 
@@ -147,9 +165,14 @@ let add t k e =
     if status = Closed
     then raise UnboundTable
     else
+      let fd = descr_of_out_channel outch in
       begin
 	Table.add tbl k e ;
-	Marshal.to_channel outch (k,e) [Marshal.No_sharing]
+	lockf fd F_LOCK 0 ;
+	ignore (lseek fd 0 SEEK_END) ; 
+	Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
+	flush outch ;
+	unlock fd
       end
 
 let find t k =
-- 
cgit v1.2.3