0 - Running Sbuilder Benchmarks.md

This gist contains code used to run Benchmarks on Sbuilder/TLA-tools

app-generator.rb

#!/usr/bin/env ruby

require 'optparse'

APP_DOMAIN_NAME='application_domain'

def setup_yaml( contracts:, domains:, iterations: )
  <<-EOS  
   - domain-extension:

       - domain: eth_address
         cardinality: #{ '%.0f' % (contracts * iterations) }
       - domain: application_domain
         cardinality: #{domains}

   - step-extension:
#{ 
   (1..(contracts * iterations).to_i).map do |i|
      contract = (i - 1 ) % contracts + 1
      '     - interface: contract' + contract.to_s + "()"
   end.join( "\n") 
}
  EOS
end

def sbuilder_yaml( constructors:, steps:, domains:  )
  <<-EOS
  preferences:
          debug-output: false

  extend:
    loaders:
       - className: Sbuilder::Ial::Plugin
         gem: sbuilder-ial
         configuration:
         objects:
            - objectName: ialLoader
              configuration:
                application: 
                    constructors: #{constructors}
                    steps: #{steps}
                metatypes: ial2
                rubypaths:
                   - cache/ial.rb


  interfaces:
      -  objectName: ialLoader
         url: nil


  snippets:
    -  objectName: ialLoader
       snippets:
           - apu.tmp
           - xx.rb

  setups:
      - setupDirectory: setup1
        extensions:
          -  url: cnf/setup1.yaml

  invariants:
  EOS
end

def app
  <<-'EOS'
     # load MyApi from file 'ial_lib.rb'
     require 'ethereum/api'

     # sbuilder.yaml application configuration
     constructors = configuration['constructors'].nil? ?  1 : configuration['constructors']
     steps = configuration['steps'].nil? ?  1 : configuration['steps']
     # Application constants
     APPI_DOM = 'application_domain'
     VARIABLE_ADDRESS = "address1"
     CONTRACT = 'contract'
     INPUT_FIELD = 'inp1'
     INPUT_TYPE = 'input_type'
     # MACRO1 = 'macro1'

     # Application domains 

     # Add Ethreum API snippets

     Sbuilder::Ial::Ethereum.library + 
     [
       Sbuilder::Ial::Ethereum.domainDefinition(APPI_DOM),
       Sbuilder::Ial.definition { name INPUT_TYPE; properties [ {:name => 'fld1', :domain => APPI_DOM } ] },
       Sbuilder::Ial.variable { name VARIABLE_ADDRESS },
     ] + 

       (1..constructors).map do |constructorNro|
       # puts "constructorNro=#{constructorNro}"
       Sbuilder::Ial::Ethereum.constructor( contract: "#{CONTRACT}#{constructorNro}", req: [{ :name => INPUT_FIELD, :definition => INPUT_TYPE }] ) do |tx|
         # tx.output [ "Input_type", Sbuilder::Ial::Ethereum.parameterRef(INPUT_FIELD) ]
         tx.addStatements(  Sbuilder::Ial.skipStatement(){} )
         initMembers = {
           :intMember => 1,
           :strMember => :nil,
         }
         tx.addStatements Sbuilder::Ial::Ethereum.stmtsCreateContract( codeHash: 'demo', value: 0, memberVariables: initMembers )
         (1..steps).map do |stepNro|
             tx.addStatements Sbuilder::Ial::Ethereum.stmtsUpdateContract( addressRef: Sbuilder::Ial::Ethereum.currentId, memberVariable: { :intMember => stepNro, :strMember => 'hei' } )
             # tx.output [ "Contracts - after update:", Sbuilder::Ial::Ethereum.contractVariableExec ]
         end
         # tx.output [ "Accounts ", Sbuilder::Ial::Ethereum.accountVariableExec ]
         # tx.output [ "Contracts -before update:", Sbuilder::Ial::Ethereum.contractVariableExec ]

       end
     end # configuration['constructors']
  EOS
end

def createConfigs( file, constructors:, steps:, domains:  )
  File.open( file, 'w' ){ |f| f.write( sbuilder_yaml( constructors: constructors, steps: steps, domains: domains )) }
end

def createSetup( file, contracts:, domains:, iterations: )
  File.open( file, 'w' ){ |f| f.write( setup_yaml( contracts: contracts, domains: domains, iterations: iterations ) ) }
end

def createApp( file )
  
  File.open( file, 'w' ){ |f| f.write( app ) }
end

