JavaMOP3 Syntax

From FSL
Jump to: navigation, search

JavaMOP is the Java instantiation of MOP. The complete syntax of JavaMOP is given below, as an instance of the generic MOP Syntax defining the relevant modifiers and language-specific syntax (Java for declarations and event/handler actions, enriched with AspectJ for event definitions). The formal syntax below uses BNF (extended with the common {p} for zero or more and [p] for zero or one repetitions of p, respectively).

// BNF below is extended with {p} for zero or more and [p] for zero or one
<JavaMOP Specification>
::= {<Modifier>} <Id> ["(" <Java Parameters> ")"] "{"
<Java Declarations>
{<Event>}
{<Property>
{"@" <LOGIC State> "{" <Java Statements> "}"}}
"}"
<Modifier> ::= "unsynchronized" | "decentralized" | "perthread" | "suffix"
<Event> ::= ["creation"] "event" <Id> <AspectJ advice> "{" [ <Java Statements> ] "}"
<Property> ::= <LOGIC Name> ":" <LOGIC Syntax>
<Java Declarations> ::= ... <!-- syntax of declarations in Java -->
<Java Parameters> ::= ... <!-- syntax of method parameter list in Java -->
<Java Statements> ::= ... <!-- slightly extended syntax of statements in Java -->
<ApsectJ Advice> ::= ... <!-- slightly extended syntax of advice in AspectJ -->

<Modifier>

The modifier unsynchronized tells JavaMOP that the monitor state need not be protected against concurrent accesses; the default is synchronized. The unsynchronized monitor is faster, but may suffer from races on its state updates if the monitored program has multiple threads. The decentralized modifier refers to decentralized monitor indexing. The default indexing is centralized, meaning that the indexing trees needed to quickly access and garbage-collect monitor instances are stored in a common place; decentralized indexing means that the indexing trees are scattered all over the code as additional fields of objects of interest. Decentralized indexing typically yields lower runtime overhead, though it may not always work for all settings. Our OOPSLA'07 paper explains how centralized and decentralized indexing work.

<Java Parameters> and <Java Declarations>

These are ordinary Java parameters (as used in methods) and Java declarations. The former are the parameters of the JavaMOP specification and the latter are additional monitor variables that one can access and modify in both event actions and property handlers (see below).

<Event>

The event declaration code allows for the definition of events which may then be referred to in the property. As part of its defining AspectJ advice, an event can also have arbitrary code associated with it, called an event action, which is run when the event is observed; an event action can modify the program or the monitor state. The event action is represented, in the grammar, by the optional <Java Statements> within the braces at the end of the event definition.

<Property>

Properties are optional in JavaMOP. A property consists of a named formalism (<LOGIC Name>), followed by a colon, followed by a property specification using the named formalism (<LOGIC Syntax>) and usually referring to the declared events. JavaMOP, like all MOP instances, is not bound to any particular property specification formalism. New formalisms can be added to a JavaMOP installation by means of logic plugins. Each logic plugin comes with the following syntactic categories that are documented on each logic plugin page: <LOGIC Name> is the name of the logic, e.g., ere for extended regular expressions; <LOGIC Syntax> is the syntax that the named logic provides to express properties; <LOGIC State> names the states of monitors generated for the named logic to which one can associate handlers (see below). The current version of JavaMOP provides the following plugins:

If the property is missing, then the JavaMOP specification is called raw. Raw specifications are useful when no existing logic plugin is powerful or efficient enough to specify the desired property; in that case, one embeds the custom monitoring code manually within the event generation code.

"@"<LOGIC State>

This syntax allows us to define property handlers, which consist of arbitrary Java code that will be invoked whenever a certain state is reached in the generated monitor (e.g., validation or violation in linear temporal logic specifications, or a particular state in a finite state machine description). At least one handler is required anytime there is a property (i.e., anytime we are not using a raw monitor).

<Java Statement> and <AspectJ Advice>

