CN116050102A - A Dynamic Redundancy Prediction and Elimination Method for Consistency Protocol Detection - Google Patents

Abstract

The present invention provides a redundant dynamic prediction and elimination method oriented to consistency protocol detection, which includes calculating the semantics of tree nodes based on different types of constraints and deriving that under the condition of multiple truth values, the truth value of the child node determines the value of the parent node. True value, so that the link of the child node participates in the generation of the link of the parent node, and then based on the actual value of each node of the calculation tree based on multiple truth value conditions and constraints, mark all the root nodes that will be generated from top to bottom The link has nodes that affect the link; after marking all the constraint calculation tree nodes that will generate non-redundant links, when performing link generation on the constraint calculation tree nodes, if the constraint calculation tree nodes generate non-redundant links, then perform link generation, otherwise Skip this node. Under the condition of maintaining the correctness of the results, the present invention greatly reduces the total calculation amount of the link generation step by eliminating redundant calculations, improves the efficiency of the link generation step, and further improves the efficiency of the entire consistency protocol detection process.

Description

A Dynamic Redundancy Prediction and Elimination Method for Consistency Protocol Detection

technical field

The invention belongs to the technical field of software data processing, and in particular relates to a redundant dynamic prediction and elimination method oriented to consistency protocol detection.

Background technique

With the development of information technology, the complexity of software systems is increasing day by day. On the one hand, software often needs to deal with complex application scenarios and intelligently adjust its own behavior based on collected environmental information, which is often not completely reliable; Due to the scale and high complexity, the reliability of the software itself cannot be fully guaranteed. Errors in the environment information or within the software system will lead to abnormal behavior or even crash of the software, thereby preventing the software from providing services to users normally.

In order to deal with the above problems, the current stage is to write a consistency protocol. On the one hand, it stipulates the conditions that the collected environmental information should meet when applying the software, and on the other hand, it stipulates the conditions that the software code should meet when writing the software. When these conditions are violated, it can be known that there are normative errors in data such as environmental information or software codes that violate the consistency protocol, so that these errors can be checked and repaired, and errors in the data can be prevented from affecting the services of the software system. ; Among them, the step of finding out whether the statute is violated is called finding the truth value, and the process of finding out the cause of the statute being violated is called link generation. At present, there are many consistency protocol detection techniques that can be used to verify the standardization of data. However, with the growth of data size and change frequency, these technologies often cannot detect the technology that violates the consistency protocol in a timely and correct manner. Therefore, a more efficient consistency protocol detection technology needs to be proposed urgently.

Contents of the invention

Aiming at the deficiencies in the prior art, the invention provides a redundant dynamic prediction and elimination method oriented to consistency protocol detection.

The present invention provides a redundant dynamic prediction and elimination method for consistency protocol detection, wherein the consistency protocol is expressed in a protocol language based on first-order logic; the consistency protocol detection process is performed on a constraint calculation tree; The constraint calculation tree includes the syntax tree of the consistency specification formula and the assignment to variables at runtime; each node of the constraint calculation tree corresponds to a sub-formula in the specification language plus all free variables in a sub-formula An assignment; the nodes in the constraint calculation tree correspond to the formulas in the specification language;

The redundant dynamic prediction and elimination method includes:

Based on the semantics of computing tree nodes of different types of constraints, it is deduced that under the condition of multiple truth values, the truth value of the child node determines the truth value of the parent node, so that the link of the child node participates in the generation of the link of the parent node, and then multiple truth values Based on the value condition and the actual truth value of each node of the constraint calculation tree, mark all nodes that will generate links that affect the root node link from top to bottom; mark all constraint calculation tree nodes that will generate non-redundant links Finally, when link generation is performed on the constraint computation tree node, if the constraint computation tree node generates a non-redundant link, link generation is performed, otherwise, the node is skipped.

Further, the statute language includes and formula, or formula, implication formula, non-formula, full name formula, special name formula and Boolean function formula; wherein, the full name formula is used to constrain the data as a whole to meet the consistency specification condition; the special name formula uses It is used to judge whether any data satisfies the consistency condition; the Boolean function is used to detect whether the specific data meets the consistency condition.

