# Frequent Statement and Dereference Elimination for Imperative and Object-Oriented Distributed Programs

Authors: Mohamed A. El-Zawawy
Journal: The Scientific World Journal
 (2014)

---

## Abstract

This paper introduces new approaches for the analysis offrequent statement and dereference elimination for imperative and object-oriented distributed programs running on parallel machines equipped with hierarchical memories. The paper uses languages whose address spaces are globally partitioned. Distributed programs allow defining data layout and threads writing to and reading from other thread memories. Three type systems (for imperative distributed programs) are the tools of the proposed techniques. The first type system defines for every program point a set of calculated (ready) statements and memory accesses. The second type system uses an enriched version of types of the first type system and determines which of the ready statements and memory accesses are used later in the program. The third type system uses the information gather so far to eliminate unnecessary statement computations and memory accesses (the analysis of frequent statement and dereference elimination). Extensions to these type systems are also presented to cover object-oriented distributed programs. Two advantages of our work over related work are the following. The hierarchical style of concurrent parallel computers is similar to the memory model used in this paper. In our approach, each analysis result is assigned a type derivation (serves as a correctness proof).


---

## Body

## 1. Introduction

Distributed programming is about building a software that has concurrent processes cooperating in achieving some task. For a problem specification, the type, number, and the way of interaction of processes needed to solve the problem are decided beforehand. Then a supercomputer can be computationally simulated by a group of workstations to carry different processes. A group of supercomputers can in turn be combined to provide a computing power greater than that provided by any single machine. This enormous computing power provided by distributed systems is why the distributed programming style [1–3] is quite important and attractive. Among examples of distributed programming languages (DPLs), based on machines having multicore processors and using partitioned-global model, are Unified Parallel C (UPC), Chapel, Titanium which is based on Java, and X10.Among advantages of object-oriented programming (OOP) is combining other styles such as imperative, functional, and relational programming. Concepts of class, procedure, and inheritance are basics for OOP. These concepts result in dynamic behavior in various implementations of object-oriented programming languages.Recomputing a nontrivial statement and reaccessing a memory location are waste of time and power if the value of the statement and the content of the location have not been changed. The purpose offrequent statement and dereference elimination analysis is to save such wasted power and time. This is an interesting analysis because it involves connecting statement and dereference calculations to program points where the calculated values may be reused. The analysis also requires changing program points at the ends of these connections. Such changes to program points have to be done carefully so that they do not destroy the compositionality. Our approach to treat this analysis is a type system [4, 5] built on a combination of two analyses; one of them builds on the results of the other one.For different programming languages, in previous work [4, 5], we have proved that the type systems style is certainly an adaptable approach for achieving many static analyses. This paper proves that this style is flexibly useful to the involved and important problem offrequent statement and dereference elimination of imperative and object-oriented distributed programs.This paper introduces new techniques forfrequent statement and dereference elimination for imperative and object-oriented distributed programs running on hierarchical memories. Simply structured type systems are the main tools of this paper’s techniques presented using the languages w
h
i
l
e
d of Figure 2 andOODP of Figure 3. These languages are equipped with basic commands for distributed execution of programs and for pointer manipulations. The single program multiple data (SPMD) model is the execution archetypal used in this paper. On different data of different machines this archetypal runs the same program. The analysis offrequent statement and dereference elimination for distributed programs is achieved in three steps each of which is done using a type system. The first of these steps achievesready statement and memory access analysis. The second step deals withsemiexpectation analysis and builds on the type system of the first step. The third type system takes care of the analysis offrequent statement and dereference elimination and is built on the type system of the second step. The paper also illustrates how these type systems can be generalized to cover object-oriented distributed languages.This paper is an extended and revised version of [6], which treats imperative distributed programs. The work of [6] was generalized in Section 5 of the current paper to cover object-oriented distributed programs. The soundness theorems of the current paper are stated using memory model and operational semantics in the appendix of [6].Motivation. The left-hand-side of Figure 1 presents a motivating example of our work. We note that lines 4 and 6 dereference a
*
b which has already been dereferenced in line 2 with no changes to values of a and b in the path from 2 to 6. This is a waste of computational power and time (accessing a secondary storage). One objective of the research in this paper is to avoid such waste by transforming the program into that in the right-hand-side of the algorithm. This is not all; we need to do that in a way that provides a correctness proof for each transformation. We adopt a style (type systems) that provides these proofs (type derivations).Figure 1
Motivating example.Figure 2
The programming languagew
h
i
l
e
d.Figure 3
The programming languageOODP.Contributions. Contributions of this paper are new techniques, in the form of type systems, for achieving the following analyses for imperative and object-oriented distributed programs.(1)
The analysis ofready statement and memory access.
(2)
The analysis ofsemiexpectation.
(3)
The analysis offrequent statement and dereference elimination.Organization. The rest of the paper is organized as follows. Section 2 presents the type system achieving the analysis ofready statement and memory access for imperative distributed programs. The analysis ofsemiexpectation as an enrichment of the type system presented in Section 2 is outlined in Section 3. The main type system carrying the analysis offrequent statement and dereference elimination is contained in Section 4. Type systems of Sections 2, 3, and 4 are generalized in Section 5 to cover object-oriented distributed programs. Related and future works are discussed in Section 6.


## 2. Ready Statement and Memory Access Analysis ofw
h
i
l
e
d

