Running Sbuilder Benchmarks on TLA+Tools

This post documents, how Sbuilder Benchmarks were run.

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

Advertisements

Leave a Reply

Fill in your details below or click an icon to log in:

WordPress.com Logo

You are commenting using your WordPress.com account. Log Out / Change )

Twitter picture

You are commenting using your Twitter account. Log Out / Change )

Facebook photo

You are commenting using your Facebook account. Log Out / Change )

Google+ photo

You are commenting using your Google+ account. Log Out / Change )

Connecting to %s