diff options
Diffstat (limited to 'plugins/micromega/persistent_cache.ml')
-rw-r--r-- | plugins/micromega/persistent_cache.ml | 130 |
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 |