Translate existing invariants to use multiple relations and update TO invariant miners

[GoogleCodeExporter]

Issue 215 adds support for multiple relations, which enables richer models and 
richer specifications (i.e., invariants). We need to (1) generalize our 
existing totally ordered invariant types to multiple relations, and (2) update 
the invariant mining algorithms to mine these new invariant types.

Since a multi-relational trace is still totally ordered, adapting our invariant 
types shouldn't be too difficult. Here is an initial proposal:

1. x InvType y should be parametrized by a relation type and should be mined 
for all relation types present in the traces. That is, x NFby(t) y, is the 
standard x NFby y invariant over the time (t) relation. For the call/return 
relations we might mine an invariant like x AFby(c) y, which would mean that 
whenever method x is invoked, it is always eventually followed by a call to 
method y.

Note that by "mined for a relation type" I mean mined for the sub-graph formed 
by the edges of the relation type plus intermediate edges that make this 
sub-graph connected.

For example, if the trace graph is the following:
v --t,r,s--> w --t--> x --t,r--> y --t,s--> z

Then the InvType(r) invariants would be mined over the graph (where i is the 
added in intermediate edge):
v --r--> w --i--> x --r--> y

Note that certain invariants over the implicit time relation can be used to 
infer other invariants. For example: for all r, x NFby(t) y implies x NFby(r) 
y. Another example: for all r, x AP(t) y implies x AP(r) y. To reverse the 
implications in these two examples, the r invariants have hold true over all 
relations.

2. (Tentative idea) In addition to the above, x InvType y _can_ be parametrized 
by a set of relations, which would denote the intermediate relations that 
_must_ occur at least once. For example, x AFby(t,{fileio,netw}) y would mean 
that for all traces that satisfy x AFby(t) y, there must be an event between x 
and y with a relation fileio and an event with a relation netw (this could be 
satisfied with one event that has both of these relations).

Original issue reported on code.google.com by bestchai on 23 Feb 2012 at 4:32

[GoogleCodeExporter]

Please review revision cd8494f98d31

Original comment by T.101.JV on 5 Mar 2012 at 12:39

[GoogleCodeExporter]

The decomposition into Trace and RelationPath instances makes sense. I'm a 
little worried about performance, since the previous ChainWalkingTOInvMiner 
code was highly optimized and you're introducing two levels of indirection. 
But, we shouldn't worry about performance right now, so this is fine.

I left feedback on revision cd8494f98d31. Most code issues have to do with 
insufficient code comments. It's important to maintain a high commenting 
standard in this mining code. All complex data structures, loops, and 
non-trivial methods must have comments.

Original comment by bestchai on 5 Mar 2012 at 8:14

• Changed state: Started

[GoogleCodeExporter]

Addressed review in revision f868b3c541a8

Original comment by T.101.JV on 5 Mar 2012 at 9:23

[GoogleCodeExporter]

Okay, next steps in this issue are to update the invariant miner to emit 
invariants over relations other than the default relation, and to write tests 
to make sure that the mining works the way it is supposed to when multiple 
relations are present. It would be especially helpful to have the tests use the 
trace parser -- i.e., specify a log input, with regular expressions, and get 
back a set of invariants that you can check against the ground truth.

Original comment by bestchai on 6 Mar 2012 at 4:42

[GoogleCodeExporter]

Please review revision d91303134265

I wrote tests for the graphs that I constructed, but I haven't specifically 
tested different permutations of pairs of time and non time relations. I also 
have not written randomized tests.

I have not implemented required parametrized intermediate relations either.

Original comment by T.101.JV on 8 Mar 2012 at 6:51

[GoogleCodeExporter]

Okay, here are a few comments based off of the latest (revision c2bbdeb97e79) 
in the Issue224 branch. Once you're done with these I'll merge into default.

- Add comments to ChainsTraceGraph.addTrace -- describe method at top level and 
add a comment line for each loop/logical block. Currently it's not at all clear 
what it does. Also, you're using closureMap for two different purposes in the 
method. At the end you use it to map a relation to the final node in the 
relationPath, and at the start you're using it to map relations to initial 
nodes. I would use different maps, with better names, for clarity.

- The Trace.addRelationPath needs a comment. It's adding a path, but the input 
is an EventNode. It's raising an exception that path already exists, but this 
happens when the relation exists, not the path. It seems more confusing than it 
needs to be. Comments would help here, as well.

Original comment by bestchai on 13 Mar 2012 at 2:16

[GoogleCodeExporter]

Please review revision 3959d9e02120

Original comment by T.101.JV on 19 Mar 2012 at 6:41

[GoogleCodeExporter]

Fixed with revision 212c921dd926.

Original comment by bestchai on 19 Mar 2012 at 7:23

• Changed state: Fixed