This post documents, how Sbuilder Benchmarks were run.
Table of Contents
Install And Configure Ruby
Benchmark were run using Ruby version:
2.3.1
Init benchmark directory
Create directory bench for running the benchmarks
mkdir bench
Download Benchmark Utilities from Gist
The benchmark uses utilities found in gist https://gist.github.com/9ed5e11c95ba24092d6381c178770f1e. Download these utilities to bin directory:
git clone https://gist.github.com/9ed5e11c95ba24092d6381c178770f1e bin
Directory structure at this point
. ├── bench └── bin 2 directories
Create Gemfile and install tla-sbuilder with sbuilder-ial plugin
Create a Gemfile in bench directory with the following content
source "https://rubygems.org" gem 'sbuilder-ial', "=0.0.1"
and run
bundle install
to install with sbuilder-ial plugin used in this benchmark. The plugin also loads tla-sbuilder tool.
Versions of used in this benchmark
sbuilder-ial (0.0.1)
tla-sbuilder (>= 0.3.4)
tla-sbuilder (0.3.4)
sbuilder-ial (= 0.0.1)
Init Sbuilder Environment
Init sbuilder environment running following command in bench directory:
bundle exec sbuilder.rb init # remove example configurations from cluttering directory cnf directory rm cnf/*.example
Run init time.csv
Init time.csv used to collect benchmark data. In bench directory run:
../bin/run.sh init
Run cases
For example, to run one benchmark in directory bench issue the command1:
../bin/run.sh run-1 default 1 10 10 10
and observe the output
------------------------------------------------------------------ config=default, iteration: 1, domains: 10, contract: 10, stmt=10 Run ../bin/app-generator.rb -i 1 -c 10 -s 10 -d 10 fmt=time-app:\tdefault\t1\t10\t10\t10\t%E\t%U\t%S cmd=../bin/app-generator.rb -i 1 -c 10 -s 10 -d 10 The message is "time-app: default 1 10 10 10 0:00.09 0.05 0.04." Run bundle exec sbuilder.rb generate fmt=time-gen:\tdefault\t1\t10\t10\t10\t%E\t%U\t%S cmd=bundle exec sbuilder.rb generate generate setup: setup1 Unmustache src/ --> cache/unmustache - start Unmustache src/ --> cache/unmustache - done Parse snippet from repository cache/unmustache - start Initialize parserResolver context symbols 4 TLA+ symbols 6 SBuilder symbols 7 model symbols Initialize parserResolver context symbols - done Parse snippet from repository cache/unmustache - done: parsed 0 snippets The message is "time-gen: default 1 10 10 10 0:03.54 3.48 0.06." Run java -cp /home/jj/java/tla/tla2tools.jar pcal.trans model fmt=time-trans:\tdefault\t1\t10\t10\t10\t%E\t%U\t%S cmd=java -cp /home/jj/java/tla/tla2tools.jar pcal.trans model pcal.trans Version 1.8 of 2 Apr 2013 Parsing completed. Warning: symbols were renamed. Translation completed. New file model.tla written. New file model.cfg written. The message is "time-trans: default 1 10 10 10 0:00.37 1.16 0.04." The trans message is "time-trans: default 1 10 10 10 0:00.37 1.16 0.04." cache cnf Gemfile Gemfile.lock gen sbuilder.log src time.csv Run java -cp /home/jj/java/tla/tla2tools.jar tlc2.TLC setup fmt=time-tlc:\tdefault\t1\t10\t10\t10\t%E\t%U\t%S cmd=java -cp /home/jj/java/tla/tla2tools.jar tlc2.TLC setup TLC2 Version 2.07 of 1 June 2015 Running in Model-Checking mode. Parsing file setup.tla Parsing file model.tla Parsing file /tmp/TLC.tla Parsing file /tmp/FiniteSets.tla Parsing file /tmp/Sequences.tla Parsing file /tmp/Integers.tla Parsing file /tmp/Naturals.tla Semantic processing of module Naturals Semantic processing of module Sequences Semantic processing of module TLC Semantic processing of module FiniteSets Semantic processing of module Integers Semantic processing of module model Semantic processing of module setup Starting... (2017-03-15 10:56:49) Computing initial states... Finished computing initial states: 1 distinct state generated. <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> <<"Dummy macro called should replace with actual macro">> Model checking completed. No error has been found. Estimates of the probability that TLC did not check all reachable states because two distinct states had the same fingerprint: calculated (optimistic): val = 8.6E-15 based on the actual fingerprints: val = 1.3E-13 1663 states generated, 1562 distinct states found, 0 states left on queue. The depth of the complete state graph search is 162. Finished. (2017-03-15 10:56:51) The message is "time-tlc: default 1 10 10 10 0:03.16 9.31 0.54." Model checking completed. No error has been found. The tlc message is "time-tlc: default 1 10 10 10 0:03.16 9.31 0.54." Found message 'Model checking completed. No error has been found' DONE!!! config: default, iterations: 1, domains: 10, contract: 10, stmt=10 ------------------------------------------------------------------
NB: TLA formal model is generated to directory gen/setup1/tla.
Observe Statistics
Benchmark statistics are appended to time.csv file in bench directory:
cat time.csv
type config iterations domains contract stmt real user sys states lines Starting 2017.03.15-10:56:44 time-app: default 1 10 10 10 0:00.09 0.05 0.04 time-gen: default 1 10 10 10 0:03.54 3.48 0.06 time-trans: default 1 10 10 10 0:00.37 1.16 0.04 time-tlc: default 1 10 10 10 0:03.16 9.31 0.54 stat: default 1 10 10 10 1663 8319 Finished 2017.03.15-10:56:51
Fin
This blog entry has documented, how Sbuilder Benchmark were run.
Footnotes:
1
configuration default with ITERATION parameter value 1, DOMAIN parameter 10, CONTRACT parameter 10, and STMT parameter 10
jarjuk 