SRS Monitoring Algorithm3
As each event occurs in a program, a symbol representing it is added to a buffer of symbols that is the "string" for the string rewriting system. Then the rewriting algorithm is run until a normal form is reached. There are two major parts to our rewriting algorithm:
- Finding matches of the LHSs of rules; and
- Performing replacements with RHSs of rules.
To make replacements as efficiently as possible, the string of events/symbols that we rewrite is a linked listed of the MOPIntSpliceList class, which was specially created for our purposes to allow constant time replacement of a section of the list with another list (splicing).
The MOPIntSpliceList class has a special type of Iterator defined for it, called the MOPSLIterator, that does not follow the normal Iterator interface in Java. Rather than only having next() and hasNext() methods, the MOPSLIterator has next(int i), which moves the MOPSLIterator forward i times and returns true if it is successful (i.e., does not reach the end of the MOPIntSpliceList), and get(), which returns the current element that the MOPIntSLIterator points to. MOPSLIterator also has a method, splice(MOPSLIterator second, MOPIntSpliceList replacement), which takes another MOPSLIterator to the same MOPIntSpliceList and replaces the sequence denoted by those two MOPSLIterators, inclusively, by a specified sequence replacement. It is because of the inclusive nature of the splice method that the MOPSLIterator must have a method to retrieve its current element without advancing. The splice method makes it imperative for our string matching algorithm to maintain MOPSLIterators to the beginning and end of the current left hand side of a rule under consideration.
Special care must be taken to ensure proper handling of patterns when "^" and "$" occur. Because rules that match "^" and "$" remove them, they must be reinserted every time they are removed.
Matching the left hand sides of rules is performed using a modified version of the Aho-Corasick String searching algorithm. The modification properly adjusts the first MOPSLIterator. More details can be found in our technical report:
- Efficient Parametric Runtime Verification with Deterministic String Rewriting
- Patrick Meredith and Grigore Rosu
Technical Report http://www.ideals.illinois.edu/handle/2142/30467, March 2012
PDF, TR@UIUC, BIB