If the value of a statement and the content of a memory location have not been changed, then the compiler should not recompute the statement or reaccess the location. The purpose offrequent statement and dereference elimination is to save the wasted power and time involved in these repeated computations. This is not a trivial task; compared to other program analyses, it is a bit complex. This task is done in stages. The first stage is to analyze the given program to recognizeready statements and memory locations.The analysis ofready statements and memory locations calculates for every program point the set of statements and memory locations that areready at that point in the sense of Definition 1. This section presents a type system (ready type system) to achieve this analysis for imperative distributed programs.Definition 1.
(1) At a program pointp
t, a statement S isready if each computational path to p
t
(a)
contains an evaluation ofS at some point (say p
t
′) and
(b)
does not modifyS (changing value of any of S’s variables) between p
t
′ and p
t.
(2) At a program pointp
t, a memory location l isready if each computational path to p
t
(a)
readsl at some point (say p
t
′) and
(b)
does not modify content ofl between p
t
′ and p
t.Theready analysis is a forward analysis that takes as an input a set of statements and memory locations (theready set of the first program point). It is sensible to let this set be the empty set. The set of types of ourready type system has the form: p
o
i
n
t
s
-
t
o
-
t
y
p
e
s
×
𝒫
(
S
t
m
t
+
∪
g
A
d
d
r
s
), where(1)
S
t
m
t
+ is the set of nontrivial statements (Figure 2),
(2)
g
A
d
d
r
s is the set of global addresses. This set is defined precisely in the appendix of [6], and
(3)
points-to-types is a set of points-to-types (typically have the form of maps from the union of variables and global addresses to the power set of global addresses [4, 7]).The subtyping relation has the form≤
p
×
⊇, where ≤
p is the order relation on the points-to-types and ⊇ is the order relation on 𝒫
(
S
t
m
t
+
∪
g
A
d
d
r
s
). A state on an execution path is of type r
s
∈
𝒫
(
S
t
m
t
+
∪
g
A
d
d
r
s
) if all elements of r
s areready at this state according to Definition 1. Judgments of theready type system have the form S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
). The symbols p and p
′ denote the points-to-types of the before and after states of executing S. The set A
′ denotes the set of addresses that S may evaluate. We assume that all such pointer information is given along with the statement S. Techniques like [4, 7] are available to compute the pointer information. For a given statement along with pointer information and aready pretypers, we present a type system to calculate a postready-type r
s
′ such that S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
). The type derivation of this typing process is a proof for the correctness of theready information. The meaning of the judgment is that if elements of r
s areready before executing S, then elements of r
s
′ areready after executing S.The inference rules of theready type system are presented in Algorithm 1. Comments on the inference rules are in order. We note that numbers, variables, and the allocating statement (new) do not affect theready pretype. In line with semantic rules (
i
o
p
r
) and (
b
o
p
r
) [6], nontrivial arithmetic and Boolean statements and their nontrivial substatements are madeready. The direct assignment rule (
∶
=
r
) expresses that after executing the assignment the substatements of r.h.s. becomeready and that all statements involving x becomeunready as the value of x may become different. The rule (
*
r
) reflects the fact that the statement *
S becomesready after executing the dereference. Moreover if S evaluates a single address according to the underlying pointer analysis, then this address becomesready as well. However if S evaluates a large set of addresses (more than one), then we are not sure which of these addresses is the concerned one and hence cannot conclude any readiness information about addresses. The rule (
←
r
) adds the substatements of S
1 and S
2 to theready pretype. Since the content of address referenced by S
1 is possibly changed after executing the statement, all statements involving dereferencing this address are removed from the set ofready items. Remaining rules are self-explanatory. The Boolean statements t
r
u
e and f
a
l
s
e have inference rules similar to that of n.Algorithm 1:Inference rules of the ready type system.
n
:
p
→
m
(
A
′
,
p
′
)
n
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
) S
1
:
(
p
,
r
s
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
)
S
2
:
(
p
′
′
,
r
s
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
)
S
1
i
op
S
2
:
(
p
,
r
s
)
→
m
(
∅
,
p
′
,
r
s
′
∪
{
S
1
i
op
S
2
}
)
(
i
op
r
) x
:
p
→
m
(
A
′
,
p
′
)
x
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
)
S
1
:
(
p
,
r
s
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
)
S
2
:
(
p
′
′
,
r
s
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
)
S
1
b
op
S
2
:
(
p
,
r
s
)
→
m
(
∅
,
p
′
,
r
s
′
∪
{
S
1
b
op
S
2
}
)
(
b
op
r
) *
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
)
*
S
:
(
p
,
r
s
)
→
m
{
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
,
g
}
)
,
A
′
′
=
{
g
}
;
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
}
)
,
|
A
′
′
|
≠
1
.
(
*
r
)
s
k
i
p
:
(
p
,
r
s
)
→
m
(
∅
,
p
,
r
s
) x
:
=
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
)
x
:
=
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
′
∖
{
S
∈
S
t
m
t
∣
x
∈
f
r
e
e
(
S
)
}
)
(
≔
r
)
S
1
←
S
2
:
p
→
m
(
A
′
,
p
′
)
S
1
:
(
p
,
r
s
)
→
m
(
A
1
,
p
1
,
a
s
1
)
S
2
:
(
p
1
,
a
s
1
)
→
m
(
A
2
,
p
2
,
a
s
2
)
S
1
←
S
2
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
a
s
2
∖
(
A
′
∪
{
S
∣
S
:
p
→
m
(
A
s
,
—
)
&
A
s
∩
A
′
≠
∅
}
)
)
(
←
r
)
S
1
:
(
p
,
r
s
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
)
S
2
:
(
p
′
′
,
r
s
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
)
S
1
;
S
2
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
s
e
q
r
) S
:
(
p
,
r
s
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
)
S
t
:
(
p
,
r
s
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
)
S
f
:
(
p
,
r
s
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
)
i
f
S
t
h
e
n
S
t
e
l
s
e
S
f
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
i
f
r
)
S
1
[
S
2
/
x
]
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
λ
x
·
S
1
)
S
2
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
a
p
p
l
r
) S
:
(
p
,
r
s
)
→
(
A
′
′
,
p
′
′
,
r
s
′
)
S
t
:
(
p
′
′
,
r
s
′
)
→
m
(
A
′
,
p
′
,
r
s
)
w
h
i
l
e
S
d
o
S
t
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
w
h
l
r
)
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
λ
x
·
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
a
b
s
r
) f
d
(
n
a
m
e
)
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
n
a
m
e
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
n
a
m
e
r
)
(
λ
x
·
S
′
)
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
l
e
t
r
e
c
x
=
S
i
n
S
′
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
l
e
t
r
e
c
r
) n
e
w
l
:
p
→
m
(
A
′
,
p
′
)
n
e
w
l
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
)
(
n
e
w
r
)
c
o
n
v
e
r
t
(
S
,
n
)
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
)
→
m
(
A
,
p
′
′
,
r
s
′
)
c
o
n
v
e
r
t
(
S
,
n
)
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
c
o
n
v
e
r
t
r
) t
r
a
n
s
m
i
t
S
1
f
r
o
m
S
2
:
p
→
(
A
′
,
p
′
)
S
2
:
(
p
,
r
s
)
→
m
(
A
2
,
p
2
,
a
s
2
)
S
1
:
(
p
2
,
a
s
2
)
→
m
(
A
1
,
p
1
,
r
s
′
)
t
r
a
n
s
m
i
t
S
1
f
r
o
m
S
2
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
t
r
a
n
s
r
)
(
p
1
′
,
r
s
1
′
)
≤
(
p
1
,
a
s
1
)
S
:
(
p
1
,
a
s
1
)
→
m
(
p
2
,
a
s
2
)
(
p
2
,
a
s
2
)
≤
(
p
2
′
,
r
s
2
′
)
S
:
(
p
1
′
,
r
s
1
′
)
→
m
(
p
2
′
,
r
s
2
′
)
(
c
s
q
r
) D
e
f
s
:
∅
↷
f
d
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
D
e
f
s
:
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
p
r
g
r
)All in all, the information provided by type derivations obtained using this and the following type system is classified into two sorts. The first sort is about knowing the program point at which a particular statement becomesready. The second sort of information is about the program point at which a precomputed value of aready statement can be replaced with the statement.Now we recall the assumption that our distributed system consists of|
M
| machines. For a given statement S and a given machine m, the type system of Algorithm 1 calculates for each program point of S, the set ofready items. The following rule can be used to combine the information calculated for each machine to get newready information for each program point. The newready information is valid on any of the |
M
| machines.Consider(1)
∀
m
∈
M
·
S
:
(
sup
⁡
⁡
{
p
,
p
j
∣
j
≠
i
}
,
sup
⁡
⁡
{
r
s
,
r
s
j
∣
j
≠
i
}
)
⟶
m
(
A
m
,
p
m
,
r
s
m
)
S
:
(
p
,
r
s
)
⟶
M
(
∪
i
A
i
,
sup
⁡
⁡
{
p
1
,
…
,
p
n
}
,
sup
⁡
⁡
{
r
s
1
,
…
,
r
s
n
}
)
(
m
a
i
n
-
r
s
)
.The rule (main-rs) supposes a suitable notion for the join of pointer types. The soundness of theready type system is stated as follows.Theorem 2.
Suppose that(
S
,
δ
)
→
(
V
,
δ
′
)
,
S
:
(
p
,
r
s
)
→
(
A
′
,
p
′
,
r
s
′
), and the items of r
s areready at the point corresponding to δ on the execution path. Then the items of r
s
′ areready at the point corresponding to δ
′ on the execution path.


