11institutetext: Moscow State University, Faculty of Mechanics and Mathematics
<EMAIL_ADDRESS>
# Verification of MPI programs

Andrew M. Mironov

###### Abstract

In this paper, we outline an approach to verifying parallel programs. A new
mathematical model of parallel programs is introduced. The introduced model is
illustrated by the verification of the matrix multiplication MPI program.

##  1 Introduction

Parallel programs are computer programs designed to be executed on
multiprocessor computing systems (MPCS). The problem of developing correct and
safe parallel programs is currently highly topical. Formal verification of
correctness and safety properties of parallel programs is a complex
mathematical problem. The existing methods for solving this problem are
suitable only for a limited class of parallel programs.

One of the most widely used languages for describing parallel programs is MPI
(Message Passing Interface).

In this paper, a new mathematical model of MPI programs is introduced. On the
basis of this model one can solve the problems of verifying parallel programs
presented on a certain subset of MPI. The introduced model is illustrated by
the verification of the matrix multiplication MPI program.

The most essential feature of the approach to modeling and verification of MPI
programs presented in this paper is the possibility of using this approach for
MPI programs that can generate any number of processes.

Among other approaches to modeling and verifying MPI programs for any number
of processes it should be noted the approach in the work [1]. In this work the
tool for modeling and verifying MPI programs called ParTypes is presented. It
requires the user to provide a protocol which specifies the communication
pattern of an execution. Unfortunately, it has some limitations. In
particular, it does not work for wildcard receives, which means it cannot be
applied to the MPI program for matrix multiplication considered in the present
paper. There are other approaches using symbolic execution and model checking
([3]-[10]), but all of them require a bound on the number of processes.

##  2 Essentials for MPI

###  2.1 MPI programs

MPI (Message Passing Interface) is a set of functions, types and constants for
a development of parallel programs (called MPI programs). A MPI program is a C
program in which functions, types and constants from MPI can be used. An
execution of an MPI program on a MPCS has the following form: at each node of
the MPCS, a computational process corresponding to this MPI program is
generated. All processes generated by the MPI program operate in parallel and
can exchange information with each other through message passing.

Each process generated by a MPI program has a rank, which is a number from the
set $\\{0,\ldots,m-1\\}$, where $m$ is the number of processes generated by
the MPI program. A process with rank 0 is called a root process.

MPI has functions `MPI_Comm_rank `and `MPI_Comm_size`. Each process generated
by a MPI program can use these functions to find out its rank and a number of
processes generated by this MPI program, respectively:

  * •

`MPI_Comm_rank (MPI_COMM_WORLD, &rank);`
after executing this function, a value of variable `rank` (`int`) will be
equal to the rank of the process that called this function,

  * •

`MPI_Comm_size (MPI_COMM_WORLD, &nprocs);`
after executing this function, a value of variable `nprocs` (`int`) will be
equal to the number of processes generated by the MPI program.

###  2.2 Message Passing Functions

In MPI, a message is an array of data of a certain type, and message passing
(MP) is an action, as a result of which a message is sent by one process and
is received by other process (or processes). A sent message is placed in a
queue, from which it will then be taken by the receiving process.

We will consider the following types of MP MPI functions:

  * •

pairwise MP (PMP): there are two processes involved in a PMP: a sender of a
message, and a receiver of this message,

  * •

broadcast MP (BMP): all processes generated by a MPI program participate in an
executing of a BMP, root process is a sender of a message, and other processes
are receivers of this message.

Messages sent by PMP functions cannot be received by BMP functions, and vice
versa. Below we describe some of MP functions. In the descriptions, for each
argument of these functions, we indicate its type in parentheses.

  1. 1.

Sending a message (PMP) :

$\begin{array}[]{llllllllllllll}{\tt MPI\\_Send}&(p,n,\tau,r,l,{\tt
MPI\\_COMM\\_WORLD});\end{array}$ (1)

This function is performed by sending a message to a process with rank $r$
(`int`). The message being sent is an array of $n$ (`int`) elements of type
$\tau$ (`MPI_Datatype`), the beginning of which is at $p$ (`void *`). The tag
(i.e. label) $l$ (`int`) is appended to the message being sent.

  2. 2.

Receiving a message (PMP):

$\begin{array}[]{llllllllllllll}{\tt MPI\\_Recv}&(p,n,\tau,{\tt
MPI\\_ANY\\_SOURCE},{\tt MPI\\_ANY\\_TAG},{\tt
MPI\\_COMM\\_WORLD},q);\end{array}$ (2)

This function is performed by receiving a message, which should be placed in
the memory location the beginning of which is at $p$. It is assumed that the
received message is an array of no more than $n$ elements of type $\tau$.

$q$ `(MPI_Status *)` is an address of a structure in which information about
the received message should be placed. This structure contains the following
fields: `MPI_SOURCE` (the sender’s rank must be placed in it), `MPI_TAG` (the
received message tag must be placed in it), and other fields.

  3. 3.

Sending a message from a root process to other processes (BMP):

$\begin{array}[]{llllllllllllll}{\tt MPI\\_Bcast}&(p,n,\tau,0,{\tt
MPI\\_COMM\\_WORLD});\end{array}$ (3)

This function is performed as follows.

     * •

In a root process, a message is sent to all other processes, which is an array
of $n$ (`int`) elements of type $\tau$ (`MPI_Datatype`), the beginning of
which is located at $p$ (`void *`).

     * •

In other processes, a message is received from the root process, which must be
located in the memory location at $p$. It is assumed that the received message
is an array of no more than $n$ elements of type $\tau$.

##  3  Matrix Multiplication MPI Program

In this section, we present an example of a matrix multiplication MPI program.
The example is taken from [2]. This example is used below to illustrate the
application of the model of MPI programs described in this work for verifying
MPI programs.

###  3.1 Informal Description of Matrix Multiplication MPI Program

The problem of matrix multiplication is to calculate a product $C=AB$ given
the matrices $A$ and $B$. Informally, the work of the MPI program $\Pi$ for
multiplying the matrices $A$ and $B$, stated in this section, can be described
as follows. We will call a root process of $\Pi$ a manager and other processes
of $\Pi$ workers. Manager’s job consists of the following actions:

  * •

sending second matrix ($B$) to all workers,

  * •

assigning tasks to workers, and receiving results from workers.

Each task for a worker is to calculate one row of the matrix $C=AB$. The
manager assigns this task by sending the worker a message containing one row
of matrix $A$. A tag of this message is equal to the number of the row being
sent. As soon as the manager receives a result from a worker (i.e., a message
with the calculated row of the product, its tag is equal to the number of this
row), he sends this worker either a new task (if there are still unassigned
tasks), or a message with tag 0 (if there are no unassigned tasks).

###  3.2 MPI Matrix Multiplication Program

The following matrix multiplication MPI program $\Pi$ uses auxiliary function
`vecmat` to multiply the row `vector[L]` by the matrix `matrix[L][M]` and
write the result to the array `result[M]`. This function looks like this:

    void vecmat (double vector[L],
                 double matrix[L][M],
                 double result[M])
    { int j, k;
      for (j = 0; j < M; j++)
        for (k = 0, result[j] = 0.0; k < L; k++)
          result[j] += vector[k]*matrix[k][j];
    }

In the MPI program $\Pi$ presented below, we use the following notation:
`input(a, b);` and `output(c);` are abbreviations of the functions for reading
from the file of the factors and writing to the file of the product,
respectively.

A MPI program $\Pi$ for multiplying matrices $A$ and $B$ has the following
form (in this program, to the left of each line, we indicate its number, this
is necessary to describe the correspondence between components of this program
and components of the model ${\cal P}_{\Pi}$ of this program):

    01 #define comm MPI_COMM_WORLD
    02
    03 int main(int argc, char *argv[])
    04 { int rank, nprocs, i, j;
    05   MPI_Status status;
    06
    07   MPI_Init(&argc, &argv);
    08   MPI_Comm_size(comm, &nprocs);
    09   MPI_Comm_rank(comm, &rank);
    10
    11   if (rank == 0)
    12   { int count;
    13     double a[N][L], b[L][M], c[N][M], tmp[M];
    14
    15     input(a, b);
    16     MPI_Bcast(b, L*M, MPI_DOUBLE,
    17               0, comm);
    18     for (count = 0;
    19          count < nprocs-1 && count < N;
    20          count++)
    21       MPI_Send(&a[count][0], L, MPI_DOUBLE,
    22                count+1, count+1, comm);
    23     for (i = 0; i < N; i++)
    24     { MPI_Recv(tmp, M, MPI_DOUBLE,
    25                MPI_ANY_SOURCE, MPI_ANY_TAG,
    26                comm, &status );
    27       for (j = 0; j < M; j++)
    28         c[status.MPI_TAG-1][j] = tmp[j];
    29       if (count < N)
    30       { MPI_Send(&a[count][0], L, MPI_DOUBLE,
    31                  status.MPI_SOURCE, count+1, comm);
    32         count++;
    33       }
    34     }
    35     for (i = 1; i < nprocs; i++)
    36       MPI_Send(NULL, 0, MPI_INT,
    37                i, 0, comm);
    38     output (c);
    39   }
    40
    41   else
    42   { double b[L][M], in[L], out[M];
    43
    44     MPI_Bcast(b, L*M, MPI_DOUBLE,
    45               0, comm);
    46     while (1)
    47     { MPI_Recv(in, L, MPI_DOUBLE,
    48                0, MPI_ANY_TAG,
    49                comm, &status);
    50       if (status.MPI_TAG == 0) break;
    51       vecmat(in, b, out);
    52       MPI_Send(out, M, MPI_DOUBLE,
    53                0, status.MPI_TAG, comm);
    54     }
    55   }
    56
    57   MPI_Finalize();
    58   return 0;
    59 }

###  3.3 Auxiliary notation

For the convenience of modeling and verification this program, we introduce
special designations for some of the objects used in it:

  * •

arrays `a[N][L]`, `b[L][M]`, `c[N][M]`, will be denoted by symbols $A,B,C$ and
interpreted as corresponding matrices,

  * •

the message sent by the `MPI_Send` functions in lines 21, 22 and 30, 31 of the
program will be understood as the corresponding row of the matrix $A$, and
denoted by $A_{i}$, where $i={{\tt count}+1}$,

  * •

array `c[status.MPI_TAG-1][M]`, into which the message received by the
`MPI_Recv` function in lines 24, 25, 26 is copied, we interpret it as a
corresponding row of $C$, and denote it by $C_{l}$, where $l=$
`status.MPI_TAG`,

  * •

from the definition of the `vecmat` function it follows that array `out`
calculated as a result of the execution of the `vecmat` function on line 51
corresponds to the product of the row $Y$ corresponding to array `in` by
matrix $B$, we will denote this array `out` in the model of $\Pi$ by the
product $YB$.

###  3.4 A specification of the matrix multiplication MPI program

A specification of the MPI program $\Pi$ is the following statement: after a
completion of any execution of $\Pi$ the equality $C=AB$ holds, i.e.

$\forall\,i=1,\ldots,N\quad C_{i}=A_{i}B.$ (4)

##  4 A model of a MPI program

In this section, we introduce a concept of a model of a MPI program. This
model is designed for formal representation of MPI programs that use the above
message passing functions. The basic concepts of this model are sequential and
distributed processes. A sequential process is a model of a computational
process generated by a MPI program on a node of a MPCS, and a distributed
process is a model of a MPI program on the whole. The proposed model is a
theoretical basis for solving problems of verifying MPI programs.

