Notice to GitKraken users: A vulnerability has been found in the SSH key generation of GitKraken versions 7.6.0 to 8.0.0 (https://www.gitkraken.com/blog/weak-ssh-key-fix). If you use GitKraken and have generated a SSH key using one of these versions, please remove it both from your local workstation and from your LRZ GitLab profile.

21.10.2021, 9:00 - 11:00: Due to updates GitLab may be unavailable for some minutes between 09:00 and 11:00.

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

Added promela versions of benchmarks to test with spin

parent 8300488b
#define CHECK 0
byte x[N];
active [N] proctype p() {
int j;
s1: x[_pid] = true;
s2: j = 0;
do
:: j == _pid ->
break;
:: j < _pid && x[j] ->
x[_pid] = false;
do
:: x[j] -> skip;
:: else -> break;
od
goto s1;
:: j < _pid && !x[j] ->
j++;
od
s3: j = _pid + 1;
do
:: j == N ->
break;
:: j < N ->
do
:: x[j] -> skip;
:: else -> break;
od
j++;
od
s4: if
:: _pid == CHECK ->
progress: skip;
:: else ->
skip;
fi
s5: x[_pid] = false;
s6: goto s1;
}
#define SIZE short
#define NEXT(x) (x+1) % N
chan m[N] = [1] of { SIZE };
SIZE leader = 0;
active [N] proctype p() {
SIZE rec;
l: m[NEXT(_pid)] ! _pid;
do
:: m[_pid]?rec ->
if
:: _pid < rec ->
m[NEXT(_pid)] ! rec;
:: _pid > rec ->
skip;
:: else ->
progress: leader = _pid + 1;
// reset
leader = 0;
goto l;
fi
:: leader > 0 ->
goto l;
od
}
#define SIZE short
#define NEXT(x) (x+1) % N
chan m1[N] = [1] of { SIZE };
chan m2[N] = [1] of { SIZE };
SIZE leader = 0;
active [N] proctype p() {
SIZE rec;
SIZE left;
SIZE max;
l: max = _pid;
left = 0;
m1[NEXT(_pid)] ! max;
do
:: m1[_pid]?rec ->
if
:: max != rec ->
m2[NEXT(_pid)] ! rec;
left = rec;
:: else ->
int i;
progress: leader = max + 1;
// reset
leader = 0;
goto l;
fi
:: m2[_pid]?rec ->
if
:: left > rec && left > max ->
max = left
m1[NEXT(_pid)] ! max;
:: else ->
goto pa;
fi
od
pa: do
:: m1[_pid]?rec ->
m1[NEXT(_pid)] ! rec;
:: m2[_pid]?rec ->
m2[NEXT(_pid)] ! rec;
:: leader > 0 ->
goto l;
od
}
#define CHECK 0
#define SIZE short
SIZE q[N];
SIZE turn[N];
active [N] proctype p() {
int j;
int k;
s1: for (j : 1 .. (N-1)) {
q[_pid] = j;
turn[j] = _pid;
s4: k = 0;
s5: if
:: k == N || (k == _pid && _pid == N - 1) ->
goto s6;
:: k == _pid && _pid < N - 1 ->
k = _pid + 1;
:: else ->
skip;
fi
if
:: q[k] >= j && turn[j] == _pid ->
goto s4;
:: else ->
k++;
goto s5;
fi
}
s6:
q[_pid] = N;
if
:: _pid == CHECK ->
progress: skip;
:: else ->
skip;
fi
cs: skip;
q[_pid] = 0;
goto s1;
}
#define NEXT(x) (x+1) % N
mtype = { marker }
chan m[N] = [0] of { mtype };
bool done[N];
bool sampled[N];
active [N] proctype p() {
bool red;
bool sent;
bool received;
s: done[_pid] = false;
sampled[_pid] = false;
red = false;
sent = false;
received = false;
do
:: !red ->
if
:: true ->
red = true;
sampled[_pid] = true;
:: m[_pid] ? marker ->
received = true;
red = true;
sampled[_pid] = true;
fi
:: red && !sent && !received ->
if
:: m[NEXT(_pid)] ! marker ->
sent = true;
:: m[_pid] ? marker ->
received = true;
fi
:: red && !sent && received ->
m[NEXT(_pid)] ! marker;
sent = true;
:: red && sent && !received ->
m[_pid] ? marker;
received = true;
:: red && sent && received && !done[_pid] ->
skip;
:: red && received && sent && done[_pid] ->
goto s;
od
}
active proctype monitor() {
int i = 0;
do
:: i < N && !sampled[i] -> skip;
:: i < N && sampled[i] -> i++;
:: i == N ->
progress:
for (i in sampled) {
sampled[i] = false;
}
for (i in done) {
done[i] = true;
}
i = 0;
od
}
#define CHECK 1
byte flag[N];
active [N] proctype p() {
int j;
s1: skip;
s2: flag[_pid] = 1;
s3: j = 0;
do
:: j == N ->
break;
:: j < N && flag[j] <= 2 ->
j++;
:: j < N && flag[j] > 2 ->
skip;
od
s4: flag[_pid] = 3
s5: j = 0
do
:: j == N ->
goto s8;
:: j < N && flag[j] == 1 ->
goto s6;
:: j < N && flag[j] != 1 ->
j++;
od
s6: flag[_pid] = 2
s7: j = 0
do
:: j == N ->
j = 0;
:: j < N && flag[j] == 4 ->
break;
:: j < N && flag[j] != 4 ->
j++;
od
s8: flag[_pid] = 4
s9: j = 0;
do
:: j == _pid ->
break;
:: j < _pid && flag[j] <= 1 ->
j++;
:: j < _pid && flag[j] > 1 ->
skip;
od
s10: if
:: _pid == CHECK ->
progress: skip;
:: else ->
skip;
fi
s11: j = _pid + 1;
do
:: j == N ->
break;
:: j < N && (flag[j] <= 1 || flag[j] == 4) ->
j++;
:: j < N && (flag[j] == 2 || flag[j] == 3) ->
skip;
od
s12: flag[_pid] = 0
s13: goto s1;
}
#!/bin/bash
benchmarks=( 'Snapshot' 'Peterson' 'Lamport' 'Szymanski' 'LeaderElectionCR79' 'LeaderElectionDKR82' )
#benchmarks=( 'Lamport' )
nmax=5
#2 hours
time_soft=$(expr 2 \* 3600)
time_hard=$(expr $time_soft + 60)
#2 gigabyte
mem_soft=$(expr 2 \* 1024 \* 1024)
mem_hard=$(expr $mem_soft + 1024)
for benchmark in ${benchmarks[@]}; do
file=$benchmark.promela
bf=$benchmark.out
echo "n user system memory" >$bf
for n in $(seq 2 $nmax); do
echo "Testing $file with n=$n"
echo -n "$n " >>$bf
output=$file-$n.out
(
ulimit -S -t $time_soft
ulimit -H -t $time_hard
ulimit -S -v $mem_soft
ulimit -H -v $mem_hard
/usr/bin/time -f "%U %S %M" -a -o $bf ./run-spin $file $output $n
)
result=$?
if [[ result -eq 0 ]]; then
echo 'Positive result'
elif [[ result -eq 1 ]]; then
echo 'Negative result'
else
echo 'Error'
fi
done
done
#!/usr/bin/env bash
set -e
set -o pipefail
if [[ -z $1 ]]; then
echo "Error: No promela script given"
exit 4
fi
if [[ -z $2 ]]; then
echo "Error: No output file given"
exit 4
fi
if [[ -z $3 ]]; then
echo "Error: No process number given"
exit 4
fi
name=$1
basename=$( basename $name )
output=$2
trail="$basename.trail"
pan="/tmp/$basename.pan"
n=$3
nfair=$(expr \( \( $n + 2 \) / 4 + 2 \) )
exit_with() {
# cleanup compiling products from spin
rm -f pan.* _spin_nvr.tmp
# remove pan file and trail
rm -f "$pan" "$trail"
exit $1
}
parsing-error () {
echo "Parsing Error: $@"
exit_with 2
}
runtime-error () {
echo "Runtime Error: $@"
exit_with 3
}
# compile Promela model
# -a : generate pan
spin -a -DN=$n "$name" >"$output" || parsing-error "Spin failed"
# compile generated pan
# -DNOREDUCE : disables the partial order reduction algorithm
# -DNFAIR : specify the number of processes for fair scheduling
# -DNP : check for non-progress cycles
gcc -DNOREDUCE -DNFAIR=$nfair -DNP pan.c -o "$pan" || parsing-error "GCC failed"
# run pan
# -l : check for non-progress cycles
# -f : use weakly fair scheduling
# -n : do not print unreached states
# -m : search depth
"$pan" -l -f -n -m10000000 >>"$output" 2>&1 || runtime-error "PAN failed"
# check for errors in pan output
grep -e "^error:" "$output" && runtime-error "PAN error"
# check for trail
if [[ -e "$trail" ]]; then
exit_with 1
else
exit_with 0
fi
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