## 3.Semiexpectation Analysis of w
h
i
l
e
d

The aim of frequent statement elimination is to introduce new variables to accommodate values of frequent statements and reusing these values rather than recomputing the statements. Analogously, the aim of frequent dereferences elimination is to introduce new variables to accommodate values of frequent dereferences and reusing these values rather than reaccessing the memory. The information gathered so far by theready type system introduced in the previous section is not enough to achieve frequent statements and dereferences elimination. We need to enrich theready information, assigned to each program point, with new information calledsemiexpectable information.Definition 3.
(1) At a program pointp, a statement S issemiexpectable if there is a computational path from p that(a)
contains an evaluation ofS at some point (say p
′), where S is ready at p
′, and
(b)
does not evaluateS between p
′ and p.
(2) At a program pointp, a memory location l issemiexpectable if each computational path to p
(a)
readsl at some point (say p
′) where l is ready at p
′, and
(b)
does not readl between p
′ and p.Thesemiexpectation analysis is a backward analysis that takes as an input a set of statements and memory locations (thesemiexpectable set of the last program point). It is sensible to let this set be the empty set. The following example gives an intuition for the previous definition:
(2)
if
(
⋯
)
,
then
a
∶
=
y
+
t
else
b
∶
=
*
r
;
c
∶
=
(
y
+
t
)
*
r
.
Neither the statement y
+
t nor the statement *
r isready after the if statement because they are not computed in all branches. Hence it is not true to replace these statements with variables towards optimizing the last statement of the example. The job of the type system presented in this section is to provide us with this sort of information. More precisely, as the statements y
+
t and *
r are notready after the if statement, the second statement of the example does not make themsemiexpectable.Thesemiexpectation analysis assigns for each program point the set of items that aresemiexpectable. The analysis is based on thereadiness analysis and is backward. The set of types of thesemiexpectation type system has the form: p
o
i
n
t
s
-
t
o
-
t
y
p
e
s
×
𝒫
(
S
t
m
t
+
∪
g
A
d
d
r
s
)
×
𝒫
(
S
t
m
t
+
∪
g
A
d
d
r
s
). The subtyping relation has the form ≤
p
×
⊇
×
⊇. A state on an execution path is of type s
e
∈
𝒫
(
S
t
m
t
+
∪
g
A
d
d
r
s
) if all elements of s
e aresemiexpectable according to Definition 3. Judgments of thesemiexpectation type system have the form S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
). For a given statement along with pointer information, readiness information, and asemiexpectation type s
e
′, we present a type system to calculate a pre-semiexpectable-type s
e such that S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
). The type derivation of this typing process is proof for the correctness of thesemiexpectable information. The meaning of the judgment is that if elements of s
e
′ aresemiexpectable after executing S, then elements of s
e must have beensemiexpectable before executing S.The inference rules of thesemiexpectation type system are shown in Algorithm 2. Some comments on the inference rules are in order. In the rule (
i
o
p
e
), given the posttype s
e
′, we calculate the pretype s
e
′′ for the statement S
2. Then the resulting pretype is used as a posttype for the statement S
1 to calculate the pretype s
e. In line with Definition 3, the arithmetic statement S
1
i
o
p
S
2 is added to s
e only if it belongs to r
s. Similar explanations illustrate the rule (
*
e
). The remaining rules mimic the rules of theready type system.Algorithm 2:Inference rules of the semiexpectationtype system.
n
:
p
→
m
(
A
′
,
p
′
)
n
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
) x
:
p
→
m
(
A
′
,
p
′
)
x
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
S
2
:
(
p
′
′
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
S
1
i
op
S
2
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
S
1
i
op
S
2
}
)
)
→
m
(
∅
,
p
′
,
r
s
′
∪
{
S
1
i
op
S
2
}
,
s
e
′
)
(
i
op
e
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
S
2
:
(
p
′
′
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
S
1
b
op
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
∅
,
p
′
,
r
s
′
∪
{
S
1
b
op
S
2
}
,
s
e
′
)
(
b
op
e
)
*
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
*
S
:
(
p
,
r
s
,
s
e
∪
(
r
e
∩
{
*
S
,
g
}
)
)
→
m
{
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
,
g
}
,
s
e
′
′
)
,
A
′
=
{
g
}
;
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
}
,
s
e
′
′
)
,
|
A
′
|
≠
1
.
(
*
e
)
s
k
i
p
:
(
p
,
r
s
,
s
e
)
→
m
(
∅
,
p
,
r
s
,
s
e
) x
≔
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
x
≔
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
′
∖
{
S
∈
S
t
m
t
∣
x
∈
f
r
e
e
(
S
)
}
,
s
e
′
′
)
(
≔
e
)
S
1
←
S
2
:
p
→
m
(
A
′
,
p
′
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
a
s
1
,
s
e
1
)
S
2
:
(
p
1
,
a
s
1
,
s
e
1
)
→
m
(
A
2
,
p
2
,
a
s
2
,
s
e
2
)
S
1
←
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
a
s
2
∖
(
A
′
∪
{
S
∣
S
:
p
→
m
(
A
s
,
_
)
&
A
s
∩
A
′
≠
∅
}
)
,
s
e
2
)
(
←
e
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
S
2
:
(
p
′
′
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
S
1
;
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
s
e
q
e
) S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
S
t
:
(
p
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
S
f
:
(
p
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
i
f
S
t
h
e
n
S
t
e
l
s
e
S
f
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
i
f
e
)
S
1
[
S
2
/
x
]
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
λ
x
·
S
1
)
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
a
p
p
l
e
)
S
:
(
p
,
r
s
,
s
e
)
→
(
A
′
′
,
p
′
′
,
r
s
′
,
s
e
′
)
S
t
:
(
p
′
′
,
r
s
′
,
s
e
′
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
w
h
i
l
e
S
d
o
S
t
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
w
h
l
e
)
f
d
(
n
a
m
e
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
n
a
m
e
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
n
a
m
e
e
) S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
λ
x
·
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
a
b
s
e
)
(
λ
x
·
S
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
l
e
t
r
e
c
x
=
S
i
n
S
′
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
l
e
t
r
e
c
e
) n
e
w
l
:
p
→
m
(
A
′
,
p
′
)
n
e
w
l
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
(
n
e
w
e
)
c
o
n
v
e
r
t
(
S
,
n
)
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
,
p
′
′
,
r
s
′
,
s
e
′
)
c
o
n
v
e
r
t
(
S
,
n
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
c
o
n
v
e
r
t
e
)
t
r
a
n
s
m
i
t
S
1
f
r
o
m
S
2
:
p
→
(
A
′
,
p
′
)
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
2
,
p
2
,
a
s
2
,
s
e
2
)
S
1
:
(
p
2
,
a
s
2
,
s
e
2
)
→
m
(
A
1
,
p
1
,
r
s
′
,
s
e
′
)
t
r
a
n
s
m
i
t
S
1
f
r
o
m
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
(
t
r
a
n
s
e
)
(
p
1
′
,
r
s
1
′
,
s
e
1
′
)
≤
(
p
1
,
a
s
1
,
s
e
1
)
S
:
(
p
1
,
a
s
1
,
s
e
1
)
→
m
(
p
2
,
a
s
2
,
s
e
2
)
(
p
2
,
a
s
2
,
s
e
2
)
≤
(
p
2
′
,
r
s
2
′
,
s
e
2
′
)
S
:
(
p
1
′
,
r
s
1
′
,
s
e
1
)
→
m
(
p
2
′
,
r
s
2
′
,
s
e
2
′
)
(
c
s
q
e
) D
e
f
s
:
∅
↷
f
d
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
,
p
′
,
r
s
′
,
s
e
′
)
D
e
f
s
:
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
,
p
′
,
r
s
′
,
s
e
′
)
(
p
r
g
e
)Now we recall the assumption that our distributed system consists of|
M
| machines. For a given statement S and a given machine m, the type system given above calculates for each program point of S the set ofsemiexpectable items. Now the following rule can be used to combine the information calculated for each machine to get newsemiexpectable information for each program point. The newsemiexpectable information is valid on any of the |
M
| machines.Consider(3)
∀
m
∈
M
⋅
S
:
(
sup
⁡
⁡
{
p
,
p
j
∣
j
≠
i
}
,
sup
⁡
⁡
{
r
s
,
r
s
j
∣
j
≠
i
}
)
⟶
m
(
A
m
,
p
m
,
r
s
m
)
S
:
(
p
,
r
s
)
⟶
M
(
∪
i
A
i
,
sup
⁡
⁡
{
p
1
,
…
,
p
n
}
,
sup
⁡
⁡
{
r
s
1
,
…
,
r
s
n
}
)
×
(
m
a
i
n
-
r
s
)
.The difference in the way that this rule treats thesemiexpectable information and the wayready information is treated is explained by the fact that theready analysis is forward while thesemiexpectation analysis is backward.It is not hard to prove the soundness of the above type system.Theorem 4.
Suppose that(
S
,
δ
)
→
(
V
,
δ
′
)
,
S
:
(
p
,
r
s
,
s
e
)
→
(
A
′
,
p
′
,
r
s
′
,
s
e
′
) and the items of s
e
′ aresemiexpectable at the point corresponding to δ
′ on the execution path. Then the items of s
e aresemiexpectable at the point corresponding to δ on the execution path.


