Embedded in Academia

Month: October 2010

  • A Quick Look at Code Size

    As part of some recent work we compiled 1,000,000 randomly generated C programs to x86 using a variety of versions of GCC and LLVM. Over the next few weeks I’ll post about some of the different things we learned from this experiment; today’s post is about code size. Each program was compiled at -O0, -O1,…

  • GCC Summit Talk

    I’m at the 2010 GCC Summit in Ottawa today. There’s a lot of interesting work going on; I’ll probably write a more detailed post later. In the meantime, the slides from my talk on finding compiler bugs are below. GCC Summit 2010 View more presentations from regehr.

  • Verifying a Driver

    Last week my student Jianjun Duan gave a talk about his PhD work at the Workshop for Systems Software Verification in Vancouver. Although preliminary — he verified only three small functions — this work is pretty cool. Jianjun started with a model for the ARM instruction set in HOL4 and augmented it so that memory-mapped…

  • Maze Rejection #2

    Bill and I planned a backpacking trip to the Fins area of the Maze District during Spring Break 2010, but were foiled when several feet of abnormally late snow made the Flint Trail (the “roughest routinely traveled road in Utah”) impassable. This week, during the University of Utah’s Fall Break, we tried again, but were…

  • More Saturating Arithmetic

    In a previous post I guessed that 91 bytes was close to the minimum size for implementing signed and unsigned saturating 32-bit addition and subtraction on x86. A commenter rightly pointed out that it should be possible to do better. Attached is my best shot: 83 bytes. Given the crappy x86 calling convention I’m going…

  • Fun With Saturating Arithmetic

    An assignment that I often give my Advanced Embedded Systems class early in the semester is to implement saturating versions of signed and unsigned addition and subtraction. Saturating operations “stick” at the maximum or minimum value. (INT_MAX +sat 1) therefore evaluates to INT_MAX. The only wrinkle in the assignment is that solutions must be capable…