diff options
Diffstat (limited to 'tools/verification/dot2/dot2k_templates')
8 files changed, 154 insertions, 273 deletions
diff --git a/tools/verification/dot2/dot2k_templates/Kconfig b/tools/verification/dot2/dot2k_templates/Kconfig new file mode 100644 index 000000000000..291b29ea28db --- /dev/null +++ b/tools/verification/dot2/dot2k_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/dot2/dot2k_templates/main.c b/tools/verification/dot2/dot2k_templates/main.c new file mode 100644 index 000000000000..83044a20c89a --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/main.c @@ -0,0 +1,91 @@ +// 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) +{ + rv_register_monitor(&rv_%%MODEL_NAME%%, %%PARENT%%); + 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%%: %%DESCRIPTION%%"); diff --git a/tools/verification/dot2/dot2k_templates/main_container.c b/tools/verification/dot2/dot2k_templates/main_container.c new file mode 100644 index 000000000000..89fc17cf8958 --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/main_container.c @@ -0,0 +1,38 @@ +// 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) +{ + rv_register_monitor(&rv_%%MODEL_NAME%%, NULL); + 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%%: %%DESCRIPTION%%"); diff --git a/tools/verification/dot2/dot2k_templates/main_container.h b/tools/verification/dot2/dot2k_templates/main_container.h new file mode 100644 index 000000000000..0f6883ab4bcc --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/main_container.h @@ -0,0 +1,3 @@ +/* SPDX-License-Identifier: GPL-2.0 */ + +extern struct rv_monitor rv_%%MODEL_NAME%%; 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/dot2/dot2k_templates/trace.h b/tools/verification/dot2/dot2k_templates/trace.h new file mode 100644 index 000000000000..87d3a1308926 --- /dev/null +++ b/tools/verification/dot2/dot2k_templates/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%% */ |