[llvm-commits] CVS: llvm-www/pubs/2009-05-EnsuringCorrectnessOfCompiledCode.html 2009-05-EnsuringCorrectnessOfCompiledCode.pdf 2009-05-EnsuringCorrectnessOfCompiledCode.ps.gz pubs.js
Chris Lattner
sabre at nondot.org
Fri May 8 09:25:52 PDT 2009
Changes in directory llvm-www/pubs:
2009-05-EnsuringCorrectnessOfCompiledCode.html added (r1.1)
2009-05-EnsuringCorrectnessOfCompiledCode.pdf added (r1.1)
2009-05-EnsuringCorrectnessOfCompiledCode.ps.gz added (r1.1)
pubs.js updated: 1.12 -> 1.13
---
Log message:
Add Anna Zaks' Ph.D. thesis, "Ensuring Correctness of Compiled Code"
---
Diffs of the changes: (+100 -0)
2009-05-EnsuringCorrectnessOfCompiledCode.html | 92 ++++++++++++++++++++++++
2009-05-EnsuringCorrectnessOfCompiledCode.pdf | 0
2009-05-EnsuringCorrectnessOfCompiledCode.ps.gz | 0
pubs.js | 8 ++
4 files changed, 100 insertions(+)
Index: llvm-www/pubs/2009-05-EnsuringCorrectnessOfCompiledCode.html
diff -c /dev/null llvm-www/pubs/2009-05-EnsuringCorrectnessOfCompiledCode.html:1.1
*** /dev/null Fri May 8 11:23:16 2009
--- llvm-www/pubs/2009-05-EnsuringCorrectnessOfCompiledCode.html Fri May 8 11:23:04 2009
***************
*** 0 ****
--- 1,92 ----
+ <!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.01 Transitional//EN">
+ <html>
+ <head>
+ <meta http-equiv="Content-Type" content="text/html; charset=UTF-8" />
+ <link rel="stylesheet" href="../llvm.css" type="text/css" media="screen" />
+ <title>Ensuring Correctness of Compiled Code</title>
+ </head>
+ <body>
+
+ <div class="pub_title">
+ Ensuring Correctness of Compiled Code
+ </div>
+ <div class="pub_author">
+ Ganna Zaks, Ph.D. thesis
+ </div>
+
+ <h2>Abstract:</h2>
+ <blockquote>
+ <p>
+ Traditionally, the verification effort is applied to the abstract
+ algorithmic descriptions of the underlining software. However, even
+ well understood protocols such as Peterson’s protocol for mutual
+ exclusion, whose algorithmic description takes only half a page, have
+ published implementations that are erroneous. Furthermore, the
+ semantics of the implementations can be altered by optimizing
+ compilers, which are very large applications and, consequently, are
+ bound to have bugs. Thus, it is highly desirable to ensure the
+ correctness of the compiled code especially in safety critical and
+ high-assurance software. This dissertation describes two alternative
+ approaches that bring us closer to solving the problem.</p>
+
+ <p>First, we present Compiler Validation via Analysis of the
+ Cross-Product (CoVaC) - a deductive framework for proving program
+ equivalence and its application to automatic verification of
+ transformations performed by optimizing compilers. To leverage the
+ existing program analysis techniques, we reduce the equivalence
+ checking problem to analysis of one system - a cross-product of the
+ two input programs. We show how the approach can be effectively used
+ for checking equivalence of single-threaded programs that are
+ structurally similar. Unlike the existing frameworks, our approach
+ accommodates absence of compiler annotations and handles most of the
+ classical intraprocedural optimizations such as constant folding,
+ reassociation, common subexpression elimination, code motion, branch
+ optimizations, and others. In addition, we have developed rules for
+ translation validation of interprocedural optimizations, which can be
+ applied when compiler annotations are available.</p>
+
+ <p>
+ The second contribution is the pancam framework for model checking
+ multi-threaded C programs. pancam first compiles a multi-threaded C
+ program into optimized bytecode format. The framework relies on Spin,
+ an existing explicit state model checker, to orchestrate the program's
+ state space search. However, the program transitions and states are
+ computed by the pancam bytecode interpreter. A feature of our approach
+ is that not only pancam checks the actual implementation, but it can
+ also check the code after compiler optimizations. Pancam addresses the
+ state space explosion problem by allowing users to define data
+ abstraction functions and to constrain the number of allowed context
+ switches. We also describe a partial order reduction method that
+ reduces context switches using dynamic knowledge computed on-the-fly,
+ while being sound for both safety and liveness properties.
+ </p>
+
+ </blockquote>
+
+ <h2>Published:</h2>
+ <blockquote>
+ "Ensuring Correctness of Compiled Code", Ganna Zaks,<br>
+ <i>Ph.D. Thesis</i>, Computer Science Dept., New York University, New York, NY, May 2009.<br>
+ </blockquote>
+
+ <h2>Download Presentation:</h2>
+ <ul>
+ <li><a href="2009-05-EnsuringCorrectnessOfCompiledCode.pdf">Ensuring Correctness of Compiled Code</a> (PDF)</li>
+ <li><a href="2009-05-EnsuringCorrectnessOfCompiledCode.ps.gz">Ensuring Correctness of Compiled Code</a> (PS)</li>
+ </ul>
+
+ <h2>BibTeX Entry:</h2>
+
+ <blockquote>
+ @PhdThesis{GZAKS:PHD,
+ author = {Ganna Zaks},
+ title = "{Ensuring Correctness of Compiled Code}",
+ school = "{Computer Science Dept., New York University}",
+ year = {2009},
+ address = {New York, NY},
+ month = {May}
+ }
+ </blockquote>
+
+ </body>
+ </html>
Index: llvm-www/pubs/2009-05-EnsuringCorrectnessOfCompiledCode.pdf
Index: llvm-www/pubs/2009-05-EnsuringCorrectnessOfCompiledCode.ps.gz
Index: llvm-www/pubs/pubs.js
diff -u llvm-www/pubs/pubs.js:1.12 llvm-www/pubs/pubs.js:1.13
--- llvm-www/pubs/pubs.js:1.12 Wed Mar 25 00:57:52 2009
+++ llvm-www/pubs/pubs.js Fri May 8 11:23:05 2009
@@ -1,6 +1,14 @@
// The array should be sorted reverse-chronologically, and will be displayed on
// the page in the order listed.
var PUBS = [
+ {url: '2009-05-EnsuringCorrectnessOfCompiledCode.html',
+ title: 'Ensuring Correctness of Compiled Code',
+ author: 'Ganna Zaks',
+ published: "Ph.D. Thesis, Computer Science Dept., New York University",
+ location: "New York, NY",
+ month: 5,
+ year: 2009},
+
{url: '2009-03-CGO-ESoftCheck.html',
title: 'ESoftCheck: Removal of Non-vital Checks for Fault Tolerance',
author: 'Jing Yu, Maria Jesus Garzaran, Marc Snir',
More information about the llvm-commits
mailing list