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 f7b62e4
Show file tree
Hide file tree
Showing 9 changed files with 121 additions and 106 deletions.
32 changes: 18 additions & 14 deletions README.md
Original file line number Diff line number Diff line change
@@ -1,16 +1,16 @@
# Essence of Demand-Driven Execution (DDE)
# Pure Demand Operational Semantics

[![Build & test
project](https://github.com/JHU-PL-Lab/dde/actions/workflows/build.yml/badge.svg)](https://github.com/JHU-PL-Lab/dde/actions/workflows/build.yml)

This repo contains a [concrete](./interpreter) and an
[abstract](./program_analysis) interpreter based on DDE, as well as
This repo contains pure demand [concrete](./interpreter) and
[abstract](./program_analysis) interpreters, as well as
[formalizations](./formal) in Coq.

## Set up

Before building the project, install `fbdk` locally so that it is visible to
this project:
Before building the project (the concrete interpreter part), install `fbdk`
locally so that it is visible to this project:

```sh
cd PATH_TO_FbDK_REPO
Expand All @@ -20,16 +20,20 @@ opam install .

Then `dune build` this project.

> Note that you currently won't be able to run the interpreter tests if you
> don't have access to `fbdk`. We will soon provide a polished, fully
> executable artifact. For now, please build the program analysis separately
> via `dune build program_analysis`.
## Develop

### 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 +46,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,10 +68,10 @@ 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.
Expand Down
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
Loading

0 comments on commit f7b62e4

Please sign in to comment.