synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
authorwenzelm
Mon Dec 03 16:07:28 2012 +0100 (2012-12-03)
changeset 503174d1590544b91
parent 50316 7bdc53fb7282
child 50318 6be9e490d82a
synchronized read access to cache file -- avoid potential conflict with ongoing write (which is non-atomic);
clarified signature -- cache init is unsynchronized and hopefully used at most once per file;
src/HOL/SMT.thy
src/HOL/Tools/SMT/smt_config.ML
src/Tools/cache_io.ML
     1.1 --- a/src/HOL/SMT.thy	Mon Dec 03 15:23:36 2012 +0100
     1.2 +++ b/src/HOL/SMT.thy	Mon Dec 03 16:07:28 2012 +0100
     1.3 @@ -256,6 +256,8 @@
     1.4  The filename should be given as an explicit path.  It is good
     1.5  practice to use the name of the current theory (with ending
     1.6  @{text ".certs"} instead of @{text ".thy"}) as the certificates file.
     1.7 +Certificate files should be used at most once in a certain theory context,
     1.8 +to avoid race conditions with other concurrent accesses.
     1.9  *}
    1.10  
    1.11  declare [[ smt_certificates = "" ]]
     2.1 --- a/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 03 15:23:36 2012 +0100
     2.2 +++ b/src/HOL/Tools/SMT/smt_config.ML	Mon Dec 03 16:07:28 2012 +0100
     2.3 @@ -202,7 +202,7 @@
     2.4    else
     2.5      Path.explode name
     2.6      |> Path.append (Thy_Load.master_directory (Context.theory_of context))
     2.7 -    |> SOME o Cache_IO.make)
     2.8 +    |> SOME o Cache_IO.unsynchronized_init)
     2.9  
    2.10  val certificates_of = Certificates.get o Context.Proof
    2.11  
     3.1 --- a/src/Tools/cache_io.ML	Mon Dec 03 15:23:36 2012 +0100
     3.2 +++ b/src/Tools/cache_io.ML	Mon Dec 03 16:07:28 2012 +0100
     3.3 @@ -16,7 +16,7 @@
     3.4  
     3.5    (*cache*)
     3.6    type cache
     3.7 -  val make: Path.T -> cache
     3.8 +  val unsynchronized_init: Path.T -> cache
     3.9    val cache_path_of: cache -> Path.T
    3.10    val lookup: cache -> string -> result option * string
    3.11    val run_and_cache: cache -> string -> (Path.T -> Path.T -> string) -> string -> result
    3.12 @@ -57,7 +57,7 @@
    3.13  
    3.14  fun cache_path_of (Cache {path, ...}) = path
    3.15  
    3.16 -fun make cache_path =
    3.17 +fun unsynchronized_init cache_path =
    3.18    let
    3.19      val table =
    3.20        if File.exists cache_path then
    3.21 @@ -84,23 +84,22 @@
    3.22        else (1, Symtab.empty)
    3.23    in Cache {path = cache_path, table = Synchronized.var "Cache_IO" table} end
    3.24  
    3.25 -fun load_cached_result cache_path (p, len1, len2) =
    3.26 -  let
    3.27 -    fun load line (i, xsp) =
    3.28 -      if i < p then (i+1, xsp)
    3.29 -      else if i < p + len1 then (i+1, apfst (cons line) xsp)
    3.30 -      else if i < p + len2 then (i+1, apsnd (cons line) xsp)
    3.31 -      else (i, xsp)
    3.32 -    val (out, err) =
    3.33 -      pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
    3.34 -  in {output = err, redirected_output = out, return_code = 0} end
    3.35 -
    3.36  fun lookup (Cache {path = cache_path, table}) str =
    3.37    let val key = SHA1.rep (SHA1.digest str)
    3.38    in
    3.39 -    (case Symtab.lookup (snd (Synchronized.value table)) key of
    3.40 -      NONE => (NONE, key)
    3.41 -    | SOME pos => (SOME (load_cached_result cache_path pos), key))
    3.42 +    Synchronized.change_result table (fn tab =>
    3.43 +      (case Symtab.lookup (snd tab) key of
    3.44 +        NONE => ((NONE, key), tab)
    3.45 +      | SOME (p, len1, len2) =>
    3.46 +          let
    3.47 +            fun load line (i, xsp) =
    3.48 +              if i < p then (i+1, xsp)
    3.49 +              else if i < p + len1 then (i+1, apfst (cons line) xsp)
    3.50 +              else if i < p + len2 then (i+1, apsnd (cons line) xsp)
    3.51 +              else (i, xsp)
    3.52 +            val (out, err) =
    3.53 +              pairself rev (snd (File.fold_lines load cache_path (1, ([], []))))
    3.54 +          in ((SOME {output = err, redirected_output = out, return_code = 0}, key), tab) end))
    3.55    end
    3.56  
    3.57  fun run_and_cache (Cache {path = cache_path, table}) key make_cmd str =