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."

Variables

• BoundVariable
• FormalVariable
• LocalVariable
• ProcessVariable
• SharedVariable

Types

• ArrayType
• FunctionType
• PointerType
• RecordType

Expressions

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

Statements

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

Functions