regehr

I adjusted the text a bit anyhow.

Yes, I'm adding them as I learn about them her (or, in this case, am reminded about them).

Anyone who enjoys this story will likely also enjoy _Tau Zero_ by Poul Anderson.

It turns out it's harder than you'd think to decide whether or not an optimization is a good idea. Of course there are some relatively simple optimizations that are obviously good, but a lot of those have already been implemented. Also, I'm not sure how many people are going to want to add a solver into their compilation path.

On the other hand, if we simply contribute optimizations then all LLVM users benefit.

We're also using Souper to reveal imprecisions in LLVM dataflow analyses such as known bits -- this turns out to work really well.

It's definitely still an active project, but I'm on sabbatical this academic year and have had much less time than usual for my regular research. I'll be getting back to it in June. Also, Raimondas Sasnauskas, who implemented the instruction synthesizer, finished his postdoc position and moved on.

In any case, there's been a lot of progress since I did that UW talk, for example here are some early synthesis results:

http://blog.regehr.org/archives/1252

Meanwhile, Java runs pretty fast.

Replying to myself because depth limit.

Let me try to think of a good way to update the post to capture this better...

Looks like your other comment hit the max reply depth so this will need to finish up, but in any case I don't agree with your reading of the vice versa.

I don't see text that justifies your one-way argument, the bit of 6.2.7.1 that we are talking about says "and vice versa".

It doesn't seem straightforward to me: you're using words like base and derived that aren't in the C standard.

Josh, what's your opinion about this situation?

https://goo.gl/3hz0em

Frama-C can be used in "interpreter mode" where it acts like a checking C interpreter. It then catches a superset of the bugs that would be caught by Valgrind / ASan / UBSan. On the other hand it is slower and harder to use than those tools.

_A Perfect Spy_ has my vote, it's an incredible book.

Also we're all waiting for the strict aliasing checker.

For new code and for actively maintained old code you are perfectly correct. But there is a huge amount of C code we still rely on that isn't getting enough attention and I don't want that getting broken either.

I'm not sure if the QuickCheck people have explored these ideas, perhaps they'll chime in.

Shrinkers, reducers, minimizers -- all are the same thing and all operate using the basic ideas outlined in the original Delta Debugging paper.

Delta Debugging provided a name and a generic algorithm for something that people had already been doing, but they hadn't been calling it anything and hadn't formulated it as an abstract problem.

DD just removes stuff. C-Reduce does lots more, such as inlining functions, rewriting the class hierarchy, instantiating templates, ...

More: http://blog.regehr.org/archives/527

ftp.flux.utah.edu is responding fine for me.

If you can't find what you're looking for we can help, I'm regehr@cs.utah.edu

HintHunt in Paris is awesome.

I'm one of the Souper developers and can offer a few pointers that may be more helpful than the github repo. Here's a somewhat recent blog post showing things that Souper can do:

  http://blog.regehr.org/archives/1252

Here's a talk I gave at the University of Washington last winter (before Souper did synthesis):

  https://www.youtube.com/watch?v=Ux0YnVEaI6A

Recently we've been teaching Souper to use dataflow facts such as LLVM's known bits and demanded bits. Perhaps interestingly, Souper can also teach LLVM how to compute these facts more precisely:

  http://lists.llvm.org/pipermail/llvm-dev/2015-September/089904.html

One really common question about Souper is "why operate on LLVM IR instead of instructions?" One of the main answers is "so that we can interact with dataflow analyses." This isn't something that previous superoptimizers have done. It seems to be working out really well.

Quest was a much earlier tool (ca. 2005) with similar goals: https://github.com/lindig/quest

My kids enjoy finger binary since they only need to count to four in order to give me the finger.

Sure :).

Many people have observed the LLVM appears to move unusually quickly. This is good except when it's bad.

Adrian might have mentioned an important drawback of using LLVM: active effort is required to keep up with it. Many an LLVM-based research project has gotten stuck on 2.9 or 3.2 at which point it starts becoming less and less relevant.

It's not that big of a deal, but active effort is required. The amount of effort depends on how many and which APIs your project uses; for a small/medium project perhaps a couple of hours every couple of weeks.

Pretty good book about this incident: http://www.amazon.com/Idaho-Falls-Americas-Nuclear-Accident/...

Sean, when I visited in 2012 I don't remember any security lines, is this new?

I found the Beijing subway to be far nicer than the ones found in major American cities. No surprise since it's much newer.

One of my favorite things is an old highway in Kansas that emerges from a reservoir that was created in the 1960s and then drops back into the water a short distance away. It's in an out-of-the-way location and we used to go sit on the pavement and drink beer when I was in high school.

The "without requiring you to think too much about the problem space" is pretty huge and it is where solver-based testing currently falls over (in my experience).