regehr

Here's a different study with similar findings:

http://www.econ.ucdavis.edu/faculty/scarrell/profqual2.pdf

"... our results show that student evaluations reward professors who increase achievement in the contemporaneous course being taught, not those who increase deep learning."

Watching TV/movies is definitely something that we learn to do, though most of us learned so early that we no longer remember it.

Source: anecdotal evidence from friends/relatives who observed childrens' reactions when first exposed to TV/movies when they were relatively old.

Often, the sound from the scene following the cut precedes the cut itself. There must be a name for this technique and a reason for it-- anyone know?

Awesome books on this topic:

http://www.amazon.com/Commissar-Vanishes-Falsification-Photo...

http://www.amazon.com/Photo-Fakery-History-Deception-Manipul...

512 kbps DSL -- just barely, frustratingly capable of watching Netflix at the worst quality level

I bought a house about 1 mile from downtown Salt Lake City in 2008 and it took until last year to get a decent internet connection (from Comcast). First world problems!

It's usually a combination of (1) being afraid of sounding unrigorous or unintelligent and (2) not knowing any better and having been trained on lots of bad examples

This book is excellent: http://www.amazon.com/Stylish-Academic-Writing-Helen-Sword/d...

I routinely forego summer salary in order to make sure the students are fed. This works because I receive a perfectly adequate 9-month salary from the state (and also my household has two incomes).

I'm the author of this piece. Everyone should go try out Alive instead of reading the blogpost:

https://github.com/nunoplopes/alive

Alive automates all of the stuff described in the post. Here's some info:

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

Also we gave a talk at the LLVM Dev meeting a few weeks ago, the talk doesn't seem to be online (yet?) but here are David's slides:

http://www.cs.utah.edu/~regehr/devconf14.pdf

Does this example help?

http://markshroyer.com/2012/06/c-both-true-and-false/

The linked articles by Chris Lattner explain why this is very difficult.

http://blog.llvm.org/2011/05/what-every-c-programmer-should-...

We found that UNSAFE/TRUSTED code wasn't needed very often. YMMV.

Wrong, incorrect Deputy annotations (other than the UNSAFE annotation) cannot lead to memory safety violations. I edited to post a bit to make this more clear.

It's not just the function that becomes undefined, it's the entire program. There's literally nothing that the compiler is supposed to do following undefined behavior.

Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.

I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here:

http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf

John Regehr (me) did in fact find something like 11 bugs in CompCert, most of which caused it to emit wrong code. But the bugs were not in the proved part.

Metamorphic testing means taking an existing test case and mutating it into a new test case that produces the same answer (or at least an answer that can be easily predicted).

Property-based testing is, as far as I can tell, a meaningless term since all testing is property-based.

4. PROFIT

Please do, if it is not too much trouble.

I'm still interested in somehow creating such a test suite, Pascal -- one that is designed to test corner cases in the standard rather than testing corner cases in the optimizer. It would somehow be derived from various formalizations of the standard such as yours, Xavier's, Chucky's.

Pascal, have you reported the bug? Xuejun is doing some Csmith work right now and we can probably get him to fix it.

Sorry if I was unclear. The missing folds are at the C level. At the LLVM level we definitely run InstCombine before Souper (otherwise we would find lots of optimizations that are not actually missing).

The immediate goal is simply to inspire LLVM hackers to improve the instruction combiner.

But yes, these results can be made persistent and used directly to optimize code. We are working on it.

Applying this tool to code emitted by GHC or rustc is trivial, it's all LLVM bitcode. One of my ideas is that these languages are a good use case for a superoptimizer since the LLVM passes aren't tuned for them, but we'll have to see how that plays out.

They're just following the financial jobs!

I wasn't much of an outdoors person before moving to Utah and really, really like that stuff now too.

A major natural disaster is a certainty in the SLC area: we're surrounded by active faults.

I live in SLC and have met quite a few people over the last few years who lost jobs in the financial sector, usually in the NYC area, and subsequently moved to Utah.

Fucking Dreamhost...

I always find it depressing when I take a picture by moonlight and it ends up looking very much like a picture taken by sunlight, as opposed to looking like the scene looks to our eyes. Always have to keep in mind that a CCD != rods and cones.

Sensitivity is nice but as far as I'm concerned, dynamic range is the main thing that's needed in digital photography. DSLR sensors have gotten much, much better over the last 10 years but there's still plenty of room for improvement.

Same here. Perhaps it uses a direct drawing API.