diff options
Diffstat (limited to 'tools/verification')
41 files changed, 2148 insertions, 614 deletions
diff --git a/tools/verification/dot2/Makefile b/tools/verification/dot2/Makefile deleted file mode 100644 index 021beb07a521..000000000000 --- a/tools/verification/dot2/Makefile +++ /dev/null @@ -1,26 +0,0 @@ -INSTALL=install - -prefix ?= /usr -bindir ?= $(prefix)/bin -mandir ?= $(prefix)/share/man -miscdir ?= $(prefix)/share/dot2 -srcdir ?= $(prefix)/src - -PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') - -.PHONY: all -all: - -.PHONY: clean -clean: - -.PHONY: install -install: - $(INSTALL) automata.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/automata.py - $(INSTALL) dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2c.py - $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ - $(INSTALL) dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/dot2/dot2k.py - $(INSTALL) dot2k -D -m 755 $(DESTDIR)$(bindir)/ - - mkdir -p ${miscdir}/ - cp -rp dot2k_templates $(DESTDIR)$(miscdir)/ diff --git a/tools/verification/dot2/dot2k b/tools/verification/dot2/dot2k deleted file mode 100644 index d4d7e52d549e..000000000000 --- a/tools/verification/dot2/dot2k +++ /dev/null @@ -1,45 +0,0 @@ -#!/usr/bin/env python3 -# SPDX-License-Identifier: GPL-2.0-only -# -# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> -# -# dot2k: transform dot files into a monitor for the Linux kernel. -# -# For further information, see: -# Documentation/trace/rv/da_monitor_synthesis.rst - -if __name__ == '__main__': - from dot2.dot2k import dot2k - import argparse - import ntpath - import os - import platform - import sys - - parser = argparse.ArgumentParser(description='transform .dot file into kernel rv monitor') - parser.add_argument('-d', "--dot", dest="dot_file", required=True) - parser.add_argument('-t', "--monitor_type", dest="monitor_type", required=True) - parser.add_argument('-n', "--model_name", dest="model_name", required=False) - parser.add_argument("-D", "--description", dest="description", required=False) - params = parser.parse_args() - - print("Opening and parsing the dot file %s" % params.dot_file) - try: - monitor=dot2k(params.dot_file, params.monitor_type) - except Exception as e: - print('Error: '+ str(e)) - print("Sorry : :-(") - sys.exit(1) - - # easier than using argparse action. - if params.model_name != None: - print(params.model_name) - - print("Writing the monitor into the directory %s" % monitor.name) - monitor.print_files() - print("Almost done, checklist") - print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name)) - print(" - Edit include/trace/events/rv.h to add the tracepoint entry") - print(" - Move it to the kernel's monitor directory") - print(" - Edit kernel/trace/rv/Makefile") - print(" - Edit kernel/trace/rv/Kconfig") diff --git a/tools/verification/dot2/dot2k.py b/tools/verification/dot2/dot2k.py deleted file mode 100644 index 016550fccf1f..000000000000 --- a/tools/verification/dot2/dot2k.py +++ /dev/null @@ -1,177 +0,0 @@ -#!/usr/bin/env python3 -# SPDX-License-Identifier: GPL-2.0-only -# -# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> -# -# dot2k: transform dot files into a monitor for the Linux kernel. -# -# For further information, see: -# Documentation/trace/rv/da_monitor_synthesis.rst - -from dot2.dot2c import Dot2c -import platform -import os - -class dot2k(Dot2c): - monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } - monitor_templates_dir = "dot2k/rv_templates/" - monitor_type = "per_cpu" - - def __init__(self, file_path, MonitorType): - super().__init__(file_path) - - self.monitor_type = self.monitor_types.get(MonitorType) - if self.monitor_type == None: - raise Exception("Unknown monitor type: %s" % MonitorType) - - self.monitor_type = MonitorType - self.__fill_rv_templates_dir() - self.main_c = self.__open_file(self.monitor_templates_dir + "main_" + MonitorType + ".c") - self.enum_suffix = "_%s" % self.name - - def __fill_rv_templates_dir(self): - - if os.path.exists(self.monitor_templates_dir) == True: - return - - if platform.system() != "Linux": - raise Exception("I can only run on Linux.") - - kernel_path = "/lib/modules/%s/build/tools/verification/dot2/dot2k_templates/" % (platform.release()) - - if os.path.exists(kernel_path) == True: - self.monitor_templates_dir = kernel_path - return - - if os.path.exists("/usr/share/dot2/dot2k_templates/") == True: - self.monitor_templates_dir = "/usr/share/dot2/dot2k_templates/" - return - - raise Exception("Could not find the template directory, do you have the kernel source installed?") - - - def __open_file(self, path): - try: - fd = open(path) - except OSError: - raise Exception("Cannot open the file: %s" % path) - - content = fd.read() - - return content - - def __buff_to_string(self, buff): - string = "" - - for line in buff: - string = string + line + "\n" - - # cut off the last \n - return string[:-1] - - def fill_tracepoint_handlers_skel(self): - buff = [] - for event in self.events: - buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) - buff.append("{") - if self.monitor_type == "per_task": - buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;"); - buff.append("\tda_handle_event_%s(p, %s%s);" % (self.name, event, self.enum_suffix)); - else: - buff.append("\tda_handle_event_%s(%s%s);" % (self.name, event, self.enum_suffix)); - buff.append("}") - buff.append("") - return self.__buff_to_string(buff) - - def fill_tracepoint_attach_probe(self): - buff = [] - for event in self.events: - buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) - - def fill_tracepoint_detach_helper(self): - buff = [] - for event in self.events: - buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) - return self.__buff_to_string(buff) - - def fill_main_c(self): - main_c = self.main_c - min_type = self.get_minimun_type() - nr_events = self.events.__len__() - tracepoint_handlers = self.fill_tracepoint_handlers_skel() - tracepoint_attach = self.fill_tracepoint_attach_probe() - tracepoint_detach = self.fill_tracepoint_detach_helper() - - main_c = main_c.replace("MIN_TYPE", min_type) - main_c = main_c.replace("MODEL_NAME", self.name) - main_c = main_c.replace("NR_EVENTS", str(nr_events)) - main_c = main_c.replace("TRACEPOINT_HANDLERS_SKEL", tracepoint_handlers) - main_c = main_c.replace("TRACEPOINT_ATTACH", tracepoint_attach) - main_c = main_c.replace("TRACEPOINT_DETACH", tracepoint_detach) - - return main_c - - def fill_model_h_header(self): - buff = [] - buff.append("/*") - buff.append(" * Automatically generated C representation of %s automaton" % (self.name)) - buff.append(" * For further information about this format, see kernel documentation:") - buff.append(" * Documentation/trace/rv/deterministic_automata.rst") - buff.append(" */") - buff.append("") - - return buff - - def fill_model_h(self): - # - # Adjust the definition names - # - self.enum_states_def = "states_%s" % self.name - self.enum_events_def = "events_%s" % self.name - self.struct_automaton_def = "automaton_%s" % self.name - self.var_automaton_def = "automaton_%s" % self.name - - buff = self.fill_model_h_header() - buff += self.format_model() - - return self.__buff_to_string(buff) - - def __create_directory(self): - try: - os.mkdir(self.name) - except FileExistsError: - return - except: - print("Fail creating the output dir: %s" % self.name) - - def __create_file(self, file_name, content): - path = "%s/%s" % (self.name, file_name) - try: - file = open(path, 'w') - except FileExistsError: - return - except: - print("Fail creating file: %s" % path) - - file.write(content) - - file.close() - - def __get_main_name(self): - path = "%s/%s" % (self.name, "main.c") - if os.path.exists(path) == False: - return "main.c" - return "__main.c" - - def print_files(self): - main_c = self.fill_main_c() - model_h = self.fill_model_h() - - self.__create_directory() - - path = "%s.c" % self.name - self.__create_file(path, main_c) - - path = "%s.h" % self.name - self.__create_file(path, model_h) diff --git a/tools/verification/dot2/dot2k_templates/main_global.c b/tools/verification/dot2/dot2k_templates/main_global.c deleted file mode 100644 index a5658bfb9044..000000000000 --- a/tools/verification/dot2/dot2k_templates/main_global.c +++ /dev/null @@ -1,91 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <linux/ftrace.h> -#include <linux/tracepoint.h> -#include <linux/kernel.h> -#include <linux/module.h> -#include <linux/init.h> -#include <linux/rv.h> -#include <rv/instrumentation.h> -#include <rv/da_monitor.h> - -#define MODULE_NAME "MODEL_NAME" - -/* - * XXX: include required tracepoint headers, e.g., - * #include <trace/events/sched.h> - */ -#include <trace/events/rv.h> - -/* - * This is the self-generated part of the monitor. Generally, there is no need - * to touch this section. - */ -#include "MODEL_NAME.h" - -/* - * Declare the deterministic automata monitor. - * - * The rv monitor reference is needed for the monitor declaration. - */ -static struct rv_monitor rv_MODEL_NAME; -DECLARE_DA_MON_GLOBAL(MODEL_NAME, MIN_TYPE); - -/* - * This is the instrumentation part of the monitor. - * - * This is the section where manual work is required. Here the kernel events - * are translated into model's event. - * - */ -TRACEPOINT_HANDLERS_SKEL -static int enable_MODEL_NAME(void) -{ - int retval; - - retval = da_monitor_init_MODEL_NAME(); - if (retval) - return retval; - -TRACEPOINT_ATTACH - - return 0; -} - -static void disable_MODEL_NAME(void) -{ - rv_MODEL_NAME.enabled = 0; - -TRACEPOINT_DETACH - - da_monitor_destroy_MODEL_NAME(); -} - -/* - * This is the monitor register section. - */ -static struct rv_monitor rv_MODEL_NAME = { - .name = "MODEL_NAME", - .description = "auto-generated MODEL_NAME", - .enable = enable_MODEL_NAME, - .disable = disable_MODEL_NAME, - .reset = da_monitor_reset_all_MODEL_NAME, - .enabled = 0, -}; - -static int __init register_MODEL_NAME(void) -{ - rv_register_monitor(&rv_MODEL_NAME); - return 0; -} - -static void __exit unregister_MODEL_NAME(void) -{ - rv_unregister_monitor(&rv_MODEL_NAME); -} - -module_init(register_MODEL_NAME); -module_exit(unregister_MODEL_NAME); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); -MODULE_DESCRIPTION("MODEL_NAME"); diff --git a/tools/verification/dot2/dot2k_templates/main_per_cpu.c b/tools/verification/dot2/dot2k_templates/main_per_cpu.c deleted file mode 100644 index 03539a97633f..000000000000 --- a/tools/verification/dot2/dot2k_templates/main_per_cpu.c +++ /dev/null @@ -1,91 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <linux/ftrace.h> -#include <linux/tracepoint.h> -#include <linux/kernel.h> -#include <linux/module.h> -#include <linux/init.h> -#include <linux/rv.h> -#include <rv/instrumentation.h> -#include <rv/da_monitor.h> - -#define MODULE_NAME "MODEL_NAME" - -/* - * XXX: include required tracepoint headers, e.g., - * #include <linux/trace/events/sched.h> - */ -#include <trace/events/rv.h> - -/* - * This is the self-generated part of the monitor. Generally, there is no need - * to touch this section. - */ -#include "MODEL_NAME.h" - -/* - * Declare the deterministic automata monitor. - * - * The rv monitor reference is needed for the monitor declaration. - */ -static struct rv_monitor rv_MODEL_NAME; -DECLARE_DA_MON_PER_CPU(MODEL_NAME, MIN_TYPE); - -/* - * This is the instrumentation part of the monitor. - * - * This is the section where manual work is required. Here the kernel events - * are translated into model's event. - * - */ -TRACEPOINT_HANDLERS_SKEL -static int enable_MODEL_NAME(void) -{ - int retval; - - retval = da_monitor_init_MODEL_NAME(); - if (retval) - return retval; - -TRACEPOINT_ATTACH - - return 0; -} - -static void disable_MODEL_NAME(void) -{ - rv_MODEL_NAME.enabled = 0; - -TRACEPOINT_DETACH - - da_monitor_destroy_MODEL_NAME(); -} - -/* - * This is the monitor register section. - */ -static struct rv_monitor rv_MODEL_NAME = { - .name = "MODEL_NAME", - .description = "auto-generated MODEL_NAME", - .enable = enable_MODEL_NAME, - .disable = disable_MODEL_NAME, - .reset = da_monitor_reset_all_MODEL_NAME, - .enabled = 0, -}; - -static int __init register_MODEL_NAME(void) -{ - rv_register_monitor(&rv_MODEL_NAME); - return 0; -} - -static void __exit unregister_MODEL_NAME(void) -{ - rv_unregister_monitor(&rv_MODEL_NAME); -} - -module_init(register_MODEL_NAME); -module_exit(unregister_MODEL_NAME); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); -MODULE_DESCRIPTION("MODEL_NAME"); diff --git a/tools/verification/dot2/dot2k_templates/main_per_task.c b/tools/verification/dot2/dot2k_templates/main_per_task.c deleted file mode 100644 index ffd92af87a86..000000000000 --- a/tools/verification/dot2/dot2k_templates/main_per_task.c +++ /dev/null @@ -1,91 +0,0 @@ -// SPDX-License-Identifier: GPL-2.0 -#include <linux/ftrace.h> -#include <linux/tracepoint.h> -#include <linux/kernel.h> -#include <linux/module.h> -#include <linux/init.h> -#include <linux/rv.h> -#include <rv/instrumentation.h> -#include <rv/da_monitor.h> - -#define MODULE_NAME "MODEL_NAME" - -/* - * XXX: include required tracepoint headers, e.g., - * #include <linux/trace/events/sched.h> - */ -#include <trace/events/rv.h> - -/* - * This is the self-generated part of the monitor. Generally, there is no need - * to touch this section. - */ -#include "MODEL_NAME.h" - -/* - * Declare the deterministic automata monitor. - * - * The rv monitor reference is needed for the monitor declaration. - */ -static struct rv_monitor rv_MODEL_NAME; -DECLARE_DA_MON_PER_TASK(MODEL_NAME, MIN_TYPE); - -/* - * This is the instrumentation part of the monitor. - * - * This is the section where manual work is required. Here the kernel events - * are translated into model's event. - * - */ -TRACEPOINT_HANDLERS_SKEL -static int enable_MODEL_NAME(void) -{ - int retval; - - retval = da_monitor_init_MODEL_NAME(); - if (retval) - return retval; - -TRACEPOINT_ATTACH - - return 0; -} - -static void disable_MODEL_NAME(void) -{ - rv_MODEL_NAME.enabled = 0; - -TRACEPOINT_DETACH - - da_monitor_destroy_MODEL_NAME(); -} - -/* - * This is the monitor register section. - */ -static struct rv_monitor rv_MODEL_NAME = { - .name = "MODEL_NAME", - .description = "auto-generated MODEL_NAME", - .enable = enable_MODEL_NAME, - .disable = disable_MODEL_NAME, - .reset = da_monitor_reset_all_MODEL_NAME, - .enabled = 0, -}; - -static int __init register_MODEL_NAME(void) -{ - rv_register_monitor(&rv_MODEL_NAME); - return 0; -} - -static void __exit unregister_MODEL_NAME(void) -{ - rv_unregister_monitor(&rv_MODEL_NAME); -} - -module_init(register_MODEL_NAME); -module_exit(unregister_MODEL_NAME); - -MODULE_LICENSE("GPL"); -MODULE_AUTHOR("dot2k: auto-generated"); -MODULE_DESCRIPTION("MODEL_NAME"); diff --git a/tools/verification/models/rtapp/pagefault.ltl b/tools/verification/models/rtapp/pagefault.ltl new file mode 100644 index 000000000000..d7ce62102733 --- /dev/null +++ b/tools/verification/models/rtapp/pagefault.ltl @@ -0,0 +1 @@ +RULE = always (RT imply not PAGEFAULT) diff --git a/tools/verification/models/rtapp/sleep.ltl b/tools/verification/models/rtapp/sleep.ltl new file mode 100644 index 000000000000..6379bbeb6212 --- /dev/null +++ b/tools/verification/models/rtapp/sleep.ltl @@ -0,0 +1,22 @@ +RULE = always ((RT and SLEEP) imply (RT_FRIENDLY_SLEEP or ALLOWLIST)) + +RT_FRIENDLY_SLEEP = (RT_VALID_SLEEP_REASON or KERNEL_THREAD) + and ((not WAKE) until RT_FRIENDLY_WAKE) + +RT_VALID_SLEEP_REASON = FUTEX_WAIT + or RT_FRIENDLY_NANOSLEEP + +RT_FRIENDLY_NANOSLEEP = CLOCK_NANOSLEEP + and NANOSLEEP_TIMER_ABSTIME + and (NANOSLEEP_CLOCK_MONOTONIC or NANOSLEEP_CLOCK_TAI) + +RT_FRIENDLY_WAKE = WOKEN_BY_EQUAL_OR_HIGHER_PRIO + or WOKEN_BY_HARDIRQ + or WOKEN_BY_NMI + or ABORT_SLEEP + or KTHREAD_SHOULD_STOP + +ALLOWLIST = BLOCK_ON_RT_MUTEX + or FUTEX_LOCK_PI + or TASK_IS_RCU + or TASK_IS_MIGRATION diff --git a/tools/verification/models/sched/nrp.dot b/tools/verification/models/sched/nrp.dot new file mode 100644 index 000000000000..77bb64669416 --- /dev/null +++ b/tools/verification/models/sched/nrp.dot @@ -0,0 +1,29 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = doublecircle] "any_thread_running"}; + {node [shape = circle] "any_thread_running"}; + {node [shape = circle] "nested_preempt"}; + {node [shape = plaintext, style=invis, label=""] "__init_preempt_irq"}; + {node [shape = circle] "preempt_irq"}; + {node [shape = circle] "rescheduling"}; + "__init_preempt_irq" -> "preempt_irq"; + "any_thread_running" [label = "any_thread_running", color = green3]; + "any_thread_running" -> "any_thread_running" [ label = "schedule_entry\nirq_entry" ]; + "any_thread_running" -> "rescheduling" [ label = "sched_need_resched" ]; + "nested_preempt" [label = "nested_preempt"]; + "nested_preempt" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "nested_preempt" -> "nested_preempt" [ label = "irq_entry" ]; + "nested_preempt" -> "preempt_irq" [ label = "sched_need_resched" ]; + "preempt_irq" [label = "preempt_irq"]; + "preempt_irq" -> "nested_preempt" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "preempt_irq" -> "preempt_irq" [ label = "irq_entry\nsched_need_resched" ]; + "rescheduling" [label = "rescheduling"]; + "rescheduling" -> "any_thread_running" [ label = "schedule_entry_preempt\nschedule_entry" ]; + "rescheduling" -> "preempt_irq" [ label = "irq_entry" ]; + "rescheduling" -> "rescheduling" [ label = "sched_need_resched" ]; + { rank = min ; + "__init_preempt_irq"; + "preempt_irq"; + } +} diff --git a/tools/verification/models/sched/opid.dot b/tools/verification/models/sched/opid.dot new file mode 100644 index 000000000000..840052f6952b --- /dev/null +++ b/tools/verification/models/sched/opid.dot @@ -0,0 +1,35 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_disabled"}; + {node [shape = circle] "disabled"}; + {node [shape = doublecircle] "enabled"}; + {node [shape = circle] "enabled"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "irq_disabled"}; + {node [shape = circle] "preempt_disabled"}; + "__init_disabled" -> "disabled"; + "disabled" [label = "disabled"]; + "disabled" -> "disabled" [ label = "sched_need_resched\nsched_waking\nirq_entry" ]; + "disabled" -> "irq_disabled" [ label = "preempt_enable" ]; + "disabled" -> "preempt_disabled" [ label = "irq_enable" ]; + "enabled" [label = "enabled", color = green3]; + "enabled" -> "enabled" [ label = "preempt_enable" ]; + "enabled" -> "irq_disabled" [ label = "irq_disable" ]; + "enabled" -> "preempt_disabled" [ label = "preempt_disable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "enabled" [ label = "irq_enable" ]; + "in_irq" -> "in_irq" [ label = "sched_need_resched\nsched_waking\nirq_entry" ]; + "irq_disabled" [label = "irq_disabled"]; + "irq_disabled" -> "disabled" [ label = "preempt_disable" ]; + "irq_disabled" -> "enabled" [ label = "irq_enable" ]; + "irq_disabled" -> "in_irq" [ label = "irq_entry" ]; + "irq_disabled" -> "irq_disabled" [ label = "sched_need_resched" ]; + "preempt_disabled" [label = "preempt_disabled"]; + "preempt_disabled" -> "disabled" [ label = "irq_disable" ]; + "preempt_disabled" -> "enabled" [ label = "preempt_enable" ]; + { rank = min ; + "__init_disabled"; + "disabled"; + } +} diff --git a/tools/verification/models/sched/sco.dot b/tools/verification/models/sched/sco.dot new file mode 100644 index 000000000000..20b0e3b449a6 --- /dev/null +++ b/tools/verification/models/sched/sco.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "scheduling_context"}; + {node [shape = plaintext, style=invis, label=""] "__init_thread_context"}; + {node [shape = ellipse] "thread_context"}; + {node [shape = plaintext] "thread_context"}; + "__init_thread_context" -> "thread_context"; + "scheduling_context" [label = "scheduling_context"]; + "scheduling_context" -> "thread_context" [ label = "schedule_exit" ]; + "thread_context" [label = "thread_context", color = green3]; + "thread_context" -> "scheduling_context" [ label = "schedule_entry" ]; + "thread_context" -> "thread_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_thread_context"; + "thread_context"; + } +} diff --git a/tools/verification/models/sched/scpd.dot b/tools/verification/models/sched/scpd.dot new file mode 100644 index 000000000000..340413896765 --- /dev/null +++ b/tools/verification/models/sched/scpd.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext] "can_sched"}; + {node [shape = plaintext, style=invis, label=""] "__init_cant_sched"}; + {node [shape = ellipse] "cant_sched"}; + {node [shape = plaintext] "cant_sched"}; + "__init_cant_sched" -> "cant_sched"; + "can_sched" [label = "can_sched"]; + "can_sched" -> "can_sched" [ label = "schedule_entry\nschedule_exit" ]; + "can_sched" -> "cant_sched" [ label = "preempt_enable" ]; + "cant_sched" [label = "cant_sched", color = green3]; + "cant_sched" -> "can_sched" [ label = "preempt_disable" ]; + { rank = min ; + "__init_cant_sched"; + "cant_sched"; + } +} diff --git a/tools/verification/models/sched/snep.dot b/tools/verification/models/sched/snep.dot new file mode 100644 index 000000000000..fe1300e93f21 --- /dev/null +++ b/tools/verification/models/sched/snep.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_non_scheduling_context"}; + {node [shape = ellipse] "non_scheduling_context"}; + {node [shape = plaintext] "non_scheduling_context"}; + {node [shape = plaintext] "scheduling_contex"}; + "__init_non_scheduling_context" -> "non_scheduling_context"; + "non_scheduling_context" [label = "non_scheduling_context", color = green3]; + "non_scheduling_context" -> "non_scheduling_context" [ label = "preempt_disable\npreempt_enable" ]; + "non_scheduling_context" -> "scheduling_contex" [ label = "schedule_entry" ]; + "scheduling_contex" [label = "scheduling_contex"]; + "scheduling_contex" -> "non_scheduling_context" [ label = "schedule_exit" ]; + { rank = min ; + "__init_non_scheduling_context"; + "non_scheduling_context"; + } +} diff --git a/tools/verification/models/sched/snroc.dot b/tools/verification/models/sched/snroc.dot new file mode 100644 index 000000000000..8b71c32d4dca --- /dev/null +++ b/tools/verification/models/sched/snroc.dot @@ -0,0 +1,18 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_other_context"}; + {node [shape = ellipse] "other_context"}; + {node [shape = plaintext] "other_context"}; + {node [shape = plaintext] "own_context"}; + "__init_other_context" -> "other_context"; + "other_context" [label = "other_context", color = green3]; + "other_context" -> "own_context" [ label = "sched_switch_in" ]; + "own_context" [label = "own_context"]; + "own_context" -> "other_context" [ label = "sched_switch_out" ]; + "own_context" -> "own_context" [ label = "sched_set_state" ]; + { rank = min ; + "__init_other_context"; + "other_context"; + } +} diff --git a/tools/verification/models/sched/sssw.dot b/tools/verification/models/sched/sssw.dot new file mode 100644 index 000000000000..4994c3e876be --- /dev/null +++ b/tools/verification/models/sched/sssw.dot @@ -0,0 +1,30 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_runnable"}; + {node [shape = doublecircle] "runnable"}; + {node [shape = circle] "runnable"}; + {node [shape = circle] "signal_wakeup"}; + {node [shape = circle] "sleepable"}; + {node [shape = circle] "sleeping"}; + "__init_runnable" -> "runnable"; + "runnable" [label = "runnable", color = green3]; + "runnable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup\nsched_switch_in\nsched_switch_yield\nsched_switch_preempt\nsignal_deliver" ]; + "runnable" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "runnable" -> "sleeping" [ label = "sched_switch_blocking" ]; + "signal_wakeup" [label = "signal_wakeup"]; + "signal_wakeup" -> "runnable" [ label = "signal_deliver" ]; + "signal_wakeup" -> "signal_wakeup" [ label = "sched_switch_in\nsched_switch_preempt\nsched_switch_yield\nsched_wakeup" ]; + "signal_wakeup" -> "sleepable" [ label = "sched_set_state_sleepable" ]; + "sleepable" [label = "sleepable"]; + "sleepable" -> "runnable" [ label = "sched_set_state_runnable\nsched_wakeup" ]; + "sleepable" -> "signal_wakeup" [ label = "sched_switch_yield" ]; + "sleepable" -> "sleepable" [ label = "sched_set_state_sleepable\nsched_switch_in\nsched_switch_preempt\nsignal_deliver" ]; + "sleepable" -> "sleeping" [ label = "sched_switch_suspend\nsched_switch_blocking" ]; + "sleeping" [label = "sleeping"]; + "sleeping" -> "runnable" [ label = "sched_wakeup" ]; + { rank = min ; + "__init_runnable"; + "runnable"; + } +} diff --git a/tools/verification/models/sched/sts.dot b/tools/verification/models/sched/sts.dot new file mode 100644 index 000000000000..8f5f38be04d5 --- /dev/null +++ b/tools/verification/models/sched/sts.dot @@ -0,0 +1,38 @@ +digraph state_automaton { + center = true; + size = "7,11"; + {node [shape = plaintext, style=invis, label=""] "__init_can_sched"}; + {node [shape = doublecircle] "can_sched"}; + {node [shape = circle] "can_sched"}; + {node [shape = circle] "cant_sched"}; + {node [shape = circle] "disable_to_switch"}; + {node [shape = circle] "enable_to_exit"}; + {node [shape = circle] "in_irq"}; + {node [shape = circle] "scheduling"}; + {node [shape = circle] "switching"}; + "__init_can_sched" -> "can_sched"; + "can_sched" [label = "can_sched", color = green3]; + "can_sched" -> "cant_sched" [ label = "irq_disable" ]; + "can_sched" -> "scheduling" [ label = "schedule_entry" ]; + "cant_sched" [label = "cant_sched"]; + "cant_sched" -> "can_sched" [ label = "irq_enable" ]; + "cant_sched" -> "cant_sched" [ label = "irq_entry" ]; + "disable_to_switch" [label = "disable_to_switch"]; + "disable_to_switch" -> "enable_to_exit" [ label = "irq_enable" ]; + "disable_to_switch" -> "in_irq" [ label = "irq_entry" ]; + "disable_to_switch" -> "switching" [ label = "sched_switch" ]; + "enable_to_exit" [label = "enable_to_exit"]; + "enable_to_exit" -> "can_sched" [ label = "schedule_exit" ]; + "enable_to_exit" -> "enable_to_exit" [ label = "irq_disable\nirq_entry\nirq_enable" ]; + "in_irq" [label = "in_irq"]; + "in_irq" -> "in_irq" [ label = "irq_entry" ]; + "in_irq" -> "scheduling" [ label = "irq_enable" ]; + "scheduling" [label = "scheduling"]; + "scheduling" -> "disable_to_switch" [ label = "irq_disable" ]; + "switching" [label = "switching"]; + "switching" -> "enable_to_exit" [ label = "irq_enable" ]; + { rank = min ; + "__init_can_sched"; + "can_sched"; + } +} diff --git a/tools/verification/rv/Makefile b/tools/verification/rv/Makefile index 411d62b3d8eb..5b898360ba48 100644 --- a/tools/verification/rv/Makefile +++ b/tools/verification/rv/Makefile @@ -35,12 +35,6 @@ FEATURE_TESTS += libtracefs FEATURE_DISPLAY := libtraceevent FEATURE_DISPLAY += libtracefs -ifeq ($(V),1) - Q = -else - Q = @ -endif - all: $(RV) include $(srctree)/tools/build/Makefile.include diff --git a/tools/verification/rv/Makefile.rv b/tools/verification/rv/Makefile.rv index 161baa29eb86..2497fb96c83d 100644 --- a/tools/verification/rv/Makefile.rv +++ b/tools/verification/rv/Makefile.rv @@ -27,7 +27,7 @@ endif INCLUDE := -Iinclude/ CFLAGS := -g -DVERSION=\"$(VERSION)\" $(FOPTS) $(WOPTS) $(EXTRA_CFLAGS) $(INCLUDE) -LDFLAGS := -ggdb $(EXTRA_LDFLAGS) +LDFLAGS := -ggdb $(LDFLAGS) $(EXTRA_LDFLAGS) INSTALL := install MKDIR := mkdir diff --git a/tools/verification/rv/include/in_kernel.h b/tools/verification/rv/include/in_kernel.h index 3090638c8d71..f3bfd3b9895f 100644 --- a/tools/verification/rv/include/in_kernel.h +++ b/tools/verification/rv/include/in_kernel.h @@ -1,3 +1,3 @@ // SPDX-License-Identifier: GPL-2.0 -int ikm_list_monitors(void); +int ikm_list_monitors(char *container); int ikm_run_monitor(char *monitor, int argc, char **argv); diff --git a/tools/verification/rv/include/rv.h b/tools/verification/rv/include/rv.h index 770fd6da3610..6f668eb266cb 100644 --- a/tools/verification/rv/include/rv.h +++ b/tools/verification/rv/include/rv.h @@ -1,12 +1,13 @@ // SPDX-License-Identifier: GPL-2.0 #define MAX_DESCRIPTION 1024 -#define MAX_DA_NAME_LEN 24 +#define MAX_DA_NAME_LEN 32 struct monitor { char name[MAX_DA_NAME_LEN]; char desc[MAX_DESCRIPTION]; int enabled; + int nested; }; int should_stop(void); diff --git a/tools/verification/rv/src/in_kernel.c b/tools/verification/rv/src/in_kernel.c index f2bbc75a76f4..4bb746ea6e17 100644 --- a/tools/verification/rv/src/in_kernel.c +++ b/tools/verification/rv/src/in_kernel.c @@ -6,15 +6,18 @@ */ #include <getopt.h> #include <stdlib.h> +#include <stdio.h> #include <string.h> #include <errno.h> #include <unistd.h> +#include <dirent.h> #include <trace.h> #include <utils.h> #include <rv.h> static int config_has_id; +static int config_is_container; static int config_my_pid; static int config_trace; @@ -45,6 +48,51 @@ static int __ikm_read_enable(char *monitor_name) } /* + * __ikm_find_monitor - find the full name of a possibly nested module + * + * __does not log errors. + * + * Returns 1 if we found the monitor, -1 on error and 0 if it does not exist. + * The string out_name is populated with the full name, which can be + * equal to monitor_name or container/monitor_name if nested + */ +static int __ikm_find_monitor_name(char *monitor_name, char *out_name) +{ + char *available_monitors, container[MAX_DA_NAME_LEN+1], *cursor, *end; + int retval = 1; + + available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); + if (!available_monitors) + return -1; + + cursor = strstr(available_monitors, monitor_name); + if (!cursor) { + retval = 0; + goto out_free; + } + + for (; cursor > available_monitors; cursor--) + if (*(cursor-1) == '\n') + break; + end = strstr(cursor, "\n"); + memcpy(out_name, cursor, end-cursor); + out_name[end-cursor] = '\0'; + + cursor = strstr(out_name, ":"); + if (cursor) + *cursor = '/'; + else { + sprintf(container, "%s:", monitor_name); + if (strstr(available_monitors, container)) + config_is_container = 1; + } + +out_free: + free(available_monitors); + return retval; +} + +/* * ikm_read_enable - reads monitor's enable status * * Returns the current status, or -1 on error. @@ -132,12 +180,28 @@ static char *ikm_read_desc(char *monitor_name) /* * ikm_fill_monitor_definition - fill monitor's definition * - * Returns -1 on error, 0 otherwise. + * Returns -1 on error, 1 if the monitor does not belong in the container, 0 otherwise. + * container can be NULL */ -static int ikm_fill_monitor_definition(char *name, struct monitor *ikm) +static int ikm_fill_monitor_definition(char *name, struct monitor *ikm, char *container) { int enabled; - char *desc; + char *desc, *nested_name; + + nested_name = strstr(name, ":"); + if (nested_name) { + /* it belongs in container if it starts with "container:" */ + if (container && strstr(name, container) != name) + return 1; + *nested_name = '/'; + ++nested_name; + ikm->nested = 1; + } else { + if (container) + return 1; + nested_name = name; + ikm->nested = 0; + } enabled = ikm_read_enable(name); if (enabled < 0) { @@ -151,7 +215,7 @@ static int ikm_fill_monitor_definition(char *name, struct monitor *ikm) return -1; } - strncpy(ikm->name, name, MAX_DA_NAME_LEN); + strncpy(ikm->name, nested_name, MAX_DA_NAME_LEN); ikm->enabled = enabled; strncpy(ikm->desc, desc, MAX_DESCRIPTION); @@ -270,12 +334,12 @@ static int ikm_has_id(char *monitor_name) * * Returns 0 on success, -1 otherwise. */ -int ikm_list_monitors(void) +int ikm_list_monitors(char *container) { char *available_monitors; - struct monitor ikm; + struct monitor ikm = {0}; char *curr, *next; - int retval; + int retval, list_monitor = 0; available_monitors = tracefs_instance_file_read(NULL, "rv/available_monitors", NULL); @@ -289,15 +353,29 @@ int ikm_list_monitors(void) next = strstr(curr, "\n"); *next = '\0'; - retval = ikm_fill_monitor_definition(curr, &ikm); - if (retval) + retval = ikm_fill_monitor_definition(curr, &ikm, container); + if (retval < 0) err_msg("ikm: error reading %d in kernel monitor, skipping\n", curr); - printf("%-24s %s %s\n", ikm.name, ikm.desc, ikm.enabled ? "[ON]" : "[OFF]"); + if (!retval) { + int indent = ikm.nested && !container; + + list_monitor = 1; + printf("%s%-*s %s %s\n", indent ? " - " : "", + indent ? MAX_DA_NAME_LEN - 3 : MAX_DA_NAME_LEN, + ikm.name, ikm.desc, ikm.enabled ? "[ON]" : "[OFF]"); + } curr = ++next; } while (strlen(curr)); + if (!list_monitor) { + if (container) + printf("-- No monitor found in container %s --\n", container); + else + printf("-- No monitor found --\n"); + } + free(available_monitors); return 0; @@ -343,25 +421,34 @@ ikm_event_handler(struct trace_seq *s, struct tep_record *record, unsigned long long final_state; unsigned long long pid; unsigned long long id; - int cpu = record->cpu; int val; + bool missing_id; if (config_has_id) - tep_get_field_val(s, trace_event, "id", record, &id, 1); + missing_id = tep_get_field_val(s, trace_event, "id", record, &id, 1); tep_get_common_field_val(s, trace_event, "common_pid", record, &pid, 1); if (config_has_id && (config_my_pid == id)) return 0; - else if (config_my_pid && (config_my_pid == pid)) + else if (config_my_pid == pid) return 0; - tep_print_event(trace_event->tep, s, record, "%16s-%-8d ", TEP_PRINT_COMM, TEP_PRINT_PID); + tep_print_event(trace_event->tep, s, record, "%16s-%-8d [%.3d] ", + TEP_PRINT_COMM, TEP_PRINT_PID, TEP_PRINT_CPU); - trace_seq_printf(s, "[%.3d] event ", cpu); + if (config_is_container) + tep_print_event(trace_event->tep, s, record, "%s ", TEP_PRINT_NAME); + else + trace_seq_printf(s, "event "); - if (config_has_id) - trace_seq_printf(s, "%8llu ", id); + if (config_has_id) { + if (missing_id) + /* placeholder if we are dealing with a mixed-type container*/ + trace_seq_printf(s, " "); + else + trace_seq_printf(s, "%8llu ", id); + } state = tep_get_field_raw(s, trace_event, "state", record, &val, 0); event = tep_get_field_raw(s, trace_event, "event", record, &val, 0); @@ -394,9 +481,10 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, int cpu = record->cpu; char *state, *event; int val; + bool missing_id; if (config_has_id) - tep_get_field_val(s, trace_event, "id", record, &id, 1); + missing_id = tep_get_field_val(s, trace_event, "id", record, &id, 1); tep_get_common_field_val(s, trace_event, "common_pid", record, &pid, 1); @@ -405,10 +493,20 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, else if (config_my_pid == pid) return 0; - trace_seq_printf(s, "%8lld [%03d] error ", pid, cpu); + trace_seq_printf(s, "%8lld [%03d] ", pid, cpu); - if (config_has_id) - trace_seq_printf(s, "%8llu ", id); + if (config_is_container) + tep_print_event(trace_event->tep, s, record, "%s ", TEP_PRINT_NAME); + else + trace_seq_printf(s, "error "); + + if (config_has_id) { + if (missing_id) + /* placeholder if we are dealing with a mixed-type container*/ + trace_seq_printf(s, " "); + else + trace_seq_printf(s, "%8llu ", id); + } state = tep_get_field_raw(s, trace_event, "state", record, &val, 0); event = tep_get_field_raw(s, trace_event, "event", record, &val, 0); @@ -421,6 +519,64 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, return 0; } +static int ikm_enable_trace_events(char *monitor_name, struct trace_instance *inst) +{ + char event[MAX_DA_NAME_LEN + 7]; /* max(error_,event_) + '0' = 7 */ + int retval; + + snprintf(event, sizeof(event), "event_%s", monitor_name); + retval = tracefs_event_enable(inst->inst, "rv", event); + if (retval) + return -1; + + tep_register_event_handler(inst->tep, -1, "rv", event, + ikm_event_handler, NULL); + + snprintf(event, sizeof(event), "error_%s", monitor_name); + retval = tracefs_event_enable(inst->inst, "rv", event); + if (retval) + return -1; + + tep_register_event_handler(inst->tep, -1, "rv", event, + ikm_error_handler, NULL); + + /* set if at least 1 monitor has id in case of a container */ + config_has_id = ikm_has_id(monitor_name); + if (config_has_id < 0) + return -1; + + + return 0; +} + +static int ikm_enable_trace_container(char *monitor_name, + struct trace_instance *inst) +{ + DIR *dp; + char *abs_path, rv_path[MAX_PATH]; + struct dirent *ep; + int retval = 0; + + snprintf(rv_path, MAX_PATH, "rv/monitors/%s", monitor_name); + abs_path = tracefs_instance_get_file(NULL, rv_path); + if (!abs_path) + return -1; + dp = opendir(abs_path); + if (!dp) + goto out_free; + + while (!retval && (ep = readdir(dp))) { + if (ep->d_type != DT_DIR || ep->d_name[0] == '.') + continue; + retval = ikm_enable_trace_events(ep->d_name, inst); + } + + closedir(dp); +out_free: + free(abs_path); + return retval; +} + /* * ikm_setup_trace_instance - set up a tracing instance to collect data * @@ -430,19 +586,12 @@ ikm_error_handler(struct trace_seq *s, struct tep_record *record, */ static struct trace_instance *ikm_setup_trace_instance(char *monitor_name) { - char event[MAX_DA_NAME_LEN + 7]; /* max(error_,event_) + '0' = 7 */ struct trace_instance *inst; int retval; if (!config_trace) return NULL; - config_has_id = ikm_has_id(monitor_name); - if (config_has_id < 0) { - err_msg("ikm: failed to read monitor %s event format\n", monitor_name); - goto out_err; - } - /* alloc data */ inst = calloc(1, sizeof(*inst)); if (!inst) { @@ -454,23 +603,13 @@ static struct trace_instance *ikm_setup_trace_instance(char *monitor_name) if (retval) goto out_free; - /* enable events */ - snprintf(event, sizeof(event), "event_%s", monitor_name); - retval = tracefs_event_enable(inst->inst, "rv", event); + if (config_is_container) + retval = ikm_enable_trace_container(monitor_name, inst); + else + retval = ikm_enable_trace_events(monitor_name, inst); if (retval) goto out_inst; - tep_register_event_handler(inst->tep, -1, "rv", event, - ikm_event_handler, NULL); - - snprintf(event, sizeof(event), "error_%s", monitor_name); - retval = tracefs_event_enable(inst->inst, "rv", event); - if (retval) - goto out_inst; - - tep_register_event_handler(inst->tep, -1, "rv", event, - ikm_error_handler, NULL); - /* ready to enable */ tracefs_trace_on(inst->inst); @@ -595,7 +734,7 @@ static int parse_arguments(char *monitor_name, int argc, char **argv) config_reactor = optarg; break; case 's': - config_my_pid = 0; + config_my_pid = -1; break; case 't': config_trace = 1; @@ -633,32 +772,41 @@ static int parse_arguments(char *monitor_name, int argc, char **argv) int ikm_run_monitor(char *monitor_name, int argc, char **argv) { struct trace_instance *inst = NULL; + char *nested_name, full_name[2*MAX_DA_NAME_LEN]; int retval; - /* - * Check if monitor exists by seeing it is enabled. - */ - retval = __ikm_read_enable(monitor_name); - if (retval < 0) + nested_name = strstr(monitor_name, ":"); + if (nested_name) + ++nested_name; + else + nested_name = monitor_name; + + retval = __ikm_find_monitor_name(monitor_name, full_name); + if (!retval) return 0; + if (retval < 0) { + err_msg("ikm: error finding monitor %s\n", nested_name); + return -1; + } + retval = __ikm_read_enable(full_name); if (retval) { - err_msg("ikm: monitor %s (in-kernel) is already enabled\n", monitor_name); + err_msg("ikm: monitor %s (in-kernel) is already enabled\n", nested_name); return -1; } /* we should be good to go */ - retval = parse_arguments(monitor_name, argc, argv); + retval = parse_arguments(full_name, argc, argv); if (retval) - ikm_usage(1, monitor_name, "ikm: failed parsing arguments"); + ikm_usage(1, nested_name, "ikm: failed parsing arguments"); if (config_trace) { - inst = ikm_setup_trace_instance(monitor_name); + inst = ikm_setup_trace_instance(nested_name); if (!inst) return -1; } - retval = ikm_enable(monitor_name); + retval = ikm_enable(full_name); if (retval < 0) goto out_free_instance; @@ -682,17 +830,17 @@ int ikm_run_monitor(char *monitor_name, int argc, char **argv) sleep(1); } - ikm_disable(monitor_name); + ikm_disable(full_name); ikm_destroy_trace_instance(inst); if (config_reactor && config_initial_reactor) - ikm_write_reactor(monitor_name, config_initial_reactor); + ikm_write_reactor(full_name, config_initial_reactor); return 1; out_free_instance: ikm_destroy_trace_instance(inst); if (config_reactor && config_initial_reactor) - ikm_write_reactor(monitor_name, config_initial_reactor); + ikm_write_reactor(full_name, config_initial_reactor); return -1; } diff --git a/tools/verification/rv/src/rv.c b/tools/verification/rv/src/rv.c index 1ddb85532816..b8fe24a87d97 100644 --- a/tools/verification/rv/src/rv.c +++ b/tools/verification/rv/src/rv.c @@ -41,30 +41,42 @@ static void rv_list(int argc, char **argv) { static const char *const usage[] = { "", - " usage: rv list [-h]", + " usage: rv list [-h] [container]", "", " list all available monitors", "", " -h/--help: print this menu", + "", + " [container]: list only monitors in this container", NULL, }; - int i; - - if (argc > 1) { + int i, print_help = 0, retval = 0; + char *container = NULL; + + if (argc == 2) { + if (!strcmp(argv[1], "-h") || !strcmp(argv[1], "--help")) { + print_help = 1; + retval = 0; + } else if (argv[1][0] == '-') { + /* assume invalid option */ + print_help = 1; + retval = 1; + } else + container = argv[1]; + } else if (argc > 2) { + /* more than 2 is always usage */ + print_help = 1; + retval = 1; + } + if (print_help) { 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(retval); } - ikm_list_monitors(); + ikm_list_monitors(container); + exit(0); } @@ -179,6 +191,7 @@ int main(int argc, char **argv) * and exit. */ signal(SIGINT, stop_rv); + signal(SIGTERM, stop_rv); rv_mon(argc - 1, &argv[1]); } diff --git a/tools/verification/rvgen/.gitignore b/tools/verification/rvgen/.gitignore new file mode 100644 index 000000000000..1e288a076560 --- /dev/null +++ b/tools/verification/rvgen/.gitignore @@ -0,0 +1,3 @@ +__pycache__/ +parser.out +parsetab.py diff --git a/tools/verification/rvgen/Makefile b/tools/verification/rvgen/Makefile new file mode 100644 index 000000000000..cfc4056c1e87 --- /dev/null +++ b/tools/verification/rvgen/Makefile @@ -0,0 +1,27 @@ +INSTALL=install + +prefix ?= /usr +bindir ?= $(prefix)/bin +mandir ?= $(prefix)/share/man +srcdir ?= $(prefix)/src + +PYLIB ?= $(shell python3 -c 'import sysconfig; print (sysconfig.get_path("purelib"))') + +.PHONY: all +all: + +.PHONY: clean +clean: + +.PHONY: install +install: + $(INSTALL) rvgen/automata.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/automata.py + $(INSTALL) rvgen/dot2c.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2c.py + $(INSTALL) dot2c -D -m 755 $(DESTDIR)$(bindir)/ + $(INSTALL) rvgen/dot2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/dot2k.py + $(INSTALL) rvgen/container.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/container.py + $(INSTALL) rvgen/generator.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/generator.py + $(INSTALL) rvgen/ltl2ba.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2ba.py + $(INSTALL) rvgen/ltl2k.py -D -m 644 $(DESTDIR)$(PYLIB)/rvgen/ltl2k.py + $(INSTALL) __main__.py -D -m 755 $(DESTDIR)$(bindir)/rvgen + cp -rp rvgen/templates $(DESTDIR)$(PYLIB)/rvgen/ diff --git a/tools/verification/rvgen/__main__.py b/tools/verification/rvgen/__main__.py new file mode 100644 index 000000000000..fa6fc1f4de2f --- /dev/null +++ b/tools/verification/rvgen/__main__.py @@ -0,0 +1,67 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For further information, see: +# Documentation/trace/rv/da_monitor_synthesis.rst + +if __name__ == '__main__': + from rvgen.dot2k import dot2k + from rvgen.generator import Monitor + from rvgen.container import Container + from rvgen.ltl2k import ltl2k + import argparse + import sys + + parser = argparse.ArgumentParser(description='Generate kernel rv monitor') + parser.add_argument("-D", "--description", dest="description", required=False) + parser.add_argument("-a", "--auto_patch", dest="auto_patch", + action="store_true", required=False, + help="Patch the kernel in place") + + subparsers = parser.add_subparsers(dest="subcmd", required=True) + + monitor_parser = subparsers.add_parser("monitor") + monitor_parser.add_argument('-n', "--model_name", dest="model_name") + monitor_parser.add_argument("-p", "--parent", dest="parent", + required=False, help="Create a monitor nested to parent") + monitor_parser.add_argument('-c', "--class", dest="monitor_class", + help="Monitor class, either \"da\" or \"ltl\"") + monitor_parser.add_argument('-s', "--spec", dest="spec", help="Monitor specification file") + monitor_parser.add_argument('-t', "--monitor_type", dest="monitor_type", + help=f"Available options: {', '.join(Monitor.monitor_types.keys())}") + + container_parser = subparsers.add_parser("container") + container_parser.add_argument('-n', "--model_name", dest="model_name", required=True) + + params = parser.parse_args() + + try: + if params.subcmd == "monitor": + print("Opening and parsing the specification file %s" % params.spec) + if params.monitor_class == "da": + monitor = dot2k(params.spec, params.monitor_type, vars(params)) + elif params.monitor_class == "ltl": + monitor = ltl2k(params.spec, params.monitor_type, vars(params)) + else: + print("Unknown monitor class:", params.monitor_class) + sys.exit(1) + else: + monitor = Container(vars(params)) + except Exception as e: + print('Error: '+ str(e)) + print("Sorry : :-(") + sys.exit(1) + + print("Writing the monitor into the directory %s" % monitor.name) + monitor.print_files() + print("Almost done, checklist") + if params.subcmd == "monitor": + print(" - Edit the %s/%s.c to add the instrumentation" % (monitor.name, monitor.name)) + print(monitor.fill_tracepoint_tooltip()) + print(monitor.fill_makefile_tooltip()) + print(monitor.fill_kconfig_tooltip()) + print(monitor.fill_monitor_tooltip()) diff --git a/tools/verification/dot2/dot2c b/tools/verification/rvgen/dot2c index 3fe89ab88b65..bf0c67c5b66c 100644 --- a/tools/verification/dot2/dot2c +++ b/tools/verification/rvgen/dot2c @@ -14,7 +14,7 @@ # Documentation/trace/rv/deterministic_automata.rst if __name__ == '__main__': - from dot2 import dot2c + from rvgen import dot2c import argparse import sys diff --git a/tools/verification/dot2/automata.py b/tools/verification/rvgen/rvgen/automata.py index bdeb98baa8b0..d9a3fe2b74bf 100644 --- a/tools/verification/dot2/automata.py +++ b/tools/verification/rvgen/rvgen/automata.py @@ -19,13 +19,14 @@ class Automata: invalid_state_str = "INVALID_STATE" - def __init__(self, file_path): + def __init__(self, file_path, model_name=None): self.__dot_path = file_path - self.name = self.__get_model_name() + self.name = model_name or self.__get_model_name() self.__dot_lines = self.__open_dot() self.states, self.initial_state, self.final_states = self.__get_state_variables() self.events = self.__get_event_variables() self.function = self.__create_matrix() + self.events_start, self.events_start_run = self.__store_init_events() def __get_model_name(self): basename = ntpath.basename(self.__dot_path) @@ -172,3 +173,34 @@ class Automata: cursor += 1 return matrix + + def __store_init_events(self): + events_start = [False] * len(self.events) + events_start_run = [False] * len(self.events) + for i, _ in enumerate(self.events): + curr_event_will_init = 0 + curr_event_from_init = False + curr_event_used = 0 + for j, _ in enumerate(self.states): + if self.function[j][i] != self.invalid_state_str: + curr_event_used += 1 + if self.function[j][i] == self.initial_state: + curr_event_will_init += 1 + if self.function[0][i] != self.invalid_state_str: + curr_event_from_init = True + # this event always leads to init + if curr_event_will_init and curr_event_used == curr_event_will_init: + events_start[i] = True + # this event is only called from init + if curr_event_from_init and curr_event_used == 1: + events_start_run[i] = True + return events_start, events_start_run + + def is_start_event(self, event): + return self.events_start[self.events.index(event)] + + def is_start_run_event(self, event): + # prefer handle_start_event if there + if any(self.events_start): + return False + return self.events_start_run[self.events.index(event)] diff --git a/tools/verification/rvgen/rvgen/container.py b/tools/verification/rvgen/rvgen/container.py new file mode 100644 index 000000000000..51f188530b4d --- /dev/null +++ b/tools/verification/rvgen/rvgen/container.py @@ -0,0 +1,32 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# Generator for runtime verification monitor container + +from . import generator + + +class Container(generator.RVGenerator): + template_dir = "container" + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.name = extra_params.get("model_name") + self.main_h = self._read_template_file("main.h") + + def fill_model_h(self): + main_h = self.main_h + main_h = main_h.replace("%%MODEL_NAME%%", self.name) + return main_h + + def fill_kconfig_tooltip(self): + """Override to produce a marker for this container in the Kconfig""" + container_marker = self._kconfig_marker(self.name) + "\n" + result = super().fill_kconfig_tooltip() + if self.auto_patch: + self._patch_file("Kconfig", + self._kconfig_marker(), container_marker) + return result + return result + container_marker diff --git a/tools/verification/dot2/dot2c.py b/tools/verification/rvgen/rvgen/dot2c.py index 87d8a1e1470c..b9b6f14cc536 100644 --- a/tools/verification/dot2/dot2c.py +++ b/tools/verification/rvgen/rvgen/dot2c.py @@ -13,7 +13,7 @@ # For further information, see: # Documentation/trace/rv/deterministic_automata.rst -from dot2.automata import Automata +from .automata import Automata class Dot2c(Automata): enum_suffix = "" @@ -22,8 +22,8 @@ class Dot2c(Automata): struct_automaton_def = "automaton" var_automaton_def = "aut" - def __init__(self, file_path): - super().__init__(file_path) + def __init__(self, file_path, model_name=None): + super().__init__(file_path, model_name) self.line_length = 100 def __buff_to_string(self, buff): @@ -152,28 +152,30 @@ class Dot2c(Automata): max_state_name = max(self.states, key = len).__len__() return max(max_state_name, self.invalid_state_str.__len__()) - def __get_state_string_length(self): - maxlen = self.__get_max_strlen_of_states() + self.enum_suffix.__len__() - return "%" + str(maxlen) + "s" - def get_aut_init_function(self): nr_states = self.states.__len__() nr_events = self.events.__len__() buff = [] - strformat = self.__get_state_string_length() - + maxlen = self.__get_max_strlen_of_states() + len(self.enum_suffix) + tab_braces = 2 * 8 + 2 + 1 # "\t\t{ " ... "}" + comma_space = 2 # ", " count last comma here + linetoolong = tab_braces + (maxlen + comma_space) * nr_events > self.line_length for x in range(nr_states): - line = "\t\t{ " + line = "\t\t{\n" if linetoolong else "\t\t{ " for y in range(nr_events): next_state = self.function[x][y] if next_state != self.invalid_state_str: next_state = self.function[x][y] + self.enum_suffix + if linetoolong: + line += "\t\t\t%s" % next_state + else: + line += "%*s" % (maxlen, next_state) if y != nr_events-1: - line = line + strformat % next_state + ", " + line += ",\n" if linetoolong else ", " else: - line = line + strformat % next_state + " }," + line += "\n\t\t}," if linetoolong else " }," buff.append(line) return self.__buff_to_string(buff) diff --git a/tools/verification/rvgen/rvgen/dot2k.py b/tools/verification/rvgen/rvgen/dot2k.py new file mode 100644 index 000000000000..ed0a3c901106 --- /dev/null +++ b/tools/verification/rvgen/rvgen/dot2k.py @@ -0,0 +1,129 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# dot2k: transform dot files into a monitor for the Linux kernel. +# +# For further information, see: +# Documentation/trace/rv/da_monitor_synthesis.rst + +from .dot2c import Dot2c +from .generator import Monitor + + +class dot2k(Monitor, Dot2c): + template_dir = "dot2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + self.monitor_type = MonitorType + Monitor.__init__(self, extra_params) + Dot2c.__init__(self, file_path, extra_params.get("model_name")) + self.enum_suffix = "_%s" % self.name + + def fill_monitor_type(self): + return self.monitor_type.upper() + + def fill_tracepoint_handlers_skel(self): + buff = [] + for event in self.events: + buff.append("static void handle_%s(void *data, /* XXX: fill header */)" % event) + buff.append("{") + handle = "handle_event" + if self.is_start_event(event): + buff.append("\t/* XXX: validate that this event always leads to the initial state */") + handle = "handle_start_event" + elif self.is_start_run_event(event): + buff.append("\t/* XXX: validate that this event is only valid in the initial state */") + handle = "handle_start_run_event" + if self.monitor_type == "per_task": + buff.append("\tstruct task_struct *p = /* XXX: how do I get p? */;"); + buff.append("\tda_%s_%s(p, %s%s);" % (handle, self.name, event, self.enum_suffix)); + else: + buff.append("\tda_%s_%s(%s%s);" % (handle, self.name, event, self.enum_suffix)); + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + buff = [] + for event in self.events: + buff.append("\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return '\n'.join(buff) + + def fill_tracepoint_detach_helper(self): + buff = [] + for event in self.events: + buff.append("\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_%s);" % (self.name, event)) + return '\n'.join(buff) + + def fill_model_h_header(self): + buff = [] + buff.append("/* SPDX-License-Identifier: GPL-2.0 */") + buff.append("/*") + buff.append(" * Automatically generated C representation of %s automaton" % (self.name)) + buff.append(" * For further information about this format, see kernel documentation:") + buff.append(" * Documentation/trace/rv/deterministic_automata.rst") + buff.append(" */") + buff.append("") + + return buff + + def fill_model_h(self): + # + # Adjust the definition names + # + self.enum_states_def = "states_%s" % self.name + self.enum_events_def = "events_%s" % self.name + self.struct_automaton_def = "automaton_%s" % self.name + self.var_automaton_def = "automaton_%s" % self.name + + buff = self.fill_model_h_header() + buff += self.format_model() + + return '\n'.join(buff) + + def fill_monitor_class_type(self): + if self.monitor_type == "per_task": + return "DA_MON_EVENTS_ID" + return "DA_MON_EVENTS_IMPLICIT" + + def fill_monitor_class(self): + if self.monitor_type == "per_task": + return "da_monitor_id" + return "da_monitor" + + def fill_tracepoint_args_skel(self, tp_type): + buff = [] + tp_args_event = [ + ("char *", "state"), + ("char *", "event"), + ("char *", "next_state"), + ("bool ", "final_state"), + ] + tp_args_error = [ + ("char *", "state"), + ("char *", "event"), + ] + tp_args_id = ("int ", "id") + tp_args = tp_args_event if tp_type == "event" else tp_args_error + if self.monitor_type == "per_task": + tp_args.insert(0, tp_args_id) + tp_proto_c = ", ".join([a+b for a,b in tp_args]) + tp_args_c = ", ".join([b for a,b in tp_args]) + buff.append(" TP_PROTO(%s)," % tp_proto_c) + buff.append(" TP_ARGS(%s)" % tp_args_c) + return '\n'.join(buff) + + def fill_main_c(self): + main_c = super().fill_main_c() + + min_type = self.get_minimun_type() + nr_events = len(self.events) + monitor_type = self.fill_monitor_type() + + main_c = main_c.replace("%%MIN_TYPE%%", min_type) + main_c = main_c.replace("%%NR_EVENTS%%", str(nr_events)) + main_c = main_c.replace("%%MONITOR_TYPE%%", monitor_type) + + return main_c diff --git a/tools/verification/rvgen/rvgen/generator.py b/tools/verification/rvgen/rvgen/generator.py new file mode 100644 index 000000000000..3441385c1177 --- /dev/null +++ b/tools/verification/rvgen/rvgen/generator.py @@ -0,0 +1,270 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Copyright (C) 2019-2022 Red Hat, Inc. Daniel Bristot de Oliveira <bristot@kernel.org> +# +# Abtract class for generating kernel runtime verification monitors from specification file + +import platform +import os + + +class RVGenerator: + rv_dir = "kernel/trace/rv" + + def __init__(self, extra_params={}): + self.name = extra_params.get("model_name") + self.parent = extra_params.get("parent") + self.abs_template_dir = \ + os.path.join(os.path.dirname(__file__), "templates", self.template_dir) + self.main_c = self._read_template_file("main.c") + self.kconfig = self._read_template_file("Kconfig") + self.description = extra_params.get("description", self.name) or "auto-generated" + self.auto_patch = extra_params.get("auto_patch") + if self.auto_patch: + self.__fill_rv_kernel_dir() + + def __fill_rv_kernel_dir(self): + + # first try if we are running in the kernel tree root + if os.path.exists(self.rv_dir): + return + + # offset if we are running inside the kernel tree from verification/dot2 + kernel_path = os.path.join("../..", self.rv_dir) + + if os.path.exists(kernel_path): + self.rv_dir = kernel_path + return + + if platform.system() != "Linux": + raise OSError("I can only run on Linux.") + + kernel_path = os.path.join("/lib/modules/%s/build" % platform.release(), self.rv_dir) + + # if the current kernel is from a distro this may not be a full kernel tree + # verify that one of the files we are going to modify is available + if os.path.exists(os.path.join(kernel_path, "rv_trace.h")): + self.rv_dir = kernel_path + return + + raise FileNotFoundError("Could not find the rv directory, do you have the kernel source installed?") + + def _read_file(self, path): + try: + fd = open(path, 'r') + except OSError: + raise Exception("Cannot open the file: %s" % path) + + content = fd.read() + + fd.close() + return content + + def _read_template_file(self, file): + try: + path = os.path.join(self.abs_template_dir, file) + return self._read_file(path) + except Exception: + # Specific template file not found. Try the generic template file in the template/ + # directory, which is one level up + path = os.path.join(self.abs_template_dir, "..", file) + return self._read_file(path) + + def fill_parent(self): + return "&rv_%s" % self.parent if self.parent else "NULL" + + def fill_include_parent(self): + if self.parent: + return "#include <monitors/%s/%s.h>\n" % (self.parent, self.parent) + return "" + + def fill_tracepoint_handlers_skel(self): + return "NotImplemented" + + def fill_tracepoint_attach_probe(self): + return "NotImplemented" + + def fill_tracepoint_detach_helper(self): + return "NotImplemented" + + def fill_main_c(self): + main_c = self.main_c + tracepoint_handlers = self.fill_tracepoint_handlers_skel() + tracepoint_attach = self.fill_tracepoint_attach_probe() + tracepoint_detach = self.fill_tracepoint_detach_helper() + parent = self.fill_parent() + parent_include = self.fill_include_parent() + + main_c = main_c.replace("%%MODEL_NAME%%", self.name) + main_c = main_c.replace("%%TRACEPOINT_HANDLERS_SKEL%%", tracepoint_handlers) + main_c = main_c.replace("%%TRACEPOINT_ATTACH%%", tracepoint_attach) + main_c = main_c.replace("%%TRACEPOINT_DETACH%%", tracepoint_detach) + main_c = main_c.replace("%%DESCRIPTION%%", self.description) + main_c = main_c.replace("%%PARENT%%", parent) + main_c = main_c.replace("%%INCLUDE_PARENT%%", parent_include) + + return main_c + + def fill_model_h(self): + return "NotImplemented" + + def fill_monitor_class_type(self): + return "NotImplemented" + + def fill_monitor_class(self): + return "NotImplemented" + + def fill_tracepoint_args_skel(self, tp_type): + return "NotImplemented" + + def fill_monitor_deps(self): + buff = [] + buff.append(" # XXX: add dependencies if there") + if self.parent: + buff.append(" depends on RV_MON_%s" % self.parent.upper()) + buff.append(" default y") + return '\n'.join(buff) + + def fill_kconfig(self): + kconfig = self.kconfig + monitor_class_type = self.fill_monitor_class_type() + monitor_deps = self.fill_monitor_deps() + kconfig = kconfig.replace("%%MODEL_NAME%%", self.name) + kconfig = kconfig.replace("%%MODEL_NAME_UP%%", self.name.upper()) + kconfig = kconfig.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) + kconfig = kconfig.replace("%%DESCRIPTION%%", self.description) + kconfig = kconfig.replace("%%MONITOR_DEPS%%", monitor_deps) + return kconfig + + def _patch_file(self, file, marker, line): + assert self.auto_patch + file_to_patch = os.path.join(self.rv_dir, file) + content = self._read_file(file_to_patch) + content = content.replace(marker, line + "\n" + marker) + self.__write_file(file_to_patch, content) + + def fill_tracepoint_tooltip(self): + monitor_class_type = self.fill_monitor_class_type() + if self.auto_patch: + self._patch_file("rv_trace.h", + "// Add new monitors based on CONFIG_%s here" % monitor_class_type, + "#include <monitors/%s/%s_trace.h>" % (self.name, self.name)) + return " - Patching %s/rv_trace.h, double check the result" % self.rv_dir + + return """ - Edit %s/rv_trace.h: +Add this line where other tracepoints are included and %s is defined: +#include <monitors/%s/%s_trace.h> +""" % (self.rv_dir, monitor_class_type, self.name, self.name) + + def _kconfig_marker(self, container=None) -> str: + return "# Add new %smonitors here" % (container + " " + if container else "") + + def fill_kconfig_tooltip(self): + if self.auto_patch: + # monitors with a container should stay together in the Kconfig + self._patch_file("Kconfig", + self._kconfig_marker(self.parent), + "source \"kernel/trace/rv/monitors/%s/Kconfig\"" % (self.name)) + return " - Patching %s/Kconfig, double check the result" % self.rv_dir + + return """ - Edit %s/Kconfig: +Add this line where other monitors are included: +source \"kernel/trace/rv/monitors/%s/Kconfig\" +""" % (self.rv_dir, self.name) + + def fill_makefile_tooltip(self): + name = self.name + name_up = name.upper() + if self.auto_patch: + self._patch_file("Makefile", + "# Add new monitors here", + "obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o" % (name_up, name, name)) + return " - Patching %s/Makefile, double check the result" % self.rv_dir + + return """ - Edit %s/Makefile: +Add this line where other monitors are included: +obj-$(CONFIG_RV_MON_%s) += monitors/%s/%s.o +""" % (self.rv_dir, name_up, name, name) + + def fill_monitor_tooltip(self): + if self.auto_patch: + return " - Monitor created in %s/monitors/%s" % (self.rv_dir, self. name) + return " - Move %s/ to the kernel's monitor directory (%s/monitors)" % (self.name, self.rv_dir) + + def __create_directory(self): + path = self.name + if self.auto_patch: + path = os.path.join(self.rv_dir, "monitors", path) + try: + os.mkdir(path) + except FileExistsError: + return + except: + print("Fail creating the output dir: %s" % self.name) + + def __write_file(self, file_name, content): + try: + file = open(file_name, 'w') + except: + print("Fail writing to file: %s" % file_name) + + file.write(content) + + file.close() + + def _create_file(self, file_name, content): + path = "%s/%s" % (self.name, file_name) + if self.auto_patch: + path = os.path.join(self.rv_dir, "monitors", path) + self.__write_file(path, content) + + def __get_main_name(self): + path = "%s/%s" % (self.name, "main.c") + if not os.path.exists(path): + return "main.c" + return "__main.c" + + def print_files(self): + main_c = self.fill_main_c() + + self.__create_directory() + + path = "%s.c" % self.name + self._create_file(path, main_c) + + model_h = self.fill_model_h() + path = "%s.h" % self.name + self._create_file(path, model_h) + + kconfig = self.fill_kconfig() + self._create_file("Kconfig", kconfig) + + +class Monitor(RVGenerator): + monitor_types = { "global" : 1, "per_cpu" : 2, "per_task" : 3 } + + def __init__(self, extra_params={}): + super().__init__(extra_params) + self.trace_h = self._read_template_file("trace.h") + + def fill_trace_h(self): + trace_h = self.trace_h + monitor_class = self.fill_monitor_class() + monitor_class_type = self.fill_monitor_class_type() + tracepoint_args_skel_event = self.fill_tracepoint_args_skel("event") + tracepoint_args_skel_error = self.fill_tracepoint_args_skel("error") + trace_h = trace_h.replace("%%MODEL_NAME%%", self.name) + trace_h = trace_h.replace("%%MODEL_NAME_UP%%", self.name.upper()) + trace_h = trace_h.replace("%%MONITOR_CLASS%%", monitor_class) + trace_h = trace_h.replace("%%MONITOR_CLASS_TYPE%%", monitor_class_type) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_EVENT%%", tracepoint_args_skel_event) + trace_h = trace_h.replace("%%TRACEPOINT_ARGS_SKEL_ERROR%%", tracepoint_args_skel_error) + return trace_h + + def print_files(self): + super().print_files() + trace_h = self.fill_trace_h() + path = "%s_trace.h" % self.name + self._create_file(path, trace_h) diff --git a/tools/verification/rvgen/rvgen/ltl2ba.py b/tools/verification/rvgen/rvgen/ltl2ba.py new file mode 100644 index 000000000000..f14e6760ac3d --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2ba.py @@ -0,0 +1,566 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only +# +# Implementation based on +# Gerth, R., Peled, D., Vardi, M.Y., Wolper, P. (1996). +# Simple On-the-fly Automatic Verification of Linear Temporal Logic. +# https://doi.org/10.1007/978-0-387-34892-6_1 +# With extra optimizations + +from ply.lex import lex +from ply.yacc import yacc + +# Grammar: +# ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl +# +# Operands (opd): +# true, false, user-defined names +# +# Unary Operators (unop): +# always +# eventually +# next +# not +# +# Binary Operators (binop): +# until +# and +# or +# imply +# equivalent + +tokens = ( + 'AND', + 'OR', + 'IMPLY', + 'UNTIL', + 'ALWAYS', + 'EVENTUALLY', + 'NEXT', + 'VARIABLE', + 'LITERAL', + 'NOT', + 'LPAREN', + 'RPAREN', + 'ASSIGN', +) + +t_AND = r'and' +t_OR = r'or' +t_IMPLY = r'imply' +t_UNTIL = r'until' +t_ALWAYS = r'always' +t_NEXT = r'next' +t_EVENTUALLY = r'eventually' +t_VARIABLE = r'[A-Z_0-9]+' +t_LITERAL = r'true|false' +t_NOT = r'not' +t_LPAREN = r'\(' +t_RPAREN = r'\)' +t_ASSIGN = r'=' +t_ignore_COMMENT = r'\#.*' +t_ignore = ' \t\n' + +def t_error(t): + raise ValueError(f"Illegal character '{t.value[0]}'") + +lexer = lex() + +class GraphNode: + uid = 0 + + def __init__(self, incoming: set['GraphNode'], new, old, _next): + self.init = False + self.outgoing = set() + self.labels = set() + self.incoming = incoming.copy() + self.new = new.copy() + self.old = old.copy() + self.next = _next.copy() + self.id = GraphNode.uid + GraphNode.uid += 1 + + def expand(self, node_set): + if not self.new: + for nd in node_set: + if nd.old == self.old and nd.next == self.next: + nd.incoming |= self.incoming + return node_set + + new_current_node = GraphNode({self}, self.next, set(), set()) + return new_current_node.expand({self} | node_set) + n = self.new.pop() + return n.expand(self, node_set) + + def __lt__(self, other): + return self.id < other.id + +class ASTNode: + uid = 1 + + def __init__(self, op): + self.op = op + self.id = ASTNode.uid + ASTNode.uid += 1 + + def __hash__(self): + return hash(self.op) + + def __eq__(self, other): + return self is other + + def __iter__(self): + yield self + yield from self.op + + def negate(self): + self.op = self.op.negate() + return self + + def expand(self, node, node_set): + return self.op.expand(self, node, node_set) + + def __str__(self): + if isinstance(self.op, Literal): + return str(self.op.value) + if isinstance(self.op, Variable): + return self.op.name.lower() + return "val" + str(self.id) + + def normalize(self): + # Get rid of: + # - ALWAYS + # - EVENTUALLY + # - IMPLY + # And move all the NOT to be inside + self.op = self.op.normalize() + return self + +class BinaryOp: + op_str = "not_supported" + + def __init__(self, left: ASTNode, right: ASTNode): + self.left = left + self.right = right + + def __hash__(self): + return hash((self.left, self.right)) + + def __iter__(self): + yield from self.left + yield from self.right + + def normalize(self): + raise NotImplementedError + + def negate(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.left.op.is_temporal(): + return True + if self.right.op.is_temporal(): + return True + return self._is_temporal() + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + raise NotImplementedError + +class AndOp(BinaryOp): + op_str = '&&' + + def normalize(self): + return self + + def negate(self): + return OrOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old.add(n) + return node.expand(node_set) + + tmp = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return tmp.expand(node_set) + +class OrOp(BinaryOp): + op_str = '||' + + def normalize(self): + return self + + def negate(self): + return AndOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.is_temporal(): + node.old |= {n} + return node.expand(node_set) + + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class UntilOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return VOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.left} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class VOp(BinaryOp): + def normalize(self): + return self + + def negate(self): + return UntilOp(self.left.negate(), self.right.negate()) + + def _is_temporal(self): + return True + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + node1 = GraphNode(node.incoming, + node.new | ({n.op.right} - node.old), + node.old | {n}, + node.next | {n}) + node2 = GraphNode(node.incoming, + node.new | ({n.op.left, n.op.right} - node.old), + node.old | {n}, + node.next) + return node2.expand(node1.expand(node_set)) + +class ImplyOp(BinaryOp): + def normalize(self): + # P -> Q === !P | Q + return OrOp(self.left.negate(), self.right) + + def _is_temporal(self): + return False + + def negate(self): + # !(P -> Q) === !(!P | Q) === P & !Q + return AndOp(self.left, self.right.negate()) + +class UnaryOp: + def __init__(self, child: ASTNode): + self.child = child + + def __iter__(self): + yield from self.child + + def __hash__(self): + return hash(self.child) + + def normalize(self): + raise NotImplementedError + + def _is_temporal(self): + raise NotImplementedError + + def is_temporal(self): + if self.child.op.is_temporal(): + return True + return self._is_temporal() + + def negate(self): + raise NotImplementedError + +class EventuallyOp(UnaryOp): + def __str__(self): + return "eventually " + str(self.child) + + def normalize(self): + # <>F == true U F + return UntilOp(ASTNode(Literal(True)), self.child) + + def _is_temporal(self): + return True + + def negate(self): + # !<>F == [](!F) + return AlwaysOp(self.child.negate()).normalize() + +class AlwaysOp(UnaryOp): + def normalize(self): + # []F === !(true U !F) == false V F + new = ASTNode(Literal(False)) + return VOp(new, self.child) + + def _is_temporal(self): + return True + + def negate(self): + # ![]F == <>(!F) + return EventuallyOp(self.child.negate()).normalize() + +class NextOp(UnaryOp): + def normalize(self): + return self + + def _is_temporal(self): + return True + + def negate(self): + # not (next A) == next (not A) + self.child = self.child.negate() + return self + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + tmp = GraphNode(node.incoming, + node.new, + node.old | {n}, + node.next | {n.op.child}) + return tmp.expand(node_set) + +class NotOp(UnaryOp): + def __str__(self): + return "!" + str(self.child) + + def normalize(self): + return self.child.op.negate() + + def negate(self): + return self.child.op + + def _is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if n.op.child is f: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Variable: + def __init__(self, name: str): + self.name = name + + def __hash__(self): + return hash(self.name) + + def __iter__(self): + yield from () + + def negate(self): + new = ASTNode(self) + return NotOp(new) + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + for f in node.old: + if isinstance(f, NotOp) and f.op.child is n: + return node_set + node.old |= {n} + return node.expand(node_set) + +class Literal: + def __init__(self, value: bool): + self.value = value + + def __iter__(self): + yield from () + + def __hash__(self): + return hash(self.value) + + def __str__(self): + if self.value: + return "true" + return "false" + + def negate(self): + self.value = not self.value + return self + + def normalize(self): + return self + + def is_temporal(self): + return False + + @staticmethod + def expand(n: ASTNode, node: GraphNode, node_set) -> set[GraphNode]: + if not n.op.value: + return node_set + node.old |= {n} + return node.expand(node_set) + +def p_spec(p): + ''' + spec : assign + | assign spec + ''' + if len(p) == 3: + p[2].append(p[1]) + p[0] = p[2] + else: + p[0] = [p[1]] + +def p_assign(p): + ''' + assign : VARIABLE ASSIGN ltl + ''' + p[0] = (p[1], p[3]) + +def p_ltl(p): + ''' + ltl : opd + | binop + | unop + ''' + p[0] = p[1] + +def p_opd(p): + ''' + opd : VARIABLE + | LITERAL + | LPAREN ltl RPAREN + ''' + if p[1] == "true": + p[0] = ASTNode(Literal(True)) + elif p[1] == "false": + p[0] = ASTNode(Literal(False)) + elif p[1] == '(': + p[0] = p[2] + else: + p[0] = ASTNode(Variable(p[1])) + +def p_unop(p): + ''' + unop : ALWAYS ltl + | EVENTUALLY ltl + | NEXT ltl + | NOT ltl + ''' + if p[1] == "always": + op = AlwaysOp(p[2]) + elif p[1] == "eventually": + op = EventuallyOp(p[2]) + elif p[1] == "next": + op = NextOp(p[2]) + elif p[1] == "not": + op = NotOp(p[2]) + else: + raise ValueError(f"Invalid unary operator {p[1]}") + + p[0] = ASTNode(op) + +def p_binop(p): + ''' + binop : opd UNTIL ltl + | opd AND ltl + | opd OR ltl + | opd IMPLY ltl + ''' + if p[2] == "and": + op = AndOp(p[1], p[3]) + elif p[2] == "until": + op = UntilOp(p[1], p[3]) + elif p[2] == "or": + op = OrOp(p[1], p[3]) + elif p[2] == "imply": + op = ImplyOp(p[1], p[3]) + else: + raise ValueError(f"Invalid binary operator {p[2]}") + + p[0] = ASTNode(op) + +parser = yacc() + +def parse_ltl(s: str) -> ASTNode: + spec = parser.parse(s) + + rule = None + subexpr = {} + + for assign in spec: + if assign[0] == "RULE": + rule = assign[1] + else: + subexpr[assign[0]] = assign[1] + + if rule is None: + raise ValueError("Please define your specification in the \"RULE = <LTL spec>\" format") + + for node in rule: + if not isinstance(node.op, Variable): + continue + replace = subexpr.get(node.op.name) + if replace is not None: + node.op = replace.op + + return rule + +def create_graph(s: str): + atoms = set() + + ltl = parse_ltl(s) + for c in ltl: + c.normalize() + if isinstance(c.op, Variable): + atoms.add(c.op.name) + + init = GraphNode(set(), set(), set(), set()) + head = GraphNode({init}, {ltl}, set(), set()) + graph = sorted(head.expand(set())) + + for i, node in enumerate(graph): + # The id assignment during graph generation has gaps. Reassign them + node.id = i + + for incoming in node.incoming: + if incoming is init: + node.init = True + else: + incoming.outgoing.add(node) + for o in node.old: + if not o.op.is_temporal(): + node.labels.add(str(o)) + + return sorted(atoms), graph, ltl diff --git a/tools/verification/rvgen/rvgen/ltl2k.py b/tools/verification/rvgen/rvgen/ltl2k.py new file mode 100644 index 000000000000..b075f98d50c4 --- /dev/null +++ b/tools/verification/rvgen/rvgen/ltl2k.py @@ -0,0 +1,271 @@ +#!/usr/bin/env python3 +# SPDX-License-Identifier: GPL-2.0-only + +from pathlib import Path +from . import generator +from . import ltl2ba + +COLUMN_LIMIT = 100 + +def line_len(line: str) -> int: + tabs = line.count('\t') + return tabs * 7 + len(line) + +def break_long_line(line: str, indent='') -> list[str]: + result = [] + while line_len(line) > COLUMN_LIMIT: + i = line[:COLUMN_LIMIT - line_len(line)].rfind(' ') + result.append(line[:i]) + line = indent + line[i + 1:] + if line: + result.append(line) + return result + +def build_condition_string(node: ltl2ba.GraphNode): + if not node.labels: + return "(true)" + + result = "(" + + first = True + for label in sorted(node.labels): + if not first: + result += " && " + result += label + first = False + + result += ")" + + return result + +def abbreviate_atoms(atoms: list[str]) -> list[str]: + def shorten(s: str) -> str: + skip = ["is", "by", "or", "and"] + return '_'.join([x[:2] for x in s.lower().split('_') if x not in skip]) + + abbrs = [] + for atom in atoms: + for i in range(len(atom), -1, -1): + if sum(a.startswith(atom[:i]) for a in atoms) > 1: + break + share = atom[:i] + unique = atom[i:] + abbrs.append((shorten(share) + shorten(unique))) + return abbrs + +class ltl2k(generator.Monitor): + template_dir = "ltl2k" + + def __init__(self, file_path, MonitorType, extra_params={}): + if MonitorType != "per_task": + raise NotImplementedError("Only per_task monitor is supported for LTL") + super().__init__(extra_params) + with open(file_path) as f: + self.atoms, self.ba, self.ltl = ltl2ba.create_graph(f.read()) + self.atoms_abbr = abbreviate_atoms(self.atoms) + self.name = extra_params.get("model_name") + if not self.name: + self.name = Path(file_path).stem + + def _fill_states(self) -> str: + buf = [ + "enum ltl_buchi_state {", + ] + + for node in self.ba: + buf.append("\tS%i," % node.id) + buf.append("\tRV_NUM_BA_STATES") + buf.append("};") + buf.append("static_assert(RV_NUM_BA_STATES <= RV_MAX_BA_STATES);") + return buf + + def _fill_atoms(self): + buf = ["enum ltl_atom {"] + for a in sorted(self.atoms): + buf.append("\tLTL_%s," % a) + buf.append("\tLTL_NUM_ATOM") + buf.append("};") + buf.append("static_assert(LTL_NUM_ATOM <= RV_MAX_LTL_ATOM);") + return buf + + def _fill_atoms_to_string(self): + buf = [ + "static const char *ltl_atom_str(enum ltl_atom atom)", + "{", + "\tstatic const char *const names[] = {" + ] + + for name in self.atoms_abbr: + buf.append("\t\t\"%s\"," % name) + + buf.extend([ + "\t};", + "", + "\treturn names[atom];", + "}" + ]) + return buf + + def _fill_atom_values(self, required_values): + buf = [] + for node in self.ltl: + if str(node) not in required_values: + continue + + if isinstance(node.op, ltl2ba.AndOp): + buf.append("\tbool %s = %s && %s;" % (node, node.op.left, node.op.right)) + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.OrOp): + buf.append("\tbool %s = %s || %s;" % (node, node.op.left, node.op.right)) + required_values |= {str(node.op.left), str(node.op.right)} + elif isinstance(node.op, ltl2ba.NotOp): + buf.append("\tbool %s = !%s;" % (node, node.op.child)) + required_values.add(str(node.op.child)) + + for atom in self.atoms: + if atom.lower() not in required_values: + continue + buf.append("\tbool %s = test_bit(LTL_%s, mon->atoms);" % (atom.lower(), atom)) + + buf.reverse() + + buf2 = [] + for line in buf: + buf2.extend(break_long_line(line, "\t ")) + return buf2 + + def _fill_transitions(self): + buf = [ + "static void", + "ltl_possible_next_states(struct ltl_monitor *mon, unsigned int state, unsigned long *next)", + "{" + ] + + required_values = set() + for node in self.ba: + for o in sorted(node.outgoing): + required_values |= o.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.extend([ + "", + "\tswitch (state) {" + ]) + + for node in self.ba: + buf.append("\tcase S%i:" % node.id) + + for o in sorted(node.outgoing): + line = "\t\tif " + indent = "\t\t " + + line += build_condition_string(o) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t\t__set_bit(S%i, next);" % o.id) + buf.append("\t\tbreak;") + buf.extend([ + "\t}", + "}" + ]) + + return buf + + def _fill_start(self): + buf = [ + "static void ltl_start(struct task_struct *task, struct ltl_monitor *mon)", + "{" + ] + + required_values = set() + for node in self.ba: + if node.init: + required_values |= node.labels + + buf.extend(self._fill_atom_values(required_values)) + buf.append("") + + for node in self.ba: + if not node.init: + continue + + line = "\tif " + indent = "\t " + + line += build_condition_string(node) + lines = break_long_line(line, indent) + buf.extend(lines) + + buf.append("\t\t__set_bit(S%i, mon->states);" % node.id) + buf.append("}") + return buf + + def fill_tracepoint_handlers_skel(self): + buff = [] + buff.append("static void handle_example_event(void *data, /* XXX: fill header */)") + buff.append("{") + buff.append("\tltl_atom_update(task, LTL_%s, true/false);" % self.atoms[0]) + buff.append("}") + buff.append("") + return '\n'.join(buff) + + def fill_tracepoint_attach_probe(self): + return "\trv_attach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_example_event);" \ + % self.name + + def fill_tracepoint_detach_helper(self): + return "\trv_detach_trace_probe(\"%s\", /* XXX: tracepoint */, handle_sample_event);" \ + % self.name + + def fill_atoms_init(self): + buff = [] + for a in self.atoms: + buff.append("\tltl_atom_set(mon, LTL_%s, true/false);" % a) + return '\n'.join(buff) + + def fill_model_h(self): + buf = [ + "/* SPDX-License-Identifier: GPL-2.0 */", + "", + "/*", + " * C implementation of Buchi automaton, automatically generated by", + " * tools/verification/rvgen from the linear temporal logic specification.", + " * For further information, see kernel documentation:", + " * Documentation/trace/rv/linear_temporal_logic.rst", + " */", + "", + "#include <linux/rv.h>", + "", + "#define MONITOR_NAME " + self.name, + "" + ] + + buf.extend(self._fill_atoms()) + buf.append('') + + buf.extend(self._fill_atoms_to_string()) + buf.append('') + + buf.extend(self._fill_states()) + buf.append('') + + buf.extend(self._fill_start()) + buf.append('') + + buf.extend(self._fill_transitions()) + buf.append('') + + return '\n'.join(buf) + + def fill_monitor_class_type(self): + return "LTL_MON_EVENTS_ID" + + def fill_monitor_class(self): + return "ltl_monitor_id" + + def fill_main_c(self): + main_c = super().fill_main_c() + main_c = main_c.replace("%%ATOMS_INIT%%", self.fill_atoms_init()) + + return main_c diff --git a/tools/verification/rvgen/rvgen/templates/Kconfig b/tools/verification/rvgen/rvgen/templates/Kconfig new file mode 100644 index 000000000000..291b29ea28db --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/Kconfig @@ -0,0 +1,9 @@ +# SPDX-License-Identifier: GPL-2.0-only +# +config RV_MON_%%MODEL_NAME_UP%% + depends on RV +%%MONITOR_DEPS%% + select %%MONITOR_CLASS_TYPE%% + bool "%%MODEL_NAME%% monitor" + help + %%DESCRIPTION%% diff --git a/tools/verification/rvgen/rvgen/templates/container/Kconfig b/tools/verification/rvgen/rvgen/templates/container/Kconfig new file mode 100644 index 000000000000..a606111949c2 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/Kconfig @@ -0,0 +1,5 @@ +config RV_MON_%%MODEL_NAME_UP%% + depends on RV + bool "%%MODEL_NAME%% monitor" + help + %%DESCRIPTION%% diff --git a/tools/verification/rvgen/rvgen/templates/container/main.c b/tools/verification/rvgen/rvgen/templates/container/main.c new file mode 100644 index 000000000000..7d9b2f95c7e9 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/main.c @@ -0,0 +1,37 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> + +#define MODULE_NAME "%%MODEL_NAME%%" + +#include "%%MODEL_NAME%%.h" + +struct rv_monitor rv_%%MODEL_NAME%%; + +struct rv_monitor rv_%%MODEL_NAME%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = NULL, + .disable = NULL, + .reset = NULL, + .enabled = 0, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/container/main.h b/tools/verification/rvgen/rvgen/templates/container/main.h new file mode 100644 index 000000000000..0f6883ab4bcc --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/container/main.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +extern struct rv_monitor rv_%%MODEL_NAME%%; diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/main.c b/tools/verification/rvgen/rvgen/templates/dot2k/main.c new file mode 100644 index 000000000000..e0fd1134bd85 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/dot2k/main.c @@ -0,0 +1,90 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> +#include <rv/da_monitor.h> + +#define MODULE_NAME "%%MODEL_NAME%%" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +%%INCLUDE_PARENT%% +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "%%MODEL_NAME%%.h" + +/* + * Declare the deterministic automata monitor. + * + * The rv monitor reference is needed for the monitor declaration. + */ +static struct rv_monitor rv_%%MODEL_NAME%%; +DECLARE_DA_MON_%%MONITOR_TYPE%%(%%MODEL_NAME%%, %%MIN_TYPE%%); + +/* + * This is the instrumentation part of the monitor. + * + * This is the section where manual work is required. Here the kernel events + * are translated into model's event. + * + */ +%%TRACEPOINT_HANDLERS_SKEL%% +static int enable_%%MODEL_NAME%%(void) +{ + int retval; + + retval = da_monitor_init_%%MODEL_NAME%%(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ + rv_%%MODEL_NAME%%.enabled = 0; + +%%TRACEPOINT_DETACH%% + + da_monitor_destroy_%%MODEL_NAME%%(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_%%MODEL_NAME%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = enable_%%MODEL_NAME%%, + .disable = disable_%%MODEL_NAME%%, + .reset = da_monitor_reset_all_%%MODEL_NAME%%, + .enabled = 0, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR("dot2k: auto-generated"); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/dot2k/trace.h b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h new file mode 100644 index 000000000000..87d3a1308926 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/dot2k/trace.h @@ -0,0 +1,13 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% +DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, +%%TRACEPOINT_ARGS_SKEL_EVENT%%); + +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, +%%TRACEPOINT_ARGS_SKEL_ERROR%%); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/main.c b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c new file mode 100644 index 000000000000..f85d076fbf78 --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/main.c @@ -0,0 +1,102 @@ +// SPDX-License-Identifier: GPL-2.0 +#include <linux/ftrace.h> +#include <linux/tracepoint.h> +#include <linux/kernel.h> +#include <linux/module.h> +#include <linux/init.h> +#include <linux/rv.h> +#include <rv/instrumentation.h> + +#define MODULE_NAME "%%MODEL_NAME%%" + +/* + * XXX: include required tracepoint headers, e.g., + * #include <trace/events/sched.h> + */ +#include <rv_trace.h> +%%INCLUDE_PARENT%% + +/* + * This is the self-generated part of the monitor. Generally, there is no need + * to touch this section. + */ +#include "%%MODEL_NAME%%.h" +#include <rv/ltl_monitor.h> + +static void ltl_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon) +{ + /* + * This is called everytime the Buchi automaton is triggered. + * + * This function could be used to fetch the atomic propositions which + * are expensive to trace. It is possible only if the atomic proposition + * does not need to be updated at precise time. + * + * It is recommended to use tracepoints and ltl_atom_update() instead. + */ +} + +static void ltl_atoms_init(struct task_struct *task, struct ltl_monitor *mon, bool task_creation) +{ + /* + * This should initialize as many atomic propositions as possible. + * + * @task_creation indicates whether the task is being created. This is + * false if the task is already running before the monitor is enabled. + */ +%%ATOMS_INIT%% +} + +/* + * This is the instrumentation part of the monitor. + * + * This is the section where manual work is required. Here the kernel events + * are translated into model's event. + */ +%%TRACEPOINT_HANDLERS_SKEL%% +static int enable_%%MODEL_NAME%%(void) +{ + int retval; + + retval = ltl_monitor_init(); + if (retval) + return retval; + +%%TRACEPOINT_ATTACH%% + + return 0; +} + +static void disable_%%MODEL_NAME%%(void) +{ +%%TRACEPOINT_DETACH%% + + ltl_monitor_destroy(); +} + +/* + * This is the monitor register section. + */ +static struct rv_monitor rv_%%MODEL_NAME%% = { + .name = "%%MODEL_NAME%%", + .description = "%%DESCRIPTION%%", + .enable = enable_%%MODEL_NAME%%, + .disable = disable_%%MODEL_NAME%%, +}; + +static int __init register_%%MODEL_NAME%%(void) +{ + return rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); +} + +static void __exit unregister_%%MODEL_NAME%%(void) +{ + rv_unregister_monitor(&rv_%%MODEL_NAME%%); +} + +module_init(register_%%MODEL_NAME%%); +module_exit(unregister_%%MODEL_NAME%%); + +MODULE_LICENSE("GPL"); +MODULE_AUTHOR(/* TODO */); +MODULE_DESCRIPTION("%%MODEL_NAME%%: %%DESCRIPTION%%"); diff --git a/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h new file mode 100644 index 000000000000..49394c4b0f1c --- /dev/null +++ b/tools/verification/rvgen/rvgen/templates/ltl2k/trace.h @@ -0,0 +1,14 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +/* + * Snippet to be included in rv_trace.h + */ + +#ifdef CONFIG_RV_MON_%%MODEL_NAME_UP%% +DEFINE_EVENT(event_%%MONITOR_CLASS%%, event_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task, char *states, char *atoms, char *next), + TP_ARGS(task, states, atoms, next)); +DEFINE_EVENT(error_%%MONITOR_CLASS%%, error_%%MODEL_NAME%%, + TP_PROTO(struct task_struct *task), + TP_ARGS(task)); +#endif /* CONFIG_RV_MON_%%MODEL_NAME_UP%% */ |