<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 href="http://infoscience.epfl.ch/record/186012?ln=en​">http://infoscience.epfl.ch/record/186012?ln=en​</a></p>
<div title="MDH:RGVhciBSb2JlcnQsPGRpdj48YnI+PC9kaXY+PGRpdj5hIHdoaWxlIGFnbywgd2UgaGFkIHRoaXMg
aWRlYSBvZiB1c2luZyBjb21waWxlciBvcHRpbWl6YXRpb25zIHRvIGluY3JlYXNlIHRoZSBwZXJm
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>