@@ -10,15 +10,117 @@ The generator utilizes integer programming to find an optimal combination
of slice length + strategy. The generated problems are not too difficult
and can be solved on a laptop with open source integer programming tools.
## Documentation
## Overview
Unfortunately, the project currently lacks documentation.
The `schedgen` toolbox is a standard Python package. It has been tested with Python 3.10. To install the package it is enough to execute
On NixOS one can use the `shell.nix` file to bring the
dependencies into context. On other systems Python3, Pandas, and
[PuLP](https://coin-or.github.io/pulp/) is needed.
```bash
$ python setup.py install
```
On NixOS one can use the `shell.nix` file to bring the dependencies into context. On other systems Python3, Pandas, and [PuLP](https://coin-or.github.io/pulp/) is needed.
This will install the following tools that are part of the `schedgen` toolbox on the user systems.
*`schedgen-optimize.py` is the main tool that performs the schedule generation. It takes the name of a folder that contains the experiments, a list of time slices, and the total timeout. After the generation is finished the result is written as a schedule into a CSV file. It is also possible to provide an existing scheduler to build a joint schedule. The benchmarks used to generate the schedule can be filtered as described above.
*`schedgen-finalize.py` takes CSV files describing schedules, as generated by `schedgen-optimize.py`, and produces a shell script that runs a solver according to the schedules. The user can provide a template for the script and change various parameters used during generation. The default script can pick schedules by {\smtlib} logic.
*`schedgen-simulate.py` can be used to predict the outcome of running a scheduler. To do so the user has to provide experiments for the strategies included in the schedule, but can use different benchmarks. Furthermore, it is possible to add noise to the simulation.
*`schedgen-query.py` is a small tool that produces lists of benchmarks for debugging and analysis purposes. For example, it can list the union of the benchmarks solved by some strategies, or find the benchmarks from this list that a specific schedule cannot solve.
*`schedgen-visualize.py` can be used to visualize one or multiple schedules. It generates a bar plot that represents a schedule visually.
Each of those tools can generate an extensive documentation of the options it exposes via the standard `--help` option.
## A verit-schedgen Tutorial
This section shows how the `schedgen` toolbox can be used. We will build and explore an optimal schedule for some hand-crafted, artificialexample benchmark data. This data can be found in the file `contrib/example_data.csv`. The first strategy `base-strategy}`solves 20 benchmarks within one second. The five other strategies `extra01` to `extra05` solve up to five benchmarks exclusively such that `extra01` solves five benchmarks not solved by any other strategy, `extra02` solves four, and so on. There is one benchmark `unsolved.smt2` that is not solved by any strategy and a strategy `bad-strategy` that solves only one benchmark in 1.5 seconds. Hence, if the total timeout is six seconds we expect the optimal schedule to run the strategies in the order just presented for one second each. The solving times have been sampled from a normal distribution to ensure the resulting graphs look interesting.
Since the example data is in the CSV format described above the first four lines of `base-strategy` are:
```
benchmark;logic;strategy;solved;time
base01.smt2;UF;base-strategy;yes;0.5189
base02.smt2;UF;base-strategy;yes;0.2164
base03.smt2;UF;base-strategy;yes;0.1754
...
```
The first step is to generate a schedule. To do so we invokethe `schedgen-optimize.py` command:
The option `-l UF` selects the UF logic, the option `-s 0.9 1.0 1.1` defines the time slices, and `-t 6` sets the total timeout. Hence, every picked strategy can run for either 0.9, 1, or 1.1 second. Overall, the schedule is not allowed to use more than 6s. Finally, `-c` tells the tool to use the CSV parser, and the option `-d` gives the data location.
The tool then searches the optimal schedule and writes the result to `contrib/example_schedule.csv`.
The first four lines of the schedule are:
```
time;strategy
1.100;base-strategy
1.000;extra01
0.900;extra02
...
```
The first column indicates how long the strategy in the second column should be used. As enforced by the synthetic data, the generated schedule uses the strategies in the order outlined above.
Furthermore, the output by the tool predicts how well the schedule will perform. It prints the number of benchmarks solved in the given timeout and the sum of the time needed to solve those benchmarks.
```
['UF']: This schedule solves 35/37 benchmarks.
Time needed: 52.19s.
```
Two benchmarks are not solved by this strategy: the benchmark only solved by the `bad` strategy and the benchmark not solved by any strategy. Furthermore, we learn that solving all benchmarks solved by this schedule will take 52.19 seconds. The output also tells us the solving time before order optimization, but in this case nothing changes.
The simulator can give us a better prediction of the schedule performance, but let us first visualize the schedule:
```
$ schedgen-visualize.py -t 6 -p out.pgf \
contrib/example_schedule.csv
```
\in{Figure}[fig:sched-vis] shows the result of this command. The `-t` option works as before and defines the overall timeout. The options `-c -p out.pgf` tells the visualizer to generate a TikZ picture. If this option is omitted, the tool instead opens a window that shows the schedules. Finally, the tool expects a list of pre-schedules to visualize.
Since the different strategies are all used for roughly the same timeout, every strategy is shown as a block of similar size. Because some strategies are used for less than one second, there is a small gap of 0.1 seconds at the end. By default the visualizer simply assigns a number to each strategy when it is used the first time. Strategies often correspond to command line options and those can be long. A number ensures that there are no printing problems, but makes it possible to compare different schedules based on the same strategies.
It is possible to customize the names used for some strategies and to highlight them. This is done with the help of a *shorthand* file: a CSV file with three columns. As in all other CSV files, the fields are separated by a semicolon and there must be a header line. The `strategy` column lists the full strategy string, the `shorthand` column gives the name that should be printed, and the `highlight` can be set to `true` to indicate that the strategy should be highlighted (`false` otherwise). Strategies not listed in the shorthand files get assigned a number and stay unhighlighted. In \in{Figure}[fig:sched-vis] the base strategy and the second additional strategy are highlighted and every strategy has a custom shorthand name. The command to produce this figure is:
```bash
$ schedgen-visualize.py -t 6 -c-p out.pgf \
-a contrib/example_shorthand.csv \
contrib/example_schedule.csv
```
Let us now simulate the generated schedule. To do so we can use the simulation tool:
```
$ schedgen-simulate.py -l UF -t 6 \
-c -d contrib/example_data.csv \
--mu 0.05 --sigma 0.01 --seed 1 \
contrib/example_schedule.csv simulation_1.txt
```
The options `-l`, `-t`, `-c`, and `-d` are as for the other tools. The tool expects two positional arguments.First, the schedule to simulate and; second, the file to write the results to. The output is always using the GridTPT format, independent of the input format. The remaining options are `--mu`, `--sigma`, and `--seed`. Those control the random jitter that is applied to each solving time in the input dataset. The jitter is sampled from a normal distribution. The options `--mu` and `--sigma` control the mean and the standard deviation, respectively. To ensure simulations can be repeated it is possible to fix an integer seed for the random number generator with the option `--seed`. In this case we choose a slight jitter.
The cumulative density functions generated by the simulation are shown in the figure above. As expected, the graph for the simulation with slight jitter follows almost exactly the base strategy for the first second. The plot also shows the result of using more jitter ($μ = 0.2$, $σ = 0.05$). In this case two benchmarks are no longer solved. The script used to generate these graphs is the script `contrib/cdf.py` in the repository.
If we want to have a list of the benchmarks not solved by the schedule, we can use the `schedgen-query` tool:
The option `-q unsolved` asks the tool to print the list of all benchmarks not solved. An alternative is `-q compare` that shows benchmarks not solved by any strategy. To see the benchmarks that are solved by any strategy together with the minimal solving time, the `-q best` option can be used. Finally, `-q schedule` lists all benchmarks solved by the given schedule together with the predicted solving time (without jitter).
The main script is `schedgen-optimize.py` in the folder `schedgen`.
Running this command with `--help` produces an overview of the available
options. For some pointers on how to use everything, take a look at the