## 4. Frequent Statement and Dereference Elimination ofw
h
i
l
e
d

This section presents a type system that is an enrichment of the type system presented in the previous section. The type system of this section achieves thefrequent statement and dereference elimination. The type system uses a function s
n
:
S
+
→
S
t
m
t
-
n
a
m
e
s that assigns each nontrivial statement a name. These names are meant to carry values of frequent statements and dereferences. The judgments of our type system have the form S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
). The type information (
p
,
r
s
,
s
e
) and (
A
′
,
p
′
,
r
s
′
,
s
e
′
) were calculated by the previous type system. S
′ is the optimization of S and n
s is a sequence of assignments that links optimized statements with the names of their unoptimized versions.Algorithms3 and 4 present inference rules for thefrequent statements and dereferences elimination. We note the following on the inference rules. A big deal of optimization is achieved by the three rules for *
S. These rules are (
*
1
f
)
,
(
*
2
f
), and (
*
3
f
). The rule (
*
1
f
) takes care of the case where *
S isready and is replaceable by its name under the function s
n. The rule (
*
2
f
) treats the case where *
S issemiexpectable and is notready before calculating the statement. In this case, a statement name of *
S is used. The rule (
*
3
f
) considers the case where *
S is neithersemiexpectable at the program point after execution norready before calculating the statement. In this case, the statement *
S does not get changed. Similarly, the three rules (
i
o
p
(
1
)
f
)
,
(
i
o
p
(
2
)
f
), and (
i
o
p
(
3
)
f
) treat different cases for arithmetic statements. The Boolean statements are treated with rules quite similar to that of arithmetic statements. The rule (
w
h
l
f
) reuses frequent substatements of the guard. This is done via adding n
s in the positions clarified in the rule. Remaining rules of system are self-explanatory.Algorithm 3:Inference rules for the frequent statements and dereferences elimination (1).
n
:
p
→
m
(
A
′
,
p
′
)
n
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
⇛
(
s
k
i
p
,
n
)     x
:
p
→
m
(
A
′
,
p
′
)
x
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
⇛
(
s
k
i
p
,
x
)
*
S
∈
r
s
*
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
,
S
′
)
*
S
:
(
p
,
r
s
,
s
e
∪
(
r
e
∩
{
*
S
,
g
}
)
)
→
m
{
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
,
g
}
,
s
e
′
′
)
,
A
′
=
{
g
}
;
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
}
,
s
e
′
′
)
,
|
A
′
|
≠
1
.
⇛
(
n
s
,
s
n
(
*
S
)
)
(
*
1
f
)
*
S
∉
r
s
*
S
∈
s
e
′
*
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
,
S
′
)
*
S
:
(
p
,
r
s
,
s
e
∪
(
r
e
∩
{
*
S
,
g
}
)
)
→
m
{
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
,
g
}
,
s
e
′
′
)
,
A
′
=
{
g
}
;
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
}
,
s
e
′
′
)
,
|
A
′
|
≠
1
.
⇛
(
n
s
;
s
n
(
*
S
)
≔
*
S
′
,
s
n
(
*
S
)
)
(
*
2
f
)
*
S
∉
r
s
*
S
∉
s
e
′
*
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
,
S
′
)
*
S
:
(
p
,
r
s
,
s
e
∪
(
r
e
∩
{
*
S
,
g
}
)
)
→
m
{
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
,
g
}
,
s
e
′
′
)
,
A
′
=
{
g
}
;
(
A
′
,
p
′
,
r
s
′
′
∪
{
*
S
}
,
s
e
′
′
)
,
|
A
′
|
≠
1
.
⇛
(
n
s
,
*
S
′
)
(
*
3
f
)
S
1
i
op
S
2
∈
r
s
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
1
,
S
1
′
)
S
2
:
(
p
′
′
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
2
,
S
2
′
)
S
1
i
op
S
2
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
S
1
i
o
p
S
2
}
)
)
→
m
(
∅
,
p
′
,
r
s
′
∪
{
S
1
i
op
S
2
}
,
s
e
′
)
⇛
(
n
s
1
;
n
s
2
,
s
n
(
S
1
i
o
p
S
2
)
)
(
i
op
(
1
)
f
)
S
1
i
op
S
2
∉
r
s
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
1
,
S
1
′
)
S
1
i
op
S
2
∈
s
e
′
S
2
:
(
p
′
′
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
2
,
S
2
′
)
S
1
i
op
S
2
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
S
1
i
o
p
S
2
}
)
)
→
m
(
∅
,
p
′
,
r
s
′
∪
{
S
1
i
op
S
2
}
,
s
e
′
)
⇛
(
n
s
1
;
n
s
2
;
s
n
(
S
1
i
op
S
2
)
≔
(
S
1
′
i
op
S
2
′
)
,
s
n
(
S
1
i
op
S
2
)
)
(
i
op
(
2
)
f
)
S
1
i
op
S
2
∉
r
s
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
1
,
S
1
′
)
S
1
i
op
S
2
∉
s
e
′
S
2
:
(
p
′
′
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
2
,
S
2
′
)
S
1
i
op
S
2
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
S
1
i
op
S
2
}
)
)
→
m
(
∅
,
p
′
,
r
s
′
∪
{
S
1
i
op
S
2
}
,
s
e
′
)
⇛
(
n
s
1
;
n
s
2
,
S
1
′
i
op
S
2
′
)
(
i
o
p
(
3
)
f
)
s
k
i
p
:
(
p
,
r
s
,
s
e
)
→
m
(
∅
,
p
,
r
s
,
s
e
)
⇛
(
s
k
i
p
,
s
k
i
p
)
x
≔
S
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
s
n
,
S
′
)
x
≔
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
′
∖
{
S
∈
S
t
m
t
∣
x
∈
f
r
e
e
(
S
)
}
,
s
e
′
′
)
⇛
(
s
k
i
p
,
n
s
;
x
≔
S
′
)
(
:
=
f
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
a
s
1
,
s
e
1
)
⇛
(
n
s
1
,
S
1
′
)
S
2
:
(
p
1
,
a
s
1
,
s
e
1
)
→
m
(
A
2
,
p
2
,
a
s
2
,
s
e
2
)
⇛
(
n
s
2
,
S
2
′
)
S
1
←
S
2
:
p
→
m
(
A
′
,
p
′
)
S
1
←
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
a
s
2
∖
(
A
′
∪
{
S
∣
S
:
p
→
m
(
A
s
,
—
)
&
A
s
∩
A
′
≠
∅
}
)
,
s
e
2
)
⇛
(
s
k
i
p
,
n
s
1
;
n
s
2
;
S
1
′
←
S
2
′
)
(
←
f
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
1
,
S
1
′
)
S
2
:
(
p
′
′
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
2
,
S
2
′
)
S
1
;
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
1
;
n
s
2
,
S
1
′
;
S
2
′
)
(
s
e
q
f
)Algorithm 4:Inference rules for the frequent statements and dereferences elimination (2).
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
′
,
p
′
′
,
r
s
′
′
,
s
e
′
′
)
⇛
(
n
s
,
S
′
)
S
t
:
(
p
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
t
,
S
t
′
)
S
f
:
(
p
,
r
s
′
′
,
s
e
′
′
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
f
,
S
f
′
)
i
f
S
t
h
e
n
S
t
e
l
s
e
S
f
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
s
k
i
p
,
n
s
;
i
f
S
′
t
h
e
n
n
s
t
;
S
t
′
e
l
s
e
n
s
f
;
S
f
′
)
(
i
f
f
)
(
λ
x
·
S
1
)
[
S
2
/
x
]
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
(
λ
x
·
S
1
)
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
(
a
p
p
l
f
)
S
:
(
p
,
r
s
,
s
e
)
→
(
A
′
′
,
p
′
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
S
t
:
(
p
′
′
,
r
s
′
,
s
e
′
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
⇛
(
n
s
t
,
S
t
′
)
w
h
i
l
e
S
d
o
S
t
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
s
k
i
p
,
n
s
;
w
h
i
l
e
S
′
d
o
(
n
s
t
;
S
t
′
;
n
s
)
)
(
w
h
l
f
)
f
d
(
n
a
m
e
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
n
a
m
e
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
(
n
a
m
e
f
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
λ
x
·
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
s
k
i
p
,
n
s
;
λ
x
·
S
′
)
(
a
b
s
f
)
n
e
w
l
:
p
→
m
(
A
′
,
p
′
)
n
e
w
l
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
⇛
(
s
k
i
p
,
n
e
w
l
)
(
n
e
w
f
)
(
λ
x
·
S
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
′
)
l
e
t
r
e
c
x
=
S
i
n
S
′
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
′
)
(
l
e
t
r
e
c
f
)
c
o
n
v
e
r
t
(
S
,
n
)
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
,
p
′
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
c
o
n
v
e
r
t
(
S
,
n
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
s
k
i
p
,
n
s
;
c
o
n
v
e
r
t
(
S
′
,
n
)
)
(
c
o
n
v
e
r
t
f
)
t
r
a
n
s
m
i
t
S
1
f
r
o
m
S
2
:
p
→
(
A
′
,
p
′
)
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
2
,
p
2
,
a
s
2
,
s
e
2
)
⇛
(
n
s
2
,
S
2
′
)
S
1
:
(
p
2
,
a
s
2
,
s
e
2
)
→
m
(
A
1
,
p
1
,
r
s
′
,
s
e
′
)
⇛
(
n
s
1
,
S
1
′
)
t
r
a
n
s
m
i
t
S
1
f
r
o
m
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
1
;
n
s
2
,
t
r
a
n
s
m
i
t
S
1
′
f
r
o
m
S
2
′
)
(
t
r
a
n
s
f
)
(
p
1
′
,
r
s
1
′
,
s
e
1
′
)
≤
(
p
1
,
a
s
1
,
p
a
1
)
(
p
2
,
a
s
2
,
p
a
2
)
≤
(
p
2
′
,
r
s
2
′
,
s
e
2
′
)
S
:
(
p
1
,
a
s
1
,
p
a
1
)
→
m
(
p
2
,
a
s
2
,
p
a
2
)
⇛
(
n
s
,
S
′
)
S
:
(
p
1
′
,
r
s
1
′
,
p
a
1
)
→
m
(
p
2
′
,
r
s
2
′
,
s
e
2
′
)
⇛
(
n
s
,
S
′
)
(
c
s
q
f
)
D
e
f
s
:
∅
↷
f
d
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
)
D
e
f
s
:
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
,
p
′
,
r
s
′
,
s
e
′
)
⇛
D
e
f
s
:
n
s
;
S
′
(
p
r
g
f
)For expressing the soundness, we introduce the following definition.Definition 5.
Suppose thatδ is a state defined on the set of locations,Loc ([6, Definition 4]). Suppose also that δ
* is a state defined on L
o
c
∪
S
t
m
t
-
n
a
m
e
s. The expression δ
≡
s
e
δ
* denotes the fact that δ and δ
* are equivalent with respect to thesemiexpectation typese. More precisely δ
≡
s
e
δ
* if and only if (1)
for
all
j
∈
L
o
c
.
δ
(
j
)
=
δ
*
(
j
), and
(2)
for
all
S
∈
s
e
.
(
S
,
δ
)
⇝
m
(
v
,
δ
′
)
⇒
δ
*
(
s
n
(
S
)
)
=
v.The soundness offrequent statements and dereferences elimination means that the original and optimized programs are equivalent in the following sense:(i)
the states of the two programs coincide on theLoc, and
(ii)
if a statement is bothready andsemiexpectable, then its semantics in the original-program state equals the value of its corresponding name in optimized-program state.This gives an intuition to the previous definition. The following soundness theorem is proved by a structure induction.Theorem 6.
Suppose thatS
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
) and δ
≡
s
e
δ
*. Then (i)
(
S
,
δ
)
⇝
m
(
v
,
δ
′
)
⇒
∃
δ
*
′
.
δ
′
≡
s
e
′
δ
*
′
a
n
d
(
S
′
,
δ
*
)
⇝
m
(
v
,
δ
*
′
);
(ii)
(
S
′
,
δ
*
)
⇝
m
(
v
,
δ
*
′
)
⇒
∃
δ
′
.
δ
′
≡
s
e
′
δ
*
′
a
n
d
(
S
,
δ
)
⇝
m
(
v
,
δ
′
).


