Information Technology Reference
In-Depth Information
Tabl e 1.
Measurements
Pass
Original Witness Avg. runtime in
LOC Gen. LOC ms (overhead multiple)
Simple Constant Propagation
99
118
101.36 (12x)
Dead Code Elimination
135
37
41.71 (10x)
Loop Invariant Code Motion
895
65
200.03 (31x)
The framework design is based on the following main components: Op-
timizer/Analyzer, Witness Generator, Translator, Witness Checker, Invariant
Propagator. The
Optimizer/Analyzer
augments the LLVM pass to store the anal-
ysis invariants; the
Witness Generator
takes care of generating the optimization-
specific witness using the invariants found during the analysis; the
Translator
builds the transition relation of a given CFG and is usually run over the target
and the source of every optimization pass; and the
Witness Checker
combines
the generated witness and the target and source transition relation to verify
that the witness is a stuttering simulation using Z3. In addition, an
Invariant
Propagator
uses the witness relation and symbolic manipulations using Z3 to
propagate invariants (computed during analysis or externally supplied) from a
source program to the target. Out of these five components only the first two
are optimization-specific.
Table 1 gives measurements which show (a) the effort required to write a
witness generator and (b) the overhead incurred to check the correctness of
witnesses. The implemented passes are chosen by their commonality, ease of
study and for clearly highlighting some of the critical parts of the framework. The
lines of code (LOC) for witness generation are those that are required specifically
for that optimization. In addition, there is code which is common to all passes,
and implements a witness checker, the invariant propagator, the translator, and
basic definitions, amounting in total to approximately 1 KLOC.
The LOC numbers are encouraging: compared to the effort required to define
the optimization, the effort required to define a witness generator is high only
for the simple constant propagation pass, but is much lower for the other two
passes. The run-time overhead measures the overhead of witness generation and
checking compared to the optimization time, measured with the
time-passes
tool of the LLVM optimizer. The current runtime overhead for witness checking
is very high. However, this is a rough, unoptimized implementation, so we expect
this overhead to reduce substantially as the implementation is improved.
4 Conclusion and Related Work
The implementation described here is a work in progress, and is currently at an
early stage. Support for the instruction set of the IR is limited to binary oper-
ations over integers, return, branch (conditional and unconditional), compare,
and
φ
nodes. (This set suces to describe
while
programs over the integers.) For
