Skip to content

Commit

Permalink
[PA] Tweak simple system caching
Browse files Browse the repository at this point in the history
Working on a correct way of optimizing the program analysis caching
mechanism.
  • Loading branch information
robertzhidealx committed Dec 29, 2023
1 parent 28fddd6 commit 129bf0e
Show file tree
Hide file tree
Showing 9 changed files with 115 additions and 101 deletions.
21 changes: 12 additions & 9 deletions README.md
Original file line number Diff line number Diff line change
Expand Up @@ -25,11 +25,10 @@ Then `dune build` this project.
### utop

`dune utop` to start an interactive environment with all libraries loaded.
Or, `dune utop interpreter`, `dune utop program_analysis`, `dune utop
interpreter/access_links` to run each separately.
Or, `dune utop program_analysis/full`, `dune utop interpreter/src` to run each separately.

```ocaml
open Interpreter;; (* first if only working with program analysis *)
open Interp;; (* first if only working with interpreter *)
open Debugutils;; (* to simplify calling utility functions such as `peu` *)
Expand All @@ -42,20 +41,20 @@ application, etc. on the concrete interpretation result. *)

### Binary

`dune exec interpreter/main.exe` to run the interpreter. Same applies
to `program_analysis/main.exe`.
`dune exec interpreter/src/main.exe` to run the interpreter. Same applies
to `program_analysis/full/main.exe`.

Optionally pass in the `--debug` flag to print debug information from the
evaluation:

```sh
dune exec -- interpreter/main.exe --debug
dune exec -- interpreter/src/main.exe --debug
```

Optionally pass in a file name to run the interpreter on the file:

```sh
dune exec -- interpreter/main.exe <path-to-file> --debug
dune exec -- interpreter/src/main.exe <path-to-file> --debug
```

Same applies to `--simplify`.
Expand All @@ -64,14 +63,18 @@ Same applies to `--simplify`.

`dune test` to run the associated test suite *without* benchmarking.

To also benchmark the DDE interpreter's performance, pass in the `--bench` flag:
To also benchmark the interpreter's performance, pass in the `--bench` flag:

```sh
dune exec -- tests/tests.exe --bench
dune exec -- interpreter/tests/tests.exe --bench
```

`bisect-ppx-report html` or `bisect-ppx-report summary` to view coverage.

> Note that you currently won't be able to run the interpreter tests due to
> an external dependency that's not public. We will soon provide a polished,
> fully executable artifact.
# Formalizations

Please refer to [formal/README.md](./formal/README.md) for details.
2 changes: 1 addition & 1 deletion interpreter/tests/dune
Original file line number Diff line number Diff line change
@@ -1,6 +1,6 @@
(test
(name tests)
(modules tests tests_subst tests_env tests_self tests_al bench utils)
(modules tests tests_subst tests_env tests_self tests_display bench utils)
(libraries
ounit2
core_bench
Expand Down
6 changes: 3 additions & 3 deletions interpreter/tests/tests.ml
Original file line number Diff line number Diff line change
Expand Up @@ -3,10 +3,10 @@ open OUnit2
let tests =
"All tests"
>::: [
(* Tests_subst.dde_subst;
Tests_env.dde_env; *)
Tests_subst.dde_subst;
Tests_env.dde_env;
Tests_self.dde_self;
(* Tests_al.dde_al; *)
Tests_display.dde_display;
]

let () =
Expand Down
Original file line number Diff line number Diff line change
@@ -1,5 +1,5 @@
open OUnit2
open Al_interp
open Dinterp

let peu s =
s |> Core.Fn.flip ( ^ ) ";;" |> Lexing.from_string |> Parser.main Lexer.token
Expand All @@ -19,5 +19,5 @@ let test_recursion _ =
"let fib = fun self -> fun n -> if n <= 1 then n else self self (n - 1) \
+ self self (n - 2) in fib fib 4")

let al_tests = [ "Recursion" >:: test_recursion ]
let dde_al = "DDE against self" >::: al_tests
let display_tests = [ (* "Recursion" >:: test_recursion *) ]
let dde_display = "DDE against self" >::: display_tests
8 changes: 4 additions & 4 deletions interpreter/tests/tests_self.ml
Original file line number Diff line number Diff line change
Expand Up @@ -78,11 +78,11 @@ let test_misc _ =

let dde_self_tests =
[
"Memoization" >:: test_memoization;
(* "Memoization" >:: test_memoization; *)
(* "Record rec" >:: test_record_rec; *)
(* "Laziness" >:: test_laziness; *)
(* "Record operations" >:: test_record;
"letassert" >:: test_letassert; *)
"Laziness" >:: test_laziness;
"Record operations" >:: test_record;
"letassert" >:: test_letassert;
(* "Misc." >:: test_misc; *)
]

Expand Down
4 changes: 2 additions & 2 deletions program_analysis/full/main.ml
Original file line number Diff line number Diff line change
Expand Up @@ -19,8 +19,8 @@ let toplevel_loop =
in
let safe_analyze_and_print ast =
try
let r = Lib.analyze ast ~debug_mode:false in
Format.printf "==> %a\n" Utils.pp_res r
let r = Lib.analyze ast in
Format.printf "==> %a\n" Grammar.Res.pp r
with ex -> print_exception ex
in
while true do
Expand Down
42 changes: 23 additions & 19 deletions program_analysis/simple/lib.ml
Original file line number Diff line number Diff line change
Expand Up @@ -92,9 +92,9 @@ let cache key data =
let%bind { c; _ } = get () in
let%bind () = set_cache (Map.add_exn (Map.remove c key) ~key ~data) in
let expr, _, _, _ = key in
(match Map.find c key with
| Some r -> debug (fun m -> m "[Cache] Found: %a" Res.pp r)
| None -> debug (fun m -> m "[Cache] Not found"));
(* (match Map.find c key with
| Some r -> debug (fun m -> m "[Cache] Found: %a" Res.pp r)
| None -> debug (fun m -> m "[Cache] Not found")); *)
debug (fun m -> m "[Cache] Add: %a -> %a" Interp.Pp.pp_expr expr Res.pp data);
return data

Expand All @@ -109,10 +109,14 @@ let rec analyze_aux ?(caching = true) d expr sigma : Res.t T.t =
let%bind vid = get_vid v in
let%bind sid = get_sid s in
let%bind () = inc_freq (expr, sigma, vid, sid) in
let cache_key = (expr, sigma, vid, sid) in
(* let cache_key = (expr, sigma, vid, sid) in *)
(* let cache_key = (expr, sigma, v, s) in *)
let cache_key = (expr, sigma, v, sid) in
(* debug (fun m -> m "V: %a" V.pp v); *)
match Map.find c cache_key with
| Some r
when not (exists_lone_stub r)
when caching
(* when not (exists_lone_stub r) *)
(* when caching && ((not rerun) || iter = 2) *) ->
debug (fun m -> m "Cache hit: %a -> %a" Interp.Pp.pp_expr expr Res.pp r);
return r
Expand Down Expand Up @@ -166,7 +170,7 @@ let rec analyze_aux ?(caching = true) d expr sigma : Res.t T.t =
Interp.Pp.pp_expr e1);
let%bind rs = acc in
let%bind r0 =
local
local d
(fun ({ v; _ } as env) ->
{ env with v = Set.add v v_new })
(analyze_aux ~caching d e1 pruned_sigma')
Expand Down Expand Up @@ -226,7 +230,7 @@ let rec analyze_aux ?(caching = true) d expr sigma : Res.t T.t =
(* stitch the stack to gain more precision *)
let%bind rs = acc in
let%bind r0 =
local
local d
(fun ({ v; _ } as env) ->
{ env with v = Set.add v est })
(analyze_aux ~caching d e2 suf)
Expand Down Expand Up @@ -291,7 +295,7 @@ let rec analyze_aux ?(caching = true) d expr sigma : Res.t T.t =
d Interp.Pp.pp_expr e1 Sigma.pp suf);
let%bind rs = acc in
let%bind r0 =
local
local d
(fun ({ v; rerun; iter; _ } as env) ->
{
env with
Expand All @@ -306,14 +310,14 @@ let rec analyze_aux ?(caching = true) d expr sigma : Res.t T.t =
return (Set.union rs r0))
in
let r1 = simplify r1 in
let%bind { c; _ } = get () in
let c =
List.fold sufs ~init:c ~f:(fun acc suf ->
let cache_key = (e1, suf, vid, sid) in
Map.add_exn (Map.remove acc cache_key)
~key:cache_key ~data:r1)
in
let%bind () = set_cache c in
(* let%bind { c; _ } = get () in
let c =
List.fold sufs ~init:c ~f:(fun acc suf ->
let cache_key = (e1, suf, vid, sid) in
Map.add_exn (Map.remove acc cache_key)
~key:cache_key ~data:r1)
in
let%bind () = set_cache c in *)
debug (fun m -> m "r1 length: %d" (Set.length r1));
debug (fun m ->
m
Expand All @@ -340,7 +344,7 @@ let rec analyze_aux ?(caching = true) d expr sigma : Res.t T.t =
x l1);
let%bind rs = acc in
let%bind r0' =
local
local d
(fun ({ v; _ } as env) ->
{ env with v = Set.add v est })
(analyze_aux ~caching d
Expand Down Expand Up @@ -464,15 +468,15 @@ let analyze ?(caching = true) e =
analyze_aux ~caching 0 e []
{
v = empty_v;
vids = Map.singleton (module V) empty_v "V0";
vids = Map.singleton (module V) empty_v 0;
cnt = 1;
rerun = false;
iter = 0;
}
{
c = Map.empty (module Cache_key);
s = empty_s;
sids = Map.singleton (module S) empty_s "S0";
sids = Map.singleton (module S) empty_s 0;
cnt = 1;
freqs = Map.empty (module Freq_key);
}
Expand Down
68 changes: 42 additions & 26 deletions program_analysis/simple/utils.ml
Original file line number Diff line number Diff line change
Expand Up @@ -6,7 +6,7 @@ let ff = Format.fprintf

module Sigma = struct
module T = struct
type t = sigma [@@deriving compare, sexp, show { with_path = false }, hash]
type t = sigma [@@deriving compare, sexp, show { with_path = false }]
end

include T
Expand All @@ -16,13 +16,13 @@ end
module St = struct
module T = struct
type lstate = int * sigma
[@@deriving compare, sexp, hash, show { with_path = false }]
[@@deriving compare, sexp, show { with_path = false }]

type estate = expr * sigma
[@@deriving compare, sexp, hash, show { with_path = false }]
[@@deriving compare, sexp, show { with_path = false }]

type t = Lstate of lstate | Estate of estate
[@@deriving compare, sexp, hash, show { with_path = false }]
[@@deriving compare, sexp, show { with_path = false }]
end

include T
Expand All @@ -31,24 +31,23 @@ end

module V_key = struct
module T = struct
type lstate = int * sigma * string [@@deriving compare, sexp, hash]
type lstate = int * sigma * int [@@deriving compare, sexp]

let pp_lstate fmt (l, sigma, s) =
Format.fprintf fmt "(%d, %a, %s)" l Sigma.pp sigma s
let pp_lstate fmt (l, sigma, sid) =
Format.fprintf fmt "(%d, %a, %d)" l Sigma.pp sigma sid

let show_lstate (l, sigma, s) =
Format.sprintf "(%d, %s, %s)" l (Sigma.show sigma) s
let show_lstate (l, sigma, sid) =
Format.sprintf "(%d, %s, %d)" l (Sigma.show sigma) sid

type estate = expr * sigma * string [@@deriving compare, sexp, hash]
type estate = expr * sigma * int [@@deriving compare, sexp]

let pp_estate fmt (e, sigma, s) =
Format.fprintf fmt "(%a, %a, %s)" Interp.Ast.pp_expr e Sigma.pp sigma s
let pp_estate fmt (e, sigma, sid) =
Format.fprintf fmt "(%a, %a, %d)" Interp.Ast.pp_expr e Sigma.pp sigma sid

let show_estate (e, sigma, s) =
Format.asprintf "(%a, %s, %s)" Interp.Ast.pp_expr e (Sigma.show sigma) s
let show_estate (e, sigma, sid) =
Format.asprintf "(%a, %s, %d)" Interp.Ast.pp_expr e (Sigma.show sigma) sid

type t = Lstate of lstate | Estate of estate
[@@deriving compare, sexp, hash]
type t = Lstate of lstate | Estate of estate [@@deriving compare, sexp]

let pp fmt (k : t) =
match k with
Expand All @@ -65,7 +64,11 @@ end

module Cache_key = struct
module T = struct
type t = expr * sigma * string * string [@@deriving compare, sexp, hash]
(* type t = expr * sigma * int * int [@@deriving compare, sexp] *)
(* type t = expr * sigma * Set.M(V_key).t * Set.M(Sigma).t
[@@deriving compare, sexp] *)
(* type t = expr * sigma * int * Set.M(Sigma).t [@@deriving compare, sexp] *)
type t = expr * sigma * Set.M(V_key).t * int [@@deriving compare, sexp]
end

include T
Expand All @@ -87,6 +90,8 @@ module V = struct

include T
include Comparable.Make (T)

(* let compare = Set.compare_direct *)
end

module S = struct
Expand All @@ -104,11 +109,13 @@ module S = struct

include T
include Comparable.Make (T)

(* let compare = Set.compare_direct *)
end

module Freq_key = struct
module T = struct
type t = expr * sigma * string * string [@@deriving compare, sexp]
type t = expr * sigma * int * int [@@deriving compare, sexp]
end

include T
Expand Down Expand Up @@ -210,8 +217,8 @@ let single_res = Set.singleton (module Res_key)
module ReaderState = struct
module T = struct
type cache = Res.t Map.M(Cache_key).t
type vids = string Map.M(V).t
type sids = string Map.M(S).t
type vids = int Map.M(V).t
type sids = int Map.M(S).t
type freqs = int64 Map.M(Freq_key).t
type env = { v : V.t; vids : vids; cnt : int; rerun : bool; iter : int }
type state = { s : S.t; c : cache; freqs : freqs; sids : sids; cnt : int }
Expand All @@ -227,26 +234,35 @@ module ReaderState = struct
let map = `Define_using_bind
let ask () : env t = fun env st -> (env, st)