Further, the constraint calculation tree includes an AND node, an OR node, an implied node, a non-node, a full name node, a specific name node, and a Boolean function node; wherein, the AND node, the OR node, and the implied node in the constraint calculation tree include two sub-nodes Nodes, non-nodes include a sub-node; the number of sub-nodes corresponding to nodes, or nodes, implied nodes, and non-nodes is the same as the number of sub-formulas corresponding to formulas, or formulas, implied formulas, and non-formulas.

Further, the step of obtaining the truth value in the consistency protocol detection process is carried out from bottom to top on the constraint calculation tree; for the Boolean function node, the assignment information is passed into the corresponding Boolean function to obtain the truth value of the Boolean function node; for And node, or node, implication node and non-node, according to the semantics of and, or, implication and non-node in first-order logic and the truth value of each node's child nodes, the truth value of each node is obtained; for full name nodes, only if the full name When the truth values of all child nodes of a node are all true or have no child nodes, the truth value of the full name node is true, otherwise it is false; The true value of a particular node is false, otherwise it is true.

Further, the link associates the violation of the protocol with a specific assignment to the variable; the specific assignment assigns specific data to the variable, indicates the semantic role of the specific data in the consistent protocol, and provides an explanation for the violation of the protocol;

Link generation is carried out on the constraint calculation tree from bottom to top, generating intermediate links for each non-root node, and using the intermediate links of child nodes to generate links to parent nodes; the link of the only root node of the constraint calculation tree is the final required link ; For any node, the link generation step selects the link of the child node that can determine the true value of the node, and synthesizes the link of the node according to the semantics of the node type.

Further, perform semantic analysis on different types of formulas in the consistency specification language, and deduce that each child node of the constraint calculation tree node can be the truth value calculation of the child node of the constraint calculation tree node under the condition of multiple truth value values. Form the key contribution, that is, the child node can independently determine the truth value of its parent node; starting from the root node, according to the truth value obtained by each node in the truth value calculation step, mark all the truth values that can contribute to the root node the node;

For an AND node, when its truth value is true, both child nodes key contribute to the truth value of the AND node; when its truth value is false, all nodes whose truth value is false key contribute to the truth value of the AND node;

For an OR node, when its truth value is false, both child nodes key contribute to the truth value of the or node; when its truth value is true, all child nodes key contribution to the truth value of the or node;

For an implied node, when its truth value is false, both child nodes contribute critically to the true value of the implied node; when its truth value is true, the left child node whose truth value is false and the right child node whose truth value is true contribute critically to the implication the truth value of the node;

For a non-node, its only child node always contributes its truth value critically;

For a full name node, its truth value is key contributed by all child nodes whose truth value is false;

For a specific node, its truth value is mainly contributed by all truth-valued child nodes.

Furthermore, after marking all the nodes that can make a key contribution to the true value of the root node, the calculation of all unmarked nodes is redundant calculation, and the actual link generation step is only to generate links from the bottom up for the marked nodes, while No link is generated for other nodes; the link generated on the unique root node of the entire constraint computation tree is the link of the final result.

The invention provides a redundant dynamic prediction and elimination method oriented to consistency protocol detection, which can dynamically predict and eliminate redundant calculation in the step of generating constraints detection links. The former means that all redundant calculations in the link generation step will be eliminated, and the latter means that no non-redundant calculations in the link generation step will be eliminated by mistake. Under the condition of maintaining the correctness of the results, by eliminating redundant calculations, the total calculation amount of the link generation step is greatly reduced, thereby improving the efficiency of the link generation step, and then improving the efficiency of the entire consistency protocol detection process.

The present invention also provides a method for judging whether the links to be generated by constrained computation tree nodes are redundant based on statute syntax and semantics analysis and constrained computation tree node truth value prediction, and based on this judgment, the link generation process is limited to only generate non-redundant links nodes, thus avoiding the calculation of redundant links.

Description of drawings

In order to illustrate the technical solution of the present invention more clearly, the accompanying drawings that need to be used in the embodiments will be briefly introduced below. Obviously, for those of ordinary skill in the art, on the premise of not paying creative work, they can also Additional figures can be derived from these figures.

