JavaMOP Syntax

From FSL
(Redirected from MOP Specification)
Jump to: navigation, search

The formal syntax of JavaMOP is given below using BNF. Some examples are also given at the end.

// BNF below is extended with {p} for zero or more and [p] for zero or one repetitions of p
 
<Specification> ::= {<Modifier>} <Id> <Parameters> "{"
{<Declaration>}
{<Event>}
{ <Property>
{<Property Handler>}
}
"}"
<Modifier> ::= "unsynchronized" | "decentralized" | "perthread" | "suffix"
<Event> ::= "event" <Id> <Event Definition> <Action>
<Property> ::= <Logic Name> ":" <Logic Syntax>
<Property Handler> ::= "@" <Logic State> <Action>
<Event Definition> ::= <Advice Specification> ":" <Extended Pointcut>
<Action> ::= "{" [ <Statements> ] "}"
<Extended Pointcut> ::= <Pointcut>
| <Extended Pointcut> "&&" <Extended Pointcut>
| "thread" "(" <Id> ")"
| "condition" "(" <Boolean Expression> ")"
 
<Parameters> ::= "(" [ <Parameter> { "," <Parameter> } ] ")"
<Parameter> ::= <Type Pattern> <Id>
<Type Pattern> ::= <!-- AspectJ Type Pattern -->
<Id> ::= <!-- Java Identifier -->
<Declaration> ::= <!-- Java variable declaration -->
<Advice Specification> ::= <!-- AspectJ AdviceSpec -->
<Pointcut> ::= <!-- AspectJ Pointcut -->
<Statements> ::= <!-- Java statements -->
<Boolean Expression> ::= <!-- Java boolean expressions -->

<Specification>

JavaMOP syntax instantiates the generic MOP Syntax by defining the relevant modifiers and language-specific syntax: Java syntax for declarations and event/handler actions and AspectJ syntax for event definitions. Specific explanation is given below.

<Modifier>

JavaMOP supports four modifiers which can be used to control the running mode of the monitor. As the grammar shows, modifiers are placed at the beginning of the specification definition.

  • unsynchronized

When this modifier is specified, the monitor state is not protected against concurrent accesses during monitoring; otherwise, the accesses to the monitor state will be synchronized. The unsynchronized monitor is faster, but may suffer from races on its state updates, if the monitored program has multiple threads.

  • decentralized

When this modifier is specified, decentralized monitor indexing is used to store the monitor for different parameter instances. If it is not specified, the default mode is centralized monitor indexing. Decentralized indexing means that the indexing trees used to search for monitors are scattered all over the running system as additional fields of objects of interest, while centralized indexing means the indexing trees are stored in a common place. Decentralized indexing typically yields lower runtime overhead, but it does not work for all settings, such as when the objects of interest cannot be modified with aspects. Our OOPSLA'07 paper on THIS PAGE explains how centralized and decentralized indexing work.

  • perthread

When this modifier is specified, each thread is monitored separately, and every monitor never receives events from more than one thread. JavaMOP will optimize the monitoring code accordingly. For example, perthread monitors are automatically unsynchronized.

  • suffix

When this modifier is specified, suffix matching is used. If it is not specified, the default mode is total matching. In total matching, the given property is checked against the whole execution trace. In suffix matching, the given property is checked against every suffix of the execution trace. For example, for a regular pattern a b and a trace a a b, total matching will find no match of the pattern, while suffix matching will generate one match for the suffix a b starting from the second a.

<Event>

The event declaration defines events that will be observed at runtime and referred to in the specified property (see below). Every event declaration begins with keyword event followed by an <Id> that gives the name of the event. <Event Definition> and <Action> define a condition and its behavior when triggered.

<Property>

Every JavaMOP specification may contain zero or more properties. 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. Please refer to the OOPSLA'07, RV'05 and ICFEM'04 papers on THIS PAGE for discussions about logic plugins in MOP. The current version of JavaMOP provides the following logics that one can use in the property specification:

A JavaMOP specification containing no property 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 action.

<Property Handler>

Property handlers may be defined for certain states (designated by <Logic State>) of the generated monitor. A property handler consists of any arbitrary Java statements that will be invoked whenever the designated state is reached in the generated monitor. Just as the event action, the handler may modify the program or the monitor state. The monitor states to which one can associate handlers are determined by the underlying formalism, e.g., validation or violation in linear temporal logic specifications, match or fail for ERE or CFG, or a particular state in a finite state machine description. One may refer to the input syntax page of a certain logic for the complete definition of allowed states.

<Event Definition>

<Event Definition> in JavaMOP makes uses of AspectJ syntax. It consists of <Advice Specification> and <Extended Pointcut>, which define where the event is triggered by the program.

<Action>

Events and handlers can also have arbitrary code associated with them, called an action. The action is run when the associated event is observed, or the handler triggered. An action is surrounded by curly braces ("{" and "}"), and can contain any arbitrary Java statements. <Action>s may modify the program or the monitor state. They have access to the special expressions defined in the <Statements>.

<Extended Pointcut>

<Extended Pointcut> extends the AspectJ Pointcut with the following two JavaMOP-specific pointcuts:

  • thread captures the current thread and takes an identifier as the parameter. The identifier is bound to the running thread object. The captured thread object is stored into the given variable so that the monitor can access it later.
  • condition takes a boolean expression as the parameter. The event is triggered only when the given boolean expression evaluates to true.

<Parameters>, <Parameter>, and <Type Pattern>

<Parameters> is a list of parameters (<Parameter>) separated by commas. <Parameter> is composed of a type pattern (<Type Pattern>) that defines the type of the parameter and an identifier (<Id>) that gives the name of the parameter. <Type Pattern> is the AspectJ type pattern, which allows for using wildcards, such as + and *, to define patterns of types. The list of parameters defines which parameters may be used in the events of the specification.

<Id> and <Declaration>

<Id> are ordinary Java identifiers; and <Declaration> is a Java declaration. The declarations are additional monitor variables that one can access and modify in both event actions and property handlers.

<Advice Specification> and <Pointcut>

This syntax refers to the ApsectJ AdviceSpec and Pointcut, respectively. JavaMOP borrows AspectJ syntax for its expressiveness and also to facilitate code synthesis.

<Statements> and <Boolean Expression>

<Statements> are ordinary Java statements. <Statements> also support three special expressions that can be used in the property handler (see examples below):

  • __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 where the current event is generated;
  • __MONITOR: a special variable that evaluates to the current monitor object, so that one can read/write monitor variables.

<Boolean Expression> is the ordinary Java boolean expression.


Examples

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

decentralized unsynchronized 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);
}
}

This example showcases the thread pointcut. Here it is used to ensure that events from separate threads are not seen by different parameter instance monitors. This allows us to use the unsynchronized keyword, because a monitor will never be accessed by separate threads, and has no need to be reentrant or synchronized.

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((++(__MONITOR.counter)) + ":" + __MONITOR.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 unsafe_contains 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){}
 
ftltl : add -> (! unsafe_contains 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