###  4.1 Auxiliary concepts

We assume that there are given sets ${\cal T}$, ${\it{\it{\cal X}}}$ and
${\cal F}$, elements of which are called types, variables, and function
symbols (FS), respectively. Each element $x$ of ${\it{\cal X}}$ and ${\cal F}$
is associated with some type $\tau_{x}\in{\cal T}$. $\forall\,f\in{\cal F}$
$\tau_{f}$ has the form

$(\tau_{1},\ldots,\tau_{n})\to\tau,\quad\mbox{where
}\tau_{1},\ldots,\tau_{n},\tau\in{\cal T}.$ (5)

$\forall\,\tau\in{\cal T}$ a set ${\cal D}_{\tau}$ of values of type $\tau$ is
given. ${\cal D}$ denotes a set of values of all types. ${\cal T}$ has the
types B, N, C, where ${\cal D}_{\bf B}=\\{0,1\\}$, ${\cal D}_{\bf N}$ is the
set of natural numbers $\\{0,1,\ldots\\}$, values of type C are called
channels.

$\forall\,f\in{\cal F}$, if $\tau_{f}$ has form (5), then this FS is
associated with a function (denoted by the same symbol $f$) of the form ${\cal
D}_{\tau_{1}}\times\ldots\times{\cal D}_{\tau_{n}}\to{\cal D}_{\tau}$.

The set ${\cal E}$ of terms is defined inductively. Each term $e\in{\cal E}$
is associated with a type $\tau_{e}\in{\cal T}$. The definition of a term is
as follows: each $e\in{\cal D}\cup{\cal X}$ is a term of the type $\tau_{e}$,
and if $f\in{\cal F}$, $e_{1},\ldots,e_{n}\in{\cal E}$, and
$\tau_{f}=(\tau_{e_{1}},\ldots,\tau_{e_{n}})\to\tau,$ then
$f(e_{1},\ldots,e_{n})$ is a term of type $\tau$.

$\forall\,e\in{\cal E}\;\;{\cal X}_{e}=\\{x\in{\cal X}\mid x\mbox{ occurrs in
}e\\}$, ${\cal E}_{0}=\\{e\in{\cal E}\mid{\cal X}_{e}=\emptyset\\}$. Each
$e\in{\cal E}_{0}$ is associated with a value $value(e)\in{\cal D}$, where
$\forall\,e\in{\cal D}\;\;value(e)=e$, and if $e=f(e_{1},\ldots,e_{n})\in{\cal
E}_{0}$, then $value(e)=f(value(e_{1}),\ldots,value(e_{n}))$.
$\forall\,e\in{\cal E}_{0}$ the value $value(e)$ will be denoted by the same
notation $e$.

We will assume that

  * •

$\forall\,n\geq 1$ ${\cal F}$ has FS $tuple_{n}$, which allows to construct
tuples: for each list of terms $e_{1},\ldots,e_{n}$, the set ${\cal E}$ has
the term $tuple_{n}(e_{1},\ldots,e_{n})$, which we will denote by
$(e_{1},\ldots,e_{n})$ and interpret as a tuple of terms $e_{1},\ldots,e_{n}$,

  * •

${\cal F}$ has FS $channel$ of the type ${\bf N}\to{\bf C}$, $\forall\,i\geq
0$ the channel $channel(i)$ is said to be an $i$-th channel, a term of the
form $channel(e)$ will be denoted by $c_{e}$,

  * •

${\cal D}_{\bf C}$ has a broadcast channel $\circ$, it differs from all
channels $c_{i}\;(i\geq 0)$.

$\forall\,E\subseteq{\cal E}\;\;\forall\,\tau\in{\cal T}\;\;E_{\tau}=\\{e\in
E\mid\tau_{e}=\tau\\}$. The sets ${\cal E}_{\bf B}$ and ${\cal E}_{\bf C}$ are
denoted by ${\cal B}$ and ${\cal C}$, elements of ${\cal B}$ are called
formulas. $\forall\,X\subseteq{\it{\cal X}}\;\;{\cal E}(X)=\\{e\in{\cal
E}\mid{\it{\cal X}}_{e}\subseteq X\\}$, ${\cal B}(X)={\cal E}(X)\cap{\cal B}$.
Below, for each function $f:E\to E^{\prime}$ under consideration, where
$E,E^{\prime}\subseteq{\cal E}$, we assume that $\forall\,e\in
E\;\;\tau_{f(e)}=\tau_{e}$.

${\cal D}^{*}$ denotes the set of all tuples of the form
$(d_{1},\ldots,d_{n})$, where $n\geq 0$ and $d_{1},\ldots,d_{n}\in{\cal D}$,
if $n=0$ then the corresponding tuple is said to be empty and is denoted by
$\varepsilon$. Elements of ${\cal D}^{*}$ are called queues.
$\forall\,D\in{\cal D}^{*}$ $|D|$ denotes the number of components in $D$. If
$D\in{\cal D}^{*}$ and $1\leq i\leq|D|$, then $D_{i}$ denotes $i$-th component
of $D$. $\forall\,M\subseteq{\cal D}^{*}$, $\forall\,i\geq 1\;\;M_{i}$ denotes
the set of $i$-th components of tuples from $M$. If
$D=(d_{1},\ldots,d_{n})\in{\cal D}^{*}\setminus\\{\varepsilon\\}$, then
$head(D)$ and $tail(D)$ denote the value $d_{1}$ and the queue
$(d_{2},\ldots,d_{n})$ respectively.

A binding is a function $\theta:{\it{\cal X}}\to{\cal E}$. The set of all
bindings is denoted by $\Theta$.

We will use the following notation:

  * •

$\forall\,X\subseteq{\it{\cal
X}}\quad\Theta(X)=\\{\theta\in\Theta\mid\forall\,x\in{\it{\cal X}}\setminus
X\;\;\theta(x)=x\\},$

  * •

$\forall\,\theta\in\Theta,\;\forall\,e\in{\cal E}\;\;e^{\theta}$ is a term
obtained from $e$ by replacing $\forall\,x\in{\it{\cal X}}_{e}$ each
occurrence of $x$ in $e$ on the term $\theta(x)$,

  * •

$\forall\,\theta,\theta^{\prime}\in\Theta\;\;\theta\theta^{\prime}$ is a
binding such that $\forall\,x\in{\cal
X}\;\;(\theta\theta^{\prime})(x)=(x^{\theta})^{\theta^{\prime}}$.

###  4.2 Sequential processes

In this section we define a concept of a sequential process (SP). A SP is a
model of a computational process generated by a MPI program on a node of a
MPCS.

Elementary actions (EA) are notations of the following forms:

$\begin{array}[]{llllllllllllll}c!e,\quad c?e,\quad
e:=e^{\prime},\quad[\\![\varphi]\\!],\quad\mbox{where }\;c\in{\cal
C},\;e,e^{\prime}\in{\cal E},\tau_{e}=\tau_{e^{\prime}},\varphi\in{\cal
B},\end{array}$

which are called a sending message $e$ to channel $c$, a receiving message $e$
from channel $c$, an assignment, and a conditional transition, respectively.

An action is a finite sequence of EAs, in which there is no more than one
sending or receiving. An action $\alpha$ is called a sending or a receiving if
one of EAs occurred in $\alpha$ is a sending or a receiving, respectively. An
action that is not a sending or a receiving is called an internal action. Each
EA can be considered as an action consisting of this EA. The set of all
actions is denoted by ${\cal A}$. $\forall\,\alpha\in{{\cal A}}\;\;{\it{\cal
X}}_{\alpha}$ is the set of all variables occurred in $\alpha$.
$\forall\,\theta\in\Theta,\forall\,\alpha\in{\cal A}\;\;\alpha^{\theta}$
denotes an action obtained from $\alpha$ by replacing each $x\in{\cal
X}_{\alpha}$ on $x^{\theta}$.

A sequential process (SP) is a triple $(P,X,\varphi)$, components of which
have the following meaning:

  * •

$P$ is a graph with a selected node $P^{0}$ (called an initial node), each
edge of which has a label $\alpha\in{\cal A}$,

  * •

$X\subseteq{\it{\cal X}}$ is a set of input variables of SP $P$, and

  * •

$\varphi\in{\cal B}$ is an initial condition of SP $P$.

For each SP $(P,X,\varphi)$

  * •

this SP is denoted by the same symbol $P$ as a graph of this SP, the set of
nodes of the graph $P$ is also denoted by $P$,

  * •

$X_{P}$ and $\varphi_{P}$ denote the second and third components of $P$
respectively,

  * •

${\it{\cal X}}_{P}$ is the set of all variables occurred in $P$,

  * •

$\hat{X}_{P}$ denotes the set ${\cal X}_{P}\setminus X_{P}$ of private
variables of SP $P$,

  * •

${\cal A}_{P}$ denotes the set of labels of edges of $P$,

  * •

$P^{v\to v^{\prime}}$ denotes an edge of $P$ from $v$ to $v^{\prime}$.

  * •

each node of the graph $P$ is an element of the set ${\cal D}$,

  * •

$P$ contains private variable $at_{P}$, and for each edge of the graph $P$, if
$v$ and $v^{\prime}$ are the start and the end of this edge, respectively,
then the first EA in the label of this edge has the form $[\\![at_{P}=v]\\!]$,
and the last one is $at_{P}:=v^{\prime}$, these EAs will not be specified
explicitly.

A SP is a formal description of a behavior of a dynamic system, a work of
which is a sequential execution of actions.

A state of SP $P$ is a pair $s=(\theta^{s},\\{[c]^{s}\mid c\in{\cal D}_{\bf
C}\\})$, where

  * •

$\theta^{s}\in\Theta({{\cal X}_{P}})$ is a binding, such that
$\forall\,x\in{\cal X}_{P}\;\;{\theta^{s}}(x)\in{\cal E}_{0}$,

  * •

$\forall\,c\in{\cal D}_{\bf C}\;\;[c]^{s}\in{\cal D}^{*}$ is a queue called a
content of channel $c$ in state $s$.

The set of all states of SP $P$ is denoted by $\Sigma_{P}$.

$\forall\,s\in\Sigma_{P}$, $\forall\,e\in{\cal E}({\cal X}_{P})$, the value
$e^{\theta^{s}}$ is denoted by $e^{s}$.

A state $s\in\Sigma_{P}$ is said to be initial, if
$s=(\theta,\\{\varepsilon\mid c\in{\cal D}_{\bf C}\\})$, where
$\varphi_{P}^{\theta}=1$ and $at_{P}^{s}=P^{0}$. An initial state of $P$ is
denoted by $0_{P}$. A state $s$ of SP $P$ is said to be terminal if there is
no an edge outgoing from $at_{P}^{s}$.

Below we define a concept of a transition of a SP $P$ corresponding to some
action $\alpha\in{\cal A}_{P}$. This transition is a pair $(s,s^{\prime})$ of
states from $\Sigma_{P}$, the relationship between $s$ and $s^{\prime}$ can be
understood as follows: if $P$ is in the state $s$ at the current time, then
after sequential execution of EAs from $\alpha$, a state of $P$ will be
$s^{\prime}$.

$\forall\,s,s^{\prime}\in\Sigma_{P}$, $\forall\,\alpha\in{\cal A}_{P}$ the
notation $s\;\mathop{\to}\limits^{\\!\\!\alpha}\;s^{\prime}$ denotes the
statement that $(s,s^{\prime})$ is a transition corresponding to $\alpha$.
This statement holds if $\alpha$ is a sequence of EAs of the form
$\alpha_{1}\ldots\alpha_{n}$, and