## 5. Frequent Statement and Dereference Elimination ofOODP Programs

This section generalizes the type systems of previous sections to cover object-oriented distributed programs. Hence, a new model for object-oriented distributed programs and necessary changes to proposed type systems for the analysis offrequent statement and dereference elimination are presented in this section. Object-oriented concepts such as subtyping and inheritance are included in the model language (dubbedOODP) whose syntax is shown in Figure 3.In line with OOP concepts, local variables are contained in functions and live while their functions are live. While parameters of function are represented using local variables, a class’s internal state is contained in its instance variables. A class is a container for a set of function definitions. Each functionf has parameter p
f, a main statement S
f, and a statement S
f representing value returned by the function. Hence anOODP program is a set of classes followed by a “main” function. Figure 4 presents semantic spaces and naming conventions used in the rest of the paper.Figure 4
Semantic spaces and naming conventions.As shown in the previous sections, the analysis offrequent statement and dereference eliminationfor imperative distributed programs is achieved in three steps. In the following, we show necessary changes to the three type systems presented so far to cover object-oriented distributed programs.For each program point,ready statements and memory locations (Definition 1) are computed by the analysis ofready statements and memory locations. Adding rules of Algorithm 5 to that of Algorithm 1 results in a type system that calculates this analysis for object-oriented distributed programs of Figure 3. Using semantics notions of Figure 4, Definitions 1, 3, and 5 are applicable and convenient for the analyses in this section for the languageOODP.Algorithm 5:An extension for the ready type system to cover OODP programs.
o
·
v
:
p
→
m
(
A
′
,
p
′
)
o
·
v
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
) this
:
p
→
m
(
A
′
,
p
′
)
this
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
) S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
C
)
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
∪
{
(
C
)
S
}
)
S
1
·
v
:
=
S
2
:
p
→
m
(
A
′
,
p
′
)
S
1
:
(
p
,
r
s
)
→
m
(
A
1
,
p
1
,
r
s
1
)
S
1
:
p
→
C
s
S
2
:
(
p
1
,
r
s
1
)
→
m
(
A
2
,
p
′
,
r
s
′
)
S
1
·
v
≔
S
2
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
∖
{
S
∈
S
t
m
t
s
∣
C
∈
C
s
∧
C
·
v
∈
f
r
e
e
(
S
)
}
)
(
≔
S
·
v
r
)
o
1
≔
o
2
·
f
(
S
)
:
p
→
m
(
A
′
,
p
′
)
{
S
1
,
…
,
S
m
}
=
{
S
f
,
S
r
∣
∃
C
∈
C
s
∧
F
C
(
f
)
=
(
p
,
S
f
,
S
r
)
}
S
:
(
p
,
r
s
)
→
m
(
A
1
,
p
1
,
r
s
1
)
o
2
:
p
→
C
s
S
i
:
(
p
i
,
r
s
i
)
→
m
(
A
i
+
1
,
p
i
+
1
,
r
s
i
+
1
)
o
1
:
=
o
2
·
f
(
S
)
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
m
+
1
∖
{
S
∈
S
t
m
t
s
∣
o
1
∈
f
r
e
e
(
S
)
}
)
(
≔
o
·
f
r
)
o
1
≔
s
u
p
e
r
·
f
(
S
)
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
)
→
m
(
A
1
,
p
1
,
r
s
1
)
t
h
i
s
:
p
→
C
s
′
S
i
:
(
p
i
,
r
s
i
)
→
m
(
A
i
+
1
,
p
i
+
1
,
r
s
i
+
1
)
{
S
1
,
…
,
S
m
}
=
{
S
f
,
S
r
∣
∃
D
∈
C
s
′
∧
s
u
p
e
r
(
D
,
f
)
=
C
∧
F
C
(
f
)
=
(
p
,
S
f
,
S
r
)
}
o
1
≔
s
u
p
e
r
·
f
(
S
)
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
m
+
1
∖
{
S
∈
S
t
m
t
s
∣
o
1
∈
f
r
e
e
(
S
)
}
)
(
≔
s
u
p
e
r
r
)
o
:
=
new
C
:
p
→
m
(
A
′
,
p
′
)
o
:
=
new
C
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
∖
{
S
∈
S
t
m
t
s
∣
o
∈
f
r
e
e
(
S
)
}
)
(
≔
n
e
w
r
)Comments on the inference rules are in order. The rules of Algorithm5 suppose the existence of aclass analysis that calculates the set of classes that a statement may reference. The judgments of the proposed analysis have the form S
:
p
→
C
s. The intuition of such judgments is that the pointer information are used to calculate the set C
s. In the rule (
∶
=
S
·
v
r
),ready substatements of S
1 and S
2 are added to r
s to produce r
s
′. Then for any class C that S
1 may reference, statements involving C
·
v are removed from r
s
′. In the rule (
∶
=
o
·
f
r
)
,
C
s includes classes that o
2 may reference. For all functions named f in classes of C
s, the body and return statements are enumerated in the set {
S
1
,
…
,
S
m
}.Ready substatements of these statements are added to r
s to produce r
s
m
+
1. Then all statements involving o
1 are removed from r
s
m
+
1.Using semantics notations of Figure4, soundness of the type system of Algorithm 5 is stated as follows.Theorem 7.
Suppose that(
S
,
s
,
h
)
→
(
V
,
s
′
,
h
′
)
,
S
:
(
p
,
r
s
)
→
(
A
′
,
p
′
,
r
s
′
) and the items of r
s areready at the point corresponding to (
s
,
h
) on the execution path. Then the items of r
s
′ areready at the point corresponding to (
s
′
,
h
′
) on the execution path.The goals of main analysis of this section forOODP are as follows.Introducing new variables to maintain values of frequent statements and dereferences and then reusing these values instead of recomputing the statements and reaccessing the memory.To achieve this goal theready information needs to be enriched with information ofsemiexpectable.Adding rules of Algorithm6 to that of Algorithm 2 results in a type system that calculates the analysis ofsemiexpectation for object-oriented distributed programs of Figure 3. Some comments on the inference rules of Algorithm 6 are in order. In the rule (
∶
=
S
·
v
e
), starting with the posttype s
e
′, the pretype s
e
′′ is calculated for the statement S
2. Then s
e
′ is used as a posttype for S
1 to get the main pretype s
e. Similarly to (
∶
=
o
·
f
r
), the rule (
∶
=
o
·
f
e
) enumerates body and return statements of convenient functions. Then sequentially s
e is calculated starting from s
e
′. The remaining rules mimic the rules of theready type system.Algorithm 6:An extension for the semi-expectation type system.
o
·
v
:
p
→
m
(
A
′
,
p
′
)
o
·
v
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
) this
:
p
→
m
(
A
′
,
p
′
)
this
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
(
C
)
S
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
(
C
)
S
}
)
)
→
m
(
A
′
,
p
′
,
r
s
′
∪
{
(
C
)
S
}
,
s
e
′
)
S
1
·
v
≔
S
2
:
p
→
m
(
A
′
,
p
′
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
r
s
1
,
s
e
1
)
S
1
:
p
→
C
s
S
2
:
(
p
1
,
r
s
1
,
s
e
1
)
→
m
(
A
2
,
p
′
,
r
s
′
,
s
e
′
)
S
1
·
v
≔
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
∖
{
S
∈
S
t
m
t
s
∣
C
∈
C
s
∧
C
·
v
∈
f
r
e
e
(
S
)
}
,
s
e
′
)
(
≔
S
·
v
e
)
o
1
≔
o
2
·
f
(
S
)
:
p
→
m
(
A
′
,
p
′
)
{
S
1
,
…
,
S
m
}
=
{
S
f
,
S
r
∣
∃
C
∈
C
s
∧
F
C
(
f
)
=
(
p
,
S
f
,
S
r
)
}
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
r
s
1
,
s
e
1
)
o
2
:
p
→
C
s
S
i
:
(
p
i
,
r
s
i
,
s
e
i
)
→
m
(
A
i
+
1
,
p
i
+
1
,
r
s
i
+
1
,
s
e
i
+
1
)
o
1
≔
o
2
·
f
(
S
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
m
+
1
∖
{
S
∈
S
t
m
t
s
∣
o
1
∈
f
r
e
e
(
S
)
}
,
s
e
m
+
1
)
(
≔
o
·
f
e
)
o
1
≔
s
u
p
e
r
·
f
(
S
)
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
r
s
1
,
s
e
1
)
t
h
i
s
:
p
→
C
s
′
S
i
:
(
p
i
,
r
s
i
,
s
e
i
)
→
m
(
A
i
+
1
,
p
i
+
1
,
r
s
i
+
1
,
s
e
i
+
1
)
{
S
1
,
…
,
S
m
}
=
{
S
f
,
S
r
∣
∃
D
∈
C
s
′
∧
s
u
p
e
r
(
D
,
f
)
=
C
∧
F
C
(
f
)
=
(
p
,
S
f
,
S
r
)
}
o
1
≔
s
u
p
e
r
·
f
(
S
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
m
+
1
∖
{
S
∈
S
t
m
t
s
∣
o
1
∈
f
r
e
e
(
S
)
}
,
s
e
m
+
1
)
(
≔
s
u
p
e
r
e
)
o
:
=
new
C
:
p
→
m
(
A
′
,
p
′
)
o
:
=
new
C
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
∖
{
S
∈
S
t
m
t
s
∣
o
∈
f
r
e
e
(
S
)
}
,
s
e
)
(
≔
n
e
w
e
)Using semantics notations of Figure4, soundness of the type system of Algorithm 6 is stated as follows.Theorem 8.
Suppose that(
S
,
s
,
h
)
→
(
V
,
s
′
,
h
′
)
,
S
:
(
p
,
r
s
,
s
e
)
→
(
A
′
,
p
′
,
r
s
′
,
s
e
′
), and the items of s
e
′ aresemiexpectable at the point corresponding to (
s
′
,
h
′
) on the execution path. Then the items of s
e aresemiexpectable at the point corresponding to (
s
,
h
) on the execution path.Adding rules of Algorithm7 to that of Algorithm 3 results in the main type system achieving the analysis offrequent statement and dereference elimination for object-oriented distributed programs of Figure 3. We note the following on the inference rules. Optimization is based on rules for (
C
)
S; (
(
C
)
S
1
f
), (
(
C
)
S
2
f
), and (
(
C
)
S
3
f
). The case that (
C
)
S isready and is replaceable by its name under the function s
n is treated by (
(
C
)
S
1
f
). The case (
C
)
S issemiexpectable but notready before calculating the statement is treated by (
(
C
)
S
2
f
). The rule (
(
C
)
S
3
f
) takes care of the case, where (
C
)
S is neitherready before the calculation norsemiexpectable after execution.Algorithm 7:An extension for the frequent statements and de-references elimination type system.
o
·
v
:
p
→
m
(
A
′
,
p
′
)
o
·
v
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
⇛
(
skip
,
o
·
v
)  this
:
p
→
m
(
A
′
,
p
′
)
this
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
,
s
e
)
⇛
(
skip
,
this
)
(
C
)
S
∈
r
s
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
⇛
(
n
s
,
S
′
)
(
C
)
S
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
(
C
)
S
}
)
)
→
m
(
A
′
,
p
′
,
r
s
′
∪
{
(
C
)
S
}
,
s
e
′
)
⇛
(
n
s
,
n
s
(
(
C
)
S
)
)
(
(
C
)
S
1
f
)
(
C
)
S
∉
s
e
′
∖
r
s
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
⇛
(
n
s
,
S
′
)
(
C
)
S
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
(
C
)
S
}
)
)
→
m
(
A
′
,
p
′
,
r
s
′
∪
{
(
C
)
S
}
,
s
e
′
)
⇛
(
n
s
;
n
s
(
(
C
)
S
)
=
(
C
)
S
′
,
n
s
(
(
C
)
S
)
)
(
(
C
)
S
2
f
)
(
C
)
S
∉
r
s
∪
s
e
′
S
:
(
p
,
r
s
)
→
m
(
A
′
,
p
′
,
r
s
′
)
⇛
(
n
s
,
S
′
)
(
C
)
S
:
(
p
,
r
s
,
s
e
∪
(
r
s
∩
{
(
C
)
S
}
)
)
→
m
(
A
′
,
p
′
,
r
s
′
∪
{
(
C
)
S
}
,
s
e
′
)
⇛
(
n
s
,
(
C
)
S
′
)
(
(
C
)
S
3
f
)
S
1
·
v
≔
S
2
:
p
→
m
(
A
′
,
p
′
)
S
1
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
r
s
1
,
s
e
1
)
⇛
(
n
s
1
,
S
1
′
)
S
1
:
p
→
C
s
S
2
:
(
p
1
,
r
s
1
,
s
e
1
)
→
m
(
A
2
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
2
,
S
2
′
)
S
1
·
v
≔
S
2
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
∖
{
S
∈
S
t
m
t
s
∣
C
∈
C
s
∧
C
·
v
∈
f
r
e
e
(
S
)
}
,
s
e
′
)
⇛
(
n
s
1
;
n
s
2
,
S
1
′
·
v
≔
S
2
′
)
(
≔
S
·
v
f
)
o
1
≔
o
2
·
f
(
S
)
:
p
→
m
(
A
′
,
p
′
)
o
2
:
p
→
C
s
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
r
s
1
,
s
e
1
)
⇛
(
n
s
,
S
′
)
{
S
1
,
…
,
S
m
}
=
{
S
f
,
S
r
∣
∃
C
∈
C
s
∧
F
C
(
f
)
=
(
p
,
S
f
,
S
r
)
}
S
i
:
(
p
i
,
r
s
i
,
s
e
i
)
→
m
(
A
i
+
1
,
p
i
+
1
,
r
s
i
+
1
,
s
e
i
+
1
)
⇛
(
n
s
i
,
S
i
′
)
o
1
≔
o
2
·
f
(
S
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
m
+
1
∖
{
S
∈
S
t
m
t
s
∣
o
1
∈
f
r
e
e
(
S
)
}
,
s
e
m
+
1
)
⇛
(
n
s
;
n
s
1
;
…
;
n
s
m
,
o
1
≔
o
2
·
f
(
S
′
)
)
(
≔
o
·
f
f
)
o
1
≔
s
u
p
e
r
·
f
(
S
)
:
p
→
m
(
A
′
,
p
′
)
S
:
(
p
,
r
s
,
s
e
)
→
m
(
A
1
,
p
1
,
r
s
1
,
s
e
1
)
⇛
(
n
s
,
S
′
)
t
h
i
s
:
p
→
C
s
′
S
i
:
(
p
i
,
r
s
i
,
s
e
i
)
→
m
(
A
i
+
1
,
p
i
+
1
,
r
s
i
+
1
,
s
e
i
+
1
)
⇛
(
n
s
i
,
S
i
′
)
{
S
1
,
…
,
S
m
}
=
{
S
f
,
S
r
∣
∃
D
∈
C
s
′
∧
s
u
p
e
r
(
D
,
f
)
=
C
∧
F
C
(
f
)
=
(
p
,
S
f
,
S
r
)
}
o
1
≔
s
u
p
e
r
·
f
(
S
)
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
m
+
1
∖
{
S
∈
S
t
m
t
s
∣
o
1
∈
f
r
e
e
(
S
)
}
,
s
e
m
+
1
)
⇛
(
n
s
;
n
s
1
;
…
;
n
s
m
,
o
1
≔
s
u
p
e
r
·
f
(
S
′
)
)
(
≔
s
u
p
e
r
f
)
o
≔
new
C
:
p
→
m
(
A
′
,
p
′
)
o
:
=
new
C
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
∖
{
S
∈
S
t
m
t
s
∣
o
∈
f
r
e
e
(
S
)
}
,
s
e
)
⇛
(
s
k
i
p
,
o
:
=
new
C
)
(
≔
n
e
w
f
)The following definition generalizes Definition5 and is necessary to express soundness.Definition 9.
Suppose that(
s
,
h
) is a state defined on the set of locationsLoc ([6, Definition 4]). Suppose also that (
s
*
,
h
*
) is a state defined on L
o
c
∪
S
t
m
t
-
n
a
m
e
s. The expression (
s
,
h
)
≡
s
e
(
s
*
,
h
*
) denotes the fact that (
s
,
h
) and (
s
*
,
h
*
) are equivalent with respect to thesemiexpectation typese. More precisely (
s
,
h
)
≡
s
e
(
s
*
,
h
*
) if and only if (1)
for alll
∈
L
o
c
.
s
(
l
)
=
s
*
(
l
), and
(2)
for allS
∈
s
e
.
(
S
,
s
,
h
)
→
m
(
v
,
s
′
,
h
′
)
⇒
s
*
(
s
n
(
S
)
)
=
v.Using semantics notations of Figure4, soundness of the type system of Algorithm 7 is stated as follows.Theorem 10.
Suppose thatS
:
(
p
,
r
s
,
s
e
)
→
m
(
A
′
,
p
′
,
r
s
′
,
s
e
′
)
⇛
(
n
s
,
S
′
) and (
s
,
h
)
≡
s
e
(
s
*
,
h
*
). Then (i)
(
S
,
s
,
h
)
→
m
(
v
,
s
′
,
h
′
)
⇒
∃
(
s
*
′
,
h
*
′
). (
s
′
,
h
′
)
≡
s
e
′
(
s
*
′
,
h
*
′
) and (
S
′
,
s
*
,
h
*
)
→
m
(
v
,
s
*
′
,
h
*
′
);
(ii)
(
S
′
,
s
*
,
h
*
)
→
m
(
v
,
s
*
′
,
h
*
′
)
⇒
∃
(
s
′
,
h
′
). (
s
′
,
h
′
)
≡
s
e
′
(
s
*
′
,
h
*
′
) and (
S
,
s
,
h
)
→
m
(
v
,
s
′
,
h
′
).


