regehr | 11 years ago | on: Proposal for a Friendly Dialect of C
regehr's comments
regehr | 11 years ago | on: Non-Transparent Memory Safety
We found that UNSAFE/TRUSTED code wasn't needed very often. YMMV.
regehr | 11 years ago | on: Non-Transparent Memory Safety
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.
regehr | 11 years ago | on: Undefined behavior can result in time travel
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.
regehr | 11 years ago | on: Sel4: We’re going open source
Absence of undefined behavior in the C implementation is of course one of the things covered by the seL4 proof.
regehr | 11 years ago | on: Sel4: We’re going open source
I never wrote up all the details (which seemed somewhat mundane, since the bugs were in unproved code) but see Section 3.1 here:
regehr | 11 years ago | on: Sel4: We’re going open source
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.
regehr | 11 years ago | on: Finding Compiler Bugs by Removing Dead Code
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.
regehr | 11 years ago | on: Finding Compiler Bugs by Removing Dead Code
4. PROFIT
regehr | 11 years ago | on: Finding Compiler Bugs by Removing Dead Code
Please do, if it is not too much trouble.
regehr | 11 years ago | on: Finding Compiler Bugs by Removing Dead Code
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.
regehr | 11 years ago | on: Finding Compiler Bugs by Removing Dead Code
Pascal, have you reported the bug? Xuejun is doing some Csmith work right now and we can probably get him to fix it.
regehr | 12 years ago | on: Early Superoptimizer Results
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).
regehr | 12 years ago | on: Early Superoptimizer Results
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.
regehr | 12 years ago | on: Stellar Wind (code name)
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.
regehr | 12 years ago | on: Stellar Wind (code name)
A major natural disaster is a certainty in the SLC area: we're surrounded by active faults.
regehr | 12 years ago | on: Stellar Wind (code name)
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.
regehr | 13 years ago | on: The declining value of the MS in Computer Science
Fucking Dreamhost...
regehr | 13 years ago | on: Canon develops 35 mm full-frame CMOS sensor for video capture
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.
regehr | 13 years ago | on: Minecraft: Pi Edition is available for download
Same here. Perhaps it uses a direct drawing API.
http://blog.llvm.org/2011/05/what-every-c-programmer-should-...