The MiniMP Intermediate Representation

Model

A model is an abstract representation of a MiniMP program. It has a name, a set of shared variables, and a sequence of processes.

Processes

Processes are numbered 0,1,...,n-1, where n is the number of processes. The number n is fixed when the model is created and can never change. The unique number associated to a process is known as the process's "pid."

Each process contains a number of process variables, and a number of functions. One of the functions is designated the "main" function (though that function's name does not have to be "main"). In particular, every process must contain at least one function.

Variables

There are four different scopes to which a variable may belong.

• SharedVariable

Shared scope includes all input and output variables, and general shared variables; these are variables that can be accessed by any process.

• ProcessVariable

Process variables have the scope of one process; they can be accessed by any function in that process.

• LocalVariable

Local variables are local to a specific function in a specific process. They can only be accessed within the function body.

• FormalVariable

Formal variables are the formal parameters to a function. They are a special type of local variable.

• BoundVariable

Bound variables are specific to an expression; these are variables from forall and exists statements.

Types

• ArrayType
• FunctionType
• PointerType
• RecordType

Expressions

• PlusExpression
• TimesExpression
• DivideExpression
• AddressOfExpression
• LHSExpression
  • DereferenceExpression
  • RecordNavigationExpression
• ExistsExpression
• ForallExpression
• IfThenElseExpression
• LiteralExpression
• NotEmptyExpression
• NotFullExpression
• QuantifierExpression
• VariableExpression

Locations

The locations fall into a number of categories, for the most part corresponding to the kinds of statements that can emanate from that location. Some locations only allow one outgoing statement, while others allow several, and others none.

• AllocateLocation
• AssertionLocation
• AssignmentLocation
• AssumeLocation
• BranchLocation
• ChoiceLocation
• DeallocateLocation
• ForLoopLocation
• InvocationLocation
• ReceiveLocation
• ReturnLocation
• SendLocation
• TerminalLocation

Statements

Each statement has a single source location and a single destination location.

• AllocateStatement
• AssertionStatement
• AssignmentStatement
• AssumeStatement
• DeallocateStatement
• InvocationStatement
• NoopStatement
• ReceiveStatement
• SendStatement

Functions

A function specifies a number of formal parameters, or "formal variables." In addition, it specifies a number of "proper local variables." All of these (formal and proper locals) are referred to as "local variables." The local variables can only be accessed within the function body.

The function body itself is a transition system. The function contains a set of locations and a set of statements. These define a directed graph in which the locations are nodes and the statements are edges. A function has a designated "start location," and thus every function must have at least one location.