Figure 2.31. Concrete Syntax for Actions
|
Figure 2.31, “Concrete Syntax for Actions” presents the concrete syntax for BIR actions declarations. Non-atomic high-level actions are translated to their 3-address code low-level equivalent.
Abstract Syntax Tree.
The top level Java AST class for BIR actions is the Action class.
Assign action is used to update the value of a variable, a record/array field, or an array element.
Examples.
- x := 1;
- x.f := 1;
- x[0] := 1;
Abstract Syntax Tree. The Java AST class for assign action is the AssignAction class.
Assert action is used to check whether the assert's condition (of type boolean) holds. If the condition does not hold, then it is considered as an error in the model.
Examples.
- assert f(x);
- assert x > 0;
Abstract Syntax Tree. The Java AST class for assert action is the AssertAction class.
Assume action is used to filter paths. If the assume's condition is false, then Bogor will backtrack from exploring the current path.
Examples.
- assume f(x);
- assume x > 0;
Abstract Syntax Tree. The Java AST class for assume action is the AssumeAction class.
Lock operation action is used to change the state of a lock value:
- lock acquires the given lock so it is held by the current executing thread and set the lock count to one if the lock is free. Otherwise, if the lock has been held by the current executing thread, then it increases its lock count by one. If not, then a bad monitor exception is raised.
- unlock releases the given lock if the lock is held by the current executing thread; it decreases the lock's lock count by one. If the lock count is zero after the decrement, then the lock becomes free. If the current executing thread does not hold the lock, then a bad monitor exception is raised.
- wait puts the current executing thread in the lock wait set and stores its lock count in the state if the lock is held by the current executing thread. Otherwise, a bad monitor exception is raised.
- unwait removes the current executing thread from the lock's notification set and makes the thread as the owner of the lock as well as restoring the lock's lock count from the thread's lock count stored in the state (i.e., the thread's lock count is removed from the state). The lock must be free before unwait is executed, otherwise, a bad monitor exception is raised.
- notify non-deterministically removes one thread from the lock's wait set, if any, and puts it in the lock's notification set. The current executing thread must hold the lock, otherwisem a bad monitor exception is raised.
- notifyAll removes all threads from the lock's wait set and put them in the lock's notification set. The current executing thread must hold the lock, otherwisem a bad monitor exception is raised.
Examples.
- lock(a.l);
- unwait(l);
Abstract Syntax Tree. The Java AST class for lock operation actions is the LockAction class. The lock operators are defined in the LockOp class.
Throw exception action is used to raise a throwable record value.
Examples.
- throw r;
- throw new ThrowableRecord;
Abstract Syntax Tree. The Java AST class for throw exception action is the ThrowAction class.
Start thread action is used to create an instance of a thread, and returns the newly created thread descriptor value (of type tid).
Examples.
- start T(5);
- myTID := start T();
Abstract Syntax Tree. The Java AST class for start thread action is the ExpAction class with the StartThreadExp class.
Exit thread action is used to terminate the current executing thread.
Example.
- exit;
Abstract Syntax Tree. The Java AST class for exit thread action is the ExitThreadAction class.
Extension call action is used to call an action extension. For a parametric action extension, Bogor tries to infer the arguments to the declared parametric type variables.
Examples.
- Set.add(myset, 5);
- Set.remove(myset, 5);
Abstract Syntax Tree. The Java AST class for extension call action is the ExpAction class with the ExtExp class.