2. SIMP - Abstract Machine

We define an abstract machine with:

• a control stack $c$
• an auxiliary stack $r$
• memory (also called store) modelled by partial function $m$, mapping each address to an integer. The domain of $m$, $dom(m)$, denotes the locations where $m$ is defined. $m[I\mapsto n]$ is the function that maps each $I^{\prime }\ne I$ to the value $m(I^{\prime })$, and $I$ to value $n$.
  • $m[I\mapsto n](I)=n$
  • $m[I\mapsto n](I^{\prime })=m(I^{\prime })\text{ if }I\ne I^{\prime }$

An abstract machine is a transition system. The configuration is a triple: $⟨Control,Results,Memory⟩$

Definition of control and result stacks:

• $c::=nil|i\cdot c$
• $i::=P|\text{ op }|\neg |\wedge |\text{ bop }|:=|\text{ if }|\text{ while}$
• $r::=nil|P\cdot r|I\cdot r$

Where $P$, $\text{bop}$, and $\text{op}$ are non-terminals used in the rules defining SIMP programs. To model the execution of a program, we will define transitions between initial and final configurations.

• Initial config: $⟨C\cdot nil,nil,m⟩$
• Final config: $⟨nil,nil,m⟩$

Semantics

If there is a sequence of transitions $(C\cdot nil,nil,m){\to }^{\ast }(nil,nil,m^{\prime })$ then we say that program $C$ executed in the state $m$ terminates successfully producing the state $m^{\prime }$.

If there is a sequence $(E\cdot c,r,m){\to }^{\ast }(c,v\cdot r,m^{\prime })$ then we say that the value of expression $E$ in the state $m$ is $v$.

Transition Rules

A transition rule has the form $c\to c^{\prime }$, where each describe configurations. We divide these rules into two groups, one for evaluation of expressions and the other of commands.

Evaluation of expressions:

$$\begin{array}{rlrl}⟨n\cdot c,r,m⟩& \to ⟨c,n\cdot r,m⟩& & \\ ⟨b\cdot c,r,m⟩& \to ⟨c,b\cdot r,m⟩& & \\ ⟨\neg B\cdot c,r,m⟩& \to ⟨B\cdot \neg \cdot c,r,m⟩& & \\ ⟨(B_1\wedge B_2)\cdot c,r,m⟩& \to ⟨B_1\cdot B_2\cdot \wedge \cdot c,r,m⟩& & \\ ⟨\neg \cdot c,b\cdot r,m⟩& \to ⟨c,b^{\prime }\cdot r,m⟩& & \text{if }{b}^{\prime }=\text{not }b\\ ⟨\wedge \cdot c,b_2\cdot b_1\cdot r,m⟩& \to ⟨c,b\cdot r,m⟩& & \text{if }{b}_1\text{ and }{b}_2=b\\ ⟨(E_1\text{ op }{E}_2)\cdot c,r,m⟩& \to ⟨E_1\cdot E_2\cdot c,r,m⟩& & \\ ⟨(E_1\text{ bop }{E}_2)\cdot c,r,m⟩& \to ⟨E_1\cdot E_2\cdot c,r,m⟩& & \\ ⟨\text{op }\cdot c,n_2\cdot n_1\cdot r,m⟩& \to ⟨c,n\cdot r,m⟩& & \text{if }{n}_1\text{ op }{n}_2=n\\ ⟨\text{bop }\cdot c,n_2\cdot n_1\cdot r,m⟩& \to ⟨c,b\cdot r,m⟩& & \text{if }{n}_1\text{ bop }{n}_2=b\\ ⟨!I\cdot c,r,m⟩& \to ⟨c,n\cdot r,m⟩& & \text{if }m(I)=n\end{array}$$

Example: Assume $m=\{I\mapsto 4\}$ and we want to evaluate $!I>0$. Given the initial configuration, we find:

\begin{aligned} \langle !I > 0 \cdot nil, nil, m \rangle &\rightarrow \langle !I \cdot 0 \cdot > \cdot nil, nil, m \rangle \ &\rightarrow \langle 0 \cdot > \cdot nil, 4 \cdot nil, nil \rangle \ &\rightarrow \langle > \cdot nil, 0 \cdot 4 \cdot nil, m \rangle \ &\rightarrow \langle nil, \text{True} \cdot nil, m \rangle \end{aligned}$$

Evaluation of commands:

$$\begin{array}{rl}⟨\text{skip }\cdot c,r,m⟩& \to ⟨c,r,m⟩\\ ⟨(I:=E)\cdot c,r,m⟩& \to ⟨E\cdot :=\cdot c,l\cdot r,m⟩\\ ⟨:=\cdot c,n\cdot I\cdot r,m⟩& \to ⟨c,r,m[I\mapsto n]⟩\\ ⟨(C_1;C_2)\cdot c,r,m⟩& \to ⟨C_1\cdot C_2\cdot c,r,m⟩\\ & \\ ⟨(\text{if }B\text{ then }{C}_1\text{ else }{C}_2)\cdot c,r,m⟩& \to ⟨B\cdot \text{if}\cdot c,C_1\cdot C_2\cdot r,m⟩\\ ⟨\text{if}\cdot c,\text{True}\cdot C_1\cdot C_2\cdot r,m⟩& \to ⟨C_1\cdot c,r,m⟩\\ ⟨\text{if}\cdot c,\text{False}\cdot C_1\cdot C_2\cdot r,m⟩& \to ⟨C_2\cdot c,r,m⟩\\ & \\ ⟨(\text{while }B\text{ do }C)\cdot c,r,m⟩& \to ⟨B\cdot \text{while}\cdot c,B\cdot C\cdot r,m⟩\\ ⟨\text{while}\cdot c,\text{True}\cdot B\cdot C\cdot r,m⟩& \to ⟨C\cdot (\text{while }B\text{ do }C)\cdot c,r,m⟩\\ ⟨\text{while}\cdot c,\text{False}\cdot B\cdot C\cdot r,m⟩& \to ⟨c,r,m⟩\end{array}$$

The advantage of this definition is that it explains the execution of commands step by step which is useful if we have to implement the language. However, it is not very intuitive. Many transitions are just analysing the phrase and not performing computations.

To overcome this issue, we use a structural approach to transition systems.