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

Used to allocate contiguous memory for an array of elements, similar to C's "malloc." You specify the type of element and the number of elements to allocate an array of that length and element type. An allocation statement returns a pointer to the first element in the array.

• AssertionStatement

Used to input a boolean condition. The condition will be checked, and an error returned if it cannot be shown to hold.

• AssignmentStatement

Statement of the form lhs = rhs;. Note that rhs is an expression. Expressions are side-effect free. In particular, they cannot involve function calls. There is a special InvocationStatement for dealing with function calls and assigning the returned value of the function call to a variable.

• AssumeStatement

Used to add a boolean statement to the path condition. A statement added in this was will be assumed to hold for future statements.

• DeallocateStatement

A deallocate statement deallocates previously allocated memory, similar to C's "free."

• InvocationStatement

Represents a statement of the form lhs = f(a0, a1, ...); or the form f(a0, a1, ...); In the left hand side is null.

• NoopStatement

A statement that does nothing.

• ReceiveStatement

A statement to receive a message.

• SendStatement

A statement to send a message.

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.