Artifact for "Handling Exceptions and Effects with Automatic Resource Analysis"

Artifact for "Handling Exceptions and Effects with Automatic Resource Analysis" This artifact contains 2 tools described in the paper: RaML and RaML+ with Effects, henceforth also called RaML 2. RaML is an existing tool from a previous paper, so this artifact only contains the compiled executable for RaML. RaML 2 is the tool that implements the type system developed in this paper, so this artifact contains its source code as well as a Dockerfile that can build the executable. The artifact also contains the 21 benchmarks on which we evaluate RaML and RaML 2. Building the Artifact We provide a Dockerfile that builds the RaML 2 source code into an executable. To build the Docker image, make sure you are in the topmost directory of the artifact and run the following command: docker build -t raml-effects-docker . Alternatively, go to the RaML 2 specific README for instructions on how to manually build it from source. Those instructions should also be helpful for anyone interested in interfacing with RaML 2. Once the docker image is built, enter it via the following command: docker run -it raml-effects-docker This should put you in the directory /home/opam, with 2 subdirectories raml1 and raml2 that respectively contain files for RaML and RaML+ with Effects. RaML vs RaML 2 Benchmarks RaML uses OCaml for its frontend syntax, while RaML 2 uses Standard ML (SML) for its frontend syntax. Therefore, the benchmarks are at two separate locations: The 6 benchmarks involving exceptions which RaML can analyze are located at raml1/tests/sml/exceptions. The 21 benchmarks which RaML 2 can analyze are located at raml2/tests/sml. Of these, the 12 benchmarks involving exceptions in the exceptions subdirectory, and the 9 benchmarks involving effects are in the effects subdirectory. The 6 benchmarks sqdist, distances_1, zip', map2', eval_exp', and sort' can be analyzed by both RaML and RaML 2. But since we do not have a transpiler between SML and OCaml, this artifact actually contains two instances of each of these benchmarks, once in SML and once in OCaml. Furthermore, while the OCaml benchmarks for RaML contain Raml.tick expressions which have been strategically inserted to count the number of function applications, the SML benchmarks for RaML mostly do not have Raml.tick expressions. This is because RaML 2 supports the command line flag -capps to automatically incur a cost of 1 for each function call, which we take advantage of, whereas RaML does not have this feature. Running the RaML Benchmarks Run cd raml1 to enter raml1/. The RaML executable is located at bin/raml. The 6 benchmarks that RaML is capable of analyzing are spread across 3 files in tests/exceptions. To verify the results from our paper, run the following commands to analyze the benchmarks with RaML: # sqdist, distances_1 bin/raml analyze ticks 2 -m tests/exceptions/exceptions.ml # zip', map2', eval_exp' bin/raml analyze ticks 1 -m tests/exceptions/exceptions3.ml # sort' bin/raml analyze ticks 2 -m tests/exceptions/sort.ml Each command has a comment above it listing the benchmarks within the given .ml file. Using the given commands, RaML should analyze each toplevel function within the given file and report its bounds. For example, the first command should contain the following report for sqdist. ... ==== Analyzing function sqdist ... Trying degree: 2 == sqdist : float list * float list -> float Non-zero annotations of the argument: 1 874 derived bound -> x2 x2 : the length(s) of the list(s) within component 0 of the tuple, which is the argument ... The report should be largely self-explanatory; here RaML has determined that sqdist (l1, l2) performs at most ∣l1∣+1|l_1| + 1∣l1∣+1 ticks. It also reports analyzing sqdist took 0.004939 seconds, and caused 874 linear programming constraints to be generated. Note that unlike RaML, RaML 2 uses 0-indexing when discussing components of a tuple. Furthermore, we apologize that the printed bounds for RaML 2 are somewhat harder to read than those of RaML 1 -- this tool is still being actively developed, and most of the effort has not been directed toward the UI. Expected Bounds Here are the expected bounds that RaML and RaML 2 should report for all the benchmarks. Exception Benchmarks Benchmark RaML Bound RaML 2 Bound sqdist(v1, v2) $\|v_2\|$ $\|v_1\|$ distances_1(vs, p) $1 + 3 \|vs\| + \sum_i \|vs_i\|$ $1 + 3 \|vs\| + \sum_i \|vs_i\|$ distances_2(vs, p) -- $1 + 3 \|vs\| + \sum_i \|vs_i\|$ nearest(vs, p) -- $1 + 3 \|vs\| + \sum_i \|vs_i\|$ zip(l1, l2) -- $1 + 2\|l_1\|$ map2(f, l1, l2) -- $1 + 4 \|l_2\|$ eval_exp(e) -- $1 + 2c + 2p + t$ sort(l) -- $\|l\| + \binom{\|l\|}{2}$ zip'(l1, l2) $\|l_1\|$ $\|l_1\|$ map2'(f, l1, l2) $2 \|l_1\|$ $2 \|l_1\|$ eval_exp'(e) $2t + 2p$ $c + p + t$ sort'(l) $\binom{\|l\|}{2}$ $\binom{\|l\|}{2}$ Effect Benchmarks Benchmark RaML 2 Bound simple_IO(()) $11$ store_lists(vs) $6 + 9 \|vs\| + \sum_i\|vs_i\|$ store_lists_q_naive(vs) LP Infeasible store_lists_q(vs) $8 + 13 \|vs\| + \sum_i\|vs_i\|$ store_suffix_lists(vs) $14 + 10 \|vs\| + \binom{\|vs\|}{2}$ generator_to_list(n) $1 + 3\|n\|$ generator_to_list_2(n) $1 + 5\|n\| + \binom{\|n\|}{2}$ generator_counter(n) $3 + 11\|n\| + \binom{\|n\|}{2}$ prefix_sum_list(ns) $2 + 12 \|ns\| + \sum_i \|ns_i\|$