FIG. 1 is a structural diagram of a redundant dynamic prediction and elimination method oriented to consistency protocol detection provided by an embodiment of the present invention;

Fig. 2 is a schematic diagram of the basic formula types of the constraint language provided by the embodiment of the present invention;

FIG. 3 is a schematic structural diagram of a constraint computation tree provided by an embodiment of the present invention;

Fig. 4 is a schematic diagram of redundant link analysis generated under the true value for different types of nodes of the constrained computation tree provided by the embodiment of the present invention;

Fig. 5 is a schematic flow chart of all algorithms that will generate non-redundant link nodes in the label-constrained computation tree provided by the embodiment of the present invention;

FIG. 6 is a schematic flowchart of an algorithm for generating links only on marked constrained computing tree nodes provided by an embodiment of the present invention.

Detailed ways

The technical solutions in the embodiments of the present invention will be clearly and completely described below in conjunction with the accompanying drawings in the embodiments of the present invention. Obviously, the described embodiments are only some, not all, embodiments of the present invention. Based on the embodiments of the present invention, all other embodiments obtained by persons of ordinary skill in the art without creative efforts fall within the protection scope of the present invention.

特称公式

和布尔函数公式(bfunc)；其中，全称公式用于约束数据整体满足一致性规约条件；特称公式用于判断是否存在任何数据满足一致性条件；布尔函数用于检测具体数据与某一个一致性条件的符合情况；剩下四类公式则将全称公式、特称公式和布尔函数公式组合起来表达更复杂的规约语义。需要说明的是，其中只有全称公式和特称公式能够定义变元，在检测时，这些变元将和数据相关联，从而将一致性规约公式的语法树扩展为约束计算树(Constraint Computation Tree，CCT)。As shown in Figure 1, the embodiment of the present invention provides a redundant dynamic prediction and elimination method oriented to consistent protocol detection, and the consistent protocol is expressed in a protocol language based on first-order logic; as shown in Figure 2, the The specification language includes and formula (and), or formula (or), implied formula (implies), non-formula (not), full name formula

Special formula

And the Boolean function formula (bfunc); among them, the full name formula is used to constrain the data to meet the consistency specification condition as a whole; the special name formula is used to judge whether there is any data that meets the consistency condition; the Boolean function is used to detect specific data and a certain consistency The conditions are met; the remaining four types of formulas combine full-name formulas, special-name formulas, and Boolean function formulas to express more complex semantics. It should be noted that only the full-name formula and the special-name formula can define variables, and these variables will be associated with the data during detection, thereby expanding the syntax tree of the consistency reduction formula into a constraint computation tree (Constraint Computation Tree, CCT).

As shown in Figure 3, the process of the consistency protocol detection is carried out on the constraint calculation tree; the constraint calculation tree includes the syntax tree of the consistency protocol formula and the assignment to variables at runtime; each of the constraint calculation trees A node corresponds to a sub-formula in the specification language plus an assignment to all free variables in a sub-formula; nodes in the constraint computation tree correspond to formulas in the specification language one-to-one. The constraint computation tree includes an AND node, an OR node, an implied node, a non-node, a full name node, a particular node, and a Boolean function node; wherein, the AND node, the OR node, and the implied node in the constraint computation tree include two child nodes, and the non- A node includes one child node; the number of child nodes corresponding to node, or node, implied node, and non-node corresponds to the number of child formulas of formula, or formula, implied formula, and non-formula, respectively. The full name node and the specific name node have a variable number of child nodes, although the full name formula and the specific name formula in first-order logic have only one sub-formula, the reason is that the full name and specific name nodes in CCT not only need to consider sub-formulas, but also Consider different possible assignments to variables, and each possible assignment corresponds to a child node.

First, according to the information obtained when the truth value is used before the link generation step, the redundant dynamic prediction algorithm is used to judge which nodes will generate intermediate links that will be necessary to calculate the final result, and which nodes will generate intermediate links that will lead to redundant calculations . Then, by limiting the link generation to only the nodes that generate non-redundant links, the generation of redundant intermediate links is avoided, thereby avoiding redundant calculations.

The redundant dynamic prediction and elimination method includes:

Based on different types of constraints to calculate the semantics of tree nodes, it is deduced that under the condition of multiple truth values, the truth value of the child node determines the truth value of the parent node, so that the link of the child node participates in the generation of the link of the parent node, and then multiple truth values Based on the value condition and the actual truth value of each node of the constraint calculation tree, mark all nodes that will generate links that affect the root node link from top to bottom; mark all constraint calculation tree nodes that will generate non-redundant links Finally, when link generation is performed on the constraint computation tree node, if the constraint computation tree node generates a non-redundant link, link generation is performed, otherwise, the node is skipped.

The truth value seeking step in the consistency protocol detection process is carried out from bottom to top on the constraint calculation tree; for the Boolean function node, the assignment information is passed into the corresponding Boolean function to obtain the truth value of the Boolean function node; for the node with, Or nodes, implied nodes and non-nodes, according to the semantics of and, or, implied and non-nodes in first-order logic and the truth value of each node's child nodes to obtain the truth value of each node; When the truth value of the node is all true or has no child nodes, the truth value of the full node is true; otherwise, it is false; True is false, otherwise true.

The link associates the violation of the protocol with a specific assignment to the variable; the specific assignment assigns specific data to the variable, indicates the semantic role of the specific data in the consistent protocol, and provides an explanation for the violation of the protocol.

Link generation is carried out on the constraint calculation tree from bottom to top, generating intermediate links for each non-root node, and using the intermediate links of child nodes to generate links to parent nodes; the link of the only root node of the constraint calculation tree is the final required link ; For any node, the link generation step selects the link of the child node that can determine the true value of the node, and synthesizes the link of the node according to the semantics of the node type.

As shown in Figure 4, semantic analysis is performed on different types of formulas in the consistency specification language, and the child nodes of each constraint calculation tree node can be the child nodes of the constraint calculation tree node under the condition of multiple truth values. The truth value calculation forms a key contribution, that is, a child node can independently determine the truth value of its parent node, that is, interpret the truth value of the node semantically; starting from the root node, according to each node in the truth value calculation step The obtained truth value marks all the nodes that can contribute to the truth value of its root node.

For an AND node, when its truth value is true, both child nodes key contribute to the truth value of the AND node; when its truth value is false, all nodes whose truth value is false key contribute to the truth value of the AND node.

For an OR node, when its truth value is false, both child nodes contribute critically to the truth value of the or node; when its truth value is true, all child nodes contribute critically to the truth value of the or node.

For an implied node, when its truth value is false, both child nodes contribute critically to the true value of the implied node; when its truth value is true, the left child node whose truth value is false and the right child node whose truth value is true contribute critically to the implication The truth value of the node.

For a non-node, its only child node always contributes its truth value critically.

For a full node, its truth value is key contributed by all child nodes whose truth value is false.

For a specific node, its truth value is mainly contributed by all truth-valued child nodes.

The Boolean function node has no child nodes, and there is no need to consider which child nodes contribute to the truth value of the Boolean function node.

After marking all the nodes that can make a key contribution to the true value of the root node, the calculation of all unmarked nodes is redundant calculation, and the actual link generation step is only to generate links from the bottom up for the marked nodes, not for other nodes. Nodes generate links; the links generated on the unique root node of the entire constraint calculation tree are the links of the final result.

It should be noted that the meaning of the truth value condition means that under these truth values, the truth value of the child node semantically determines the truth value of the parent node, therefore, in order to explain the truth value of the parent node Value, the link of the parent node must include the link of the child node as part of it.

It should be noted that the content of the truth value condition refers to if the type of the parent node, the true value of the parent node, the position of the child node relative to the parent node, and the true value of the child node meet any of the truth value conditions. One, the truth value of the child node has a decisive influence on the truth value of the parent node, so the link of the child node must be included in the link of the parent node.

It should be noted that the meaning of the node marking algorithm means that if the link of a node must be included in the link of the parent node, and the link of its parent node must be included in the link of the root node (the required final generated link ), the link of the child node must be included in the link of the root node; otherwise, the link of the child node will not affect the link of the root node, that is, the link of the child node will be a redundant link.