The Java code used in JavaMOP specifications slightly extends Java with three special variables:

  • __RESET: a special expression (evaluates to void) that resets the monitor to its initial state;
  • __LOC: a string variable that evaluates to the line number generating the current event;
  • __SKIP: a special expression that returns null, skipping the original code of the around event advice. It will be ignored for the other types of advices (before and after advices).
  • __STATICSIG: a special expression that returns an org.aspectj.lang.Signature object of the static signature of the current event.

Similarly, the advise used to define JavaMOP events slightly extends the ApsectJ advice syntax as follows:

<AspectJ Advice>      ::= [ "strictfp" ] <AspectJ AdviceSpec> [ "throws" <TypeList> ] ":" 
<Pointcut> [ "&&" <JavaMOP Pointcut> ]
"{" <Java Statement> "}"
<JavaMOP Pointcut> ::= "thread" "(" <Id> ")"
| "condition" "(" <BooleanExpression> ")"
| <JavaMOP Pointcut> "&&" <JavaMOP Pointcut>
<Pointcut> ::= ... <!-- syntax of Pointcut in AspectJ -->
<AspectJ AdviceSpec> ::= ... <!-- syntax of AdviceSpec in AspectJ -->
<TypeList> ::= ... <!-- list of Exception types in Java -->
<BooleanExpression> ::= ... <!-- syntax of boolean expressions in Java -->

<AspectJ Advice> above follows the AspectJ syntax except for its optional extension with <JavaMOP Pointcut>, which can only be added in a top-level conjunct pointcut context. <Pointcut> and <AspectJ AdviceSpec> are both standard AspectJ syntax. The <Java statement> associated to each event advice is called an event action and is executed each time the event is generated. The two additional JavaMOP pointcuts have the following meaning:

  • thread: this pointcut captures the current thread and takes an identifier as the parameter. The identifier can be a class name or a variable name. For the former, the type of the captured thread should be a sub-class of the given class to trigger the event. For the latter, the captured thread is bound to the variable.
  • condition: this pointcut takes a boolean expression as the parameter. The event is triggered only when the given boolean expression evaluates to true.


Examples

The following JavaMOP specification states that each thread releases each lock as many times as it acquires it:

unsynchronized decentralized SafeLock(Lock l, Thread t) {
 
event acq after(Lock l, Thread t) :
call(* Lock.acquire()) && target(l) && thread(t) {
}
event rel after(Lock l, Thread t) :
call(* Lock.release()) && target(l) && thread(t) {
}
 
cfg : S -> S acq S rel | epsilon
 
@fail {
System.out.println("Too many releases found at line " + __LOC);
}
}

The following JavaMOP program profiles a file system; it logs how many times a file has been open, written to and then closed, and if that was the case then it also outputs the number of writes:

SafeFile(File f) {
static int counter = 0;
int writes = 0;
 
event open after(File f) :
call(* File.open(..)) && target(f){
writes = 0;
}
event write after(File f) :
call(* File.write(..)) && target(f) {
writes ++;
}
event close after(File f) :
call(* File.close(..)) && target(f) {
}
 
ere : (open write write* close)*
 
@fail { __RESET; }
@match { File.log((++(this.counter)) + ":" + this.writes); }
}

The following JavaMOP specification checks the following property: the hashcode of an object should not be changed if the object is an element in some hashset.

SafeHashSet(HashSet t, Object o) {
int hashcode;
 
event add after(HashSet t, Object o) :
call(* Collection+.add(Object)) && target(t) && args(o) {
hashcode = o.hashCode();
}
event bad_use before(HashSet t, Object o) :
call(* Collection+.contains(Object)) && target(t) && args(o)
&& condition(hashcode != o.hashCode()) {
}
event remove after(HashSet t, Object o) :
call(* Collection+.remove(Object)) && target(t) && args(o){
}
 
ltl : add => (not bad_use U remove)
 
@violation{
System.err.println("HashCode changed for Object " + o + " while being in a Hashtable!");
System.exit(1);
}
}
Personal tools
Namespaces

Variants
Actions
Navigation