| lists.openwall.net | lists / announce owl-users owl-dev john-users john-dev passwdqc-users yescrypt popa3d-users / oss-security kernel-hardening musl sabotage tlsify passwords / crypt-dev xvendor / Bugtraq Full-Disclosure linux-kernel linux-netdev linux-ext4 linux-hardening linux-cve-announce PHC | |
|
Open Source and information security mailing list archives
| ||
|
Message-Id: <0b03a7d779707c598068d6ec00f3e5a19de336d8.1741708239.git.namcao@linutronix.de>
Date: Tue, 11 Mar 2025 18:05:04 +0100
From: Nam Cao <namcao@...utronix.de>
To: Steven Rostedt <rostedt@...dmis.org>,
Gabriele Monaco <gmonaco@...hat.com>,
john.ogness@...utronix.de,
linux-trace-kernel@...r.kernel.org,
linux-kernel@...r.kernel.org
Cc: Nam Cao <namcao@...utronix.de>
Subject: [PATCH 03/10] rv: Add infrastructure for linear temporal logic monitor
Prepare the infrastructure for linear temporal logic monitors:
- add scripts for generating the monitors
- implement data structures
For details, see:
Documentation/trace/rv/linear_temporal_logic.rst
Signed-off-by: Nam Cao <namcao@...utronix.de>
---
.../trace/rv/linear_temporal_logic.rst | 73 +++
include/linux/rv.h | 26 +-
kernel/fork.c | 5 +-
tools/verification/ltl2ba/.gitignore | 3 +
tools/verification/ltl2ba/generate.py | 154 +++++
tools/verification/ltl2ba/ltl.py | 556 ++++++++++++++++++
tools/verification/ltl2ba/template.c | 131 +++++
tools/verification/ltl2ba/template.h | 157 +++++
8 files changed, 1097 insertions(+), 8 deletions(-)
create mode 100644 Documentation/trace/rv/linear_temporal_logic.rst
create mode 100644 tools/verification/ltl2ba/.gitignore
create mode 100755 tools/verification/ltl2ba/generate.py
create mode 100644 tools/verification/ltl2ba/ltl.py
create mode 100644 tools/verification/ltl2ba/template.c
create mode 100644 tools/verification/ltl2ba/template.h
diff --git a/Documentation/trace/rv/linear_temporal_logic.rst b/Documentation/trace/rv/linear_temporal_logic.rst
new file mode 100644
index 000000000000..9b0ce6a143ec
--- /dev/null
+++ b/Documentation/trace/rv/linear_temporal_logic.rst
@@ -0,0 +1,73 @@
+Introduction
+============
+
+Deterministic automaton runtime verification monitor is a verification technique which checks that
+the kernel follows a specification in the form of deterministic automaton (DA). It does so by using
+tracepoints to monitor the kernel's execution trace, and verifying that the execution trace
+sastifies the specification.
+
+However, while attempting to implement DA monitors for some complex specifications, deterministic
+automaton is found to be inappropriate as the specification language. The automaton is complicated,
+hard to understand, and error-prone.
+
+Thus, RV monitors based on linear temporal logic (LTL for short) are introduced. This type of
+monitor uses LTL as specification, instead of DA. For some cases, writing the specification as LTL
+is more concise and intuitive.
+
+Documents regarding LTL are widely available on the internet, this document will not go into
+details.
+
+Grammar
+========
+
+Unlike some existing syntax, kernel's implementation of LTL is more verbose. This is motivated by
+considering that the people who read the LTL specifications may not be well-versed in LTL.
+
+Grammar:
+ ltl ::= opd | ( ltl ) | ltl binop ltl | unop ltl
+
+Operands (opd):
+ true, false, user-defined names consisting of upper-case characters, digits, and underscore.
+
+Unary Operators (unop):
+ always
+ eventually
+ not
+
+Binary Operators (binop):
+ until
+ and
+ or
+ imply
+ equivalent
+
+This grammar is ambiguous: operator precedence is not defined. Parentheses must be used.
+
+Monitor synthesis
+=================
+
+To synthesize an LTL into a kernel monitor, conversion scripts are provided:
+`tools/verification/ltl2ba`. The specification needs to be provided as a file, and it must have a
+"RULE = LTL" assignment, which specifies the LTL property to verify. For example:
+
+ .. code-block::
+
+ RULE = always (ACQUIRE imply ((not KILLED and not CRASHED) until RELEASE))
+
+The LTL can be broken down if required using sub-expressions. For example, the above is equivalent
+to:
+
+ .. code-block::
+
+ RULE = always (ACQUIRE imply (ALIVE until RELEASE))
+ ALIVE = not KILLED and not CRASHED
+
+The ltl file can be converted into C code:
+
+ .. code-block::
+
+ .tools/verification/ltl2ba/generate.py -l <ltl file> -n <model name> -o <output diretory>
+
+The above command generates `ba.c` and `ba.h`, the Buchi automaton that verifies the LTL property.
+The Buchi automaton needs to be manually glued to the kernel. Please see the comments in `ba.h` for
+further details.
diff --git a/include/linux/rv.h b/include/linux/rv.h
index 5482651ed020..6de4f93b390e 100644
--- a/include/linux/rv.h
+++ b/include/linux/rv.h
@@ -10,6 +10,8 @@
#define MAX_DA_NAME_LEN 24
#ifdef CONFIG_RV
+#include <linux/types.h>
+
/*
* Deterministic automaton per-object variables.
*/
@@ -18,6 +20,24 @@ struct da_monitor {
unsigned int curr_state;
};
+enum ltl_truth_value {
+ LTL_FALSE,
+ LTL_TRUE,
+ LTL_UNDETERMINED,
+};
+
+/*
+ * In the future, if the number of atomic propositions or the custom data size is larger, we can
+ * switch to dynamic allocation. For now, the code is simpler this way.
+ */
+#define RV_MAX_LTL_ATOM 10
+#define RV_MAX_DATA_SIZE 16
+struct ltl_monitor {
+ unsigned int state;
+ enum ltl_truth_value atoms[RV_MAX_LTL_ATOM];
+ u8 data[RV_MAX_DATA_SIZE];
+};
+
/*
* Per-task RV monitors count. Nowadays fixed in RV_PER_TASK_MONITORS.
* If we find justification for more monitors, we can think about
@@ -27,11 +47,9 @@ struct da_monitor {
#define RV_PER_TASK_MONITORS 1
#define RV_PER_TASK_MONITOR_INIT (RV_PER_TASK_MONITORS)
-/*
- * Futher monitor types are expected, so make this a union.
- */
union rv_task_monitor {
- struct da_monitor da_mon;
+ struct da_monitor da_mon;
+ struct ltl_monitor ltl_mon;
};
#ifdef CONFIG_RV_REACTORS
diff --git a/kernel/fork.c b/kernel/fork.c
index 735405a9c5f3..5d6c1caca702 100644
--- a/kernel/fork.c
+++ b/kernel/fork.c
@@ -2127,10 +2127,7 @@ static void copy_oom_score_adj(u64 clone_flags, struct task_struct *tsk)
#ifdef CONFIG_RV
static void rv_task_fork(struct task_struct *p)
{
- int i;
-
- for (i = 0; i < RV_PER_TASK_MONITORS; i++)
- p->rv[i].da_mon.monitoring = false;
+ memset(p->rv, 0, sizeof(p->rv));
}
#else
#define rv_task_fork(p) do {} while (0)
diff --git a/tools/verification/ltl2ba/.gitignore b/tools/verification/ltl2ba/.gitignore
new file mode 100644
index 000000000000..9c47b9724860
--- /dev/null
+++ b/tools/verification/ltl2ba/.gitignore
@@ -0,0 +1,3 @@
+__pycache__/
+parsetab.py
+parser.out
diff --git a/tools/verification/ltl2ba/generate.py b/tools/verification/ltl2ba/generate.py
new file mode 100755
index 000000000000..52d5b3618e64
--- /dev/null
+++ b/tools/verification/ltl2ba/generate.py
@@ -0,0 +1,154 @@
+#!/usr/bin/env python3
+# SPDX-License-Identifier: GPL-2.0-only
+
+import argparse
+import ntpath
+import os
+import platform
+from pathlib import Path
+import sys
+import ltl
+
+parser = argparse.ArgumentParser(description='transform ltl file into kernel rv monitor')
+parser.add_argument('-l', "--ltl", dest="ltl", required=True)
+parser.add_argument('-n', "--model_name", dest="model_name", required=True)
+parser.add_argument('-o', "--outdir", dest="outdir", required=True)
+params = parser.parse_args()
+
+with open(params.ltl) as f:
+ atoms, graph = ltl.create_graph(f.read())
+states = []
+transitions = []
+init_conditions = []
+
+COLUMN_LIMIT = 100
+
+def build_condition_string(node: ltl.GraphNode):
+ if not node.labels:
+ return "(true)"
+
+ result = "("
+
+ first = True
+ for l in sorted(node.labels):
+ if not first:
+ result += " && "
+ result += '(' + l + ')'
+ first = False
+
+ result += ")"
+
+ return result
+
+def build_states() -> str:
+ states = ''
+ for node in graph:
+ states += "\t%s,\n" % node.name
+ return states
+
+def build_atoms() -> str:
+ global atoms
+ s = ''
+ for a in sorted(atoms):
+ s += "\t%s,\n" % a
+ return s
+
+def build_transitions() -> list[str]:
+ transitions = []
+ for node in graph:
+ transitions.append("\tcase %s:\n" % node.name)
+
+ result = ""
+ first = True
+ for o in sorted(node.outgoing):
+ if first:
+ result += "\t\tif "
+ cursor = 19
+ else:
+ result += "\t\telse if "
+ cursor = 24
+
+ condition = build_condition_string(o)
+
+ while len(condition) + cursor > COLUMN_LIMIT:
+ i = condition[:COLUMN_LIMIT - cursor].rfind(' ')
+ result += condition[:i]
+ if cursor == 19:
+ result += '\n\t\t '
+ elif cursor == 24:
+ result += '\t\t\t\t'
+ else:
+ raise ValueError()
+ condition = condition[i + 1:]
+
+ result += condition
+
+ result += '\n'
+ result += ("\t\t\tmon->state = %s;\n" % o.name)
+ first = False
+ result += "\t\telse\n\t\t\tillegal_state(task, mon);\n"
+ result += "\t\tbreak;\n"
+ transitions.append(result)
+ return transitions
+
+def build_initial_conditions() -> str:
+ result = ""
+ first = True
+
+ for node in graph:
+ if not node.init:
+ continue
+
+ if not first:
+ result += "\telse if "
+ cursor = 16
+ else:
+ result += "\tif "
+ cursor = 11
+
+ condition = build_condition_string(node)
+ while len(condition) + cursor > COLUMN_LIMIT:
+ i = condition[:COLUMN_LIMIT - cursor].rfind(' ')
+ result += condition[:i]
+ if cursor == 16:
+ result += '\n\t\t'
+ elif cursor == 11:
+ result += '\n\t '
+ else:
+ raise ValueError()
+ condition = condition[i + 1:]
+
+ result += condition
+ result += '\n'
+ result += ("\t\tmon->state = %s;\n" % node.name)
+ first = False
+ result += "\telse\n\t\tillegal_state(task, mon);\n"
+ return result
+
+template = Path(__file__).with_name('template.h')
+out = os.path.join(params.outdir, "ba.h")
+with template.open() as template, open(out, "w") as file:
+ for line in template:
+ if line == "%%ATOM_LIST%%\n":
+ file.write(build_atoms())
+ else:
+ line = line.replace("%%MODEL_NAME%%", params.model_name)
+ file.write(line)
+
+template = Path(__file__).with_name('template.c')
+out = os.path.join(params.outdir, "ba.c")
+with template.open() as template, open(out, "w") as file:
+ for line in template:
+ if line == "%%STATE_LIST%%\n":
+ file.write(build_states())
+ elif line == "%%BUCHI_START%%\n":
+ file.write(build_initial_conditions())
+ elif line == "%%BUCHI_TRANSITIONS%%\n":
+ for t in build_transitions():
+ file.write(t)
+ elif line == "%%ERROR_MESSAGE%%\n":
+ file.write(build_error_message())
+ else:
+ line = line.replace("%%MODEL_NAME%%", params.model_name)
+ line = line.replace("%%LTL%%", params.ltl)
+ file.write(line)
diff --git a/tools/verification/ltl2ba/ltl.py b/tools/verification/ltl2ba/ltl.py
new file mode 100644
index 000000000000..aa3a11d78a8e
--- /dev/null
+++ b/tools/verification/ltl2ba/ltl.py
@@ -0,0 +1,556 @@
+#!/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
+# not
+#
+# Binary Operators (binop):
+# until
+# and
+# or
+# imply
+# equivalent
+
+tokens = (
+ 'AND',
+ 'OR',
+ 'IMPLY',
+ 'UNTIL',
+ 'ALWAYS',
+ 'EVENTUALLY',
+ '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_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("Illegal character '%s'" % t.value[0])
+
+lexer = lex()
+
+_new_name_counter = 0
+def new_name():
+ global _new_name_counter
+
+ _new_name_counter += 1
+
+ return "S" + str(_new_name_counter)
+
+class GraphNode:
+ def __init__(self, name: str, incoming: set['GraphNode'], new, old, _next):
+ self.init = False
+ self.outgoing = set()
+ self.labels = set()
+ self.incoming = incoming
+ self.name = name
+ self.new = new.copy()
+ self.old = old.copy()
+ self.next = _next.copy()
+
+ 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
+ for i in self.incoming:
+ i.outgoing.add(nd)
+ return node_set
+
+ new_current_node = GraphNode(new_name(), {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.name < other.name
+
+class ASTNode:
+ def __init__(self,op):
+ self.op = op
+
+ def __hash__(self):
+ return hash(self.op)
+
+ def __str__(self):
+ return str(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 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 __str__(self):
+ return "(%s %s %s)" % (self.left, self.op_str, self.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 NotImplemented
+
+ def negate(self):
+ raise NotImplemented
+
+ def _is_temporal(self):
+ raise NotImplemented
+
+ 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 NotImplemented
+
+class AndOp(BinaryOp):
+ op_str = '&&'
+
+ def __init__(self, left, right):
+ super().__init__(left, right)
+
+ 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.name, 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 __init__(self, left, right):
+ super().__init__(left, right)
+
+ 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(new_name(), node.incoming,
+ node.new | ({n.op.left} - node.old),
+ node.old | {n},
+ node.next)
+ node2 = GraphNode(new_name(), 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 __init__(self, left, right):
+ super().__init__(left, right)
+
+ 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(new_name(), node.incoming,
+ node.new | ({n.op.left} - node.old),
+ node.old | {n},
+ node.next | {n})
+ node2 = GraphNode(new_name(), 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 __init__(self, left, right):
+ super().__init__(left, right)
+
+ 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(new_name(), node.incoming,
+ node.new | ({n.op.right} - node.old),
+ node.old | {n},
+ node.next | {n})
+ node2 = GraphNode(new_name(), 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 __init__(self, left, right):
+ super().__init__(left, right)
+
+ def normalize(self):
+ # P -> Q === !P | Q
+ return OrOp(self.left.negate(), self.right)
+
+ def _is_temporal(self):
+ return False
+
+ def negate():
+ # !(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 NotImplemented
+
+ def _is_temporal(self):
+ raise NotImplemented
+
+ def is_temporal(self):
+ if self.child.op.is_temporal():
+ return True
+ return self._is_temporal()
+
+ def negate(self):
+ raise NotImplemented
+
+class EventuallyOp(UnaryOp):
+ def __init__(self, child):
+ super().__init__(child)
+
+ def __str__(self):
+ return "eventually " + str(self.child)
+
+ def normalize(self):
+ # <>F == true U F
+ return UntilOp(Literal(True), self.right)
+
+ def _is_temporal(self):
+ return True
+
+ def negate(self):
+ # !<>F == [](!F)
+ return AlwaysOp(self.right.negate()).normalize()
+
+class AlwaysOp(UnaryOp):
+ def __init__(self, child):
+ super().__init__(child)
+
+ 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.left, self.right.negate()).normalize()
+
+class NotOp(UnaryOp):
+ def __init__(self, child):
+ super().__init__(child)
+
+ 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 __str__(self):
+ return "mon->atoms[%s]" % self.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
+ | NOT ltl
+ '''
+ if p[1] == "always":
+ op = AlwaysOp(p[2])
+ if p[1] == "eventually":
+ op = EventuallyOp(p[2])
+ if p[1] == "not":
+ op = NotOp(p[2])
+
+ 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("Invalid binary operator: %s" % p[2])
+
+ p[0] = ASTNode(op)
+
+parser = yacc()
+
+def parse_ltl(s: str) -> ASTNode:
+ spec = parser.parse(s)
+
+ for assign in spec:
+ if assign[0] == "RULE":
+ rule = assign[1]
+
+ for assign in spec:
+ if assign[0] == "RULE":
+ continue
+
+ subexpr = assign[0]
+ for node in rule:
+ if isinstance(node.op, Variable) and node.op.name == subexpr:
+ node.op = assign[1].op
+
+ return rule
+
+def create_graph(s: str):
+ atoms = set()
+
+ x = parse_ltl(s)
+ for c in x:
+ c.normalize()
+ if isinstance(c.op, Variable):
+ atoms.add(c.op.name)
+
+ init = GraphNode("init", set(), set(), set(), set())
+ head = GraphNode("first", {init}, {x}, set(), set())
+ graph = head.expand(set())
+
+ for node in graph:
+ for incoming in node.incoming:
+ if incoming.name == "init":
+ node.init = True
+ for o in node.old:
+ if not o.op.is_temporal():
+ node.labels.add(str(o))
+
+ return atoms, sorted(graph)
diff --git a/tools/verification/ltl2ba/template.c b/tools/verification/ltl2ba/template.c
new file mode 100644
index 000000000000..31c5a209d71d
--- /dev/null
+++ b/tools/verification/ltl2ba/template.c
@@ -0,0 +1,131 @@
+// SPDX-License-Identifier: GPL-2.0
+/*
+ * This file is generated, do not edit.
+ */
+#include <linux/rv.h>
+#include <rv/instrumentation.h>
+#include <trace/events/task.h>
+#include <trace/events/sched.h>
+
+#include "ba.h"
+
+static_assert(NUM_ATOM <= RV_MAX_LTL_ATOM);
+
+enum buchi_state {
+ INIT,
+%%STATE_LIST%%
+ DEAD,
+};
+
+int rv_%%MODEL_NAME%%_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+static void init_monitor(struct task_struct *task)
+{
+ struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ for (int i = 0; i < NUM_ATOM; ++i)
+ mon->atoms[i] = LTL_UNDETERMINED;
+ mon->state = INIT;
+}
+
+static void handle_task_newtask(void *data, struct task_struct *task, unsigned long flags)
+{
+ struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ init_monitor(task);
+
+ rv_%%MODEL_NAME%%_atoms_init(task, mon);
+ rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+}
+
+int rv_%%MODEL_NAME%%_init(size_t data_size)
+{
+ struct task_struct *g, *p;
+ int ret, cpu;
+
+ if (WARN_ON(data_size > RV_MAX_DATA_SIZE))
+ return -EINVAL;
+
+ ret = rv_get_task_monitor_slot();
+ if (ret < 0)
+ return ret;
+
+ rv_%%MODEL_NAME%%_task_slot = ret;
+
+ rv_attach_trace_probe("%%MODEL_NAME%%", task_newtask, handle_task_newtask);
+
+ read_lock(&tasklist_lock);
+
+ for_each_process_thread(g, p)
+ init_monitor(p);
+
+ for_each_present_cpu(cpu)
+ init_monitor(idle_task(cpu));
+
+ read_unlock(&tasklist_lock);
+
+ return 0;
+}
+
+void rv_%%MODEL_NAME%%_destroy(void)
+{
+ rv_put_task_monitor_slot(rv_%%MODEL_NAME%%_task_slot);
+ rv_%%MODEL_NAME%%_task_slot = RV_PER_TASK_MONITOR_INIT;
+
+ rv_detach_trace_probe("%%MODEL_NAME%%", task_newtask, handle_task_newtask);
+}
+
+static void illegal_state(struct task_struct *task, struct ltl_monitor *mon)
+{
+ mon->state = INIT;
+ rv_%%MODEL_NAME%%_error(task, mon);
+}
+
+static void rv_%%MODEL_NAME%%_attempt_start(struct task_struct *task, struct ltl_monitor *mon)
+{
+ int i;
+
+ mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+
+ for (i = 0; i < NUM_ATOM; ++i) {
+ if (mon->atoms[i] == LTL_UNDETERMINED)
+ return;
+ }
+
+%%BUCHI_START%%
+}
+
+static void rv_%%MODEL_NAME%%_step(struct task_struct *task, struct ltl_monitor *mon)
+{
+ switch (mon->state) {
+%%BUCHI_TRANSITIONS%%
+ case DEAD:
+ case INIT:
+ break;
+ default:
+ WARN_ON_ONCE(1);
+ }
+}
+
+void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task, unsigned int atom, bool value)
+{
+ struct ltl_monitor *mon = rv_%%MODEL_NAME%%_get_monitor(task);
+
+ rv_%%MODEL_NAME%%_atom_set(mon, atom, value);
+
+ if (mon->state == DEAD)
+ return;
+
+ if (mon->state == INIT)
+ rv_%%MODEL_NAME%%_attempt_start(task, mon);
+ if (mon->state == INIT)
+ return;
+
+ mon->atoms[atom] = value;
+
+ rv_%%MODEL_NAME%%_atoms_fetch(task, mon);
+
+ rv_%%MODEL_NAME%%_step(task, mon);
+}
diff --git a/tools/verification/ltl2ba/template.h b/tools/verification/ltl2ba/template.h
new file mode 100644
index 000000000000..65d342891e70
--- /dev/null
+++ b/tools/verification/ltl2ba/template.h
@@ -0,0 +1,157 @@
+/* SPDX-License-Identifier: GPL-2.0 */
+/*
+ * This file is generated, do not edit.
+ *
+ * This file includes necessary functions to glue the Buchi automaton and the kernel together.
+ * Some of these functions must be manually implemented (look for "Must be implemented", or just
+ * let the compiler tells you).
+ *
+ * Essentially, you need to manually define the meaning of the atomic propositions in the LTL
+ * property. The primary function for that is rv_%%MODEL_NAME%%_atom_update(), which can be called
+ * in tracepoints' handlers for example. In some specific cases where
+ * rv_%%MODEL_NAME%%_atom_update() is not convenient, rv_%%MODEL_NAME%%_atoms_fetch() can be used.
+ *
+ * rv_%%MODEL_NAME%%_init()/rv_%%MODEL_NAME%%_destroy() must be called while enabling/disabling
+ * the monitor.
+ *
+ * If the fields in struct ltl_monitor is not enough, extra custom data can be used. See
+ * rv_%%MODEL_NAME%%_get_data().
+ */
+
+#include <linux/sched.h>
+
+enum %%MODEL_NAME%%_atom {
+%%ATOM_LIST%%
+ NUM_ATOM
+};
+
+/**
+ * rv_%%MODEL_NAME%%_init
+ * @data_size: required custom data size, can be zero
+ *
+ * Must be called while enabling the monitor
+ */
+int rv_%%MODEL_NAME%%_init(size_t data_size);
+
+/**
+ * rv_%%MODEL_NAME%%_destroy
+ *
+ * must be called while disabling the monitor
+ */
+void rv_%%MODEL_NAME%%_destroy(void);
+
+/**
+ * rv_%%MODEL_NAME%%_error - report violation of the LTL property
+ * @task: the task violating the LTL property
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function should invoke the RV reactor and the monitor's tracepoints.
+ */
+void rv_%%MODEL_NAME%%_error(struct task_struct *task, struct ltl_monitor *mon);
+
+extern int rv_%%MODEL_NAME%%_task_slot;
+
+/**
+ * rv_%%MODEL_NAME%%_get_monitor - get the struct ltl_monitor of a task
+ */
+static inline struct ltl_monitor *rv_%%MODEL_NAME%%_get_monitor(struct task_struct *task)
+{
+ return &task->rv[rv_%%MODEL_NAME%%_task_slot].ltl_mon;
+}
+
+/**
+ * rv_%%MODEL_NAME%%_atoms_init - initialize the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called during task creation, and should initialize all
+ * atomic propositions. rv_%%MODEL_NAME%%_atom_set() should be used to implement this function.
+ *
+ * This function does not have to initialize atomic propositions that are updated by
+ * rv_%%MODEL_NAME%%_atoms_fetch(), because the two functions are called together.
+ */
+void rv_%%MODEL_NAME%%_atoms_init(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_%%MODEL_NAME%%_atoms_fetch - fetch the atomic propositions
+ * @task: the task
+ * @mon: the LTL monitor
+ *
+ * Must be implemented. This function is called anytime the Buchi automaton is triggered. Its
+ * intended purpose is to update the atomic propositions which are expensive to trace and can be
+ * easily read from @task. rv_%%MODEL_NAME%%_atom_set() should be used to implement this function.
+ *
+ * Using this function may cause incorrect verification result if it is important for the LTL that
+ * the atomic propositions must be updated at the correct time. Therefore, if it is possible,
+ * updating atomic propositions should be done with rv_%%MODEL_NAME%%_atom_update() instead.
+ *
+ * An example where this function is useful is with the LTL property:
+ * always (RT imply not PAGEFAULT)
+ * (a realtime task does not raise page faults)
+ *
+ * In this example, adding tracepoints to track RT is complicated, because it is changed in
+ * differrent places (mutex's priority boosting, sched_setscheduler). Furthermore, for this LTL
+ * property, we don't care exactly when RT changes, as long as we have its correct value when
+ * PAGEFAULT==true. Therefore, it is better to update RT in rv_%%MODEL_NAME%%_atoms_fetch(), as it
+ * can easily be retrieved from task_struct.
+ *
+ * This function can be empty.
+ */
+void rv_%%MODEL_NAME%%_atoms_fetch(struct task_struct *task, struct ltl_monitor *mon);
+
+/**
+ * rv_%%MODEL_NAME%%_atom_update - update an atomic proposition
+ * @task: the task
+ * @atom: the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition and trigger the Buchi atomaton to check for violation of the LTL
+ * property. This function can be called in tracepoints' handler, for example.
+ */
+void rv_%%MODEL_NAME%%_atom_update(struct task_struct *task, unsigned int atom, bool value);
+
+/**
+ * rv_%%MODEL_NAME%%_atom_get - get an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ *
+ * Returns the value of an atomic proposition.
+ */
+static inline
+enum ltl_truth_value rv_%%MODEL_NAME%%_atom_get(struct ltl_monitor *mon, unsigned int atom)
+{
+ return mon->atoms[atom];
+}
+
+/**
+ * rv_%%MODEL_NAME%%_atom_set - set an atomic proposition
+ * @mon: the monitor
+ * @atom: the atomic proposition, one of enum %%MODEL_NAME%%_atom
+ * @value: the new value for @atom
+ *
+ * Update an atomic proposition without triggering the Buchi automaton. This can be useful to
+ * implement rv_%%MODEL_NAME%%_atoms_fetch() and rv_%%MODEL_NAME%%_atoms_init().
+ *
+ * Another use case for this function is when multiple atomic propositions change at the same time,
+ * because calling rv_%%MODEL_NAME%%_atom_update() (and thus triggering the Buchi automaton)
+ * multiple times may be incorrect. In that case, rv_%%MODEL_NAME%%_atom_set() can be used to avoid
+ * triggering the Buchi automaton, and rv_%%MODEL_NAME%%_atom_update() is only used for the last
+ * atomic proposition.
+ */
+static inline
+void rv_%%MODEL_NAME%%_atom_set(struct ltl_monitor *mon, unsigned int atom, bool value)
+{
+ mon->atoms[atom] = value;
+}
+
+/**
+ * rv_%%MODEL_NAME%%_get_data - get the custom data of this monitor.
+ * @mon: the monitor
+ *
+ * If this function is used, rv_%%MODEL_NAME%%_init() must have been called with a positive
+ * data_size.
+ */
+static inline void *rv_%%MODEL_NAME%%_get_data(struct ltl_monitor *mon)
+{
+ return &mon->data;
+}
--
2.39.5
Powered by blists - more mailing lists