-
Notifications
You must be signed in to change notification settings - Fork 0
Expand file tree
/
Copy pathprofile.sh
More file actions
executable file
·59 lines (49 loc) · 2.05 KB
/
profile.sh
File metadata and controls
executable file
·59 lines (49 loc) · 2.05 KB
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
#!/usr/bin/env bash
# Receives at least three arguments: a name, a binary and one or more inputs
# The inputs can be either filenames (ending in .in) or direct input text to be piped to the binary
# The binary is run with each input, and its execution time and memory usage are recorded using GNU time
# The results are appended to profile.csv in the current directory
# The script can be run concurrently as it locks the CSV file when writing
if [[ $# -lt 3 ]]; then
echo "Usage: $0 name binary input1 [input2 ...]"
exit 1
fi
what="$1"
read -r -a binary <<< "$2"
shift 2
inputs=("$@")
# Find GNU time (gtime on macOS, time elsewhere)
TIME_CMD=$(command -v gtime || command -v time || true)
if [[ -z "$TIME_CMD" ]]; then
echo "GNU time not found. On Linux: 'apt install time'. On macOS: 'brew install gnu-time'."
exit 1
fi
CSV="profile.csv"
# Add header if new file
if [[ ! -f "$CSV" ]]; then
echo "what,input,user_time,sys_time,wall_time,max_rss,date" > "$CSV"
fi
for input in "${inputs[@]}"; do
if [[ -f "$input" && "$input" == *.in ]]; then
inputname=$(basename "$input" .in)
runout="bin/$what.$inputname.runout"
profile="bin/$what.$inputname.profile"
echo "Running ${binary[@]} with input file $input..."
"$TIME_CMD" -v ${binary[@]} < "$input" > "$runout" 2> "$profile"
else
runout="bin/$what.$input.runout"
profile="bin/$what.$input.profile"
echo "Running ${binary[@]} with input argument $input..."
echo "$input" | "$TIME_CMD" -v ${binary[@]} > "$runout" 2> "$profile"
fi
user_time=$(grep "User time" "$profile" | awk '{print $4}')
sys_time=$(grep "System time" "$profile" | awk '{print $4}')
wall_time=$(grep "Elapsed (wall clock)" "$profile" | awk '{print $8}')
max_rss=$(grep "Maximum resident set size" "$profile" | awk '{print $6}')
date=$(date +"%Y-%m-%d %H:%M:%S")
(
flock -x 200
echo "$what,$input,$user_time,$sys_time,$wall_time,$max_rss,$date" >> "$CSV"
) 200>>"$CSV"
done
echo "Profiling complete. Results saved in $CSV"