$\exists\,s_{1},\ldots,s_{n-1}\in\Sigma_{P}:s\;\mathop{\longrightarrow}\limits^{\alpha_{1}}\;s_{1},\;s_{1}\;\mathop{\longrightarrow}\limits^{\alpha_{2}}\;s_{2},\;\ldots,\;s_{n-1}\;\mathop{\longrightarrow}\limits^{\alpha_{n}}\;s^{\prime},$

where the statement $s\;\mathop{\to}\limits^{\\!\\!\alpha}\;s^{\prime}$ in the
case when $\alpha$ is an EA is defined separately for each form of $\alpha$,
after the formal definition of this statement for each specific form of
$\alpha$ we informally interpret the state change as a result of this
transition:

  * (a)

if $\alpha=c!e$, then $\theta^{s^{\prime}}=\theta^{s}$, and

$[c^{s}]^{s^{\prime}}=([c^{s}]^{s},{e^{s}}),\;\;\forall\,c^{\prime}\in{\cal
D}_{\bf C}\setminus\\{c^{s}\\}\;\;[c^{\prime}]^{s^{\prime}}=[c^{\prime}]^{s},$

in this case, $P$ sends the value $e^{s}$ to the channel $c^{s}$, after which

    * –

the content of the channel $c^{s}$ has been increased by adding $e^{s}$,

    * –

the binding of variables from ${\cal X}_{P}$ did not change, and contents of
all channels, except for the $c^{s}$ channel, also did not change,

  * (b)

if $\alpha=c?e$, then $[c^{s}]^{s}\neq\emptyset$ and

$\begin{array}[]{llllllllllllll}\,\exists\,\theta\in\Theta(\hat{X}_{P}):{(e^{\theta})^{s}}=head([c^{s}]^{s}),\theta^{s^{\prime}}=\theta\theta^{s},\\\
\,[c^{s}]^{s^{\prime}}=tail([c^{s}]^{s}),\;\;\forall\,c^{\prime}\in{\cal
D}_{\bf
C}\setminus\\{c^{s}\\}\;\;[c^{\prime}]^{s^{\prime}}=[c^{\prime}]^{s}\end{array}$

in this case, $P$ takes the value $head([c^{s}]^{s})$ from the channel $c^{s}$
and changes the current binding so that the value of the term $e$ coincides
with the accepted value on a new binding, after which

    * –

the content of the channel $c^{s}$ becomes $tail([c^{s}]^{s})$,

    * –

contents of the other channels have not changed,

  * (c)

if $\alpha=(e:=e^{\prime})$, then
$\left\\{\begin{array}[]{llllllllllllll}\exists\,\theta\in\Theta({\hat{X}_{P}}):{(e^{\theta})^{s}}={(e^{\prime})^{s}},\theta^{s^{\prime}}=\theta\theta^{s},\\\
\forall\,c\in{\cal D}_{\bf C}\;\;[c]^{s^{\prime}}=[c]^{s},\end{array}\right.$
in this case, $P$ changes the current binding so that the value of the term
$e$ on the new binding would be equal to the value of the $e^{\prime}$ term on
the old binding, contents of the channels does not change,

  * (d)

if $\alpha=[\\![\varphi]\\!]$, then $\varphi^{s}=1$,
$\theta^{s^{\prime}}=\theta^{s}$, and $\forall\,c\in{\cal D}_{\bf
C}\;\;[c]^{s^{\prime}}=[c]^{s}$,
in this case, the binding and contents of the channels are not changed.

An empty transition of SP $P$ is a pair $(s,s^{\prime})$ of states from
$\Sigma_{P}$, such that $\theta^{s}=\theta^{s^{\prime}}$. The empty transition
is denoted by $s\to s^{\prime}$.

If a pair $(s,s^{\prime})$ is a transition of a SP, then we say that this is a
transition from $s$ to $s^{\prime}$, $s$ and $s^{\prime}$ is called a start
and an end of this transition, respectively.

Let $P$ be a SP, and $v\in P$, $v\neq P^{0}$. If sets of all edges of $P$
ending in $v$ and starting at $v$ are
$\\{v_{i}\;\mathop{\longrightarrow}\limits^{\alpha_{i}}\;v\mid
i=1,\ldots,n\\}$ and
$\\{v\;\mathop{\longrightarrow}\limits^{\alpha^{\prime}_{i}}\;v^{\prime}_{i}\mid
i=1,\ldots,n^{\prime}\\}$ respectively, where $v$ differs from all the nodes
$v_{i}$ and $v^{\prime}_{i}$, and either all actions
$\alpha_{1},\ldots,\alpha_{n}$ are internal, or all actions
$\alpha^{\prime}_{1},\ldots,\alpha^{\prime}_{n^{\prime}}$ are internal, then a
reduction operation can be applied to $P$, which consists of transforming this
graph by

  * •

removing the node $v$ and associated edges, and

  * •

adding edges of the form
$v_{i}\;\mathop{\longrightarrow}\limits^{\alpha_{i}\alpha^{\prime}_{i^{\prime}}}\;v^{\prime}_{i^{\prime}}$,
where $i=1,\ldots,n,i^{\prime}=1,\ldots,n^{\prime}$, and
$\alpha_{i}\alpha^{\prime}_{i^{\prime}}$ is a concatenation of sequences
$\alpha_{i}$ and $\alpha^{\prime}_{i^{\prime}}$.

A renaming is an injective function $\eta:X\to X^{\prime}$, where
$X,X^{\prime}\subseteq{\cal X}$. For each renaming $\eta:X\to X^{\prime}$,
each $e\in{\cal E}$ and each SP $P$, the notations $e^{\eta}$ and $P^{\eta}$
denote a term or a SP respectively, obtained from $e$ or $P$ by replacing
$\forall\,x\in X$ of each occurrence of $x$ by $\eta(x)$. If $P$ is a SP, and
$\eta$ is a renaming of the form $\eta:\hat{X}_{P}\to{\it{\cal X}}\setminus
X_{P}$, then we will consider SP $P$ and $P^{\eta}$ as equal.

###  4.3 Distributed Processes

In this section we introduce a concept of a distributed process, which can be
used for formal representation of MPI programs.

A distributed process (DP) is a family of SPs ${\cal P}=\\{P_{i}\mid i\in
I\\}$, where components of $\\{\hat{X}_{P_{i}}\mid i\in I\\}$ are disjoint and
do not intersect with $X_{\cal
P}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize def}}}}\bigcup_{i\in
I}X_{P_{i}}$ (if this condition does not met, then we replace each SP $P_{i}$
by an equal to it, in the sense defined at the end of section 4.2, so that
this condition will be met). Below we assume that this condition does met,
even if private variables of SPs $P_{i}$ and $P_{i^{\prime}}$ from ${\cal P}$,
where $i\neq i^{\prime}$, have the same designations.

For each DP ${\cal P}$ ${\cal X}_{\cal P}$ denotes the set of all variables
occurred in ${\cal P}$.

A state of DP ${\cal P}$ is a pair $s=(\theta^{s},\\{c^{s}\mid c\in{\cal
D}_{\bf C}\\})$, where $\theta^{s}\in\Theta({{\cal X}_{\cal P}}),c^{s}\in{\cal
D}^{*}$. A set of all states of a DP ${\cal P}$ is denoted by $\Sigma_{\cal
P}$.

$\forall\,s\in\Sigma_{\cal P}$, $\forall\,e\in{\cal E}({\cal X}_{\cal P})$ the
value $e^{\theta^{s}}$ is denoted by $e^{s}$.

Let ${\cal P}=\\{P_{i}\mid i\in I\\}$ be a DP. $\forall\,s\in\Sigma_{\cal P}$,
$\forall\,i\in I$ $s_{i}\mathbin{{\mathop{=}\limits^{\mbox{\scriptsize
def}}}}(\theta_{i}^{s},\\{c^{s}\mid c\in{\cal D}_{\bf
C}\\})\in\Sigma_{P_{i}}$, where $\theta_{i}^{s}\in\Theta({\cal X}_{P_{i}})$,
$\forall\,x\in{\cal X}_{P_{i}}\;\;x^{\theta_{i}^{s}}=x^{\theta^{s}}$.

A state $s\in\Sigma_{\cal P}$ is said to be initial (and is denoted by
$0_{\cal P}$), if $\forall\,i\in I\;\;s_{i}=0_{P_{i}}$, terminal, if
$\forall\,i\in I\;s_{i}$ is terminal, and deadlock if it is nonterminal, and
$\forall\,i\in I$ there is no non-empty transition of $P_{i}$ from $s_{i}$.

Let ${\cal P}=\\{P_{i}\mid i\in I\\}$ be a DP. A transition in ${\cal P}$
corresponding to an action $\alpha\in{\cal A}_{P_{i}}$ is a pair
$(s,s^{\prime})$ of states from $\Sigma_{{\cal P}}$, such what

$s_{i}\;\mathop{\to}\limits^{\\!\\!\alpha}\;s^{\prime}_{i},\;\forall\,i^{\prime}\in
I\setminus\\{i\\}\;\;{s_{i^{\prime}}}\to{s^{\prime}_{i^{\prime}}}.$ (6)

Property (6) is denoted by $P_{i}^{v\to v^{\prime}}:s\to s^{\prime}$, where
$v=at_{P_{i}}^{s}$, $v^{\prime}=at_{P_{i}}^{s^{\prime}}$. If $(s,s^{\prime})$
is a transition of ${\cal P}$, then we will denote it by $s\to s^{\prime}$.

The relationship between states $s,s^{\prime}\in\Sigma_{{\cal P}}$ satisfying
(6) can be interpreted as follows: if ${\cal P}$ is in the state $s$ at the
current time, and from that moment on, a SP $P_{i}\in{\cal P}$ sequentially
performed EAs from $\alpha$, and $\forall\,i^{\prime}\in I\setminus\\{i\\}$
$P_{i^{\prime}}$ did not perform any actions during all this time, then after
completion the execution of EAs from $\alpha$, the new state of ${\cal P}$ is
$s^{\prime}$.

The set $\Sigma_{{\cal P}}$ can be considered as a graph in which there is an
edge from $s$ to $s^{\prime}$ labeled $\alpha_{P_{i}}$ if and only if (6) is
true.

An execution of a DP ${\cal P}$ is a sequence of states $s_{0},s_{1},\ldots$,
such that $s_{0}=0_{\cal P}$, and each pair $s_{i},s_{i+1}$ of neighboring
states in this sequence is a transition of ${\cal P}$.

A state $s$ of a DP ${\cal P}$ is said to be reachable if there is a path from
$0_{\cal P}$ to $s$. Below $\Sigma_{\cal P}$ denotes the set of reachable
states of ${\cal P}$.

###  4.4 A method for constructing a distributed process which is a model of a
MPI program

We will consider only such MPI programs that contain

  * •

operators of assignment, conditional transition, loop,

  * •

functions of sending and receiving messages, defined in section 2.2, and

  * •

service MPI functions (`MPI_Init`, etc.) mentioned in the program from section
3.2.

Let $\Pi$ be a MPI program, $X_{\Pi}\subseteq{\cal X}$ be a set of input
variables of $\Pi$, and $\varphi_{\Pi}\in{\cal B}$ be an initial condition of
$\Pi$. A model of $\Pi$ is the DP ${\cal P}_{\Pi}=\\{P_{i}\mid i\geq 0\\}$,
where $\forall\,i\geq 0$ SP $P_{i}$ is constructed as follows.

  * •