def main( sbuilder:, setup:, app:, config: {} )

  createConfigs( sbuilder, constructors: config[:contracts], steps: config[:steps], domains: config[:domains]  )
  createSetup( setup, contracts: config[:contracts], domains: config[:domains], iterations: config[:iterations] )
  createApp( app )    
  
end

CACHE='cache'
CNF='cnf'
SBUILDER_FILE = "sbuilder.yaml"
SETUP_FILE = "setup1.yaml"
SBUILDER_PATH = "#{CNF}/#{SBUILDER_FILE}"
SETUP_PATH = "#{CNF}/#{SETUP_FILE}"
APP_FILE='ial.rb'
APP_PATH = "#{CACHE}/#{APP_FILE}"

config = {}
OptionParser.new do |opts|
  opts.banner = "Usage #{__FILE__} [options]"

  opts.on( '-i' '--iterations COUNT', 'Number of iterations' ) { |v| config[:iterations] = v.to_f }  
  opts.on( '-c' '--contracts COUNT', 'Number of contracts' ) { |v| config[:contracts] = v.to_i }
  opts.on( '-s' '--stmt COUNT', 'Number of statements in a contract' ) { |v| config[:steps] = v }
  opts.on( '-d' '--domains COUNT', 'Number of domains in a mode' ) { |v| config[:domains] = v }    
end.parse!

# use default
config =  {
  :iterations => 1,
  :contracts => 1,
  :steps => 1,
  :domains => 1,      
}.merge( config )



main( sbuilder:SBUILDER_PATH, setup: SETUP_PATH, app: APP_PATH, config: config )

run.sh

#!/bin/bash


# set -e

# ------------------------------------------------------------------
# configuration

TS_FORMAT="+%Y.%m.%d-%T"
export LANG=fi_FI
export TIME_MSG
TIME_CMD=/usr/bin/time
TIME_DB=$(pwd)/time.csv
TIME_HDR="type	config	iterations	domains	contract	stmt	real	user	sys	states	lines"
# TIME_FMT appeded after 'type:, $cmd, $config' -string
TIME_FMT='%E\t%U\t%S'

# ruby creating sbuilder.yaml, setup and ial.rb
APP_GENERATOR=../bin/app-generator.rb

# tla-sbuilder generator
SBUILDER="bundle exec sbuilder.rb"

# File locations
CNF=cnf
OPT_DEBUG=ERROR

# Ttlatool jar
# SDIR="$( cd "$( dirname "${BASH_SOURCE[0]}" )" && pwd )"
SDIR=~/java/tla
TLATOOLS_JAR="$SDIR/tla2tools.jar"

# expect to find this string when TLC verification passes
MSG_OK="Model checking completed. No error has been found"


# options for java & TLC

# OPT_JAVA_OPTS=" -d64 -Xmx6g  -Xss1g -Xms3g "
# OPT_JAVA_OPTS=
# options for tlc
#OPT_TLC_COMMON=
# options for normal run i.e. not possibliti
#OPT_TLC=

# Java options
# xss# -Xms<heap size>[g|m|k] -Xmx<heap size>[g|m|k]
#

declare -A OPTIONS=(

    ['default-ok']="Y"
    ['default-java']=""
    ['default-TLC']=""    

    ['config1-ok']="Y"
    ['config1-java']=" -d64 -Xmx6g  -Xss1g -Xms3g "
    ['config1-TLC']="-workers 8"    

    
)
    

usage() {
    cat <<EOF
    $0 Usage

    $0 init
    $0 run-1 CONFIG ITERATIONS DOMAINS CONTRACTS STMT
    $0 run-domain-contract DOMAINS
    $0 run-all
    
    CONFIG values:

EOF

    for KEY in $(echo ${!OPTIONS[@]} ) ;  do
	if [[ $KEY =~  '-TLC' ]]; then
	    echo $(echo "$KEY" | sed -e 's/-TLC//g' )
	fi
    done

}

