mirror of
https://github.com/neondatabase/neon.git
synced 2026-01-07 21:42:56 +00:00
fa909c27fc
The spec was written for the buggy protocol which we had before the one more similar to Raft was implemented. Update the spec with what we currently have. ref https://github.com/neondatabase/neon/issues/8699
50 lines
1.6 KiB
Bash
Executable File
50 lines
1.6 KiB
Bash
Executable File
#!/bin/bash
|
|
|
|
# Usage: ./modelcheck.sh <config_file> <spec_file>, e.g.
|
|
# ./modelcheck.sh models/MCProposerAcceptorStatic_p2_a3_t3_l3.cfg MCProposerAcceptorStatic.tla
|
|
CONFIG=$1
|
|
SPEC=$2
|
|
|
|
MEM=7G
|
|
TOOLSPATH="/opt/TLA+Toolbox/tla2tools.jar"
|
|
|
|
mkdir -p "tlc-results"
|
|
CONFIG_FILE=$(basename -- "$CONFIG")
|
|
outfilename="$SPEC-${CONFIG_FILE}-$(date --utc +%Y-%m-%d--%H-%M-%S)".log
|
|
outfile="tlc-results/$outfilename"
|
|
touch $outfile
|
|
|
|
# Save some info about the run.
|
|
GIT_REV=`git rev-parse --short HEAD`
|
|
INFO=`uname -a`
|
|
|
|
# First for Linux, second for Mac.
|
|
CPUNAMELinux=$(lscpu | grep 'Model name' | cut -f 2 -d ":" | awk '{$1=$1}1')
|
|
CPUCORESLinux=`nproc`
|
|
CPUNAMEMac=`sysctl -n machdep.cpu.brand_string`
|
|
CPUCORESMac=`sysctl -n machdep.cpu.thread_count`
|
|
|
|
echo "git revision: $GIT_REV" >> $outfile
|
|
echo "Platform: $INFO" >> $outfile
|
|
echo "CPU Info Linux: $CPUNAMELinux" >> $outfile
|
|
echo "CPU Cores Linux: $CPUCORESLinux" >> $outfile
|
|
echo "CPU Info Mac: $CPUNAMEMac" >> $outfile
|
|
echo "CPU Cores Mac: $CPUCORESMac" >> $outfile
|
|
echo "Spec: $SPEC" >> $outfile
|
|
echo "Config: $CONFIG" >> $outfile
|
|
echo "----" >> $outfile
|
|
cat $CONFIG >> $outfile
|
|
echo "" >> $outfile
|
|
echo "----" >> $outfile
|
|
echo "" >> $outfile
|
|
|
|
# see
|
|
# https://lamport.azurewebsites.net/tla/current-tools.pdf
|
|
# for TLC options.
|
|
# OffHeapDiskFPSet is the optimal fingerprint set implementation
|
|
# https://docs.tlapl.us/codebase:architecture#fingerprint_sets_fpsets
|
|
#
|
|
# Add -simulate to run in infinite simulation mode.
|
|
java -Xmx$MEM -XX:MaxDirectMemorySize=$MEM -XX:+UseParallelGC -Dtlc2.tool.fp.FPSet.impl=tlc2.tool.fp.OffHeapDiskFPSet \
|
|
-cp "${TOOLSPATH}" tlc2.TLC $SPEC -config $CONFIG -workers auto -gzip | tee -a $outfile
|