## 6. Related Work

The techniques of common subexpression elimination (CSE) [8, 9] are closed to our work. In [10], a type system for CSE of thewhile language is introduced. The work presented in our paper can be realized as a generalization of that presented in [10]. The generality of our work is evident in our language models which are much richer with distributed, pointer, and object-oriented commands. Consequently, the operational semantics that we measure the soundness of our system against are much more involved than that used in [10]. Using new opportunities appearing while scheduling control-intensive designs, the work in [11] introduces a technique that dynamically eliminates CSE. To optimize polynomial expressions (important for applications like domains, computer graphics, and signal processing), the paper [12] generalizes algebraic techniques originally designed for multilevel logic synthesis. The generalization in [12] uses factoring to eliminate common subexpressions of polynomial expressions.There are many analyses for optimizing object-oriented programs. In [13] evolutionary multiobjective optimization methods are used to present a Class-Based Elitist Genetic Algorithm (CBEGA) for testing OOP. A new method to optimize OOP for field access in concurrent object-oriented programs is presented in [14]. This work utilizes the correctness concept that concurrency control must be used by programmers. A new model concurrency abstraction is presented in [15]. This model has the advantage of separating the specification of the synchronization code from the method bodies.The association of a correctness proof with each result of the static analysis is important and needed by applications like proof-carrying code and certified code. The work presented in this paper has the advantage over most related work of constructing these proofs. Adding to the value of using type systems, the proofs constructed in our proposed approach have the form of type derivations. The work in [4, 16, 17] presents many examples of other static analyses that are in the form of type systems.In [18], a technique for flow-insensitive pointer analysis of programs that run on parallel and hierarchical machines and that share memory is introduced. Via a two-level hierarchy, [19, 20] present constraint-based approaches to evaluate locality information and sharing attributes of references. Our language model is a generalization of models presented in [18, 19].Much research acclivities [18, 21] was devoted to analyze distributed programs. This is motivated by the importance of distributed programming as a main stream of programming today. The examining and capturing of causal and concurrent relationships are among important issues to many distributed systems applications. In [22], an analysis that examines the source code of each process constructs an inclusive graph, POG, of the possible behaviors of systems. Data racing bugs [23] can be a side effect of the parallel access of cores of a multicore process to a physically distributed memory. In [23] a technique, called DRARS, is proposed for avoidance and replay of this data race. Parallel programs on DSM or multicore systems can be debugged using DRARS. The classical problems of satisfiability decidability and algorithmic decidability are approached in [24] on the distributed-programs model of message sending. In this work, distributed programs are represented by communicating via buffers.


## 7. Conclusion

This paper introduces new techniques for the analysis offrequent statement and dereference elimination for imperative and object-oriented distributed programs running on parallel machines equipped with hierarchical memories. Type systems are the tools of the techniques presented in this paper. The first sort of proposed type systems defines for program points of a distributed program sets of calculated (ready) statements andmemory accesses. The second sort determines which of theready statements andmemory accesses are used later in the program. The final sort eliminates unnecessary statement computations andmemory accesses.



---

*Source: 839121-2014-04-27.xml*