cleanupConfigs() {
    rm -f $CNF/*.example
}

runit() {

    local fmt="$1";shift
    fmt=$(echo $fmt | sed -e 's/ /\\t/g' -)
    local cmd="$1"; shift
    local out="$1"; shift

    echo Run $cmd

    echo "fmt=$fmt"
    echo "cmd=$cmd"    
#    exec 3>&1 4>&2 #set up extra file descriptors
    exec 3>&1 #set up extra file descriptors    

    
    if [ -z "$out" ]; then
	TIME_MSG=$( ((/usr/bin/time -f "$fmt" $cmd  1>&3) )  2>&1 )
    else
	TIME_MSG=$( ((/usr/bin/time -f "$fmt" $cmd  | tee $out  1>&3 )   )   2>&1   )	
    fi
    TIME_MSG=$(echo $TIME_MSG | sed -e 's/ /	/g' -)
    export TIME_MSG
    # TIME_MSG=$( (/usr/bin/time -f $fmt $cmd 2>&1&4 1>&3); 2>&1 )    
    # /usr/bin/time -f $fmt $cmd     
    ISTAT=$?
    if [ $ISTAT != 0 ]; then
	echo "Error in runit $ISTAT: $TIME_MSG"
	exit 1
    fi
    # TIME_MSG=$($cmd 3>&1 1>&2) 2>&3
    # TIME_MSG=$($cmd 3>&1 1>&2 2>&3 )
    echo "The message is \"${TIME_MSG}.\""
    exec 3>&- #  4>&- # release the extra file descriptors
    # exec 3>&-   4>&- # release the extra file descriptors    
 }

run_case() {

    local config=$1; shift
    local iterations=$1; shift
    local domains=$1; shift
    local contracts=$1; shift
    local stmt=$1; shift
    local setup=setup1

    echo "------------------------------------------------------------------"
    echo "config=$config, iteration: $iterations, domains: $domains, contract: $contracts, stmt=$stmt"
    echo "Starting $(echo $(date $TS_FORMAT))" >> $TIME_DB

    local hdr="$config\t$iterations\t$domains\t$contracts\t$stmt"    

    # Create sbuilder.yaml, setup1.yaml && ial.rb
    local cmd="$APP_GENERATOR -i $iterations -c $contracts -s $stmt -d $domains"
    ISTAT=$?
    runit "time-app:\t$hdr\t$TIME_FMT" "$cmd"    
    if [ $ISTAT = 0 ]; then
	echo "$TIME_MSG" >> $TIME_DB
    else
	echo error $ISTAT
	exit 1
    fi
    

    # Create gen/setup1/tla/model.tla
    # local cmd="$SBUILDER generate -l $OPT_DEBUG"
    local cmd="$SBUILDER generate"    
    runit "time-gen:\t$hdr\t$TIME_FMT" "$cmd"
    if [ $ISTAT = 0 ]; then
	echo "$TIME_MSG" >> $TIME_DB
    else
	echo error $ISTAT
	exit 1
    fi

    # translater gen/setup1/tla/model.tla
    local out=$(pwd)/gen/trans.out
    cd gen/$setup/tla;
    local cmd="java -cp $TLATOOLS_JAR pcal.trans model"
    runit "time-trans:\t$hdr\t$TIME_FMT" "$cmd" "$out"
    grep error $out
    if [ $? = 0 ]; then
    	echo >&2 ""		
    	echo >&2 ""		
    	echo  "ERROR: in pcal.trans"
    	cat $out >&2
    	exit 1;
    else
	echo "The trans message is \"${TIME_MSG}.\""
	echo "$TIME_MSG" >> $TIME_DB
    fi
    cd ../../../
    
    ls 
    local out=$(pwd)/gen/tlc.out
    if [ "${OPTIONS[$config-ok]}" != 'Y' ];then
	echo Configuration $config does not exist
	usage
	exit 1
    fi
    local java_opts=${OPTIONS[$config-java]}
    local tlc_opts=${OPTIONS[$config-TLC]}
    local cmd="java $java_opts -cp $TLATOOLS_JAR tlc2.TLC setup $tlc_opts"
    cd gen/$setup/tla
    runit "time-tlc:\t$hdr\t$TIME_FMT" "$cmd" "$out"
    grep -e "$MSG_OK" $out
    if [ $? != 0 ]; then
	echo >&2 ""		
	echo >&2 ""		
	echo >&2 "ERROR ($setup): Message '${MSG_OK}' - not seen"
	exit 1;
    else
	echo "The tlc message is \"${TIME_MSG}.\""
        STATES=$(cat $out | grep 'states generated, '| cut -d' ' -f1 )
        LINES=$(wc -l model.tla | cut -d' ' -f1 )	
	echo "$TIME_MSG" >> $TIME_DB
	# echo "$TIME_MSG	$STATES	$LINES" >> $TIME_DB
	echo "stat:	$config	$iterations	$domains	$contracts	$stmt				$STATES	$LINES" >> $TIME_DB
	echo >&2 ""		
	echo >&2 ""		
	echo >&2  "SUCCESS ($setup)"
	echo      "Found message '${MSG_OK}'"	
    fi
    cd ../../../    


    echo "Finished $(echo $(date $TS_FORMAT))" >> $TIME_DB
    echo ""  >> $TIME_DB	
    echo "DONE!!!"
    echo "config: $config, iterations: $iterations, domains: $domains, contract: $contracts, stmt=$stmt"
    echo "------------------------------------------------------------------"
    
}

run_large_domain_contract() {

        local config=$1; shift 
        local iterations=1; 
        local domains=$1; shift

	run_case  $config $iterations $domains 25 75
    	run_case  $config $iterations $domains 25 100

	run_case  $config $iterations $domains 50 50
	run_case  $config $iterations $domains 50 75
    
}

run_domain_contract() {

    local config=$1; shift 
    local iterations=1
    local domains=$1; shift

	    run_case  $config $iterations  $domains 1 1 
	    run_case  $config $iterations  $domains 1 5
	    run_case  $config $iterations  $domains 1 10
	    run_case  $config $iterations  $domains 1 25
	    run_case  $config $iterations  $domains 1 50
	    run_case  $config $iterations  $domains 1 75
	    run_case  $config $iterations  $domains 1 100
	    run_case  $config $iterations  $domains 1 110	    
	    run_case  $config $iterations  $domains 1 120

	    run_case  $config $iterations  $domains 2 1 
	    run_case  $config $iterations  $domains 2 5
	    run_case  $config $iterations  $domains 2 10
	    run_case  $config $iterations  $domains 2 25
	    run_case  $config $iterations  $domains 2 50
	    run_case  $config $iterations  $domains 2 75
	    run_case  $config $iterations  $domains 2 100

	    run_case  $config $iterations  $domains 5 1 
	    run_case  $config $iterations  $domains 5 5
	    run_case  $config $iterations  $domains 5 10
	    run_case  $config $iterations  $domains 5 25
	    run_case  $config $iterations  $domains 5 50
	    run_case  $config $iterations  $domains 5 75
	    run_case  $config $iterations  $domains 5 100

	    run_case  $config $iterations  $domains 10 1 
	    run_case  $config $iterations  $domains 10 5
	    run_case  $config $iterations  $domains 10 10
	    run_case  $config $iterations  $domains 10 25
	    run_case  $config $iterations  $domains 10 50
	    run_case  $config $iterations  $domains 10 75
	    run_case  $config $iterations  $domains 10 100

	    run_case  $config $iterations  $domains 25 1 
	    run_case  $config $iterations  $domains 25 5
	    run_case  $config $iterations  $domains 25 10
	    run_case  $config $iterations  $domains 25 25
	    run_case  $config $iterations  $domains 25 50
#	    run_case  $config $iterations  $domains 25 200

	    run_case  $config $iterations  $domains 50 1 
	    run_case  $config $iterations  $domains 50 5
	    run_case  $config $iterations  $domains 50 10
	    run_case  $config $iterations  $domains 50 25
#	    run_case  $config $iterations  $domains 50 100

	    run_case  $config $iterations  $domains 55 1 	    

}


initTime() {
    rm -f $TIME_DB
    if [ ! -f $TIME_DB ]; then
	echo "$TIME_HDR" >$TIME_DB
    fi
}





while :
do

    if [  $# -lt 1 ]; then
	break
    fi

    CMD=$1
    shift

    case "$CMD" in

	app-generate)
	    if [ $# -lt 4 ];then
		usage
		exit 1
	    fi
	    # create cnf/sbuilder.yaml
	    ITERATIONS=$1; shift
	    DOMAINS=$1; shift
	    CONTRACTS=$1; shift
	    STMT=$1; shift
	    $APP_GENERATOR -i $ITERATIONS -c $CONTRACTS -s $STMT -d $DOMAINS	    
	    ;;


	run-domain-contract)
	    if [ $# -lt 1 ];then
		usage
		exit 1
	    fi
	    DOMAINS=$1
	    run_domain_contract $DOMAINS
	    ;;

	run-large)
	    if [ $# -lt 1 ];then
		usage
		exit 1
	    fi
	    DOMAINS=$1
	    run_large_domain_contract $DOMAINS
	    ;;
	

	run-all)
	    run_domain_contract 1
	    run_domain_contract 2
	    run_domain_contract 5
	    run_domain_contract 10
	    run_large_domain_contract 1
	    run_large_domain_contract 2
	    run_large_domain_contract 5
	    run_large_domain_contract 10	    
	    ;;

	run-iterations)
	    run_case default 1 1 10 50
	    run_case default 2 1 10 50
	    run_case default 5 1 10 50
	    run_case default 10 1 10 50
	    run_case default 25 1 10 50	    	    	    	    
	    run_case default 50 1 10 50	    	    	    	    
	    run_case default 75 1 10 50
	    run_case default 100 1 10 50	    	    	    	    	    
	    ;;

	run-config1)
	    run_case config1 10 1 1 10
	    run_case config1 5 1 2 10	    
	    run_case config1 1 1 10 10
	    run_case config1 0.5 1 20 10
	    run_case config1 0.25 1 40 10
	    run_case config1 0.125 1 80 10	    	    	    	    
	    run_case config1 0.1 1 100 10	    	    	    
	    ;;
	
	run-config1-10)
	    run_case config1 10     10 1 10
	    run_case config1 5      10 2 10	    
	    run_case config1 1      10 10 10
	    run_case config1 0.5    10 20 10
	    run_case config1 0.25   10 40 10
	    run_case config1 0.125  10 80 10	    	    	    	    
	    run_case config1 0.1    10 100 10	    	    	    
	    ;;
	
	run-default-inv-10)
	    run_case default 10     10 1 10
	    run_case default 5      10 2 10	    
	    run_case default 1      10 10 10
	    run_case default 0.5    10 20 10
	    run_case default 0.25   10 40 10
	    run_case default 0.125  10 80 10	    	    	    	    
	    run_case default 0.1    10 100 10	    	    	    
	    ;;

	run-default-trace-dom10)
	    run_case default 1  10 1 20
	    run_case default 10  10 1 20
	    run_case default 50  10 1 20
	    run_case default 100  10 1 20
	    run_case default 500  10 1 20
	    run_case default 1000  10 1 20
	    run_case default 2500  10 1 20
	    run_case default 5000  10 1 20

	    ;;
	
	
	
	run-config1-stmt)
	    run_case config1 1 1 10 10
	    run_case config1 1 1 10 25
	    run_case config1 1 1 10 50
	    run_case config1 1 1 10 100
	    run_case config1 1 1 10 200
	    run_case config1 1 1 10 250
	    run_case config1 1 1 10 400	    	    
	    ;;
	
	run-config1-stmt-dom-10)
	    run_case config1 1 10 10 10
	    run_case config1 1 10 10 25
	    run_case config1 1 10 10 50
	    run_case config1 1 10 10 100
	    run_case config1 1 10 10 200
	    run_case config1 1 10 10 250
	    run_case config1 1 10 10 400	    	    
	    ;;

	run-config1-doms)
	    run_case config1 1 1 1 10
	    run_case config1 1 10 1 10
	    run_case config1 1 50 1 10
	    run_case config1 1 100 1 10
	    run_case config1 1 1000 1 10
	    run_case config1 1 5000 1 10	    	    	    	    	    
	    run_case config1 1 10000 1 10
	    run_case config1 1 50000 1 10
	    run_case config1 1 100000 1 10	    
	    ;;
	
	
	run-config1-if)
	    run_case config1 1 1 1 20
	    run_case config1 10 1 1 20	    
	    run_case config1 100 1 1 20	    
	    run_case config1 1000 1 1 20	    
	    run_case config1 2500 1 1 20	    
	    run_case config1 5000 1 1 20	    
	    ;;
	
	run-config1-if-dom10)
	    run_case config1 1    10  1 20
	    run_case config1 10   10  1 20	    
	    run_case config1 100  10  1 20	    
	    run_case config1 1000 10  1 20	    
	    run_case config1 2500 10  1 20	    
	    run_case config1 5000 10  1 20	    
	    ;;
	
	

	run-default-stmt-dom-10)
	    run_case default 1 10 10 10
	    run_case default 1 10 10 25
	    run_case default 1 10 10 50
	    run_case default 1 10 10 100
	    run_case default 1 10 10 200
	    run_case default 1 10 10 250
	    run_case default 1 10 10 400	    	    
	    ;;
	
	

	run-1)
	    if [ $# -lt 5 ];then
		usage
		exit 1
	    fi
	    # create cnf/sbuilder.yaml
	    CONFIG=$1; shift	    
	    ITERATIONS=$1; shift
	    DOMAINS=$1; shift
	    CONTRACTS=$1; shift
	    STMT=$1; shift	    
	    run_case $CONFIG $ITERATIONS $DOMAINS $CONTRACTS $STMT
	    ;;
	
	init)
	    # rm cnf/*.example
	    cleanupConfigs
	    initTime
	    echo $TIME_DB cleaned
	    ;;

	*)
	    usage
	    echo  "Unknown action $CMD"
	    exit 3
	    ;;
	
    esac
done