<!DOCTYPE HTML PUBLIC "-//W3C//DTD HTML 4.0 Transitional//EN">
<HTML xmlns="http://www.w3.org/TR/REC-html40" xmlns:v =
"urn:schemas-microsoft-com:vml" xmlns:o =
"urn:schemas-microsoft-com:office:office" xmlns:w =
"urn:schemas-microsoft-com:office:word" xmlns:m =
"http://schemas.microsoft.com/office/2004/12/omml"><HEAD>
<META http-equiv=Content-Type content="text/html; charset=us-ascii">
<META content="MSHTML 6.00.6000.16544" name=GENERATOR>
<STYLE>
<!--
/* Font Definitions */
@font-face
{font-family:"Cambria Math";
panose-1:2 4 5 3 5 4 6 3 2 4;}
@font-face
{font-family:Calibri;
panose-1:2 15 5 2 2 2 4 3 2 4;}
/* Style Definitions */
p.MsoNormal, li.MsoNormal, div.MsoNormal
{margin:0in;
margin-bottom:.0001pt;
font-size:11.0pt;
font-family:"Calibri","sans-serif";}
a:link, span.MsoHyperlink
{mso-style-priority:99;
color:blue;
text-decoration:underline;}
a:visited, span.MsoHyperlinkFollowed
{mso-style-priority:99;
color:purple;
text-decoration:underline;}
span.EmailStyle17
{mso-style-type:personal-compose;
font-family:"Calibri","sans-serif";
color:windowtext;}
.MsoChpDefault
{mso-style-type:export-only;}
@page Section1
{size:8.5in 11.0in;
margin:1.0in 1.0in 1.0in 1.0in;}
div.Section1
{page:Section1;}
-->
</STYLE>
<!--[if gte mso 9]><xml>
<o:shapedefaults v:ext="edit" spidmax="1026" />
</xml><![endif]--><!--[if gte mso 9]><xml>
<o:shapelayout v:ext="edit">
<o:idmap v:ext="edit" data="1" />
</o:shapelayout></xml><![endif]--></HEAD>
<BODY lang=EN-US vLink=purple link=blue>
<DIV dir=ltr align=left><FONT face=Arial color=#0000ff size=2><SPAN
class=645534519-13122007>Frances Perry will present her preFPO on Wednesday
December 19 at 10:30 AM in </SPAN></FONT></DIV>
<DIV dir=ltr align=left><FONT face=Arial color=#0000ff size=2><SPAN
class=645534519-13122007>Room 402. The members of her committee are:
David Walker, advisor; Andrew </SPAN></FONT></DIV>
<DIV dir=ltr align=left><FONT face=Arial color=#0000ff size=2><SPAN
class=645534519-13122007>Appel and David Tarditi (Microsoft), readers; David
August and Margaret Martonosi, </SPAN></FONT></DIV>
<DIV dir=ltr align=left><FONT face=Arial color=#0000ff size=2><SPAN
class=645534519-13122007>nonreaders. A copy of her abstract follows
below. Everyone is invited to attend her talk.</SPAN></FONT></DIV><BR>
<DIV class=OutlookMessageHeader lang=en-us dir=ltr align=left><FONT
face=Calibri>Formal Reasoning about Transient Faults<o:p></o:p></FONT></DIV>
<DIV class=Section1>
<P class=MsoNormal><o:p> </o:p></P>
<P class=MsoNormal>My thesis research focuses on guaranteeing that software is
reliable in the presence of transient faults. A transient fault occurs
when an energetic particle strikes a chip and causes a change in state in the
processor. These faults do not cause permanent damage, but they may affect the
computation that is currently executing. Transient faults have been shown to be
the cause of crashes at major companies, and current technology trends, such as
decreasing transistor size, will make future processors much more
susceptible.<o:p></o:p></P>
<P class=MsoNormal><o:p> </o:p></P>
<P class=MsoNormal>Researchers in architecture and compilers have already
developed a number of different solutions using software, hardware or a
combination of the two. The general approach of all these solutions is to
duplicate computations and check for consistency between the copies.
Unfortunately, generating correct fault-tolerant code is difficult, and there
has been very little research on verifying these techniques. Testing is rarely
sufficient because full coverage would require testing all combinations of
features in conjunction with all combinations of faults.<o:p></o:p></P>
<P class=MsoNormal><o:p> </o:p></P>
<P class=MsoNormal>Along with colleagues, I designed a new type system that
guarantees that faulty executions of a well-typed program are identical to
non-faulty executions up to the point where a fault is detected. We use a hybrid
hardware-software solution in which an added hardware queue buffers the stores
from the original computation and only writes them to memory if the duplicate
computation agrees. Faults can occur at any point and randomly modify a register
or queue value. The assembly-level type system tracks information about the two
computations which we use to rigorously prove that well-typed programs satisfy
reliability properties. We use these reliability properties to show that all
executions containing a single fault will always detect the fault before the
difference from non-faulty versions becomes observable.<o:p></o:p></P>
<P class=MsoNormal><o:p> </o:p></P>
<P class=MsoNormal>More recently, I designed a typed system for reasoning about
software solutions for control-flow faults. Control-flow faults arise when a
fault causes a jump or branch instruction to transfer control to an unexpected
code address. Current software solutions can detect most, but not all,
control-flow faults. I formally analyzed a subset of these solutions that can
detect any fault that causes incorrect control transfers between basic blocks.
Similarly to the previous work, this is accomplished by using a type system to
track reliability properties. However, the type system contains new techniques
that allow it to reason soundly even when code transfers to an unexpected
location and continues executing. Here, I proved that executions with a single
fault will visit at most one incorrect block before the fault is
detected.<o:p></o:p></P>
<P class=MsoNormal><o:p> </o:p></P></DIV></BODY></HTML>