From 071c1f56aae3c91cfe71c06c2e9fd39d8279ce3b Mon Sep 17 00:00:00 2001 From: Shachar Itzhaky Date: Sun, 11 Apr 2021 21:00:18 +0300 Subject: [PATCH] [doc] Updated README (benchmark cleanup). --- README.md | 31 +++++-------------------------- 1 file changed, 5 insertions(+), 26 deletions(-) diff --git a/README.md b/README.md index 365827e7d..a76b7ca2c 100644 --- a/README.md +++ b/README.md @@ -32,8 +32,8 @@ Running src/test/resources/synthesis/cyclic-benchmarks/rose-tree/free.syn 1.7s These instructions detail how to: -1. Reproduce the results reported in Sec 5, Table 1 (evaluating Cypress on benchmarks with _complex recursion_) -2. Reproduce the results reported in Appendix C, Table 1 (evaluating Cypress on benchmarks with _simple recursion_) +1. Reproduce the results reported in Table 1 (evaluating Cypress on benchmarks with _complex recursion_) +2. Reproduce the results reported in Table 2 (evaluating Cypress on benchmarks with _simple recursion_) 3. Run Cypress on individual synthesis problems 4. Rebuild Cypress from sources inside the VM @@ -56,7 +56,7 @@ To reproduce the results on _complex benchmarks_ (as defined in Sec 5), execute: cd ~/suslik python2 evaluation.py ``` -This will run Cypress on all benchmarks from Sec 5, Table 1, apart from benchmark 5 `intersection`, which is reported there as failing (see more details below). +This will run Cypress on all benchmarks from Table 1, except for benchmark 5 `intersection`, which takes over a minute and is therefore included in the long-running benchmarks (see below). This should take approximately *five minutes*. After the script terminates, it will create two output files in `~/suslik`: @@ -80,11 +80,11 @@ To reproduce the results on _simple benchmarks_, execute: cd ~/suslik python2 evaluation.py --simple ``` -This will run Cypress on all benchmarks from Appendix C, Table 1, apart from the really long running benchmark `BST: delete root` (see more details below). +This will run Cypress on all benchmarks from Table 2, apart from the really long running benchmark `BST: delete root` (see more details below). This should take approximately *five minutes*. After the script terminates, it will create two output files in `~/suslik`: -- `simple.csv` contains Cypress results reported in Appendix C, Table 1 (For SusLik results, see the [suslik paper](https://cseweb.ucsd.edu/~npolikarpova/publications/suslik.pdf)) +- `simple.csv` contains Cypress results reported in Table 2 (For SusLik results, see the [suslik paper](https://cseweb.ucsd.edu/~npolikarpova/publications/suslik.pdf)) - `all_resutls` contains the synthesized programs To inspect the results in a table form, you can execute: @@ -133,27 +133,6 @@ because these are the only benchmarks that take over a minute to run natively (s In particular, `intersection` takes 4 min, and `BST: delete root` takes ~45 mins to finish on the VM. -The benchmark `intersection` needs a clarification, which we have made to reviewers during the rebuttal. -Originally, we have a tried the following _destructive_ specification for this benchmark: -``` -{ r :-> x ** ulist(x, s1) ** ulist(y, s2) } -void intersect (loc r, loc y) -{ r :-> z ** ulist(z, s1 * s2) } -``` -This version of the benchmark fails, as reported in the submitted version of the paper -because of the limitation on the class of auxiliaries that Cypress can generate. -However, after the submission we realized that Cypress can actually handle the following version of this benchmark, -where one of the original lists is preserved by the procedure: -``` -{ r :-> x ** ulist(x, s1) ** ulist(y, s2) } -void intersect (loc r, loc y) -{ r :-> z ** ulist(z, s1 * s2) ** ulist(y, s2) } -``` -This version allows Cypress to first recurse on the tail of `x`, -and then check whether the head of `x` is present in `y` and hence whether it should be included in the intersection. -This is the version of `intersect` included in the artifact (and this is the version we intend to present in the camera-ready); -it can be synthesized in two minutes on native hardware (and in four minutes on the VM) - ### Running on Individual Benchmarks To run Cypress on `file.syn`, you can execute `suslik file.syn` from `~/suslik`.