1 files changed, 74 insertions, 56 deletions

diff --git a/plugins/micromega/persistent_cache.ml b/plugins/micromega/persistent_cache.ml
index 2465617a..2dc0d003 100644
--- a/plugins/micromega/persistent_cache.ml
+++ b/plugins/micromega/persistent_cache.ml
@@ -1,6 +1,6 @@
 (************************************************************************)
 (*  v      *   The Coq Proof Assistant  /  The Coq Development Team     *)
-(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2014     *)
+(* <O___,, *   INRIA - CNRS - LIX - LRI - PPS - Copyright 1999-2015     *)
 (*   \VV/  **************************************************************)
 (*    //   *      This file is distributed under the terms of the       *)
 (*         *       GNU Lesser General Public License Version 2.1        *)
@@ -8,11 +8,10 @@
 (*                                                                      *)
 (*  A persistent hashtable                                              *)
 (*                                                                      *)
-(*  Frédéric Besson (Inria Rennes) 2009-2011                            *)
+(*  Frédéric Besson (Inria Rennes) 2009-2014                            *)
 (*                                                                      *)
 (************************************************************************)
 
-
 module type PHashtable =
   sig
     type 'a t
@@ -84,7 +83,7 @@ let finally f rst =
       rst () ; res
   with reraise ->
     (try rst ()
-    with any  -> raise reraise
+    with any -> raise reraise
     ); raise reraise
 
 
@@ -93,26 +92,52 @@ let read_key_elem inch =
     Some (Marshal.from_channel inch)
   with
     | End_of_file -> None
-    | e when e <> Sys.Break -> raise InvalidTableFormat
-
-(** In win32, it seems that we should unlock the exact zone
-    that has been locked, and not the whole file *)
+    | e when Errors.noncritical e -> raise InvalidTableFormat
+
+(** 
+    We used to only lock/unlock regions.
+    Is-it more robust/portable to lock/unlock a fixed region e.g. [0;1]?  
+    In case of locking failure, the cache is not used.
+**)
+
+type lock_kind = Read | Write
+
+let lock kd fd = 
+ let pos = lseek fd 0 SEEK_CUR in 
+ let success   = 
+  try 
+   ignore (lseek fd 0 SEEK_SET);
+   let lk =  match kd with 
+    | Read  -> F_RLOCK 
+    | Write -> F_LOCK in  
+   lockf fd lk 1; true
+  with Unix.Unix_error(_,_,_) -> false in
+ ignore (lseek fd pos SEEK_SET) ; 
+ success
+
+let unlock fd = 
+  let pos = lseek fd 0 SEEK_CUR in
+  try 
+   ignore (lseek fd 0 SEEK_SET) ; 
+   lockf fd F_ULOCK 1
+  with 
+   Unix.Unix_error(_,_,_) -> ()    
+    (* Here, this is really bad news -- 
+       there is a pending lock which could cause a deadlock.
+       Should it be an anomaly or produce a warning ?
+    *);
+  ignore (lseek fd pos SEEK_SET) 
 
-let locked_start = ref 0
 
-let lock fd =
-  locked_start := lseek fd 0 SEEK_CUR;
-  lockf fd F_LOCK 0
+(* We make the assumption that an acquired lock can always be released *)
 
-let rlock fd =
-  locked_start := lseek fd 0 SEEK_CUR;
-  lockf fd F_RLOCK 0
+let do_under_lock kd fd f = 
+ if lock kd fd
+ then
+  finally f (fun () -> unlock fd)
+ else f ()
+  
 
-let unlock fd =
-  let pos = lseek fd 0 SEEK_CUR in
-  ignore (lseek fd !locked_start SEEK_SET);
-  lockf fd F_ULOCK 0;
-  ignore (lseek fd pos SEEK_SET)
 
 let open_in f =
   let flags = [O_RDONLY ; O_CREAT] in
@@ -128,37 +153,30 @@ let open_in f =
 	  xload () in
     try
       (* Locking of the (whole) file while reading *)
-      rlock finch;
-      finally 
-	(fun () -> xload () ) 
-	(fun () -> 
-	   unlock finch ;
-	   close_in_noerr inch ; 
-	) ;
+      do_under_lock Read finch xload ; 
+      close_in_noerr inch ; 
       {
-	outch = out_channel_of_descr (openfile f [O_WRONLY;O_APPEND;O_CREAT] 0o666) ;
-	status = Open ;
-	htbl = htbl
+       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 = [O_WRONLY; O_TRUNC;O_CREAT] in
-	let out =  (openfile f flags 0o666) in
-	let outch = out_channel_of_descr out in
-	  lock out;
-	  (try 
-	    Table.iter 
-	      (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
-	    flush outch ; 
-	  with e when e <> Sys.Break -> () )
-	    ;
-	    unlock out ; 
-	    { outch = outch ;
-	      status = Open ;
-	      htbl   = htbl
-	    }
-      end
+     (* The file is corrupted *)
+     begin
+      close_in_noerr inch ;
+      let flags = [O_WRONLY; O_TRUNC;O_CREAT] in
+      let out =  (openfile f flags 0o666) in
+      let outch = out_channel_of_descr out in
+      do_under_lock Write out 
+       (fun () -> 
+	Table.iter 
+	  (fun k e -> Marshal.to_channel outch (k,e) [Marshal.No_sharing]) htbl;
+        flush outch) ; 
+      { outch = outch ;
+        status = Open ;
+        htbl   = htbl
+      }
+     end
 
 
 let close t =
@@ -172,22 +190,22 @@ let close t =
 
 let add t k e =
   let {outch = outch ; status = status ; htbl = tbl} = t in
-    if status = Closed
+    if status == Closed
     then raise UnboundTable
     else
       let fd = descr_of_out_channel outch in
       begin
-	Table.add tbl k e ;
-	lock fd;
-	ignore (lseek fd 0 SEEK_END);
-	Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
-	flush outch ;
-	unlock fd
+       Table.add tbl k e ;
+       do_under_lock Write fd 
+        (fun _ -> 
+         Marshal.to_channel outch (k,e) [Marshal.No_sharing] ;
+         flush outch
+        )
       end
 
 let find t k =
   let {outch = outch ; status = status ; htbl = tbl} = t in
-    if status = Closed
+    if status == Closed
     then raise UnboundTable
     else
       let res = Table.find tbl k in