${\cal X}_{P_{i}}$ consists of variables from $X_{\Pi}$, and $i$-th copies of
private variables of $\Pi$, $X_{P_{i}}=X_{\Pi}$,
$\varphi_{P_{i}}=\varphi_{\Pi}$.

  * •

The graph $P_{i}$ is constructed by

    * –

replacing in $\Pi$ second argument of the function `MPI_Comm_rank` (in the MPI
program presented in section 3.2 this is variable `rank`) by $i$,

    * –

deleting non-executable parts of the resulting program, and

    * –

transformation the resulting program into graph form, similarly to how the
program in operator form is transformed to a flowchart (with the difference
that in flowcharts actions are associated with nodes, and in our model actions
are associated with edges).

Message passing functions are represented in $P_{i}$ by the following actions:

  * •

function (1) is represented by the action $c_{r}!(e,i,l)$, where

    * –

$e$ is a term whose value must be equal to the content of the memory segment
sent by this function,

    * –

$r$ and $l$ are the corresponding arguments of function (1) (receiver number
and tag, respectively),

  * •

function (2) is represented in $P_{i}$ by the action $c_{i}?(e,s,l)$, where

    * –

$e$ is a term whose value after performing this action must be equal to the
received message,

    * –

$s$ and $l$ are new variables,

and if the last argument of function (2) has the name $q$, then the
expressions in $P_{i}$ of the form $q$`.MPI_SOURCE` and $q$`.MPI_TAG` are
replaced with $s$ and $l$, respectively,

  * •

representation of function (3) depends on $i$:

    * –

for $i=0$ the function (3) is represented by the action $\circ!e$, where $e$
is a term whose value must be equal to the content of the memory segment sent
by this function,

    * –

for $i\neq 0$ the function (3) is represented by the action $\circ?e$, where
$e$ is a term whose value after performing this action must be equal to the
received message.

The reduction operation described in section 4.2 can be applied to the
constructed graph $P_{i}$.

To facilitate an analysis of DP ${\cal P}_{\Pi}$, one can add to actions of
this DP assignments of the form $\iota:=e$, where $\iota$ is a new variable
(called an auxiliary variable), and $e\in{\cal E}({\cal X}_{{\cal
P}_{\Pi}}\sqcup{\cal I})$, where ${\cal I}$ is a set of auxiliary variables.
The assignments of the above form $\iota:=e$ are not actually performed
actions, they are intended only to express dependencies between values of
variables during an execution of the DP. SPs from SPs $P_{i}\in{\cal P}_{\Pi}$
by adding assignments of the above form $\iota:=e$, where $\iota$ is an
auxiliary variable, will be called augmented  SPs.

##  5 Modeling and verification of the matrix multiplication MPI program

In this section, we apply the above concepts to modeling and verification of
the matrix multiplication MPI program $\Pi$ described in section 3.

###  5.1 A model of the matrix multiplication MPI program

Define DP ${\cal P}_{\Pi}=\\{P_{i}\mid i\geq 0\\}$, which is a model of $\Pi$.

We assume that the following variables belong to $X_{\Pi}$: $A$, $B$ (matrix
factors), $N$ (number of rows in $A$), `nprocs`.

$\forall\,i\geq 0$, when constructing SP $P_{i}$, the following
simplifications are used:

  * •

the function for input of matrix factors `input (a, b)` in line 15 is executed
once at the initial moment of execution of the root process, therefore in SP
$P_{0}$ it is possible to omit actions corresponding to this function,
assuming that $X_{P_{0}}$ has variables $A$ and $B$, values of which are equal
to matrix factors,

  * •

BMP functions in $P_{0}$ in lines 16-17 and in $P_{i}\;(\forall\,i\geq 1)$ in
lines 44-45 are executed once, at the initial moment of execution of these
SPs, so you can replace the corresponding actions of the form $\circ!e$ and
$\circ?e$ on the assumption that $B$ belongs to $X_{P_{i}}\;(\forall\,i\geq
1)$.

To shorten the notation in SPs below, instead of input variable `nprocs`, we
use input variable $n$, a value of which is equal to $\verb'nprocs'-1$.

To build SP $P_{0}$, only a part of $\Pi$ is used, located in lines 12-39.

In SP $P_{0}$ $A$ and $C$ are names of arrays, components of which are rows of
corresponding matrices and are indexed by numbers $1,\ldots,N$,
$\forall\,i=1,\ldots,N$ $A_{i}$ and $C_{i}$ denote $i$-th components of these
arrays.

$P_{0}$ has the following variables:
$\begin{array}[]{llllllllllllll}X_{P_{0}}=\\{A,B,N,n\\},\;\hat{X}_{P_{0}}=\\{C,i,j,k,l,p\\}.\end{array}$

Initial condition: $\begin{array}[]{llllllllllllll}\varphi_{P_{0}}=&(N\geq
1)\wedge(i=1)\wedge(k=0)\wedge(l=1).\end{array}$

SP $P_{0}$ has the form

