9.4. DETECTION AND RESOLUTION OF ASPECT INTERACTIONSBy restricting the expressiveness of our aspect language (while still adhering to stateful aspects), it is possible to automatically prove (certain) aspect properties. In this section, we consider a second instantiation of the general framework that supports a more restrictive yet expressive crosscut language in which static checking of interactions is feasible.
where T denotes terms with variables. The formulas used to express these crosscuts belong to the so-called quantifier-free equational formulas [5]. Whether such a formula has a solution is decidable. This is one of the key properties making the analysis in this section feasible. We can define, for example, a crosscut matching logins performed by the user root on any machine, or by any non-root user on any machine but the server as follows:
In this context, checking whether the current join point (which, remember, is represented by a term) matches the crosscut definition is computed by a generalized version of the unification algorithm that is well-known, e.g., from logic programming. Note that, for the sake of decidability (i.e., static analyses), the crosscuts C defined by the equation above are less expressive than those considered in the previous section. They can only denote join points as term patterns (as opposed to arbitrary term predicates).
where x matches the name of the accessed file. 9.4.1. Aspect InteractionsRemember that a parallel composition of n aspects A1 ||...|| An does not define any specific order of aspect application; the result of weaving may be non-deterministic. This situation arises when aspects interact, that is to say when at least two inserts must be executed at the same join point. For instance, consider the following aspect:
This aspect states that the reads should be encrypted. It interacts with the aspect logAccess defined previously, which describes logging for all users. When a user logs in and accesses a file, this access must be logged, and the file name must be encrypted. The algorithm to check aspects interaction is similar to the algorithm for finite-state product automata. It terminates due to the finite-state nature of our aspects. Starting with a composition A || A", the algorithm eliminates the parallel operator by producing all the possible pairs (conjunction) of crosscuts from A and A". A conjunction of crosscuts C1 and C2 is a solvable formula, and we can check if it has a solution using the algorithm of [5]. A crosscut with no solution cannot match any join point and can be removed from the aspect [7]. In the case of the example logAccess || cryptRead, we get:
Conflicts are represented using the non-deterministic function (I1 I1 ; I2 or I2 ; I1. Here, we have (addLog(x) crypt( This analysis does not depend on the base program to be woven. When there is no () in the resulting sequential aspect, the two aspects are independent for all programs. This property does not have to be checked again after any program modification. However, this property is a sufficient but not a necessary condition for aspect interaction. A more precise analysis is possible by taking into account the possible sequences of join points generated by the base program to be woven [7]. 9.4.2. Support for Conflict ResolutionWhen no conflicts have been detected, the parallel composition of aspects can be woven without modification. Otherwise, the programmer must get rid of the nondeterminism by making the composition more precise. In the following, we present some linguistic support aimed at resolving interactions. The occurrences of rules of the form C C C C I3 is a new insert that combines I1 and I2 in some way. For instance, in the previous example, (addLog(x) crypt(x) ; addLog(x) in order to generate encrypted logs. This option is flexible but can be tedious. Instead of writing a new insert for each conflict, the programmer may indicate how to compose inserts at the aspect level. We propose a parallel operator ||seq to indicate that whenever a conflict occurs, (I1 I1 ; I2 (where ";" denotes the sequencing operator of the programming language). Other parallel operators are useful, such as ||fst, which replaces (I1 I1 only. Let us reconsider the two aspects logAccess and cryptRead:
|