provide a persistent cache datastructure

[redianthus]

Hi!

I've been experimenting again with adding a global cache in Owi (because I think measuring hashconsing performances without it makes less sense). I think it would be very nice if Smtml could provide a second cache implementation that would be persistent (immutable). Currently, I have to use the cache like this :

let cache = Smtml.Cache.Strong.create 64

let cache_mutex = Mutex.create ()

let check (S (solver_module, s)) pc =
  let cached =
    Mutex.protect cache_mutex (fun () -> Smtml.Cache.Strong.find_opt cache pc)
  in
  match cached with
  | Some sat -> sat
  | None ->
    let module Solver = (val solver_module) in
    let sat = Solver.check_set s pc in
    Mutex.protect cache_mutex (fun () -> Smtml.Cache.Strong.replace cache pc sat);
    sat

Whereas, using a persistent cache I could 1. use an Atomic.t instead of a Mutex.t 2. avoid the first lock (i.e. when I'm simply reading the cache). I'm not sure it would be better, but that may very well be the case.

[filipeom]

This is very interesting, so if I understand the idea it would look something like:

let cache_ref = Atomic.make Smtml.Cache.Persistent.empty

let check (S (solver_module, s)) pc =
  let cached = Smtml.Cached.Persistent.find_opt (Atomic.get cache_ref) pc in
  match cached with
  | Some sat -> sat
  | None ->
    let module Solver = (val solver_module) in
    let sat = Solver.check_set s pc in
    (* Now you have to update cache_ref *)
    sat

But how would you update the cache_ref? Using Atomic.compare_and_set re? What do you do if compare_and_set returns false? In the case some other thread writes to the cache while the current thread is stuck in the solver?

In any case it would be easy to add an immutable cache to smtml I think 😃

[redianthus]

But how would you update the cache_ref? Using Atomic.compare_and_set re? What do you do if compare_and_set returns false?

Yes, I would do :

let cache_ref = Atomic.make Smtml.Cache.Persistent.empty

let check (S (solver_module, s)) pc =
  let cached = Smtml.Cached.Persistent.find_opt (Atomic.get cache_ref) pc in
  match cached with
  | Some sat -> sat
  | None ->
    let module Solver = (val solver_module) in
    let sat = Solver.check_set s pc in
    Atomic.modify (fun cache -> Smtmt.Cache.Strong.add pc sat cache) cache;
    sat

Atomic.modify is not in stdlib yet, but we have an equivalent in Owi. It uses a loop with compare_and_set. In Owi it is done naïvely, the stdlib version will use a more efficient exponential backoff strategy.

See https://github.com/OCamlPro/owi/pull/887/changes where I first tried to use an Atomic.t and ended up writing an Atomic.modify function that I used to refactor some old code that was using a loop.

In the case some other thread writes to the cache while the current thread is stuck in the solver?

Well... here we'll have called the solver two times, which is unfortunate, but not dramatic. And it'll be exactly as with the mutable cache. We simply have to take care to use replace in the mutable one (add actually replaces the old binding in the immutable one).