It should be noted that the content of the node marking algorithm refers to starting from the root node and judging layer by layer whether the link to be generated by the node is necessary for the root node link. Whether the link of the child node is necessary for the link of this node, all the links of the child node that are necessary for this node are also necessary for the root node.

As shown in Figure 5, non-redundant node labeling starts from the root node, firstly marks the root node as a non-redundant node, and then, for each marked non-redundant node, finds all the non-redundant true value The child nodes of the value condition are further marked as non-redundant nodes, and this step is repeated until all non-redundant nodes are marked.

As shown in Figure 6, the link generation algorithm limited to non-redundant nodes starts from the leaf nodes, first judges whether the leaf nodes are non-redundant nodes, and then calls the traditional link generation algorithm to generate links for the non-redundant leaf nodes, and then Going up layer by layer, for all non-redundant nodes, call the traditional link generation algorithm to synthesize its links from the links of its child nodes until the link of the root node is synthesized, and the link of the root node is the most needed link; in this process, All redundant nodes are skipped.

On the one hand, the present invention invokes a consistency protocol detection algorithm to detect the consistency protocol, and sequentially find out whether the protocol is violated and the reason for the violation. In the process of consistency protocol detection, there are considerable redundant calculations in the link generation step, which is manifested as a large number of irrelevant intermediate results; using the information obtained during the first step of truth value calculation, a dynamic prediction algorithm is used to determine which intermediate results will be the final result of the calculation. The results are necessary, and which intermediate results will lead to redundant calculations, and then, by limiting the calculation steps to the calculation of necessary intermediate results, avoiding the generation of redundant intermediate results, thereby avoiding redundant calculations.

On the other hand, the dynamic redundancy prediction and elimination of the present invention has optimal high-efficiency properties and safety properties. The optimal high-efficiency property means that all redundant intermediate results and their calculations will be predicted and then eliminated. After applying the technology, there will be no redundant calculations in the link generation step; the security property means that there will be no non-redundant intermediate results (for obtaining The intermediate result necessary for the final result) will be mistakenly marked as redundant and not generated, and the consistency protocol detection result will still remain correct, which is consistent with the common detection result without using the solution provided by the present invention.

The invention provides a redundant dynamic prediction and elimination method oriented to consistency protocol detection, which can dynamically predict and eliminate redundant calculation in the step of generating constraints detection links. The former means that all redundant calculations in the link generation step will be eliminated, and the latter means that no non-redundant calculations in the link generation step will be eliminated by mistake. Under the condition of maintaining the correctness of the results, by eliminating redundant calculations, the total calculation amount of the link generation step is greatly reduced, thereby improving the efficiency of the link generation step, and then improving the efficiency of the entire consistency protocol detection process.

The present invention also provides a method for judging whether the links to be generated by constrained computation tree nodes are redundant based on statute syntax and semantics analysis and constrained computation tree node truth value prediction, and based on this judgment, the link generation process is limited to only generate non-redundant links nodes, thus avoiding the calculation of redundant links.

The present invention has been described in detail above in conjunction with specific implementations and exemplary examples, but these descriptions should not be construed as limiting the present invention. Those skilled in the art understand that without departing from the spirit and scope of the present invention, various equivalent replacements, modifications or improvements can be made to the technical solutions and implementations of the present invention, all of which fall within the scope of the present invention. The protection scope of the present invention shall be determined by the appended claims.

Claims (7)

