diff options
| -rw-r--r-- | tools/verification/rv/Makefile | 119 | ||||
| -rw-r--r-- | tools/verification/rv/README.txt | 38 | ||||
| -rw-r--r-- | tools/verification/rv/include/rv.h | 12 | ||||
| -rw-r--r-- | tools/verification/rv/include/trace.h | 16 | ||||
| -rw-r--r-- | tools/verification/rv/include/utils.h | 8 | ||||
| -rw-r--r-- | tools/verification/rv/src/rv.c | 185 | ||||
| -rw-r--r-- | tools/verification/rv/src/trace.c | 133 | ||||
| -rw-r--r-- | tools/verification/rv/src/utils.c | 47 |
8 files changed, 558 insertions, 0 deletions
diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile new file mode 100644 index 000000000000..1de111ac2641 --- /dev/null +++ b/tools/verification/rv/Makefile @@ -0,0 +1,119 @@ +NAME := rv +# Follow the kernel version +VERSION := $(shell cat VERSION 2> /dev/null || make -sC ../../.. kernelversion | grep -v make) + +# From libtracefs: +# Makefiles suck: This macro sets a default value of $(2) for the +# variable named by $(1), unless the variable has been set by +# environment or command line. This is necessary for CC and AR +# because make sets default values, so the simpler ?= approach +# won't work as expected. +define allow-override + $(if $(or $(findstring environment,$(origin $(1))),\ + $(findstring command line,$(origin $(1)))),,\ + $(eval $(1) = $(2))) +endef + +# Allow setting CC and AR, or setting CROSS_COMPILE as a prefix. +$(call allow-override,CC,$(CROSS_COMPILE)gcc) +$(call allow-override,AR,$(CROSS_COMPILE)ar) +$(call allow-override,STRIP,$(CROSS_COMPILE)strip) +$(call allow-override,PKG_CONFIG,pkg-config) +$(call allow-override,LD_SO_CONF_PATH,/etc/ld.so.conf.d/) +$(call allow-override,LDCONFIG,ldconfig) + +INSTALL = install +MKDIR = mkdir +FOPTS := -flto=auto -ffat-lto-objects -fexceptions -fstack-protector-strong \ + -fasynchronous-unwind-tables -fstack-clash-protection +WOPTS := -Wall -Werror=format-security -Wp,-D_FORTIFY_SOURCE=2 -Wp,-D_GLIBCXX_ASSERTIONS -Wno-maybe-uninitialized + +TRACEFS_HEADERS := $$($(PKG_CONFIG) --cflags libtracefs) + +CFLAGS := -O -g -DVERSION=\"$(VERSION)\" $(FOPTS) $(MOPTS) $(WOPTS) $(TRACEFS_HEADERS) $(EXTRA_CFLAGS) -I include +LDFLAGS := -ggdb $(EXTRA_LDFLAGS) +LIBS := $$($(PKG_CONFIG) --libs libtracefs) + +SRC := $(wildcard src/*.c) +HDR := $(wildcard src/*.h) +OBJ := $(SRC:.c=.o) +DIRS := src +FILES := Makefile README.txt +CEXT := bz2 +TARBALL := $(NAME)-$(VERSION).tar.$(CEXT) +TAROPTS := -cvjf $(TARBALL) +BINDIR := /usr/bin +DATADIR := /usr/share +MANDIR := $(DATADIR)/man +LICDIR := $(DATADIR)/licenses +SRCTREE := $(or $(BUILD_SRC),$(CURDIR)) + +LIBTRACEEVENT_MIN_VERSION = 1.5 +LIBTRACEFS_MIN_VERSION = 1.3 + +.PHONY: all warnings show_warnings +all: warnings rv + +TEST_LIBTRACEEVENT = $(shell sh -c "$(PKG_CONFIG) --atleast-version $(LIBTRACEEVENT_MIN_VERSION) libtraceevent > /dev/null 2>&1 || echo n") +ifeq ("$(TEST_LIBTRACEEVENT)", "n") +WARNINGS = show_warnings +MISSING_LIBS += echo "** libtraceevent version $(LIBTRACEEVENT_MIN_VERSION) or higher"; +MISSING_PACKAGES += "libtraceevent-devel" +MISSING_SOURCE += echo "** https://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git/ "; +endif + +TEST_LIBTRACEFS = $(shell sh -c "$(PKG_CONFIG) --atleast-version $(LIBTRACEFS_MIN_VERSION) libtracefs > /dev/null 2>&1 || echo n") +ifeq ("$(TEST_LIBTRACEFS)", "n") +WARNINGS = show_warnings +MISSING_LIBS += echo "** libtracefs version $(LIBTRACEFS_MIN_VERSION) or higher"; +MISSING_PACKAGES += "libtracefs-devel" +MISSING_SOURCE += echo "** https://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git/ "; +endif + +define show_dependencies + @echo "********************************************"; \ + echo "** NOTICE: Failed build dependencies"; \ + echo "**"; \ + echo "** Required Libraries:"; \ + $(MISSING_LIBS) \ + echo "**"; \ + echo "** Consider installing the latest libtracefs from your"; \ + echo "** distribution, e.g., 'dnf install $(MISSING_PACKAGES)' on Fedora,"; \ + echo "** or from source:"; \ + echo "**"; \ + $(MISSING_SOURCE) \ + echo "**"; \ + echo "********************************************" +endef + +show_warnings: + $(call show_dependencies); + +ifneq ("$(WARNINGS)", "") +ERROR_OUT = $(error Please add the necessary dependencies) + +warnings: $(WARNINGS) + $(ERROR_OUT) +endif + +rv: $(OBJ) + $(CC) -o rv $(LDFLAGS) $(OBJ) $(LIBS) + +.PHONY: install +install: + $(MKDIR) -p $(DESTDIR)$(BINDIR) + $(INSTALL) rv -m 755 $(DESTDIR)$(BINDIR) + $(STRIP) $(DESTDIR)$(BINDIR)/rv + +.PHONY: clean tarball +clean: + @test ! -f rv || rm rv + @test ! -f $(TARBALL) || rm -f $(TARBALL) + @rm -rf *~ $(OBJ) *.tar.$(CEXT) + +tarball: clean + rm -rf $(NAME)-$(VERSION) && mkdir $(NAME)-$(VERSION) + echo $(VERSION) > $(NAME)-$(VERSION)/VERSION + cp -r $(DIRS) $(FILES) $(NAME)-$(VERSION) + tar $(TAROPTS) --exclude='*~' $(NAME)-$(VERSION) + rm -rf $(NAME)-$(VERSION) diff --git a/tools/verification/rv/README.txt b/tools/verification/rv/README.txt new file mode 100644 index 000000000000..e96be0dfff59 --- /dev/null +++ b/tools/verification/rv/README.txt @@ -0,0 +1,38 @@ +RV: Runtime Verification + +Runtime Verification (RV) is a lightweight (yet rigorous) method that +complements classical exhaustive verification techniques (such as model +checking and theorem proving) with a more practical approach for +complex systems. + +The rv tool is the interface for a collection of monitors that aim +analysing the logical and timing behavior of Linux. + +Installing RV + +RV depends on the following libraries and tools: + + - libtracefs + - libtraceevent + +It also depends on python3-docutils to compile man pages. + +For development, we suggest the following steps for compiling rtla: + + $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtraceevent.git + $ cd libtraceevent/ + $ make + $ sudo make install + $ cd .. + $ git clone git://git.kernel.org/pub/scm/libs/libtrace/libtracefs.git + $ cd libtracefs/ + $ make + $ sudo make install + $ cd .. + $ cd $rv_src + $ make + $ sudo make install + +For further information, please see rv manpage and the kernel documentation: + Runtime Verification: + Documentation/trace/rv/runtime-verification.rst diff --git a/tools/verification/rv/include/rv.h b/tools/verification/rv/include/rv.h new file mode 100644 index 000000000000..770fd6da3610 --- /dev/null +++ b/tools/verification/rv/include/rv.h @@ -0,0 +1,12 @@ +// SPDX-License-Identifier: GPL-2.0 + +#define MAX_DESCRIPTION 1024 +#define MAX_DA_NAME_LEN 24 + +struct monitor { + char name[MAX_DA_NAME_LEN]; + char desc[MAX_DESCRIPTION]; + int enabled; +}; + +int should_stop(void); diff --git a/tools/verification/rv/include/trace.h b/tools/verification/rv/include/trace.h new file mode 100644 index 000000000000..8d89e8c303fa --- /dev/null +++ b/tools/verification/rv/include/trace.h @@ -0,0 +1,16 @@ +// SPDX-License-Identifier: GPL-2.0 + +#include <tracefs.h> + +struct trace_instance { + struct tracefs_instance *inst; + struct tep_handle *tep; + struct trace_seq *seq; +}; + +int trace_instance_init(struct trace_instance *trace, char *name); +int trace_instance_start(struct trace_instance *trace); +void trace_instance_destroy(struct trace_instance *trace); + +int collect_registered_events(struct tep_event *event, struct tep_record *record, + int cpu, void *context); diff --git a/tools/verification/rv/include/utils.h b/tools/verification/rv/include/utils.h new file mode 100644 index 000000000000..f24ae8282bd2 --- /dev/null +++ b/tools/verification/rv/include/utils.h @@ -0,0 +1,8 @@ +// SPDX-License-Identifier: GPL-2.0 + +#define MAX_PATH 1024 + +void debug_msg(const char *fmt, ...); +void err_msg(const char *fmt, ...); + +extern int config_debug; diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c new file mode 100644 index 000000000000..a9ea1c891ce0 --- /dev/null +++ b/tools/verification/rv/src/rv.c @@ -0,0 +1,185 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * rv tool, the interface for the Linux kernel RV subsystem and home of + * user-space controlled monitors. + * + * Copyright (C) 2022 Red Hat Inc, Daniel Bristot de Oliveira <bristot@kernel.org> + */ + +#include <stdlib.h> +#include <signal.h> +#include <unistd.h> + +#include <trace.h> +#include <utils.h> + +static int stop_session; + +/* + * stop_rv - tell monitors to stop + */ +static void stop_rv(int sig) +{ + stop_session = 1; +} + +/** + * should_stop - check if the monitor should stop. + * + * Returns 1 if the monitor should stop, 0 otherwise. + */ +int should_stop(void) +{ + return stop_session; +} + +/* + * rv_list - list all available monitors + */ +static void rv_list(int argc, char **argv) +{ + static const char *const usage[] = { + "", + " usage: rv list [-h]", + "", + " list all available monitors", + "", + " -h/--help: print this menu", + NULL, + }; + int i; + + if (argc > 1) { + fprintf(stderr, "rv version %s\n", VERSION); + + /* more than 1 is always usage */ + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + + /* but only -h is valid */ + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) + exit(0); + else + exit(1); + } + + exit(0); +} + +/* + * rv_mon - try to run a monitor passed as argument + */ +static void rv_mon(int argc, char **argv) +{ + char *monitor_name; + int i, run; + + static const char *const usage[] = { + "", + " usage: rv mon [-h] monitor [monitor options]", + "", + " run a monitor", + "", + " -h/--help: print this menu", + "", + " monitor [monitor options]: the monitor, passing", + " the arguments to the [monitor options]", + NULL, + }; + + /* requires at least one argument */ + if (argc == 1) { + + fprintf(stderr, "rv version %s\n", VERSION); + + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + exit(1); + } else if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) { + + fprintf(stderr, "rv version %s\n", VERSION); + + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + exit(0); + } + + monitor_name = argv[1]; + /* + * Call all possible monitor implementations, looking + * for the [monitor]. + */ + + if (!run) + err_msg("rv: monitor %s does not exist\n", monitor_name); + exit(!run); +} + +static void usage(int exit_val, const char *fmt, ...) +{ + char message[1024]; + va_list ap; + int i; + + static const char *const usage[] = { + "", + " usage: rv command [-h] [command_options]", + "", + " -h/--help: print this menu", + "", + " command: run one of the following command:", + " list: list all available monitors", + " mon: run a monitor", + "", + " [command options]: each command has its own set of options", + " run rv command -h for further information", + NULL, + }; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stderr, "rv version %s: %s\n", VERSION, message); + + for (i = 0; usage[i]; i++) + fprintf(stderr, "%s\n", usage[i]); + + exit(exit_val); +} + +/* + * main - select which main sending the command + * + * main itself redirects the arguments to the sub-commands + * to handle the options. + * + * subcommands should exit. + */ +int main(int argc, char **argv) +{ + if (geteuid()) + usage(1, "%s needs root permission", argv[0]); + + if (argc <= 1) + usage(1, "%s requires a command", argv[0]); + + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) + usage(0, "help"); + + if (!strcmp(argv[1], "list")) + rv_list(--argc, &argv[1]); + + if (!strcmp(argv[1], "mon")) { + /* + * monitor's main should monitor should_stop() function. + * and exit. + */ + signal(SIGINT, stop_rv); + + rv_mon(argc - 1, &argv[1]); + } + + /* invalid sub-command */ + usage(1, "%s does not know the %s command, old version?", argv[0], argv[1]); +} diff --git a/tools/verification/rv/src/trace.c b/tools/verification/rv/src/trace.c new file mode 100644 index 000000000000..2c7deed47f8d --- /dev/null +++ b/tools/verification/rv/src/trace.c @@ -0,0 +1,133 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * trace helpers. + * + * Copyright (C) 2022 Red Hat Inc, Daniel Bristot de Oliveira <bristot@kernel.org> + */ + +#include <sys/sendfile.h> +#include <tracefs.h> +#include <signal.h> +#include <stdlib.h> +#include <unistd.h> +#include <errno.h> + +#include <rv.h> +#include <trace.h> +#include <utils.h> + +/* + * create_instance - create a trace instance with *instance_name + */ +static struct tracefs_instance *create_instance(char *instance_name) +{ + return tracefs_instance_create(instance_name); +} + +/* + * destroy_instance - remove a trace instance and free the data + */ +static void destroy_instance(struct tracefs_instance *inst) +{ + tracefs_instance_destroy(inst); + tracefs_instance_free(inst); +} + +/** + * collect_registered_events - call the existing callback function for the event + * + * If an event has a registered callback function, call it. + * Otherwise, ignore the event. + * + * Returns 0 if the event was collected, 1 if the tool should stop collecting trace. + */ +int +collect_registered_events(struct tep_event *event, struct tep_record *record, + int cpu, void *context) +{ + struct trace_instance *trace = context; + struct trace_seq *s = trace->seq; + + if (should_stop()) + return 1; + + if (!event->handler) + return 0; + + event->handler(s, record, event, context); + + return 0; +} + +/** + * trace_instance_destroy - destroy and free a rv trace instance + */ +void trace_instance_destroy(struct trace_instance *trace) +{ + if (trace->inst) { + destroy_instance(trace->inst); + trace->inst = NULL; + } + + if (trace->seq) { + free(trace->seq); + trace->seq = NULL; + } + + if (trace->tep) { + tep_free(trace->tep); + trace->tep = NULL; + } +} + +/** + * trace_instance_init - create an trace instance + * + * It is more than the tracefs instance, as it contains other + * things required for the tracing, such as the local events and + * a seq file. + * + * Note that the trace instance is returned disabled. This allows + * the tool to apply some other configs, like setting priority + * to the kernel threads, before starting generating trace entries. + * + * Returns 0 on success, non-zero otherwise. + */ +int trace_instance_init(struct trace_instance *trace, char *name) +{ + trace->seq = calloc(1, sizeof(*trace->seq)); + if (!trace->seq) + goto out_err; + + trace_seq_init(trace->seq); + + trace->inst = create_instance(name); + if (!trace->inst) + goto out_err; + + trace->tep = tracefs_local_events(NULL); + if (!trace->tep) + goto out_err; + + /* + * Let the main enable the record after setting some other + * things such as the priority of the tracer's threads. + */ + tracefs_trace_off(trace->inst); + + return 0; + +out_err: + trace_instance_destroy(trace); + return 1; +} + +/** + * trace_instance_start - start tracing a given rv instance + * + * Returns 0 on success, -1 otherwise. + */ +int trace_instance_start(struct trace_instance *trace) +{ + return tracefs_trace_on(trace->inst); +} diff --git a/tools/verification/rv/src/utils.c b/tools/verification/rv/src/utils.c new file mode 100644 index 000000000000..5677b439dc2f --- /dev/null +++ b/tools/verification/rv/src/utils.c @@ -0,0 +1,47 @@ +// SPDX-License-Identifier: GPL-2.0 +/* + * util functions. + * + * Copyright (C) 2022 Red Hat Inc, Daniel Bristot de Oliveira <bristot@kernel.org> + */ + +#include <stdarg.h> +#include <stdio.h> +#include <utils.h> + +int config_debug; + +#define MAX_MSG_LENGTH 1024 + +/** + * err_msg - print an error message to the stderr + */ +void err_msg(const char *fmt, ...) +{ + char message[MAX_MSG_LENGTH]; + va_list ap; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stderr, "%s", message); +} + +/** + * debug_msg - print a debug message to stderr if debug is set + */ +void debug_msg(const char *fmt, ...) +{ + char message[MAX_MSG_LENGTH]; + va_list ap; + + if (!config_debug) + return; + + va_start(ap, fmt); + vsnprintf(message, sizeof(message), fmt, ap); + va_end(ap); + + fprintf(stderr, "%s", message); +} |