Figure 2.22. Concrete Syntax for Low-level Thread or Function Body
|
Figure 2.22, “Concrete Syntax for Low-level Thread or Function Body” presents the concrete syntax for low-level thread or function body. Low-level body is designed as a target for translation from other languages and as the representation that the model checking engine works on, and also used for the representation used by the monotonic dataflow analysis framework in Bogor. Low-level body is often used for pedagogical reasons when describing concurrent models since its interleaving points are explicit, i.e., interleavings only happen between locations.
A low-level body consists of one or more locations followed by zero or more catch declarations. See the next section for examples.
Locations represent the control points of threads and functions. The first declared location in a body is called the body's initial location. When a thread is created, its program counter is set to the initial location. Similarly, when a function is called, the executing thread's program counter is set to the initial location of the functio after the thread's stack frames are stored.
Each location can be annotated with a live variable set. The live variable set indicates which parameters or local variables whose values should be preserved after executing the location's transformations. That is, parameters and local variables that are not in the live set are set to their default values once any of the location's transformation is executed. If the live set is not specified, then Bogor automatically calculates this set by using the well-known dead-variable analysis (using its monotonic dataflow analysis framework).
Namespace. Each thread or function has a dedicated namespace for its locations.
Abstract Syntax Tree. The Java AST class for location declaration is the Location class. The Java AST class for live sets is the LiveSet class.
Transformations represent transitions in BIR. There are two kinds of transformations: (1) block transformation and (2) invoke transformation. Regardless of the kind, a transformation can have a guard which is a predicate over state variables. If the guard is true in a certain state or not specified, then the transformation is called enabled in that state. In contrast, if the guard is false, then the transformation is called disabled. When a thread is executed, it non-deterministically chooses one of its enabled transformation to be executed. Evaluation of a guard should not cause an exception to be raised, however, there is a degree of freedom in the implementation of how it can be handled (e.g., consider the guard to be true/false, or raising an exception).
A transformation can be annotated with the "invisible" or the "visible" modifiers. The invisible modifier indicates that the state after the transformation is executed is invisible from the other thread, thus, it prevents a thread context switch in that state (unless all the transformations of the executing thread at the next state are all disabled or none at all). The visible modifier is the dual of the invisible modifier. When the modifiers are not specified, the transformation are usually considered visible, unless a reduction algorithm such as partial order reduction can determine that the transformation is invisible.
Abstract Syntax Tree. The top level Java AST class for transformation declaration is the Transformation class.
A block transformation consists of a sequence of actions and a jump. The actions are executed atomically.
Abstract Syntax Tree. The Java AST class for block transformation is the BlockTransformation class.
An invoke transformation is used to call a function. The call can be facilitated using a virtual table by using the "virtual" modifier. If the function that is called has a return type, then the returned value can be assigned to a local variable. The return type of the function should be compatible with the type of the local variable.
PENDING: "reflect"
Abstract Syntax Tree. The Java AST class for invoke transformation is the InvokeTransformation class.
A jump indicates the next control point after a transformation is executed. There are two kinds of jumps: (1) goto jump and (2) return jump.
Abstract Syntax Tree. The top level Java AST class for jump declaration is the NextState class.
A goto jump "goto" <loc-id> indicates that the next control point is the location <loc-id> within the same thread or function (the <loc-id> must be declared).
Abstract Syntax Tree. The Java AST class for goto jump is the GotoNextState class.
For a thread, a return jump indicates that the thread is terminated after the transformation is executed. For a function, a return jump indicates that the next control point is the next control point of the caller. If the function has a return type, then the local variable that contains the value to be returned should be specified. The type of the local variable should be compatible with the return type of the function.
Abstract Syntax Tree. The Java AST class for return jump is the ReturnNextState class.
A catch construct indicates the throwable record that can be caught at the specified locations. Once caught, the throwable record is assigned to the local variable and then the control point is transferred according to the jump construct that is specified. When an exception is raised, the catch declarations are consulted in the order of their declarations. If there is no catch whose throwable record type is equal (or the super record of the record being thrown), then the exception is propagated up to the call chain. If the exception is not handled at the top of the call chain (i.e., the threads), then the exception is uncaught. Uncaught exceptions are errors in the model.
Abstract Syntax Tree. The Java AST class for catch declaration is the Catch class.