<html>
<head>
<meta content="text/html; charset=ISO-8859-1"
http-equiv="Content-Type">
</head>
<body bgcolor="#FFFFFF" text="#000000">
<div class="moz-cite-prefix">Dear Jonas,<br>
<br>
Very cool.<br>
<br>
I've added a link to your paper on the LLVM publications page.
Please feel free to email the list about other papers you or your
group at EPFL publish that use LLVM; we love adding to the links
on the Publications page.<br>
<br>
Regards,<br>
<br>
John Criswell<br>
<br>
On 10/3/14, 4:00 AM, Jonas Wagner wrote:<br>
</div>
<blockquote
cite="mid:CAMRJFfLsmmMbrMybqtb+rjycmKZC_WiSrPxLPijREHcCXYJuTA@mail.gmail.com"
type="cite">
<div dir="ltr">
<div class="markdown-here-wrapper" style="">
<p style="margin:1.2em 0px!important">Dear Robert,</p>
<p style="margin:1.2em 0px!important">a while ago, we had this
idea of using compiler optimizations to increase the
performance of <em>verifying</em> an app, instead of the
performance of <em>executing</em> it. We found that there
were a number of settings that had an effect on verification
performance:</p>
<ul style="margin:1.2em 0px;padding-left:2em">
<li style="margin:0.5em 0px">The amount of loop unswitching
<code
style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px
0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px
solid
rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">-loop-unswitch-threshold=...</code></li>
<li style="margin:0.5em 0px">The amount of loop unrolling <code
style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px
0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px
solid
rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">-unroll-threshold=...</code></li>
<li style="margin:0.5em 0px">The amount of function inlining
<code
style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px
0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px
solid
rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">-inline-threshold=...</code></li>
<li style="margin:0.5em 0px">The amount of jump threading <code
style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px
0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px
solid
rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">-jump-threading-threshold=...</code></li>
<li style="margin:0.5em 0px">Whether to favor branches or
select instructions <code
style="font-size:0.85em;font-family:Consolas,Inconsolata,Courier,monospace;margin:0px
0.15em;padding:0px 0.3em;white-space:pre-wrap;border:1px
solid
rgb(234,234,234);border-top-left-radius:3px;border-top-right-radius:3px;border-bottom-right-radius:3px;border-bottom-left-radius:3px;display:inline;background-color:rgb(248,248,248)">-phi-node-folding-threshold=...
-max-phi-to-fold-per-bb=...</code></li>
</ul>
<p style="margin:1.2em 0px!important">The effect that these
had on verification (in our case, exhaustive symbolic
testing) was quite drastic, with speedups of 95x in some
cases.</p>
<p style="margin:1.2em 0px!important">The core idea behind the
work is that compilers use <em>cost models</em> that tell
them how expensive an operation is. For verification, the
costs are different. I’m writing you because these settings
also have an impact en execution performance. If you find
other parameters that have large effects, I’d be thrilled to
hear about it.</p>
<p style="margin:1.2em 0px!important">Cheers,<br>
Jonas</p>
<p style="margin:1.2em 0px!important">PS: more details on our
experiments: <a moz-do-not-send="true"
href="http://infoscience.epfl.ch/record/186012?ln=en%3F">http://infoscience.epfl.ch/record/186012?ln=en
</a></p>
<div
title="MDH:RGVhciBSb2JlcnQsPGRpdj48YnI+PC9kaXY+PGRpdj5hIHdoaWxlIGFnbywgd2UgaGFkIHRoaXMgaWRlYSBvZiB1c2luZyBjb21waWxlciBvcHRpbWl6YXRpb25zIHRvIGluY3JlYXNlIHRoZSBwZXJm
b3JtYW5jZSBvZiAqdmVyaWZ5aW5nKiBhbiBhcHAsIGluc3RlYWQgb2YgdGhlIHBlcmZvcm1hbmNl
IG9mICpleGVjdXRpbmcqIGl0LiBXZSBmb3VuZCB0aGF0IHRoZXJlIHdlcmUgYSBudW1iZXIgb2Yg
c2V0dGluZ3MgdGhhdCBoYWQgYW4gZWZmZWN0IG9uIHZlcmlmaWNhdGlvbiBwZXJmb3JtYW5jZTo8
L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2Pi0gVGhlIGFtb3VudCBvZiBsb29wIHVuc3dpdGNoaW5n
IGAtbG9vcC11bnN3aXRjaC10aHJlc2hvbGQ9Li4uYDwvZGl2PjxkaXY+LSBUaGUgYW1vdW50IG9m
IGxvb3AgdW5yb2xsaW5nIGAtdW5yb2xsLXRocmVzaG9sZD0uLi5gPC9kaXY+PGRpdj4tIFRoZSBh
bW91bnQgb2YgZnVuY3Rpb24gaW5saW5pbmcgYC1pbmxpbmUtdGhyZXNob2xkPS4uLmA8L2Rpdj48
ZGl2Pi0gVGhlIGFtb3VudCBvZiBqdW1wIHRocmVhZGluZyBgLWp1bXAtdGhyZWFkaW5nLXRocmVz
aG9sZD0uLi5gPC9kaXY+PGRpdj4tIFdoZXRoZXIgdG8gZmF2b3IgYnJhbmNoZXMgb3Igc2VsZWN0
IGluc3RydWN0aW9ucyBgLXBoaS1ub2RlLWZvbGRpbmctdGhyZXNob2xkPS4uLiAtbWF4LXBoaS10
by1mb2xkLXBlci1iYj0uLi5gPC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5UaGUgZWZmZWN0IHRo
YXQgdGhlc2UgaGFkIG9uIHZlcmlmaWNhdGlvbiAoaW4gb3VyIGNhc2UsIGV4aGF1c3RpdmUgc3lt
Ym9saWMgdGVzdGluZykgd2FzIHF1aXRlIGRyYXN0aWMsIHdpdGggc3BlZWR1cHMgb2YgOTV4IGlu
IHNvbWUgY2FzZXMuPC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5UaGUgY29yZSBpZGVhIGJlaGlu
ZCB0aGUgd29yayBpcyB0aGF0IGNvbXBpbGVycyB1c2UgKmNvc3QgbW9kZWxzKiB0aGF0IHRlbGwg
dGhlbSBob3cgZXhwZW5zaXZlIGFuIG9wZXJhdGlvbiBpcy4gRm9yIHZlcmlmaWNhdGlvbiwgdGhl
IGNvc3RzIGFyZSBkaWZmZXJlbnQuIEknbSB3cml0aW5nIHlvdSBiZWNhdXNlIHRoZXNlIHNldHRp
bmdzIGFsc28gaGF2ZSBhbiBpbXBhY3QgZW4gZXhlY3V0aW9uIHBlcmZvcm1hbmNlLiBJZiB5b3Ug
ZmluZCBvdGhlciBwYXJhbWV0ZXJzIHRoYXQgaGF2ZSBsYXJnZSBlZmZlY3RzLCBJJ2QgYmUgdGhy
aWxsZWQgdG8gaGVhciBhYm91dCBpdC48L2Rpdj48ZGl2Pjxicj48L2Rpdj48ZGl2PkNoZWVycyw8
L2Rpdj48ZGl2PkpvbmFzPC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj48YnI+PC9kaXY+PGRpdj5Q
UzogbW9yZSBkZXRhaWxzIG9uIG91ciBleHBlcmltZW50czogaHR0cDovL2luZm9zY2llbmNlLmVw
ZmwuY2gvcmVjb3JkLzE4NjAxMj9sbj1lbjwvZGl2PuKAiw=="
style="height:0;font-size:0em;padding:0;margin:0"></div>
</div>
</div>
<br>
<fieldset class="mimeAttachmentHeader"></fieldset>
<br>
<pre wrap="">_______________________________________________
LLVM Developers mailing list
<a class="moz-txt-link-abbreviated" href="mailto:LLVMdev@cs.uiuc.edu">LLVMdev@cs.uiuc.edu</a> <a class="moz-txt-link-freetext" href="http://llvm.cs.uiuc.edu">http://llvm.cs.uiuc.edu</a>
<a class="moz-txt-link-freetext" href="http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev">http://lists.cs.uiuc.edu/mailman/listinfo/llvmdev</a>
</pre>
</blockquote>
<br>
<br>
<pre class="moz-signature" cols="72">--
John Criswell
Assistant Professor
Department of Computer Science, University of Rochester
<a class="moz-txt-link-freetext" href="http://www.cs.rochester.edu/u/criswell">http://www.cs.rochester.edu/u/criswell</a></pre>
</body>
</html>