let local (f : env -> env) (m : 'a t) : 'a t =
let local d (f : env -> env) (m : 'a t) : 'a t =
fun env st ->
let ({ v; vids; cnt; _ } as env') = f env in
debug (fun m ->
m "[Level %d] VIDs: %s" d
(vids |> Map.to_alist |> List.unzip |> snd
|> List.sort ~compare:Int.compare
|> List.to_string ~f:string_of_int));
let vids', cnt' =
if Map.mem vids v then (vids, cnt)
else (Map.add_exn vids ~key:v ~data:(Format.sprintf "V%d" cnt), cnt + 1)
if Map.mem vids v then (
debug (fun m -> m "[Level %d] No new VID" d);
(vids, cnt))
else (
debug (fun m -> m "[Level %d] New VID: %d" d cnt);
(Map.add_exn vids ~key:v ~data:cnt, cnt + 1))
in
m { env' with vids = vids'; cnt = cnt' } st

let get () : state t = fun _ st -> (st, st)
let get_vid v : string t = fun { vids; _ } st -> (Map.find_exn vids v, st)
let get_vid v : int t = fun { vids; _ } st -> (Map.find_exn vids v, st)

let get_sid s : string t =
let get_sid s : int t =
fun _ ({ sids; _ } as st) -> (Map.find_exn sids s, st)

let set_s s : unit t =
fun _ ({ sids; cnt; _ } as st) ->
let sids', cnt' =
if Map.mem sids s then (sids, cnt)
else (Map.add_exn sids ~key:s ~data:(Format.sprintf "S%d" cnt), cnt + 1)
else (Map.add_exn sids ~key:s ~data:cnt, cnt + 1)
in
((), { st with s; sids = sids'; cnt = cnt' })

Expand Down
Loading

0 comments on commit 129bf0e

Please sign in to comment.