Skip to content

Latest commit

 

History

History
50 lines (32 loc) · 1.42 KB

README.md

File metadata and controls

50 lines (32 loc) · 1.42 KB
Raw

A simple MySQL based benchmarking setup and scripts.

A. Setup:

  1. Install and configure mysql, python, php, apache, mysql+php+apache and gnuplot 4.6 patch 1. (the version is important because we/js containts .js files from the gnuplot install that have to be compatible)

  2. Run mysql -uuser -ppass < benchmarking.sql

  3. Populate table with benchmarks directory (recursive).

    cd scripts

    add-benchmarks.sh $DIRECTORY $LOGIC

  4. Create problem set (see scripts/makeProblemSet.py for details)

  5. Create one line text files in config/{logpath,password,user,host,database} containing path for logs, mysql password and mysql user. ('database' can be empty, in which case mysql which use the default database. 'host' should be 'localhost' if using locally)

  6. Compile runlim

    cd runlim-sigxcpu

    ./configure

    make

B. Add jobs: # cd scripts # ./add-job.sh -b -p -a -t -m -n -d [-c running cvc4 (used for stats)] See example-add-job.sh for an example.

C. Runners # cd scripts # ./runner.py

D. Analyze

  1. Grab statistics in CSV (can be manipulated with R)

    cd scripts

    ./dumpCSV.py [statistics file]

  2. Visualize using the web interface (coming)

E. Misc. Database Management

  1. Reset the mysql queue using ./resetQueue.py

  2. Delete a job using ./deleteJob.py