1. A redundant dynamic prediction and elimination method for consistency protocol detection, characterized in that, the consistency protocol is expressed in a protocol language based on first-order logic; the process of the consistency protocol detection is on the constraint calculation tree carry out; the constraint calculation tree includes the syntax tree of the consistency specification formula and the assignment to the variables at runtime; each node of the constraint calculation tree corresponds to a sub-formula in the specification language plus all freedoms in a sub-formula An assignment of variables; the nodes in the constraint calculation tree correspond one-to-one to the formulas in the specification language; The redundant dynamic prediction and elimination method includes: Based on different types of constraints to calculate the semantics of tree nodes, it is deduced that under the condition of multiple truth values, the truth value of the child node determines the truth value of the parent node, so that the link of the child node participates in the generation of the link of the parent node, and then multiple truth values Based on the value condition and the actual truth value of each node of the constraint calculation tree, mark all nodes that will generate links that affect the root node link from top to bottom; mark all constraint calculation tree nodes that will generate non-redundant links Finally, when link generation is performed on the constraint computation tree node, if the constraint computation tree node generates a non-redundant link, link generation is performed, otherwise, the node is skipped. 2. The redundant dynamic prediction and elimination method for consistent protocol detection according to claim 1, wherein the protocol language includes AND formula, OR formula, implied formula, non-formula, full-name formula, special-name formula and Boolean function formulas; among them, the full name formula is used to constrain the data to meet the consistency specification condition as a whole; the special name formula is used to judge whether any data meets the consistency condition; the Boolean function is used to detect whether the specific data meets the consistency condition. 3. The redundant dynamic prediction and elimination method oriented to consistency protocol detection according to claim 2, wherein the constraint computation tree includes an AND node, an OR node, an implied node, a non-node, a full-name node, and a special-name node. node and Boolean function node; wherein, the AND node, or node and implied node in the constraint calculation tree include two child nodes, and the non-node includes a child node; the number of child nodes of the AND node, or node, implied node, and non-node is respectively and Same as the number of subformulas corresponding to formulas, or formulas, implied formulas, and non-formulas. 4. The redundant dynamic prediction and elimination method for consistency protocol detection according to claim 3, characterized in that, the truth value obtaining step in the consistency protocol detection process is carried out from bottom to top on the constraint calculation tree ;For the Boolean function node, pass the assignment information into the corresponding Boolean function to get the truth value of the Boolean function node; Semantics and the truth value of each node's child nodes to find the truth value of each node; for a full name node, only when the truth value of all child nodes of the full name node is true or there is no child node, the full name node true value is true, otherwise it is false; For a specific node, only when the true value of all child nodes of the specific node is false or has no child nodes, the true value of the specific node is false, otherwise it is true. 5. The redundant dynamic prediction and elimination method for consistent protocol detection according to claim 4, characterized in that, the link associates the violation of the protocol with the specific assignment of variables; the specific assignment assigns specific data For the variable, it indicates the semantic role of the specific data in the consistency protocol, and provides an explanation for the violation of the protocol; Link generation is carried out on the constraint calculation tree from bottom to top, generating intermediate links for each non-root node, and using the intermediate links of child nodes to generate links to parent nodes; the link of the only root node of the constraint calculation tree is the final required link ; For any node, the link generation step selects the link of the child node that can determine the true value of the node, and synthesizes the link of the node according to the semantics of the node type. 6. The redundant dynamic prediction and elimination method oriented to consistency protocol detection according to claim 5, characterized in that, semantic analysis is carried out to different types of formulas in the consistency protocol language, and derivation is performed for each constraint calculation tree node. Under the conditions of multiple truth values, child nodes can form a key contribution to the truth value calculation of the child nodes of the constraint calculation tree node, that is, the child nodes can independently determine the truth value of their parent nodes; starting from the root node, according to each node The truth value obtained in the step of obtaining the truth value marks all the nodes that can mainly contribute to the truth value of its root node; For an AND node, when its truth value is true, both child nodes key contribute to the truth value of the AND node; when its truth value is false, all nodes whose truth value is false key contribute to the truth value of the AND node; For an OR node, when its truth value is false, both child nodes key contribute to the truth value of the or node; when its truth value is true, all child nodes key contribution to the truth value of the or node; For an implied node, when its truth value is false, both child nodes contribute critically to the true value of the implied node; when its truth value is true, the left child node whose truth value is false and the right child node whose truth value is true contribute critically to the implication the truth value of the node; For a non-node, its only child node always contributes its truth value critically; For a full name node, its truth value is key contributed by all child nodes whose truth value is false; For a specific node, its truth value is mainly contributed by all truth-valued child nodes. 7. The redundant dynamic prediction and elimination method for consistency protocol detection according to claim 6, characterized in that, after marking all nodes that can have key contributions to the true value of the root node, all unmarked nodes The calculation of is a redundant calculation, and the actual link generation step only generates links from the bottom up for the marked nodes, and does not generate links for other nodes; the link generated on the unique root node of the entire constraint calculation tree is the link of the final result.

Images