Dependency State Machines
Compared to Dependent Advice, Dependency State Machines convey additional information about the order in which events have to occur – they encode flow-sensitive information. Because many developers are familiar with state machines, we believe that their semantics are easier to understand than the semantics of Dependent Advice. Hence, you may wish to use Dependency State Machines by default.
Syntax of Dependency State Machines
The figure on the right-hand side shows the full syntax of Dependency State Machines in EBNF, as an extension to Dependent Advice (shown in gray). A dependency state machine consists of the following elements:
- a list of “symbols”, i.e. advice names which the state machine should be evaluated over, and
- a list of states, where each state…
- may or may not be an initial state,
- may or may not be a final (i.e. accepting) state, and
- may or may not have a list of outgoing transitions.
Example
The following code shows a monitoring aspect that has been annotated with a Dependency State Machine (lines 2-11).
aspect ConnectionClosed {
dependency{
close, write, reconnect;
initial s0: close -> s0,
write -> s0,
reconnect -> s0,
close -> s1;
s1: close -> s1,
write -> s2;
final s2: write -> s2;
}
Set closed = new WeakIdentityHashSet();
dependent after close(Connection c) returning:
call(* Connection.close()) && target(c) {
closed.add(c);
}
dependent after reconnect(Connection c) returning:
call(* Connection.reconnect()) && target(c) {
closed.remove(c);
}
dependent after write(Connection c) returning:
call(* Connection.write(..)) && target(c) {
if(closed.contains(c))
error("May not write to "+c+", as it is closed!");
}
}
This aspect monitors the “ConnectionClosed” property, which says that one should not write to a closed connection. (Connections are assumed to be open when created and can be closed and re-connected, which transitions them back into a “connected” state in which writes are allowed.) The figure on the right shows the monitored property as a non-deterministic finite-state machine.
As you can see, the dependency annotation in lines 2-11 directly resembles this state machine. Line 3 first states the symbols that this dependency refers to. Note that the symbol names in line 3 do not refer to the connection c explicitly. This is because, by default, Clara infers variable names from the advice declarations (lines 15, 20, 25). The declaration close, write, reconnect in line 3 is a short-hand for the more verbose form close(c), write(c), reconnect(c). (see “Extended Syntax” here for details)
- Note: There is no need to write such aspects or the annotations (!) manually! One can easily use automated tools to generate monitoring aspects from high-level specification languages. We have extended one of such tools, the “tracematch” implementation in the AspectBench Compiler, to automatically generate monitoring aspects that have dependency state machines attached to them. (details here)
Semantics of Dependency State Machines
Consider the following example, which uses a single connection object.
public static void main(String args[]) {
Connection c1 = new Connection();
c1.close();
c1.reconnect();
c1.close();
c1.close();
c1.write();
c1.write();
c1.close();
c1.reconnect();
c1.write();
}
This example program violates the ConnectionClosed property two times, at lines 8 and 9, shown in red. The violations occur because the connection is closed (even twice, at lines 6 and 7, shown in orange) and then written to. In this example, the first two operations in lines 3 and 4 do not need to be monitored because they precede the fragment of the execution that constitutes the property violation. Similarly, lines 11 to 13 do not need to be monitored either because they occur after the violating fragment. A little more subtle, we need to monitor only one of the two close statements at lines 6 and 7: once we have “read” one close transition, the state machine loops on the second close transition. The Dependency State Machine in the annotation conveys enough information such that Clara’s Nop-shadow Analysis will indeed disable all shadows in this example, except for the ones at lines 6, 8 and 9 or at lines 7, 8 or 9.
The semantics of Dependency State Machines are, on purpose, very loosely defined. The only requirement is that, if the Dependency State Machine correctly represents the monitored property, then the optimized program (the one that contains the residual runtime monitor) must execute all “final” dependent advice at exactly the same time(s) as the un-optimized program would. A “final” advice is an advice that leads into an accepting state, i.e. an error state. The un-optimized program is here basically the program that one would obtain by removing the dependent modifiers from the three pieces of advice in the aspect, essentially converting them into pieces of regular AspectJ advice. Because “disabling all shadows except for the ones at lines 6, 8 and 9 or at lines 7, 8 or 9” still leads to a program that causes the monitor to reach its final state at lines 8 and 9, according to this semantics it is sound to disable all these shadows.
Note that there is no guarantee about which shadows will not execute, only a guarantee about which shadows must execute. In the example, a less precise analysis could, for instance, keep the shadows at lines 3 and 4 enabled, too. This would still be correct according to the semantics of Dependency State Machines because this program also would reach a final state at lines 8 and 9.
