Commit a68e024c authored by Philipp Meyer's avatar Philipp Meyer
Browse files

Ran more benchmarks for scalable examples

parent 859d32e7
cav-benchmarks/bug_tracking/x0_PENDING_q3_buggy
cav-benchmarks/bug_tracking/x0_BUG_REPORT_q1
cav-benchmarks/bug_tracking/x0_BUG_REPORT_q3
cav-benchmarks/bug_tracking/x0_BUG_REPORT_q5
cav-benchmarks/bug_tracking/x0_BUG_REPORT_q6
cav-benchmarks/bug_tracking/x0_BUG_REPORT_q8
cav-benchmarks/bug_tracking/x0_CLOSED_q1
cav-benchmarks/bug_tracking/x0_CLOSED_q3
cav-benchmarks/bug_tracking/x0_CLOSED_q5
cav-benchmarks/bug_tracking/x0_CLOSED_q6
cav-benchmarks/bug_tracking/x0_CLOSED_q8
cav-benchmarks/bug_tracking/x0_FIXED_q1
cav-benchmarks/bug_tracking/x0_FIXED_q3
cav-benchmarks/bug_tracking/x0_FIXED_q5
cav-benchmarks/bug_tracking/x0_FIXED_q6
cav-benchmarks/bug_tracking/x0_FIXED_q8
cav-benchmarks/bug_tracking/x0_FIX_AGAIN_q1
cav-benchmarks/bug_tracking/x0_FIX_AGAIN_q3
cav-benchmarks/bug_tracking/x0_FIX_AGAIN_q5
cav-benchmarks/bug_tracking/x0_FIX_AGAIN_q6
cav-benchmarks/bug_tracking/x0_FIX_AGAIN_q8
cav-benchmarks/bug_tracking/x0_MORE_INFO_q1
cav-benchmarks/bug_tracking/x0_MORE_INFO_q3
cav-benchmarks/bug_tracking/x0_MORE_INFO_q5
cav-benchmarks/bug_tracking/x0_MORE_INFO_q6
cav-benchmarks/bug_tracking/x0_MORE_INFO_q8
cav-benchmarks/bug_tracking/x0_MUST_FIX_q1
cav-benchmarks/bug_tracking/x0_MUST_FIX_q3
cav-benchmarks/bug_tracking/x0_MUST_FIX_q5
cav-benchmarks/bug_tracking/x0_MUST_FIX_q6
cav-benchmarks/bug_tracking/x0_MUST_FIX_q8
cav-benchmarks/bug_tracking/x0_PENDING_q1
cav-benchmarks/bug_tracking/x0_PENDING_q3
cav-benchmarks/bug_tracking/x0_PENDING_q5
cav-benchmarks/bug_tracking/x0_PENDING_q6
cav-benchmarks/bug_tracking/x0_PENDING_q8
cav-benchmarks/bug_tracking/x0_VERIFIED_q1
cav-benchmarks/bug_tracking/x0_VERIFIED_q3
cav-benchmarks/bug_tracking/x0_VERIFIED_q5
cav-benchmarks/bug_tracking/x0_VERIFIED_q6
cav-benchmarks/bug_tracking/x0_VERIFIED_q8
cav-benchmarks/medical/x0_AA_q1.spec
cav-benchmarks/medical/x0_AA_q2.spec
cav-benchmarks/medical/x0_AA_q5.spec
cav-benchmarks/medical/x0_AR_q1.spec
cav-benchmarks/medical/x0_AR_q2.spec
cav-benchmarks/medical/x0_AR_q5.spec
cav-benchmarks/medical/x0_HA_q1.spec
cav-benchmarks/medical/x0_HA_q2.spec
cav-benchmarks/medical/x0_HA_q5.spec
cav-benchmarks/medical/x0_HQ_q1.spec
cav-benchmarks/medical/x0_HQ_q2.spec
cav-benchmarks/medical/x0_HQ_q5.spec
cav-benchmarks/mist/PN/kanban
cav-benchmarks/mist/PN/leabasicapproach
cav-benchmarks/mist/PN/pncsacover
cav-benchmarks/mist/PN/pncsasemiliv
cav-benchmarks/mist/PN/MultiME
cav-benchmarks/mist/PN/basicME
cav-benchmarks/mist/PN/bingham_h150
cav-benchmarks/mist/PN/bingham_h25
cav-benchmarks/mist/PN/bingham_h250
cav-benchmarks/mist/PN/bingham_h250_attic
cav-benchmarks/mist/PN/bingham_h50
cav-benchmarks/mist/PN/csm
cav-benchmarks/mist/PN/extendedread-write
cav-benchmarks/mist/PN/extendedread-write-smallconsts
cav-benchmarks/mist/PN/fms
cav-benchmarks/mist/PN/fms_attic
cav-benchmarks/mist/PN/manufacturing
cav-benchmarks/mist/PN/mesh2x2
cav-benchmarks/mist/PN/mesh3x2
cav-benchmarks/mist/PN/multipool
cav-benchmarks/mist/PN/pingpong
cav-benchmarks/mist/boundedPN/kanban
cav-benchmarks/mist/boundedPN/lamport
cav-benchmarks/mist/boundedPN/newdekker
cav-benchmarks/mist/boundedPN/newrtp
cav-benchmarks/mist/boundedPN/peterson
cav-benchmarks/mist/boundedPN/read-write
cav-benchmarks/soter/finite_leader__single_leader__depth_0
cav-benchmarks/soter/firewall__no_pred_called_with_zero__depth_0
cav-benchmarks/soter/howait__all_workers_finished_if_wait_over__depth_0
cav-benchmarks/soter/howait__all_workers_finished_if_wait_over__depth_1
cav-benchmarks/soter/howait__all_workers_finished_if_wait_over__depth_2
cav-benchmarks/soter/safe_send__sending_to_non-pid__depth_0
cav-benchmarks/soter/stutter__we_abhorr_as__depth_0
cav-benchmarks/soter/stutter__we_abhorr_as__depth_1
cav-benchmarks/soter/stutter__we_abhorr_as__depth_2
cav-benchmarks/soter/unsafe_send__sending_to_non-pid__depth_0
cav-benchmarks/soter/unsafe_send__sending_to_non-pid__depth_1
cav-benchmarks/soter/unsafe_send__sending_to_non-pid__depth_2
cav-benchmarks/soter/concdb__single_client_writes__depth_0
cav-benchmarks/soter/concdb__single_client_writes__depth_1
cav-benchmarks/soter/concdb__single_client_writes__depth_2
cav-benchmarks/soter/finite_leader__single_leader__depth_1
cav-benchmarks/soter/finite_leader__single_leader__depth_2
cav-benchmarks/soter/firewall__no_pred_called_with_zero__depth_1
cav-benchmarks/soter/firewall__no_pred_called_with_zero__depth_2
cav-benchmarks/soter/parikh__should_already_be_initialized__depth_0
cav-benchmarks/soter/parikh__should_already_be_initialized__depth_1
cav-benchmarks/soter/parikh__should_already_be_initialized__depth_2
cav-benchmarks/soter/pipe__single_message_in_mailbox__depth_0
cav-benchmarks/soter/pipe__single_message_in_mailbox__depth_1
cav-benchmarks/soter/pipe__single_message_in_mailbox__depth_2
cav-benchmarks/soter/reslock__critical__depth_0
cav-benchmarks/soter/reslock__critical__depth_1
cav-benchmarks/soter/reslock__critical__depth_2
cav-benchmarks/soter/reslockbeh__critical__depth_0
cav-benchmarks/soter/reslockbeh__critical__depth_1
cav-benchmarks/soter/reslockbeh__critical__depth_2
cav-benchmarks/soter/ring__single_message_in_mailbox__depth_0
cav-benchmarks/soter/ring__single_message_in_mailbox__depth_1
cav-benchmarks/soter/ring__single_message_in_mailbox__depth_2
cav-benchmarks/soter/safe_send__sending_to_non-pid_1__depth_1
cav-benchmarks/soter/safe_send__sending_to_non-pid_1__depth_2
cav-benchmarks/soter/safe_send__sending_to_non-pid_2__depth_1
cav-benchmarks/soter/safe_send__sending_to_non-pid_2__depth_2
cav-benchmarks/soter/safe_send__sending_to_non-pid_3__depth_1
cav-benchmarks/soter/safe_send__sending_to_non-pid_3__depth_2
cav-benchmarks/soter/safe_send__sending_to_non-pid_4__depth_1
cav-benchmarks/soter/safe_send__sending_to_non-pid_4__depth_2
cav-benchmarks/soter/sieve__single_message_in_counter_mailbox__depth_0
cav-benchmarks/soter/sieve__single_message_in_counter_mailbox__depth_1
cav-benchmarks/soter/sieve__single_message_in_counter_mailbox__depth_2
cav-benchmarks/soter/sieve__single_message_in_filter_mailbox__depth_0
cav-benchmarks/soter/sieve__single_message_in_sieve_mailbox__depth_0
cav-benchmarks/soter/state_factory__after_receive_if_no_mail__depth_0
cav-benchmarks/soter/state_factory__single_message_in_mailbox__depth_0
cav-benchmarks/soter/state_factory__single_message_in_mailbox__depth_1
cav-benchmarks/wahl-kroening/Boop_simple_vf_satabs.1/main
cav-benchmarks/wahl-kroening/Boop_simple_vf_satabs.2/main
cav-benchmarks/wahl-kroening/Function_Pointer3_vs_satabs.1/main
cav-benchmarks/wahl-kroening/Function_Pointer3_vs_satabs.2/main
cav-benchmarks/wahl-kroening/Function_Pointer3_vs_satabs.3/main
cav-benchmarks/wahl-kroening/buggy_spaghetti_vf_satabs.1/main
cav-benchmarks/wahl-kroening/buggy_spaghetti_vf_satabs.2/main
cav-benchmarks/wahl-kroening/conditionals_vs_satabs.1/main
cav-benchmarks/wahl-kroening/constants_vf_satabs.1/main
cav-benchmarks/wahl-kroening/constants_vf_satabs.2/main
cav-benchmarks/wahl-kroening/dekker_vs_satabs.1/main
cav-benchmarks/wahl-kroening/dekker_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p1_vs_satabs.1/main
cav-benchmarks/wahl-kroening/double_lock_p1_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p1_vs_satabs.3/main
cav-benchmarks/wahl-kroening/double_lock_p2_vs_satabs.1/main
cav-benchmarks/wahl-kroening/double_lock_p2_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p3_vs_satabs.1/main
cav-benchmarks/wahl-kroening/double_lock_p3_vs_satabs.2/main
cav-benchmarks/wahl-kroening/double_lock_p3_vs_satabs.3/main
cav-benchmarks/wahl-kroening/lu-fig2_fixed_vs_satabs.1/main
cav-benchmarks/wahl-kroening/lu-fig2_fixed_vs_satabs.2/main
cav-benchmarks/wahl-kroening/lu-fig2_fixed_vs_satabs.3/main
cav-benchmarks/wahl-kroening/peterson_vs_satabs.1/main
cav-benchmarks/wahl-kroening/peterson_vs_satabs.2/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.1/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.2/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.3/main
cav-benchmarks/wahl-kroening/pthread5_vs_satabs.4/main
cav-benchmarks/wahl-kroening/rand_cas_vs_satabs.1/main
cav-benchmarks/wahl-kroening/rand_lock_p0_vs_satabs.1/main
cav-benchmarks/wahl-kroening/rand_lock_p0_vs_satabs.2/main
cav-benchmarks/wahl-kroening/rand_lock_p0_vs_satabs.3/main
cav-benchmarks/wahl-kroening/simple_loop5_vs_satabs.1/main
cav-benchmarks/wahl-kroening/simple_loop5_vs_satabs.2/main
cav-benchmarks/wahl-kroening/spin2003_vs_satabs.1/main
cav-benchmarks/wahl-kroening/spin2003_vs_satabs.2/main
cav-benchmarks/wahl-kroening/stack_cas_p0_vs_satabs.1/main
cav-benchmarks/wahl-kroening/stack_cas_p0_vs_satabs.2/main
cav-benchmarks/wahl-kroening/stack_cas_p0_vs_satabs.3/main
cav-benchmarks/wahl-kroening/stack_lock_p0_vs_satabs.1/main
cav-benchmarks/wahl-kroening/stack_lock_p0_vs_satabs.2/main
cav-benchmarks/wahl-kroening/szymanski_vs_satabs.1/main
cav-benchmarks/wahl-kroening/szymanski_vs_satabs.2/main
cav-benchmarks/wahl-kroening/conditionals_vs_satabs.2/main
cav-benchmarks/wahl-kroening/rand_cas_vs_satabs.2/main
...@@ -2,7 +2,8 @@ ...@@ -2,7 +2,8 @@
#benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' ) #benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' )
#benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' 'cav-benchmarks/medical' 'cav-benchmarks/bug_tracking' ) #benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' 'cav-benchmarks/medical' 'cav-benchmarks/bug_tracking' )
benchmarks=( 'cav-benchmarks/soter' ) benchmarks=( 'service-tech/ibm-soundness' )
#benchmarks=( 'service-tech/sap-reference' )
extensions=( 'pnet' 'tpn' 'lola' 'spec' ) extensions=( 'pnet' 'tpn' 'lola' 'spec' )
tool='lola' tool='lola'
...@@ -25,8 +26,7 @@ for benchmark in ${benchmarks[@]}; do ...@@ -25,8 +26,7 @@ for benchmark in ${benchmarks[@]}; do
>$benchmark_dir/$prop-timeout-$tool.list >$benchmark_dir/$prop-timeout-$tool.list
>$benchmark_dir/$prop-error-$tool.list >$benchmark_dir/$prop-error-$tool.list
for ext in ${extensions[@]}; do for ext in ${extensions[@]}; do
#for file in `find $benchmark_dir -name "*.$ext"`; do for file in `find $benchmark_dir -name "*.$ext"`; do
for file in $(cat $benchmark_dir/$prop.dontknow); do
timing="$(date +%s%N)" timing="$(date +%s%N)"
( (
ulimit -S -t $time_soft ulimit -S -t $time_soft
...@@ -34,7 +34,8 @@ for benchmark in ${benchmarks[@]}; do ...@@ -34,7 +34,8 @@ for benchmark in ${benchmarks[@]}; do
ulimit -S -v $mem_soft ulimit -S -v $mem_soft
ulimit -H -v $mem_hard ulimit -H -v $mem_hard
set -o pipefail; set -o pipefail;
$executable -f $file.spec.$prop.task1 $file.spec.$prop 2>&1 | tee $file.out echo $executable -f $file.$prop.task1 $file.$prop
$executable -f $file.$prop.task1 $file.$prop 2>&1 | tee $file.out
) )
result=$? result=$?
ryes=$(grep "result: yes" $file.out) ryes=$(grep "result: yes" $file.out)
......
#!/bin/bash #!/bin/bash
#benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' ) #benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' )
benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' ) #benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' )
benchmarks=( 'service-tech/sap-reference' )
extensions=( 'pnet' 'tpn' 'lola' 'spec' ) extensions=( 'pnet' 'tpn' 'lola' 'spec' )
executable='/home/philipp/local/sara-1.0/src/sara' executable='/home/philipp/local/sara-1.0/src/sara'
prop=( 'safe' )
for benchmark in ${benchmarks[@]}; do for benchmark in ${benchmarks[@]}; do
benchmark_dir="$benchmark" benchmark_dir="$benchmark"
...@@ -20,7 +22,7 @@ for benchmark in ${benchmarks[@]}; do ...@@ -20,7 +22,7 @@ for benchmark in ${benchmarks[@]}; do
echo "testing $file with $base" echo "testing $file with $base"
( (
set -o pipefail; set -o pipefail;
timeout 60 $executable -i $base.terminating.sara 2>&1 | tee $base.out timeout 60 $executable -i $base.$prop.sara 2>&1 | tee $base.out
) )
popd popd
result=$? result=$?
......
#!/bin/bash #!/bin/bash
#benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' ) benchmarks=( 'service-tech/ibm-soundness' 'service-tech/sap-reference' )
benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' 'cav-benchmarks/bug_tracking' 'cav-benchmarks/medical' ) #benchmarks=( 'service-tech/sap-reference' )
#benchmarks=( 'cav-benchmarks/mist' 'cav-benchmarks/wahl-kroening' 'cav-benchmarks/soter' 'cav-benchmarks/bug_tracking' 'cav-benchmarks/medical' )
extensions=( 'pnet' 'lola' 'tpn' 'spec' ) extensions=( 'pnet' 'lola' 'tpn' 'spec' )
executable='../slapnet' executable='../slapnet'
...@@ -9,14 +10,13 @@ executable='../slapnet' ...@@ -9,14 +10,13 @@ executable='../slapnet'
#3 hours #3 hours
time_soft=$(expr 3 \* 3600) time_soft=$(expr 3 \* 3600)
properties=( 'deadlock_free' ) properties=( 'terminating' )
prop_options=( '--no-given-properties --safe' ) prop_options=( '--no-given-properties --terminating' )
for benchmark in ${benchmarks[@]}; do for benchmark in ${benchmarks[@]}; do
benchmark_dir="$benchmark" benchmark_dir="$benchmark"
for (( propi=0;propi<${#properties[@]};propi++)); do for (( propi=0;propi<${#properties[@]};propi++)); do
prop=${properties[$propi]} prop=${properties[$propi]}
prop_options=${property_options[$propi]}
>$benchmark_dir/$prop-positive-slapnet.list >$benchmark_dir/$prop-positive-slapnet.list
>$benchmark_dir/$prop-dontknow-slapnet.list >$benchmark_dir/$prop-dontknow-slapnet.list
>$benchmark_dir/$prop-timeout-slapnet.list >$benchmark_dir/$prop-timeout-slapnet.list
...@@ -28,7 +28,9 @@ for benchmark in ${benchmarks[@]}; do ...@@ -28,7 +28,9 @@ for benchmark in ${benchmarks[@]}; do
timing="$(date +%s%N)" timing="$(date +%s%N)"
( (
set -o pipefail set -o pipefail
timeout $time_soft $executable $prop_options --$ext $file -o $file.$prop 2>&1 | tee $file.$prop.out
echo timeout $time_soft $executable $prop_options --$ext $file -o $file.$prop
timeout $time_soft $executable $prop_options --$ext $file 2>&1 | tee $file.$prop.out
) )
result=$? result=$?
timing=$(($(date +%s%N)-timing)) timing=$(($(date +%s%N)-timing))
......
#!/usr/bin/bash #!/usr/bin/bash
#folder="LeaderElectionDKR82" #folder="LeaderElectionDKR82"
folder="Snapshot" folder="LeaderElectionCR79"
suffix="-comm" #folder="Snapshot"
suffix="-ord"
#suffix="-comm"
n=100 n=100
m=2 m=3
bf="${folder}/benchmark${suffix}.out" bf="${folder}/benchmark${suffix}.out"
echo "n user system memory" >$bf echo "n user system memory" >$bf
for i in $(seq 1 $n); do for i in $(seq 10 10 100); do
net="${folder}/n${i}${suffix}.pnet" net="${folder}/n${i}${suffix}.pnet"
echo "Testing net $net" echo "Testing net $net"
for j in $(seq 1 $m); do for j in $(seq 1 $m); do
echo -n "$i " >>$bf echo -n "$i " >>$bf
/usr/bin/time -f "%U %S %M" -a -o $bf ../slapnet $net > "${net}.out" /usr/bin/time -f "%U %S %M" -a -o $bf ../../slapnet $net > "${net}.out"
done done
done done
...@@ -4,7 +4,8 @@ library("data.table") ...@@ -4,7 +4,8 @@ library("data.table")
library("Hmisc") library("Hmisc")
#folders <- c("LeaderElectionCR79", "LeaderElectionDKR82") #folders <- c("LeaderElectionCR79", "LeaderElectionDKR82")
folders <- c("LeaderElectionDKR82") #folders <- c("LeaderElectionCR79")
folders <- c("Snapshot")
for (folder in folders) { for (folder in folders) {
infile <- paste(folder, "benchmark.out", sep="/") infile <- paste(folder, "benchmark.out", sep="/")
...@@ -16,7 +17,8 @@ for (folder in folders) { ...@@ -16,7 +17,8 @@ for (folder in folders) {
datatable <- data.table(dataframe) datatable <- data.table(dataframe)
data <- datatable[,list(time=mean(user+system),err_time=sd(user+system),memory=mean(memory),err_memory=sd(memory)),by=n] data <- datatable[,list(time=mean(user+system),memory=mean(memory/1024)),by=n]
#data <- datatable[,list(time=mean(user+system),err_time=sd(user+system),memory=mean(memory/1024),err_memory=sd(memory)),by=n]
write.table(data, file=outfile, row.names=FALSE) write.table(data, file=outfile, row.names=FALSE)
......
Markdown is supported
0% or .
You are about to add 0 people to the discussion. Proceed with caution.
Finish editing this message first!
Please register or to comment