Skip to content
Snippets Groups Projects
Commit 70ff0db6 authored by Kostyantyn Vorobyov's avatar Kostyantyn Vorobyov
Browse files

Remove code related to performance evaluation

parent d3c12b60
No related branches found
No related tags found
No related merge requests found
Hide whitespace changes
Inline Side-by-side
Showing
with 0 additions and 714 deletions
src/plugins/e-acsl/.gitignore
+ 0
− 1
View file @ 70ff0db6
......@@ -73,6 +73,5 @@ top/
doc/doxygen/doxygen.cfg
doc/doxygen/html
doc/doxygen/warn.log
benchmarking/tools/fc-time
lib/libgmp-e-acsl.a
lib/libjemalloc-e-acsl.a
src/plugins/e-acsl/Makefile.in
+ 0
− 19
View file @ 70ff0db6
......@@ -118,25 +118,6 @@ clean::
endif
######################
# Benchmarking tools #
######################
EACSL_BM_SOURCES = $(wildcard $(PLUGIN_DIR)/benchmarking/tools/*.c)
EACSL_BM_BINARIES = $(patsubst %.c,%, $(EACSL_BM_SOURCES))
CFLAGS = -g3 -O2 -std=c11 -pedantic -Wall -Wno-unused-result
$(EACSL_BM_BINARIES): % : %.c
$(PRINT_CC) $@
$(CC) $(CFLAGS) -o $@ $^
all:: $(EACSL_BM_BINARIES)
clean::
$(PRINT_RM) benchmarking tools
$(RM) $(EACSL_BM_BINARIES)
################################################
# E-ACSL C Libs: libjemalloc, libgmp #
################################################
......
src/plugins/e-acsl/benchmarking/examples/plotting/dat/barplot.dat deleted 100644 → 0
+ 0
− 4
View file @ d3c12b60
Benchmark No-model Segment-model Bittree-model
grep 2 4.4 18
sed 3 9 16
diff 4 9.3 7.3
src/plugins/e-acsl/benchmarking/examples/plotting/dat/lineplot.dat deleted 100644 → 0
+ 0
− 11
View file @ d3c12b60
RUNS No-model Segment-model Bittree-model
1 1.1 4.6 8.6
2 2.3 9.2 13.8
3 1.0 9.9 11.2
4 1.9 4.3 6.9
5 3.4 6.9 12.5
6 5.4 20.4 33.4
7 8.1 21.8 36.7
8 11.6 23.7 16.2
9 16.6 40.8 22.7
10 1.15 7.4 8.1
src/plugins/e-acsl/benchmarking/examples/plotting/sample-plot.sh deleted 100755 → 0
+ 0
− 32
View file @ d3c12b60
#!/bin/sh
# Sample script showing usage of `bm.gnuplot` script
# Path to gnuplot script
BM_GNUPLOT="../../tools/bm.gnuplot"
# Build a line plot using lineplot.dat data file
gnuplot \
-e "BaseFile='dat/lineplot'" \
-e "Style='lines'" \
-e "WithOverheads=1" \
-e "PlotTitle='Sample line plot title'" \
-e "XLabel='Sample line plot label of X axis'" \
-e "YLabel='Sample line plot label of Y axis'" \
-e "OutputDir='.'" \
-e "WithOverheads='1'" \
$BM_GNUPLOT
# Build a histogram using barplot.dat data file
gnuplot \
-e "BaseFile='dat/barplot'" \
-e "Style='histogram'" \
-e "WithOverheads=1" \
-e "PlotTitle='Sample histogram title'" \
-e "XLabel='Sample histogram label of X axis'" \
-e "YLabel='Sample histogram label of Y axis'" \
-e "OutputDir='.'" \
-e "WithOverheads='1'" \
$BM_GNUPLOT
exit 0
src/plugins/e-acsl/benchmarking/tools/bm.gnuplot deleted 100755 → 0
+ 0
− 180
View file @ d3c12b60
#!/usr/bin/env gnuplot
##########################################################################
# #
# This file is part of the Frama-C's E-ACSL plug-in. #
# #
# Copyright (C) 2012-2016 #
# CEA (Commissariat à l'énergie atomique et aux énergies #
# alternatives) #
# #
# you can redistribute it and/or modify it under the terms of the GNU #
# Lesser General Public License as published by the Free Software #
# Foundation, version 2.1. #
# #
# It is distributed in the hope that it will be useful, #
# but WITHOUT ANY WARRANTY; without even the implied warranty of #
# MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the #
# GNU Lesser General Public License for more details. #
# #
# See the GNU Lesser General Public License version 2.1 #
# for more details (enclosed in the file license/LGPLv2.1). #
# #
##########################################################################
# Usage information of a script
#
# Gnuplot script for building line graphs and histograps
#
# The script should be invoked as follows:
# gnuplot \
# -e "BaseFile='<Base name of .dat file>' \
# -e "Style='<lines|histogram>' \
# -e "PlotTitle='<Optional: Plot title: [BaseFile]>'"
# -e "XLabel='<Optional: X-axis label: [""]>'"
# -e "YLabel='<Optional: Y-axis label: ["1st column title"]>'"
# -e "OutputDir='<Optional: directory where to place output files>'"
# -e "WithOverheads='<ANY>'"
# data.plot
#
# Arguments:
# - BaseName - base name of a data file with data to plot. This script expects
# BaseName.dat to exist and contain data. E.g., if the provided value is
# 'foo/bar', then foo/bar.dat file should exist
# - Style - a compulsory argument indicating the type of a plot to be constructed.
# Allowed values are 'histogram' or 'lines'. If 'lines' value is given then
# this script builds a line plot expecting the data file be of the form:
# YLabel XLabel1 XLabel2 ...
# YValue XValue1 XValue2 ...
# ...
# If 'histogram' argument is specified a data file is expected to be of the form:
# GroupLabel Label2 Label3 Label4
# Group1 Value1 Value2 Value3 ...
# Group2 Value1 Value2 Value3 ...
# ...
# - XLabel - optional string used a X-axis label
# - YLabel - optional string used a Y-axis label
# - PlotTitle - optional string used a plot title
# - OutputDir - optional directory for placement of resulting pdf files
# - WithOverheads - if any value is given to this argument then the script
# computes overheads relative to the values in the second column
# Check if a given file exists
file_exists(file) = system("test -f '".file."' && echo '1' || echo '0'") + 0
if (exists("Style") && (Style eq "histogram" && Style eq "lines")) {
print "ERROR: Unknown histogram style [histogram|lines]"
print "See inline comments for details"
exit 1
}
# Check if the base name of the datafile (name - extension .dat)
# is given via commandline
if (!exists("BaseFile")) {
print "ERROR: Variable 'BaseFile' should be set via commandline"
print "See inline comments for details"
exit
}
# Set datafile name
DataFile = BaseFile.'.dat'
# Check if it exists
if (!file_exists(DataFile)) {
print "ERROR: ".DataFile." not found."
print "See inline comments for details"
exit
}
# Unless specified the plot title is named after the base name of the file
if (!exists("PlotTitle"))
PlotTitle = BaseFile
# Unless specified the Y axis label is the leftmost column header
if (!exists("YLabel"))
YLabel = word(system(sprintf("head -n 1 %s", DataFile)),1)
# Unless specified Y label is empty
if (!exists("XLabel"))
XLabel = ""
# Fonts and background
Background = '#F7F7F7'
BaseFont = 'Arial,14'
TicsFont = "Arial,10"
LegendFont = "Arial,12"
SideLabelFont = "Arial-Bold,16"
# Line colours
set linetype 6 linewidth 2 linecolor rgb "#666633" pointtype 6 pointsize 0.7 # Dark yellow
set linetype 5 linewidth 2 linecolor rgb "#006633" pointtype 5 pointsize 0.7 # Green
set linetype 4 linewidth 2 linecolor rgb "#000000" pointtype 4 pointsize 0.7 # Black
set linetype 3 linewidth 2 linecolor rgb "#990099" pointtype 3 pointsize 0.7 # Magenta
set linetype 2 linewidth 2 linecolor rgb "#000066" pointtype 8 pointsize 0.7 # Dark blue
set linetype 1 linewidth 2 linecolor rgb "#990000" pointtype 7 pointsize 0.7 # Maroon
# Use the postscript terminal, as a PDF one is not fully featured
set terminal postscript landscape size 10,7 enhanced color font BaseFont
# Set background colour for the plot area
set object 1 rectangle from graph 0, graph 0 to graph 1, graph 1 behind fc rgbcolor Background fs noborder
# Set font for ticks and make them appear outside
# nomirror removes x2ticks and y2ticks (top and right)
set ytics font TicsFont out nomirror
set xtics font TicsFont out nomirror
set autoscale
# Legend font
set key on horizontal font LegendFont
# PlotTitle variable should come from environment via -e
set title PlotTitle
# Enable fonts for side labels
set xlabel XLabel font SideLabelFont
set ylabel YLabel font SideLabelFont
# Enable macros
set macros
PsFile = BaseFile.'.ps'
PdfFile = BaseFile.'.pdf'
if (exists("OutputDir")) {
PsFile = OutputDir."/".system("basename ".DataFile)
PdfFile = OutputDir."/".system("basename ".PdfFile)
}
Columns=`tail -n 1 @DataFile | wc -w`
# Set output file command
set output PsFile
# Overhead plotting function
# nat - time of an original executable
# mod -= time of the modified executable
# If WithOverheads var is defined then compute overheads, otherwise plot as is
ovh(nat, mod) = exists("WithOverheads") ? mod/nat : mod
###################
# Plotting
###################
# Build a line plot
if (Style eq "lines") {
plot for [COL = 2:Columns] DataFile \
using 1:(ovh(column(2), column(COL))) title columnheader(COL) with linespoints
}
# Build a histogram
if (Style eq "histogram") {
set yrange [0:]
set style data histogram
set style fill solid border -1
plot for [COL=2:Columns] DataFile using (ovh(column(2), column(COL))):xticlabels(1) title columnheader
}
# At this point postscript is generated, create PDF
!ps2pdf @PsFile @PdfFile
!rm @PsFile
src/plugins/e-acsl/benchmarking/tools/fc-time.c deleted 100644 → 0
+ 0
− 467
View file @ d3c12b60
/* Copyright (C) 1990, 91, 92, 93, 96 Free Software Foundation, Inc.
*
* This program is free software; you can redistribute it and/or modify
* it under the terms of the GNU General Public License as published by
* the Free Software Foundation; either version 2, or (at your option)
* any later version.
*
* This program is distributed in the hope that it will be useful,
* but WITHOUT ANY WARRANTY; without even the implied warranty of
* MERCHANTABILITY or FITNESS FOR A PARTICULAR PURPOSE. See the
* GNU General Public License for more details.
*
* You should have received a copy of the GNU General Public License
* along with this program; if not, write to the Free Software
* Foundation, Inc., 59 Temple Place - Suite 330, Boston, MA
* 02111-1307, USA. */
/* fc-time -- mesaure real time of an executed command */
#include <stdlib.h>
#include <string.h>
#include <stdio.h>
#include <unistd.h>
#include <stdarg.h>
#include <errno.h>
#include <getopt.h>
#include <signal.h>
#include <sys/wait.h>
#include <sys/time.h>
#include <sys/types.h>
#include <sys/resource.h>
/* Extra declarations to suppress warnings in -std=c99 or -std=c11 modes */
int kill(pid_t pid, int sig);
const char *strdup(const char *s);
pid_t wait4(pid_t pid, int *status, int options, struct rusage *rusage);
typedef void (*sighandler_t) (int);
#ifdef __linux__
#include <linux/limits.h>
#endif
/* Minimal reported runtime */
#define MINTIME 0.001
/* Minimal time limit after which a program is forcibly terminated */
#define MINLIMIT 0.1
/* Name of the output file. Only used if -o option is given. */
static const char *outfile;
/* Output stream, defaults to stderr */
static FILE *outfp;
/* If true, append to `outfile' rather than truncating it */
static int append;
/* Program name */
static const char * program_name = NULL;
/* Time limit in seconds */
long double time_limit = 0;
/* Verbosity level */
int verbose;
/* Gather memory stats via /proc/[pid]/statm */
int memory;
/* Struct for holding the results of memory statistics */
struct statistics {
unsigned long vsize; /* (1) total program size (page size) */
unsigned long rss; /* (2) resident set size (page size) */
unsigned long share; /* (3) shared pages (page size) */
unsigned long text; /* (4) text (page size) */
unsigned long lib; /* (5) library (page size) */
unsigned long data; /* (6) data + stack (page size) */
/* The number of times a procfile has been read */
unsigned long count;
int status; /* exit status */
struct timeval start; /* timestamp of program start */
struct timeval finish; /* timestamp of program end */
struct rusage resusage; /* struct for use with getrusage */
};
/* Name of the used memory stat file */
char procfile [PATH_MAX];
/* Memory stat file stream */
FILE *procfp = NULL;
/* Default report format string */
char *report_format = "%e\n";
/* Memory size units */
#define B_SZ 1
#define KB_SZ 1024
#define MB_SZ (1024*KB_SZ)
#define GB_SZ (1024*MB_SZ)
/* Reported block unit */
static int block_size;
/* Short options */
static const char *shortopts = "+ao:l:vmB:f:";
/* Long options */
static struct option longopts[] = {
{"limit", required_argument, NULL, 'l'},
{"verbose", no_argument, NULL, 'v'},
{"append", no_argument, NULL, 'a'},
{"help", no_argument, NULL, 'h'},
{"output-file", required_argument, NULL, 'o'},
{"memory", required_argument, NULL, 'm'},
{"block-bize", required_argument, NULL, 'B'},
{"format", required_argument, NULL, 'f'},
{NULL, no_argument, NULL, 0}
};
/* Print help page and exit */
static void usage (FILE *stream, int status) {
fprintf(stream,
"NAME:\n"
" fc-time -- measure execution time and/or memory consumption of a command\n"
"SYNOPSIS:\n"
" fc-time [options] command [arg...]\n"
"OPTIONS:\n"
" -h, --help print this help page and exit.\n"
" -o FILE send output to a named file [stderr].\n"
" -a, --append append an output file without truncating it (with -o).\n"
" -l SECONDS limit in seconds arter which a program is terminated\n"
" even if it is not finshed. The limit needs to be specified with seconds\n"
" precision.\n"
" -m, --memory - collect memory statistics [disabled].\n"
" -v warn if a program has been terminated via -l option.\n"
" -f printf-like report format string.\n"
" %%e - elapsed real time [seconds:milliseconds].\n"
" %%E - same as %%e\n"
" %%U - total time spent in user mode [seconds:milliseconds].\n"
" %%S - total time spent in kernel mode [seconds:milliseconds].\n"
" %%v - virtual memory consumption peak [bytes].\n"
" %%t - text segment size [bytes].\n"
" %%d - data + stack segments sizes [bytes].\n"
" %%r - maximum resident set size [bytes].\n"
" Memory-related measurements (e.g., virtual memory consumption or rss)\n"
" are disabled by default. Unless -m option is used they are reported as\n"
" zeroes. Computing memory peaks may result in the increase of runtime.\n"
" -B, --byte-size=<B|KB|MB|GB> - change reported memory unit [B].\n");
exit(status);
}
/* Error reporting function. Replica of the GNU error (3).
* Added for portability purposes. */
static void error(int status, int errnum, const char *format, ...) {
fflush(stderr); /* Flush streams */
fflush(stdout);
if (program_name) /* Report program name */
fprintf(stderr, "%s: ", program_name);
va_list va; /* Pass the error message given by the user */
va_start(va, format);
vfprintf(stderr, format, va);
va_end(va);
if (errnum) /* Report error given via errno */
fprintf(stderr, ": %s", strerror(errnum));
/* Add the newline at the end */
fprintf(stderr, "\n");
/* Exit if status is a non-zero */
if (status)
exit(status);
}
#define warning(_fmt, ...) \
if (verbose) { \
error(0, 0, _fmt, __VA_ARGS__); \
}
/* Initialize the options and parse the command line arguments.
Also note the position in ARGV where the command to time starts. */
static const char ** getargs (int argc, char **argv) {
int optc;
outfile = NULL;
outfp = stderr; /* Output to stderr by default */
append = 0;
verbose = 0;
memory = 0;
block_size = KB_SZ;
while ((optc = getopt_long(argc, argv, shortopts, longopts, NULL)) != EOF) {
switch (optc) {
case 'a':
append = 1;
break;
case 'h':
usage (stdout, 0);
case 'o':
outfile = optarg;
break;
case 'v':
verbose = 1;
break;
case 'm':
memory = 1;
break;
case 'f':
report_format = (char*)strdup(optarg);
break;
case 'l':
/* Convert time limit to seconds */
time_limit = strtold(optarg, NULL);
/* Abort if the time limit provided at input is invalid or less than
the threshold given by MINLIMIT */
if (time_limit < MINLIMIT)
error(1, errno, "Bad time limit specification: '%s'."
" Expected positive number greater than %0.3f", optarg, MINLIMIT);
/* Detect over- or underflow */
if (errno == ERANGE)
error(1, errno, "%s", optarg);
break;
case 'B': { /* reported unit size */
switch(optarg[0]) {
case 'B': /* report memory in bytes */
block_size = B_SZ;
break;
case 'K': /* ... kilobytes */
block_size = KB_SZ;
break;
case 'M': /* ... megabytes */
block_size = MB_SZ;
break;
case 'G': /* ... gigabytes */
block_size = GB_SZ;
break;
default:
error(1, 0, "Bad block size specification (%s), expected B,K,M or G", optarg);
}
break;
}
default:
usage (stderr, 1);
}
}
if (optind == argc)
usage (stderr, 1);
if (outfile) {
if (append)
outfp = fopen (outfile, "a");
else
outfp = fopen (outfile, "w");
if (outfp == NULL)
error(1, errno, "%s", outfile);
}
return (const char **) &argv[optind];
}
/* Convert timeval into a double with millisecond precision */
#define TIMEWMS(_tval) (_tval.tv_sec + (_tval.tv_usec/1000000.0))
#define TIMEDIFF(_finish,_start) (TIMEWMS(_finish) - TIMEWMS(_start))
/* Assign the max of _old and _new to _old */
#define assignmax(_old, _new) _old = (_old > _new) ? _old : _new
/* Observe the child's execution, collect memory stats and terminate the
* execution if the time limit is exceeded
*
* - This function is invoked only if either `time_limit' or `memory'
* are specified, i.e., a user requests either to collect memory stats
* or terminate the execution upon exceeding some time limit.
*
* - For the case when a time limit is given but memory statistics do not
* need to be collected the parent process checks if the time limit is
* exceeded each second. This is to limit the interference
*
* - If memory stats are collected, then checking time limit and reading
* procfile is done in a cycle without sleeping periods. This may slightly
* extend the execution of the program
*/
int observe(pid_t chpid, struct statistics * stats) {
int status;
pid_t rpid;
while (!(rpid = wait4(chpid, &status, WNOHANG, &stats->resusage))) {
gettimeofday(&stats->finish, NULL);
if (time_limit && TIMEDIFF(stats->finish, stats->start) > time_limit) {
warning("Warning: Attempting graceful termination due exceeded time "
"limit of %0.2Lf seconds", "", time_limit);
kill(chpid, SIGTERM);
break;
} else {
/* No mem stats need to be collected, sleep for one second */
if (!memory) {
sleep(1);
/* Mem stats need to be collected */
} else {
unsigned long vsize, rss, share, text, lib, data;
/* Open and read process file */
procfp = fopen(procfile, "r");
if (!procfp)
error(1, errno, "cannot open process memory stat file %s", procfile);
fscanf(procfp, "%lu %lu %lu %lu %lu %lu",
&vsize, &rss, &share, &text, &lib, &data);
assignmax(stats->vsize, vsize);
assignmax(stats->rss, rss);
assignmax(stats->share, share);
assignmax(stats->text, text);
assignmax(stats->lib, lib);
assignmax(stats->data, data);
fclose(procfp);
stats->count++;
}
}
}
if (rpid == -1)
return 0;
return 1;
}
/* Run command and return statistics on it. */
static int run_command (const char ** cmd) {
pid_t pid = 0; /* Pid of child */
int status = 0; /* Status of a child */
sighandler_t interrupt_signal, quit_signal;
struct statistics stats;
memset(&stats, 0, sizeof(struct statistics));
/* Fork the child process */
pid = fork();
/* Copy the name of the stat file to the `procfile` global */
sprintf(procfile, "/proc/%d/statm", pid);
/* Start measuring real time */
gettimeofday(&stats.start, NULL);
if (pid < 0) {
error(1, errno, "cannot fork");
} else if (pid == 0) { /* If child. */
execvp(cmd[0], (char *const*) cmd);
error(0, errno, "cannot run %s", cmd[0]);
exit(errno == ENOENT ? 127 : 126);
}
/* Have signals kill the child but not self */
interrupt_signal = signal(SIGINT, SIG_IGN);
quit_signal = signal(SIGQUIT, SIG_IGN);
/* Time limit has been specified. Observe execution of the child process
* and terminate the program after the time limit has been exceeded. */
if (time_limit || memory) {
if (observe(pid, &stats) == 0)
error(1, errno, "error waiting for child process");
/* No time limit given. Run the program as is and compute the runtime after
* the process terminates. */
} else {
pid_t rpid = wait4(pid, &status, 0, &stats.resusage);
gettimeofday(&stats.finish, NULL);
if (rpid == -1)
error (1, errno, "error waiting for child process");
}
/* Re-enable signals. */
signal(SIGINT, interrupt_signal);
signal(SIGQUIT, quit_signal);
/* Format string for report */
char *fmt = report_format;
/* Page size (/proc/[pid]/statm) reports sizes in pages */
long pagesz = sysconf(_SC_PAGESIZE);
while(*fmt != '\0') {
switch(*fmt) {
case '%': {
fmt++;
switch (*fmt) {
/* Elapsed time with millisecond precition */
case 'E':
case 'e': {
double elapsed = TIMEWMS(stats.finish) - TIMEWMS(stats.start);
fprintf(outfp, "%0.3f", (elapsed > MINTIME) ? elapsed : MINTIME);
break;
}
/* Time spent in kernel mode */
case 'S':
fprintf(outfp, "%0.3f", TIMEWMS(stats.resusage.ru_stime));
break;
/* Time spent in user mode */
case 'U':
fprintf(outfp, "%0.3f", TIMEWMS(stats.resusage.ru_utime));
break;
case 'v':
fprintf(outfp, "%lu", (stats.vsize*pagesz)/block_size);
break;
case 'd':
fprintf(outfp, "%lu", (stats.data*pagesz)/block_size);
break;
case 't':
fprintf(outfp, "%lu", (stats.text*pagesz)/block_size);
break;
case 'r':
fprintf(outfp, "%lu", (stats.rss*pagesz)/block_size);
break;
default:
fprintf(outfp, "???");
break;
}
break;
}
case '\\': {
fmt++;
switch (*fmt) {
case 't':
putc ('\t', outfp);
break;
case 'n':
putc ('\n', outfp);
break;
case '\\':
putc ('\\', outfp);
break;
default:
putc ('?', outfp);
putc ('\\', outfp);
putc (*fmt, outfp);
}
break;
}
default: {
putc (*fmt, outfp);
}
}
fmt++;
}
fflush(outfp);
/* ... and return the status of the child */
return status;
}
int main (int argc, char **argv) {
program_name = *argv;
const char **command_line = getargs(argc, argv);
int status = run_command(command_line);
/* Examining exit status of wait */
if (WIFSTOPPED(status))
exit(WSTOPSIG(status));
else if (WIFSIGNALED(status))
exit(WTERMSIG(status));
else if (WIFEXITED(status))
exit(WEXITSTATUS(status));
return 0;
}
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