$\begin{array}[]{llllllllllllll}\begin{picture}(150.0,160.0)\par\put(0.0,0.0){\oval(20.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{2}} \put(0.0,100.0){\oval(20.0,20.0)}
\put(0.0,100.0){\makebox(0.0,0.0)[c]{1}} \put(0.0,150.0){\oval(20.0,20.0)}
\put(0.0,150.0){\makebox(0.0,0.0)[c]{0}} \put(100.0,100.0){\oval(20.0,20.0)}
\put(100.0,100.0){\makebox(0.0,0.0)[c]{3}} \put(200.0,100.0){\oval(20.0,20.0)}
\put(200.0,100.0){\makebox(0.0,0.0)[c]{4}}
\par\par\put(0.0,140.0){\vector(0,-1){30.0}}
\put(-3.0,90.0){\vector(0,-1){80.0}} \put(3.0,10.0){\vector(0,1){80.0}}
\put(10.0,100.0){\vector(1,0){80.0}} \put(110.0,100.0){\vector(1,0){80.0}}
\par\par\put(10.0,153.0){\line(1,0){20.0}}
\put(30.0,147.0){\vector(-1,0){20.0}} \put(30.0,150.0){\oval(6.0,6.0)[r]}
\par\put(97.0,90.0){\line(0,-1){20.0}} \put(103.0,70.0){\vector(0,1){20.0}}
\put(100.0,70.0){\oval(6.0,6.0)[b]}
\par\par\put(150.0,102.0){\makebox(0.0,0.0)[b]{ $[\\![\,l>n]\\!]$ }}
\par\par\put(0.0,125.0){\makebox(0.0,0.0)[r]{ $[\\![\,i>\min(n,N)]\\!]$ }}
\par\par\put(50.0,100.0){\makebox(0.0,0.0)[b]{
$\begin{array}[]{lllll}[\\![k\geq N]\\!]\end{array}$ }}
\par\par\put(30.0,145.0){\makebox(0.0,0.0)[l]{
$\left\\{\begin{array}[]{lllll}[\\![\,i\leq\min(n,N)]\\!]\\\
c_{i}!(A_{i},0,i)\\\ i:=i+1\end{array}\right.$ }}
\par\put(100.0,72.0){\makebox(0.0,0.0)[l]{
$\left\\{\begin{array}[]{lllll}[\\![\,l\leq n]\\!]\\\ c_{l}!(*,0,0)\\\
l:=l+1\end{array}\right.$ }} \par\put(5.0,50.0){\makebox(0.0,0.0)[r]{
$\left\\{\begin{array}[]{lllll}[\\![\,k<N]\\!]\\\ c_{0}?(C_{j},p,j)\\\
k:=k+1\end{array}\right.$ }} \par\par\put(0.0,50.0){\makebox(0.0,0.0)[l]{
$[\\![\,i>N]\\!]$ }} \par\put(10.0,0.0){\line(1,0){40.0}}
\put(60.0,10.0){\line(0,1){75.0}} \put(50.0,95.0){\vector(-1,0){41.0}}
\put(50.0,10.0){\oval(20.0,20.0)[br]} \put(50.0,85.0){\oval(20.0,20.0)[tr]}
\par\put(55.0,18.0){\makebox(0.0,0.0)[l]{
$\left\\{\begin{array}[]{lllll}[\\![\,i\leq N]\\!]\\\ c_{p}!(A_{i},0,i)\\\
i:=i+1\end{array}\right.$ }} \par\par\end{picture}\end{array}$ (7)

In SP (7)

  * •

edge $P_{0}^{0\to 0}$ corresponds to the loop in lines 18-22 of $\Pi$, the
variable $i$ in the label of this edge corresponds to the expression
$\verb'count'+1$ in $\Pi$,

  * •

the message sent by the `MPI_Send `function in lines 21-22 of $\Pi$, is
represented by the triple $(A_{i},0,i)$, third component of which is a tag of
this message (i.e. a number of the corresponding row in the matrix $A$),

  * •

edge $P_{0}^{0\to 1}$ corresponds to the exit from this cycle,

  * •

edges $P_{0}^{1\to 2}$ and $P_{0}^{2\to 1}$ correspond to a loop in lines
23-34 of $\Pi$,

  * •

variable $k$ corresponds to variable `i` in this loop,

  * •

the function `MPI_Recv `in lines 24-26 and the loop in lines 27-28 of $\Pi$
are replaced with a single action: receiving a message and writing it to the
corresponding row of matrix $C$,

  * •

edge $P_{0}^{1\to 3}$ corresponds to the exit from this loop,

  * •

edges $P_{0}^{3\to 3}$ and $P_{0}^{3\to 4}$ correspond to the cycle in lines
35-37,

  * •

symbol $*$ in the label of edge $P_{0}^{3\to 3}$ represents the empty string.

To construct SP $P_{i}\;(i\geq 1)$, only the part of $\Pi$ located in lines
42-55 is used. $P_{i}$ has the following variables:
$X_{P_{i}}=\\{B\\},\hat{X}_{P_{i}}=\\{Y_{i},j_{i}\\}$, where a value of $B$ is
the second factor matrix, and values of $Y_{i}$ are strings of real numbers.
$P_{i}$ has the following form:

$\begin{array}[]{llllllllllllll}\begin{picture}(50.0,20.0)\par\put(-100.0,0.0){\oval(20.0,20.0)}
\put(-100.0,0.0){\makebox(0.0,0.0)[c]{0}} \put(0.0,0.0){\oval(20.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{1}} \put(100.0,0.0){\oval(20.0,20.0)}
\put(100.0,0.0){\makebox(0.0,0.0)[c]{2}}
\par\par\put(-90.0,3.0){\vector(1,0){80.0}}
\put(-10.0,-3.0){\vector(-1,0){80.0}} \put(10.0,0.0){\vector(1,0){80.0}}
\par\put(-50.0,5.0){\makebox(0.0,0.0)[b]{
$\begin{array}[]{llllllllllllll}c_{i}?(Y_{i},0,j_{i})\end{array}$ }}
\put(50.0,5.0){\makebox(0.0,0.0)[b]{ $[\\![\,j_{i}=0]\\!]$ }}
\par\put(-40.0,-5.0){\makebox(0.0,0.0)[t]{
$\left\\{\begin{array}[]{llll}[\\![\,j_{i}\neq 0]\\!]\\\
c_{0}!(Y_{i}B,i,j_{i})\\\ \end{array}\right.$ }}
\par\end{picture}\end{array}\vspace{5mm}$ (8)

###  5.2 Verification of a distributed process that is a model of the matrix
multiplication MPI program

To prove the statement that DP ${{\cal P}_{\Pi}}$ defined in section 5.1,
satisfies specification (4), we introduce auxiliary variables $\alpha$,
$\beta$, $\gamma$, and actions related to these variables that do not affect
an execution of the DP. Values of the auxiliary variables have the following
meaning: their initial values are $\emptyset$, and $\forall\,s\in\Sigma_{{\cal
P}_{\Pi}}$

  * •

$\alpha^{s}\subseteq\\{1,\ldots,n\\}$, $\alpha^{s}$ consists of channel
numbers from $\\{c_{1},\ldots,c_{n}\\}$ with non-empty content in state $s$,

  * •

$\beta^{s}\subseteq\\{1,\ldots,N\\}$, $\beta^{s}$ consists of numbers of rows
of $A$, for which their product by $B$ is calculated in state $s$,

  * •

$\gamma^{s}\subseteq\\{1,\ldots,N\\}$, $\gamma^{s}$ is the set of numbers of
rows that $P_{0}$ wrote in $C$ during an execution of ${{\cal P}_{\Pi}}$ up to
state $s$.

Augmented SP $P_{0}$ has the form

$\begin{array}[]{llllllllllllll}\begin{picture}(150.0,155.0)\par\put(0.0,0.0){\oval(20.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{2}} \put(0.0,100.0){\oval(20.0,20.0)}
\put(0.0,100.0){\makebox(0.0,0.0)[c]{1}} \put(0.0,150.0){\oval(20.0,20.0)}
\put(0.0,150.0){\makebox(0.0,0.0)[c]{0}} \put(100.0,100.0){\oval(20.0,20.0)}
\put(100.0,100.0){\makebox(0.0,0.0)[c]{3}} \put(200.0,100.0){\oval(20.0,20.0)}
\put(200.0,100.0){\makebox(0.0,0.0)[c]{4}}
\par\par\put(0.0,140.0){\vector(0,-1){30.0}}
\put(-3.0,90.0){\vector(0,-1){80.0}} \put(3.0,10.0){\vector(0,1){80.0}}
\put(10.0,100.0){\vector(1,0){80.0}} \put(110.0,100.0){\vector(1,0){80.0}}
\par\par\put(10.0,153.0){\line(1,0){20.0}}
\put(30.0,147.0){\vector(-1,0){20.0}} \put(30.0,150.0){\oval(6.0,6.0)[r]}
\par\put(97.0,90.0){\line(0,-1){20.0}} \put(103.0,70.0){\vector(0,1){20.0}}
\put(100.0,70.0){\oval(6.0,6.0)[b]}
\par\par\put(150.0,102.0){\makebox(0.0,0.0)[b]{ $[\\![\,l>n]\\!]$ }}
\par\par\put(0.0,125.0){\makebox(0.0,0.0)[r]{ $[\\![\,i>\min(n,N)]\\!]$ }}
\par\par\put(50.0,100.0){\makebox(0.0,0.0)[b]{
$\begin{array}[]{lllll}[\\![k\geq N]\\!]\end{array}$ }}
\par\par\put(30.0,140.0){\makebox(0.0,0.0)[l]{
$\left\\{\begin{array}[]{lllll}[\\![\,i\leq\min(n,N)]\\!]\\\
c_{i}!(A_{i},0,i)\\\ \alpha:=\alpha\sqcup\\{i\\},i:=i+1\end{array}\right.$ }}
\par\put(100.0,72.0){\makebox(0.0,0.0)[l]{
$\left\\{\begin{array}[]{lllll}[\\![\,l\leq n]\\!]\\\ c_{l}!(*,0,0)\\\
l:=l+1\end{array}\right.$ }} \par\put(5.0,50.0){\makebox(0.0,0.0)[r]{
$\left\\{\begin{array}[]{lllll}[\\![\,k<N]\\!]\\\ c_{0}?(C_{j},p,j)\\\
\gamma:=\gamma\sqcup\\{j\\}\\\ k:=k+1\end{array}\right.$ }}
\par\par\put(0.0,50.0){\makebox(0.0,0.0)[l]{ $[\\![\,i>N]\\!]$ }}
\par\put(10.0,0.0){\line(1,0){40.0}} \put(60.0,10.0){\line(0,1){75.0}}
\put(50.0,95.0){\vector(-1,0){41.0}} \put(50.0,10.0){\oval(20.0,20.0)[br]}
\put(50.0,85.0){\oval(20.0,20.0)[tr]}
\par\put(58.0,18.0){\makebox(0.0,0.0)[l]{
$\left\\{\begin{array}[]{lllll}[\\![\,i\leq N]\\!]\\\ c_{p}!(A_{i},0,i)\\\
\alpha:=\alpha\sqcup\\{p\\},i:=i+1\end{array}\right.$ }}
\par\par\end{picture}\end{array}\vspace{2mm}$ (9)

$\forall\,i=1,\ldots,n$ augmented SP $P_{i}$ has the form

$\begin{array}[]{llllllllllllll}\begin{picture}(50.0,35.0)\par\put(-100.0,0.0){\oval(20.0,20.0)}
\put(-100.0,0.0){\makebox(0.0,0.0)[c]{0}} \put(0.0,0.0){\oval(20.0,20.0)}
\put(0.0,0.0){\makebox(0.0,0.0)[c]{1}} \put(100.0,0.0){\oval(20.0,20.0)}
\put(100.0,0.0){\makebox(0.0,0.0)[c]{2}}
\par\par\put(-90.0,3.0){\vector(1,0){80.0}}
\put(-10.0,-3.0){\vector(-1,0){80.0}} \put(10.0,0.0){\vector(1,0){80.0}}
\par\put(-50.0,5.0){\makebox(0.0,0.0)[b]{
$\left\\{\begin{array}[]{llllllllllllll}c_{i}?(Y_{i},0,j_{i})\\\
\beta:=\beta\sqcup\\{j_{i}\\}\\\
\alpha:=\alpha\setminus\\{i\\}\end{array}\right.$ }}
\put(50.0,5.0){\makebox(0.0,0.0)[b]{ $[\\![\,j_{i}=0]\\!]$ }}
\par\put(-40.0,-5.0){\makebox(0.0,0.0)[t]{
$\left\\{\begin{array}[]{llll}[\\![\,j_{i}\neq 0]\\!]\\\
c_{0}!(Y_{i}B,i,j_{i})\\\ \beta:=\beta\setminus\\{j_{i}\\}\end{array}\right.$
}} \par\end{picture}\end{array}$ (10)

The use of $\sqcup$ in (9) and (10) for set union operations expresses the
statement (following from the following theorem 5.2) that whenever these
operations are performed, their arguments are actually disjoint sets.

Theorem 1.

$\forall\,s\in\Sigma_{{\cal P}_{\Pi}}$, if $at^{s}_{P_{0}}\neq 3,4$, then the
following statements are true:

  1. 1.

$\alpha^{s}\subseteq\\{1,\ldots,i^{s}-1\\}$,

  2. 2.

$i^{s}-1\leq N$

  3. 3.

$|\gamma^{s}|=k^{s}\leq N$,

  4. 4.

if $at_{P_{0}}^{s}=1$ and $k^{s}<N$, then $k^{s}<i^{s}-1$,

  5. 5.

$[c_{0}]^{s}_{2}\cap\alpha^{s}=\emptyset$,

  6. 6.

$\forall\,i=1,\ldots,n$

    1. (a)

$|[c_{i}]^{s}|=1$, if $i\in\alpha^{s}$, and $|[c_{i}]^{s}|=0$, otherwise,

    2. (b)

$at_{P_{i}}^{s}=1\;\Rightarrow\;(i\not\in\alpha^{s})\wedge(j^{s}_{i}\not\in\gamma^{s})$

  7. 7.

$at_{P_{0}}^{s}=2\;\Rightarrow\;p^{s}\not\in\alpha^{s}$,
$p^{s}\in\\{1,\ldots,i^{s}-1\\}$,

  8. 8.

$[c_{1}]_{3}^{s}\sqcup\ldots\sqcup[c_{n}]_{3}^{s}\sqcup\beta^{s}\sqcup[c_{0}]_{3}^{s}\sqcup\gamma^{s}=\\{1,\ldots,i^{s}-1\\}$,

  9. 9.

$\forall\,p\in\alpha^{s}\;\;[c_{p}]^{s}$ has the form $\\{(A_{i},0,i)\\}$,
where $i\in\\{1,\ldots,N\\}$,

  10. 10.

each element of $[c_{0}]^{s}$ has the form $(A_{i}B,p,i)$, where
$i\in\\{1,\ldots,N\\}$,

  11. 11.

$\forall\,j\in\gamma^{s}\;\;C_{j}=A_{j}B$,

  12. 12.

$k^{s}=N\;\Rightarrow\;\gamma^{s}=\\{1,\ldots,N\\}$.

Proof.

All the statements are substantiated inductively: they are true in $0_{{\cal
P}_{\Pi}}$, and retain their truth after each transition $s\to s^{\prime}$ of
${{\cal P}_{\Pi}}$, where $at_{P_{0}}^{s^{\prime}}\neq 3,4$.

Theorem 2.

There are no deadlocks in $\Sigma_{{\cal P}_{\Pi}}$.

Proof.

Let there is a deadlock $s\in\Sigma_{{\cal P}_{\Pi}}$. It is not hard to prove
that $at_{P_{0}}^{s}\not\in\\{0,2,3\\}$, and $\forall\,i=1,\ldots,n$
$at_{P_{i}}^{s}\neq 1$. So, $at_{P_{0}}^{s}\in\\{1,4\\}$.

  1. 1.

Let $at_{P_{0}}^{s}=1$. Since $s$ is a deadlock, then $k^{s}<N$, whence
$[c_{0}]^{s}=\emptyset$.

From statement 4 of theorem 5.2 it follows that $k^{s}<i^{s}-1$, whence, based
on statement 8 of theorem 5.2 and the equality $[c_{0}]^{s}=\emptyset$ we get:

$[c_{1}]_{3}^{s}\sqcup\ldots\sqcup[c_{n}]_{3}^{s}\sqcup\beta^{s}\neq\emptyset.$
(11)

If $\exists\,i\in\\{1,\ldots,n\\}$: $[c_{i}]^{s}\neq\emptyset$, then the
assumption that $s$ is a deadlock implies that $at_{P_{i}}^{s}\neq 0$,
therefore $at_{P_{i}}^{s}=2$, whence it is easy to get that
$at_{P_{0}}^{s}=4$. This is possible only if $k^{s}\geq N$, which contradicts
the inequality $k^{s}<N$.

Therefore, $\forall\,i\in\\{1,\ldots,n\\}\;[c_{i}]^{s}=\emptyset$, and from
(11) it follows that $\beta\neq\emptyset$. By analyzing SP
$P_{i}\;(i=0,\ldots,n)$ it is easy to prove that this is possible only if
$\exists\,i\in\\{1,\ldots,n\\}$: $at_{P_{i}}^{s}=2$. As stated above, this is
impossible.

  2. 2.

Let $at_{P_{0}}^{s}=4$. Then $k^{s}\geq N$, whence $|\gamma^{s}|=k^{s}=N$. Let
$s^{\prime}$ be first state on a path $\pi$ from $0_{{\cal P}_{\Pi}}$ to $s$,
such that $k^{s^{\prime}}=N$. It is easy to see that
$at_{P_{0}}^{s^{\prime}}=2$. From statements 2 and 8 of theorem 5.2 it follows
that $i^{s^{\prime}}-1=N$, and

$[c_{0}]^{s^{\prime}}=[c_{1}]^{s^{\prime}}=\ldots=[c_{n}]^{s^{\prime}}=\beta^{s^{\prime}}=\emptyset,\;\;at_{P_{1}}^{s^{\prime}}=0,\ldots,at_{P_{n}}^{s^{\prime}}=0.$

The only transition from $s^{\prime}$ corresponds to the action
$[\\![i>N]\\!]$, and this transition has the form $P_{0}^{2\to
1}:s^{\prime}\to s^{\prime\prime}$. The only transition from
$s^{\prime\prime}$ corresponds to the action $[\\![k\geq N]\\!]$ and this
transition has the form $P_{0}^{1\to 3}:s^{\prime\prime}\to
s^{\prime\prime\prime}$. It is easy to see that all states in the tail of
$\pi$ starting from $s^{\prime\prime\prime}$ are not deadlocks.

In both cases, we get a contradiction, which is a consequence of the
assumption that $\Sigma_{{\cal P}_{\Pi}}$ has a deadlock state. Thus, there
are no deadlock states in $\Sigma_{{\cal P}_{\Pi}}$.

Theorem 3.

Any execution of ${\cal P}_{\Pi}$ terminates after a finite sequence of steps.

Proof.

Let there is an infinite execution $\pi$ of ${\cal P}_{\Pi}$. Prove that a
number of transitions in $\pi$ corresponding to actions of $P_{0}$ is finite.
If this is not so, then

  * •

there are no states $s\in\pi$ such that $at_{P_{0}}^{s}=3$,

  * •

there is a state $s_{1}\in\pi$, such that $at_{P_{0}}^{s_{1}}=1$,

  * •

each transition in $\pi$, starting from $s_{1}$, corresponding to some action
$P_{0}$, either has the form $P_{0}^{1\to 2}:s\to s^{\prime}$, or has the form
$P_{0}^{2\to 1}:s\to s^{\prime}$, and the number of transitions of the form
$P_{0}^{1\to 2}:s\to s^{\prime}$ is infinite. This is impossible due to the
fact that each such transition increases the value of the variable $k$, which,
according to statement 3 of theorem 5.2, is bounded by $N$.

Let $s^{\prime}\in\pi$ be a state starting from which $\pi$ does not contain
transitions corresponding to actions of $P_{0}$, and $\pi^{\prime}$ is a tail
of $\pi$, starting with $s^{\prime}$. It is not hard to see that

$\begin{array}[]{llllllllllllll}\mbox{$\exists\,i\in\\{1,\ldots,n\\}$:
$\pi^{\prime}$ contains infinitely many}\\\ \mbox{transitions of the form
$P_{i}^{0\to 1}:s\to s^{\prime}$.}\end{array}$ (12)

Because $\pi^{\prime}$ does not contain transitions corresponding to actions
of $P_{0}$, then the value of $|[c_{i}]^{s}|$ cannot increase, and according
to (12) it decreases infinitely, which is impossible.

It follows from the above theorems that each execution of DP ${\cal P}_{\Pi}$
is finite and terminates in some terminal state $s$. From $at_{P_{0}}^{s}=4$
it follows that $|\gamma^{s}|=k^{s}=N$, whence, according to statements 11 and
12 of theorem 5.2, it follows that DP ${\cal P}_{\Pi}$ satisfies the
specification stated in section3.4.

##  6 Conclusion

In this article, we introduced a new mathematical model of parallel programs,
proposed an approach for verifying such programs, and considered an example of
verifying a matrix multiplication program based on the proposed model. The
main advantage of this approach is the possibility of its application for
programs that generate a unlimited set of SPs.

Problems for further research related to the proposed model can be the
following: 1). to expand the proposed model by introducing concepts for
modeling synchronous message passing, and other mechanisms for organizing
parallel execution, 2). to introduce specification language of properties of
DPs, in which properties of parallel programs are expressed in terms of
observational equivalence, and to elaborate algorithms for recognizing
observational equivalence.

## References

  * [1] Hugo A. Lopez, E. R. B. Marques, F. Martins, N. Ng, C. Santos, V.T. Vasconcelos, N. Yoshida, Protocol-based verification of message-passing parallel programs, Proceedings of the 2015 ACM SIGPLAN International Conference on Object-Oriented Programming, Systems, Languages, and Applications - OOPSLA 2015, p. 280-298.
  * [2] S. F. Siegel and G. Gopalakrishnan. Formal Analysis of Message Passing. In R. Jhala and D. Schmidt, editors, Verification, Model Checking, and Abstract Interpretation: 12th International Conference, VMCAI 2011, volume 6538 of Lecture Notes in Computer Science, pages 2-18, (2011).
  * [3] S. F. Siegel, Model Checking Nonblocking MPI Programs. In International Workshop on Verification, Model Checking, and Abstract Interpretation VMCAI 2007, pp 44-58.
  * [4] Siegel, S., Mironova, A., Avrunin, G., Clarke, L.: Combining symbolic execution with model checking to verify parallel numerical programs. ACM Transactions on Software Engineering and Methodology, Volume 17, Issue 2, 2008, 134.
  * [5] Sarvani S. Vakkalanka, Ganesh Gopalakrishnan, and Robert M. Kirby. Dynamic Verification of MPI Programs with Reductions in Presence of Split Operations and Relaxed Orderings. In International Conference on Computer Aided Verification CAV 2008, pp 66-79.
  * [6] Gopalakrishnan, G., Kirby, R.M., Siegel, S., Thakur, R., Gropp, W., Lusk, E., De Supinski, B.R., Schulz, M., Bronevetsky, G.: Formal analysis of MPI-based parallel programs. Communications ACM 54(12), 82-91, (2011).
  * [7] V. Forejt, S. Joshi, D. Kroening, G. Narayanaswamy, S. Sharma, Precise Predictive Analysis for Discovering Communication Deadlocks in MPI Programs, In: ACM Transactions on Programming Languages and Systems, V. 39, Issue 4, 2017, 127.
  * [8] Z. Luo, M. Zheng, and S. F. Siegel. Verification of MPI programs using CIVL. In EuroMPI. 6:1-6:11, 2017.
  * [9] W. Hong, Z. Chen, H. Yu, and J. Wang. Evaluation of model checkers by verifying message passing programs. Science China Information Sciences, volume 62, Article number: 200101 (2019).
  * [10] H. Yu, Z. Chen, X. Fu, J. Wang, Z. Su, J. Sun, C. Huang, and W. Dong. Symbolic Verification of Message Passing Interface Programs. In ICSE ’20: Proceedings of the ACM/IEEE 42nd International Conference on Software Engineering, p. 1248-1260, 2020.


Further author information: (Send correspondence to J.W.)
J.W.: E-mail<EMAIL_ADDRESS>
# Liger for Next-Generation Keck Adaptive Optics: Opto-Mechanical Dewar for
Imaging Camera and Slicer

James Wiley  Department of Physics, University of California San Diego, USA
Center for Astrophysics and Space Sciences, University of California San
Diego, USA  Kalp Mathur  Department of Physics, University of California San
Diego, USA  Center for Astrophysics and Space Sciences, University of
California San Diego, USA  Aaron Brown  Center for Astrophysics and Space
Sciences, University of California San Diego, USA  Shelley A. Wright
Department of Physics, University of California San Diego, USA  Center for
Astrophysics and Space Sciences, University of California San Diego, USA
Maren Cosens  Department of Physics, University of California San Diego, USA
Center for Astrophysics and Space Sciences, University of California San
Diego, USA  Jerome Maire  Center for Astrophysics and Space Sciences,
University of California San Diego, USA  Michael Fitzgerald  Department of
Physics & Astronomy, University of California Los Angeles, USA  Tucker Jones
Department of Physics, University of California Davis, USA  Marc Kassis  W.M.
Keck Observatory, Waimea, HI  Evan Kress  Department of Physics & Astronomy,
University of California Los Angeles, USA  Renate Kupke  Department of
Astronomy & Astrophysics, University of California Santa Cruz, USA  James E.
Larkin  Department of Physics & Astronomy, University of California Los
Angeles, USA  Jim Lyke  W.M. Keck Observatory, Waimea, HI  Eric Wang
Department of Physics & Astronomy, University of California Los Angeles, USA
Sherry Yeh  W.M. Keck Observatory, Waimea, HI

###### Abstract

Liger is a next generation adaptive optics (AO) fed integral field
spectrograph (IFS) and imager for the W. M. Keck Observatory. This new
instrument is being designed to take advantage of the upgraded AO system
provided by Keck All-Sky Precision Adaptive-optics (KAPA). Liger will provide
higher spectral resolving power (R$\sim$4,000-10,000), wider wavelength
coverage ($\sim$0.8-2.4 $\mu$m), and larger fields of view than any current
IFS. We present the design and analysis for a custom-made dewar chamber for
characterizing the Liger opto-mechanical system. This dewar chamber is
designed to test and assemble the Liger imaging camera and slicer IFS
components while being adaptable for future experiments. The vacuum chamber
will operate below $10^{-5}$ Torr with a cold shield that will be kept below
90 K. The dewar test chamber will be mounted to an optical vibration isolation
platform and further isolated from the cryogenic and vacuum systems with
bellows. The cold head and vacuums will be mounted to a custom cart that will
also house the electronics and computer that interface with the experiment.
This test chamber will provide an efficient means of calibrating and
characterizing the Liger instrument and performing future experiments.

###### keywords:

Integral Field Spectrograph, Vacuum, Dewar, Calibration, Characterization,
Infrared, Cryogenic, Adaptive Optics

##  1 INTRODUCTION

---
Figure 1:  A rendering of the Liger test chamber experimental setup. The test
chamber rests on a 4’$\times$6’ optical table with active pneumatic vibration
isolation supports. The cold head that rises beneath the chamber and the
vacuum connected to the side are housed on a cart made from 8020 components.
The cold head and vacuums are vibrationally isolated from the chamber with
bellows, and the cart is maneuverable and capable of mounting to the system
from multiple different positions.

Liger is a near-infrared ($\sim$0.8-2.4 $\mu$m) adaptive optics-fed imager and
integral field spectrograph for the Keck I observatory [1]. This paper
describes the design and analysis of the two cryogenic test chambers that will
characterize the imager (at UCSD) and slicer (at UCSC) components of the Liger
system. The Liger test chamber is a vibration isolated, cryogenically cooled,
vacuum chamber for testing infrared optics and electronics (Fig. 1).

The vacuum chamber is constructed from AISI 304 steel with a 6061 T6 aluminum
lid and rests on a 4’x6’ optical table with pneumatic isolators. There is a
flange on the bottom of the chamber and a through hole in the table to
accommodate the cold head that extends into the chamber. The centered NW-160
port on one side of the chamber or an off-center NW-160 port on the sides are
aligned with the cold head flange and can be used for the vacuum interface.
Both the cryogenic and vacuum systems are connected with bellows to reduce
induced vibrations into the chamber. A NW-100 Flange with a custom built
calcium fluoride window is used as the entrance for the light beam.

A 6061 T6 aluminum cold shield is connected to the base of the chamber with
G-10 A-frames. Openings are cut in the cold shield for the optical beam
entrance and the cold head, which extends into the cold shield and is
thermally connected by copper strands. The 3 sides of the cold shield not
facing the entrance beam have a 15cmx15cm slide-in feed through plate. There
is an adjustable plate between the base of the cold shield and the optical
platform to avoid induced flexure from thermal expansion and allow the system
to be easily installed and aligned in the final dewar.

A cart made from 8020 holds the rough pump, turbo pump, cold head, compressor,
and electronics that service the chamber. The cold head is mounted on a
cantilever arm that extends from the cart. It is connected to a two
dimensional railing system to simplify positioning under the chamber. A 10”
long bellows connects the cold head to the cold head flange. The vacuums are
mounted on top of the cart close to the chamber so as to reduce the length of
the vacuum line. The compressor and electronics rack are held inside the cart.

The design of the experimental setup is based on previous characterization
chambers [2] [3]. It will be used as a long term system for experiments after
the characterization of the Liger imager and slicer. The experimental setup
provides an accurate and precise way of characterizing infrared optics and
electronics while being efficient and adaptable for future experiments.

##  2 Vacuum Chamber

Figure 2:  Solid model and exploded view of the vacuum chamber showing the
lid, entrance window, and cold shield that will be housed inside the chamber.

The vacuum chamber rests on an 8” thick optical table and houses the cold
shield and optics of the experimental setup (Fig. 2). It operates below a
pressure of $\rm 10^{-5}$ Torr. The body of the vacuum chamber is made of AISI
304 steel for its strength, low porosity, and favorable vacuum properties. The
lid for the chamber is made of 6061 T6 aluminum to decrease weight and has a
cross of I-beams welded on for increased stiffness.

The vacuum chamber inner dimensions are 1100mm$\times$1100mm$\times$623mm. The
total weight of the empty vacuum chamber is 1660 pounds while the weight of
the lid alone is 250 pounds. There are three NW-100 flanges, four NW-160
flanges, and one cold head flange. Corner lips with mounting holes are located
in the lid and top flange of the chamber for installing hoist rings. The rings
thread into the lid and can be bolted onto the chamber with a nut for
maneuvering just the lid or the entire chamber. There are 1/4”-20 blind holes
around the base of the chamber for fastening to a bracket mounted onto the
optical table. This provides slight support against earthquakes and other such
events.

The base of the chamber is 1” thick steel to withstand the force on it from
the vacuum. The walls of the chamber are 5/8” thick and welded onto the base.
The top flange is 1” wide and thick, and is welded on top of the chamber
walls. The lid contains a dovetail O-ring groove and screws into the top
flange to form the vacuum seal. The lid of the chamber is 1” thick 6061 T6
aluminum. This material was chosen for its good vacuum properties, and it is
lighter than steel making the lid easier to handle. A cross made of I beams is
welded to the top of the lid which offers additional support against
deflection.

A bolt hole pattern around the base of the inside of the chamber is for
installing A-frames that connect to the cold shield. A second set of bolt
holes are centered on the base for installation of extra components and future
experiments.

###  2.1 Vacuum Analysis

Figure 3:  Static simulation of the vacuum chamber under gravity and pressure.
The maximum stress (Left) is located at the top and bottom of the sides and
the center of the edge of the lid and base. The maximum stress is about a
factor of 3 less than yield for both AISI 304 and 6061 T6. The maximum
deflection (Right) is less than a millimeter around the entire chamber.

The vacuum chamber was designed so the maximum deflection in the system would
be less than 1mm and the maximum stress would be less than a factor of 2 below
yield. The wall thicknesses (1” base, 5/8” sides) were chosen to meet this
requirement.

At high vacuum and located at sea level (1 atmosphere of pressure), the force
on the lid and base of the chamber is 27,500 lbs and on the sides is 16,000
lbs. Figure 3 shows the stress and deflection due to this applied force as
simulated in SolidWorks . The maximum stress (74.8 MPa) is located along the
top and bottom edges of the inside of the chamber and is about a factor of 3
less than yield (yield strength us 207 MPa for AISI 304 and 275 MPa for 6061
T6). The maximum deflection is located at the center of the lid and base of
the chamber and is only 0.8mm

A large rough and turbo pump and the NW-160 size port were chosen for their
longevity, as the larger the pump, the faster the pump down speed, and the
less strain on the vacuum over time. The ultimate pressure of the chamber will
be below $\rm 10^{-5}$ Torr with a projected pump down time of about an hour
from atmosphere.

###  2.2 Vibration Isolation

The location of one of the vacuum systems will be in a laboratory building at
UC San Diego. This building has large vibrations due to the HV/AC system,
engineering labs performing vibration tests, and high foot and road traffic.
To decrease vibration in the experiment, the vacuum chamber will be mounted to
an 8” optical table on active pneumatic isolators.

The optical table will provide high compliance between the light source and
vacuum chamber, while the pneumatic isolators will provide vibration
suppression. Based on measurements taken in the lab with an accelerometer
comparing the vibrations between an active pneumatic isolated table and a
regular table, the vibrations were suppressed by over an order of magnitude in
terms of RMS displacement and peak to valley distance.

The vacuum pumps and cold head are additional sources of vibration and will be
isolated from the chamber with bellows. The cold head will extend into the
chamber and be attached with copper strands with no hard contacts to avoid
transmitting vibrations. Each vacuum and the cold head will be mounted on
vibration isolation pads to further reduced induced vibrations.

##  3 Cold Shield

The cold shield is made of 6061 T6 aluminum and is similar to the vacuum
chamber in design (Fig. 4). The base is a thick 1” for rigidity and has
through holes for mounting the adapter plate. The walls and lid are non
structural and are 4mm thick, yet weigh 90 lbs welded together and therefore
require lifting points. The walls lower into a groove in the base of the cold
shield and are fastened with screws to improve thermal conduction.

There is an opening in one side concentric with the light source window on the
chamber for the optical path, and another in the base concentric with the
chamber cold head flange. There are 3 feed through plates that are
15cm$\times$15cm in size. These are cut into the side of the cold shield, and
a channel part is welded on for the feed through plate to slide into.

The cold shield base has blind mounting holes on the outside for connecting to
guides. These guides attach to the A-frames at a higher point to allow the
cold shield to sit low in the chamber while extending the length of the
A-frame. This additional length helps to reduce the power conducted into the
chamber as well as the stress induced from thermal contraction of the cold
shield on the A-frame.

Figure 4:  Solid model and exploded view of the cold shield showing the
optical plate, imaging optics, A-frames, and feed through plates. The adapter
plate, optical mounts, filter wheel, and pupil[4] are not included.

###  3.1 Thermal Analysis

To reduce the heat power conducted into the cold shield, long and thin G-10
A-frames are used. G-10 has a low thermal conductivity of k=0.288 $\rm
W\,m^{-1}\,K^{-1}$ [5]. The A-frames are bolted to guides connected to the
cold shield and blocks connected to the base of the chamber. The equation for
power conducted into the cold shield is:

$P=\frac{kA(T_{h}-T_{c})}{d}$

Where $A$ is the cross-sectional area of the A-frame, $d$ is the length heat
is conducted through the A-frame, $T_{h}$ is the temperature of the vacuum
chamber, and $T_{c}$ is the temperature of the cold shield.

For a quick estimate, we can model the thermal conduction through each leg of
the A-frame as if it were a single beam and multiply by 8 to get the total
power conducted into the cold shield. The cross-sectional area of one leg is
$\rm A=3.75\times 10^{-4}$ m2. The minimum distance from the top bolt to the
bottom is $\rm d=0.261$ m. With $T_{h}=293$ K and $T_{c}=55$ K, this gives us
a power conducted through one leg of an A-frame as $P\approx 0.1$ W and a
total power conducted into the cold shield as $P_{c}\approx 1$ W.

To reduce power radiated into the cold shield, the AISI 304 steel will be
electropolished to reduce the emissivity and coated with layers of aluminzed
mylar. To reduce the power absorbed by the cold shield, it will

Figure 5:  Thermal simulation run in SolidWorks with a 60W heat load
corresponding to a cold head temperature of 55 K. The maximum temperature in
the cold shield is 90 K located on the lid furthest from the cold head.

be highly polished 6061 T6 aluminum. At 293 K, Mylar has an emissivity of
0.044 [5]. The equation for power radiated between two bodies is given as:

$P=\frac{\sigma(T_{h}^{4}-T_{c}^{4})}{\frac{1}{A_{h}F_{hc}}+\frac{1-e_{h}}{A_{h}e_{h}}+\frac{1-e_{c}}{A_{c}e_{c}}}$

.

where $\sigma=5.6703\times 10^{-8}$ Wm-2K-4 is the Stefan-Boltzmann constant,
$T_{h}=293$ K is the temperature of the vacuum chamber, $T_{c}=55$ K is the
temperature of the cold shield, $A_{h}=5.217$ m2 is the interior surface area
of the vacuum chamber, $A_{c}=3.737$ m2 is the exterior surface area of the
cold shield, $e_{h}=0.044$ is the emissivity of the aluminized mylar layer
around the vacuum chamber at $T_{h}$, $e_{c}=0.02$ is the emissivity of the
6061 T6 aluminum of the cold shield at $T_{c}$, and $F_{hc}\approx 1$ is the
view factor. This gives a power radiated into the cold shield as $P_{r}=23.9$
W.

For a more accurate estimate, we consider radiation from the window into the
chamber which is modeled as an area with 100% emissivity. The window is 60 mm
in diameter giving an additional $P_{w}=1.2$ W into the cold shield. Another
source of power is light coming through the gaps of the mylar layers which
isn’t modeled in this estimate.

Since the chamber will be operating with a vacuum level below $10^{-5}$ Torr,
convection is negligible. The total heat load on the cold shield is:

$P_{tot}=P_{r}+P_{c}=23.9+1.2+1=26.1\text{W}$

before accounting for power from electronics. This power corresponds to a cold
head temperature of 40 K and gives a maximum temperature in the cold shield
below 77 K as simulated in SolidWorks. For an upper limit, we run a simulation
case with about double this heat load at 60 W, which yields a cold head
temperature of 55 K. Figure 5 shows the results from that case, with a maximum
temperature of 90K at the opposite end of the cold shield. These simulations
show that minimal radiation will be affecting the infrared detector system.

###  3.2 Thermal Expansion

To approximate the deformation of the cold shield, we use the linear thermal
expansion equation:

$\delta=\alpha L\Delta T$

where $\rm\alpha=2.3\times 10^{-5}\,K^{-1}$ is the coefficient of thermal
expansion for aluminum, $L$ is the length of the object, and $\Delta T$ is the
temperature change. The cold shield base measures 0.940m$\times$0.940m. After
reaching an ultimate temperature of 55 K, its new size will be
0.935m$\times$0.935m. The displacement of the A-frame where it attaches to the
cold-shield will be $\sim$2.5mm inwards on all sides. To make sure the
A-frames can withstand this bend, we calculate the minimum length the A-frames
need to be to survive using the equation:

$\rm L>\sqrt{\frac{3\delta Ew}{2\sigma_{max}}}$

where, for G-10, $E=16.5$ GPa, $\sigma_{max}=262$ MPa [5]. The width of the
A-frame is $w=0.015$ m and $\delta=0.0025$ m as before. This gives us a
minimum length of $L>0.06$ m. The current length of the A-frame far exceeds
this minimum length and simulations show the A-frames will easily withstand
the deflection.

##  4 Cart

---
Figure 6:  SolidWorks rendering of the cart housing the vacuum system,
cryogenic system, and electronics. The cold head is held on a cantilever arm
that sticks out behind the cart. The cart is constructed from standard 8020
components and is designed to be maneuverable for mounting to the vacuum
chamber in multiple orientations.

The cart servicing the test chamber will be made from 8020 extruded aluminum
and other standard 8020 components (Fig. 6). This cart will house the
computer, rough pump and turbo pump on top, and the interior of the cart will
house an electronics rack and compressor. The cold head will be extended via a
two-dimensional cantilever arm to be able to connect to the bottom of the test
chamber. This also allows the cold head to be disconnected and the cart easily
removed when not in use.

The cart is 99cm$\times$122cm$\times$79cm in size, with the cantilever arm
extending 79cm from the cart. The cart is on triangular casters with stopping
tabs, allowing it to be locked into place during operation. The rough pump,
turbo pump, and cold head will be mounted on vibration isolation pads.

The cart is made from multiple different materials: the frame of the cart, as
well as the braces, are made from 8020 extruded aluminum, while the corners
are fastened to the frame by a standard bolt assembly. The tabletops are made
from PVC 0.007 Plasticized Plastic to resist against scratches over time. The
cart rests on four triangular top casters with brakes and are attached to the
frame via a standard bolt assembly. The cantilever arm extends out
horizontally on a double thickness extruded aluminum, so as to provide
stronger lateral support and prevent deflection. There is also a two-
dimensional linear railing system on the cantilever arm so the cold head can
be adjusted in vertical height and horizontal distance. The cantilever arm is
attached to the main cart via side brackets.

##  5 Summary and Future Work

Liger is projected to be installed and operational by 2026-2027 [6],
capitalizing on the improvements to Keck AO from KAPA. It will provide higher
spectral resolving power, larger fields of view, and a wider wavelength
coverage than any existing IFS. We presented the design of the cryogenic test
chamber that will be used to characterize the imaging camera and slicer
component of the final Liger assembly.

This test chamber will operate at high vacuum and cryogenic temperatures to
perform the necessary tests. It will also be vibration isolated due to the
instrument’s sensitivity and the vibrations measured in the lab. It is
serviced by a mobile cart that houses the vacuum system, cryogenic system, and
electronics that interface with the experiment.

Future work on the experimental setup includes designing the adapter plate
between the cold shield base and the optical plate, and designing the mounting
system for the optics, detector, filter wheel, pupil wheel, and pupil viewing
camera [4]. Manufacturing work on the chamber is expected to begin in 2021.
The Liger opto-mechanical test dewar will provide an efficient means for
characterizing the imager and slicer components while being adaptable for
future cryogenic experiments.

###### Acknowledgements.

This research program was supported by the Heising-Simons Foundation.

## References

  * [1] Wright, S. A., Larkin, J. E., Jones, T., Aliado, T., Armus, L., Brown, A., Chisholm, E., Cosens, M., Dekaney, R., Do, T., Fassanacht, C., Fisher, D., Fitzgerald, M., Ghez, A., Hirtenstein, J., Johnson, C., Kassis, M., Keane, J., Kelley, P., Kirby, E., Konopacky, Q., Kress, E., Kupke, R., Lu, J., Lyke, J., Marley, M., Medling, A., Millar-Blanchaer, M., Nash, R., Nierenberg, A., Reddy, N., Rich, M., Ruffio, J.-B., Rundquist, N.-E., Sand, D., Sanders, R., Sandstrom, K., Shapley, A., Sohn, J.-M., Surya, A., Treu, T., Wang, E., Weber, B., Wiley, J., Wizinowich, P., Wong, M., Yeh, S., and Zonca, A., “Liger for Next-Generation Keck Adaptive Optics: Overall Design and Status,” in [Ground-based and Airborne Instrumentation for Astronomy VI ], Shields, J., ed., Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series 11447, 11447–331 (Dec. 2020).
  * [2] Wiley, J., Fleming, B., Renninger, N., and Egan, A., “Semi-automated high-efficiency reflectivity chamber for vacuum UV measurements,” in [Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series ], Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series 10397, 103971E (Aug. 2017).
  * [3] Fleming, B., Quijada, M., Hennessy, J., Egan, A., Del Hoyo, J., Hicks, B. A., Wiley, J., Kruczek, N., Erickson, N., and France, K., “Advanced Environmentally Resistant Lithium Fluoride Mirror Coatings for the Next-Generation of Broadband Space Observatories,” arXiv e-prints , arXiv:1801.03102 (Jan. 2018).
  * [4] Cosens, M., Wright, S. A., Arriaga, P., Brown, A., Fitzgerald, M., Jones, T., Kassis, M., Kress, E., Kupke, R., Larkin, J. E., Lyke, J., Wang, E., Wiley, J., and Yey, S., “Liger for Next-Generation Keck Adaptive Optics: Filter Wheel and Pupil Design,” in [Ground-based and Airborne Instrumentation for Astronomy VI ], Shields, J., ed., Society of Photo-Optical Instrumentation Engineers (SPIE) Conference Series 11447, 11447–280 (Dec. 2020).
  * [5] Duthil, P., “Material Properties at Low Temperature,” arXiv e-prints , arXiv:1501.07100 (Jan. 2015).
  * [6] Wright, S., Larkin, J. E., Jones, T., Kupke, R., Fitzgerald, M., Kassis, M., Cosens, M., Chisholm, E., Do, T., Fassnacht, C., Fisher, D., Ghez, A., Johnson, C., Keane, J., Kirby, E., Kress, E., Konopacky, Q., Lu, J. R., Maire, J., O’Meara, J., Reddy, N., Sand ers, R., Sandstrom, K., Shapley, A., Sohn, J.-M., Surya, A., Treu, T., Weber, R., Wiley, J., Wizinowich, P., Wong, M., and Zonca, A., “Liger: Next Generation Imager and Spectrograph for Keck Observatory Adaptive Optics,” in [Bulletin of the American Astronomical Society ], 51, 201 (Sept. 2019).


$\displaystyle=d_{g}\left(\mathtt{Exp}_{\widehat{\underline{\bm{x}}}^{(0)}}\left(\underline{\eta}\cdot\widehat{\underline{V}}_{d}(\widehat{\underline{\bm{x}}}^{(0)})\widehat{\underline{V}}_{d}(\widehat{\underline{\bm{x}}}^{(0)})^{T}\mathtt{grad}\,\widehat{f}_{h}(\widehat{\underline{\bm{x}}}^{(0)})\right),\,\underline{\bm{x}}^{*}\right)$
$\displaystyle\stackrel{{\scriptstyle\text{(i)}}}{{\leq}}d_{g}\left(\mathtt{Exp}_{\widehat{\underline{\bm{x}}}^{(0)}}\left(\underline{\eta}\cdot\underline{V}_{d}(\widehat{\underline{\bm{x}}}^{(0)})\underline{V}_{d}(\widehat{\underline{\bm{x}}}^{(0)})^{T}\mathtt{grad}\,f(\widehat{\underline{\bm{x}}}^{(0)})\right),\,\underline{\bm{x}}^{*}\right)$
$\displaystyle\quad+d_{g}\left(\mathtt{Exp}_{\widehat{\underline{\bm{x}}}^{(0)}}\left(\underline{\eta}\cdot\widehat{\underline{V}}_{d}(\widehat{\underline{\bm{x}}}^{(0)})\widehat{\underline{V}}_{d}(\widehat{\underline{\bm{x}}}^{(0)})^{T}\mathtt{grad}\,\widehat{f}_{h}(\widehat{\underline{\bm{x}}}^{(0)})\right),\,\mathtt{Exp}_{\widehat{\underline{\bm{x}}}^{(0)}}\left(\underline{\eta}\cdot\underline{V}_{d}(\widehat{\underline{\bm{x}}}^{(0)})\underline{V}_{d}(\widehat{\underline{\bm{x}}}^{(0)})^{T}\mathtt{grad}\,f(\widehat{\underline{\bm{x}}}^{(0)})\right)\right)$
$\displaystyle\stackrel{{\scriptstyle\text{(ii)}}}{{\leq}}\Upsilon\cdot
d_{g}(\widehat{\underline{\bm{x}}}^{(0)},\underline{\bm{x}}^{*})+\underline{\epsilon}_{n,h},$

where we apply the triangle inequality in (i) and leverage the result in (a)
and (90) to obtain (ii). The triangle inequality is valid in this context
because the geodesic measures the minimal distance between two points on
$\Omega_{q}$. Moreover, by the choice of $\widehat{\underline{\bm{x}}}^{(0)}$
and (90), we are ensured that
$d_{g}(\widehat{\underline{\bm{x}}}^{(1)},\underline{\bm{x}}^{*})\leq
2\arcsin\left(\underline{r}_{2}/2\right)$. In the induction from $t\mapsto
t+1$, we suppose that
$d_{g}(\widehat{\underline{\bm{x}}}^{(t)},\underline{\bm{x}}^{*})\leq
2\arcsin\left(\underline{r}_{2}/2\right)$ and the claim (91) holds at
iteration $t$. The same argument then implies that the claim (91) holds for
iteration $t+1$ and that
$d_{g}(\widehat{\underline{\bm{x}}}^{(t+1)},\underline{\bm{x}}^{*})\leq
2\arcsin\left(\underline{r}_{2}/2\right)$. The claim (91) is thus verified.
Now, given that
$\Upsilon=\sqrt{1-\frac{\underline{\beta}_{0}\underline{\eta}}{4}}<1$, we
iterate the claim (91) to show that

$\displaystyle
d_{g}(\widehat{\underline{\bm{x}}}^{(t)},\underline{\bm{x}}^{*})$
$\displaystyle\leq\Upsilon\cdot
d_{g}(\widehat{\underline{\bm{x}}}^{(t-1)},\underline{\bm{x}}^{*})+\underline{\epsilon}_{n,h}$
$\displaystyle\leq\Upsilon\left[\Upsilon\cdot
d_{g}(\widehat{\underline{\bm{x}}}^{(t-2)},\underline{\bm{x}}^{*})+\underline{\epsilon}_{n,h}\right]+\underline{\epsilon}_{n,h}$
$\displaystyle\leq\Upsilon^{t}\cdot
d_{g}(\widehat{\underline{\bm{x}}}^{(0)},\underline{\bm{x}}^{*})+\left[\sum_{s=0}^{t-1}\Upsilon^{s}\right]\underline{\epsilon}_{n,h}$
$\displaystyle\leq\Upsilon^{t}\cdot
d_{g}(\widehat{\underline{\bm{x}}}^{(0)},\underline{\bm{x}}^{*})+\frac{\underline{\epsilon}_{n,h}}{1-\Upsilon}$
$\displaystyle=\Upsilon^{t}\cdot
d_{g}(\widehat{\underline{\bm{x}}}^{(0)},\underline{\bm{x}}^{*})+O(h^{2})+O_{P}\left(\sqrt{\frac{|\log
h|}{nh^{q+4}}}\right),$

where the fourth inequality follows by summing the geometric series, and the
last equality is due to our notation
$\underline{\epsilon}_{n,h}=O(h^{2})+O_{P}\left(\sqrt{\frac{|\log
h|}{nh^{q+4}}}\right)$. It completes the proof.

(d) The result follows directly from (c) and the inequality
$d_{g}(\widehat{\underline{\bm{x}}}^{(t)},\underline{R}_{d})\leq
d_{g}(\widehat{\underline{\bm{x}}}^{(t)},\underline{\bm{x}}^{*})$ for all
$t\geq 0$. ∎