Michael Carbin


I am on the academic job market!
Materials: CV, Research Statement, Teaching Statement

I am a Ph.D. Candidate in Electrical Engineering and Computer Science at MIT. I am interested in the design of programming systems that deliver improved performance and resilience by incorporating approximate computing and self-healing.

News


  • Rely makes Slashdot and MITNews.
  • Rely wins a Best Paper Award at OOPSLA '13.
  • Rely aka "Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware" accepted to OOPSLA '13.
  • "Reasoning about Relaxed Programs" voted Best Student Talk at POPL'13 Student Session.
  • "Reasoning about Relaxed Programs" in MITnews,
  • Bolt on Slashdot, Ars Technica, and MITnews

Selected Research Projects


Not all parts of a program are created equal: some parts are more critical to a program's reliability and correctness than others. This observation allows us as researchers to explore aggressive program optimization and transformation methods that identify less critical regions of a program's code that can be replaced and approximated, producing a new program with better reliability or performance that still satisfies a developer's requirements.

Rely: a language for building reliable programs on unreliable hardware

Emerging high-performance architectures are anticipated to contain unreliable components that may exhibit soft errors, which silently corrupt the results of computations. Full detection and masking of soft errors is challenging, expensive, and, for some applications, unnecessary. For example, approximate computing applications (such as multimedia processing, machine learning, and big data analytics) can often naturally tolerate soft errors.

Rely is a programming language that enables developers to control the quantitative reliability of an application -- namely, the probability that it produces the correct result when executed on unreliable hardware. Rely allows developers to specify the reliability requirements for each value that a function produces and then use Rely's static program analysis system to verify that the function satisfies its specification. Rely therefore enables developers to productively exploit the performance benefits of emerging high-performance architectures while still maintaining control of the program's behavior.

Papers: OOPSLA '13 (slides)
Press: Slashdot, MITNews

Reasoning About Relaxed Approximate Programs

Approximate program transformations such as task skipping, loop perforation, approximate function memoization, and approximate data types produce programs that can execute at a variety of points in an underlying performance versus accuracy tradeoff space. Namely, these transformed programs trade accuracy of their results for increased performance by dynamically and nondeterministically modifying variables that control their execution. I have defined such transformed programs as relaxed programs -- they have been extended with additional nondeterminism to relax their semantics and enable greater flexibility in their execution.

This project provides programming language constructs for developing relaxed programs. It also provides proof rules for reasoning about acceptability properties, which are the key correctness properties of relaxed programs that enable them to have a range of acceptable executions. Specifically, these proof rules enable programmers to directly specify and verify relational properties that characterize the desired correctness relationships, such as accuracy, between the values of variables in a program's original semantics (before the transformation) and its relaxed semantics. Moreover, these rules enable programmers to reuse correctness properties that hold for the original program to efficiently verify the relaxed.

Paper: PLDI '12 (slides)
Press: MITNews

Bolt: dynamically detecting and escaping infinite loops in off-the-shelf software

Infinite loops can make applications unresponsive. Potential problems include lost work or output, denied access to application functionality, and a lack of responses to urgent events. Bolt is a novel system for dynamically detecting and escaping infinite loops. At the user’s request, Bolt attaches to an application to monitor its progress. Specifically, Bolt records the program state at the start of each loop iteration. If two consecutive loop iterations produce the same state, Bolt reports to the user that the application is in an infinite loop. At the user’s option, Bolt can then transfer control to a statement following the loop, thereby allowing the application to escape the infinite loop and ideally continue its productive execution.

Bolt operates on stripped x86 and x64 binaries, dynamically attaches and detaches to and from the program as needed, and dynamically detects loops and creates program state checkpoints to enable exploration of different escape strategies. Bolt can detect and escape from loops in off-the- shelf software, without available source code, and with no overhead in standard production use.

Papers: ECOOP '11 (appendix, slides), OOPSLA '12 (slides)
Press: Slashdot, Ars Technica, MIT News

Snap: Automatically Identifying Critical Input Regions and Code in Applications

Applications that process complex inputs often react in different ways to changes in different regions of the input. Small changes to forgiving regions induce correspondingly small changes in the behavior and output. Small changes to critical regions, on the other hand, can induce disproportionally large changes in the behavior or output. This paper presents Snap, a system for automatically classifying each input field and corresponding regions of code as critical or forgiving. Given an application and one or more inputs, Snap uses targeted input fuzzing in combination with dynamic execution and influence tracing to classify regions of input fields and code as critical or forgiving. Snap works well in practice and therefore enables developers and programming systems to automatically identify portions of the program that may be amenable change.

Paper: ISSTA '10 (slides)

Conference Papers


Verifying Quantitative Reliability for Programs that Execute on Unreliable Hardware
Michael Carbin, Sasa Misailovic, and Martin C. Rinard
OOPSLA '13 (Best Paper Award) — Object-Oriented Programming, Systems, Languages, and Applications.
Paper Slides
Press: Slashdot MITNews

Bolt: On-Demand Infinite Loop Escape in Unmodified Binaries
Michael Kling, Sasa Misailovic, Michael Carbin, and Martin C. Rinard
OOPSLA '12 — Object-Oriented Programming, Systems, Languages, and Applications
Paper Slides

Proving Acceptability Properties of Relaxed Nondeterministic Approximate Programs
Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard
PLDI '12 — Programming Language Design and Implementation
Paper Slides

Automatic Input Rectification
Fan Long, Vijay Ganesh, Michael Carbin, Stelios Sidirolgou, and Martin C. Rinard
ICSE '12 — International Conference on Software Engineering

Detecting and Escaping Infinite Loops with Jolt
Michael Carbin, Sasa Misailovic, Michael Kling, and Martin C. Rinard
ECOOP '11 — European Conference on Object-Oriented Programming
Paper Appendix Slides
Press: Slashdot Ars Technica MIT News

Dynamic Knobs for Power-Aware Computing
Henry Hoffman, Stelios Sidiroglou, Michael Carbin, Sasa Misailovic,
Anant Agarwal, and Martin Rinard
ASPLOS '11 — Architectural Support for Programming Languages and Operating Systems
Paper

Automatically Identifying Critical Input Regions and Code Regions in Applications
Michael Carbin and Martin C. Rinard
ISSTA '10 — International Symposium of Software Testing And Analysis
Paper

Automatically Patching Errors in Deployed Software
Jeff H. Perkins, Sunghun Kim, Sam Larsen, Saman Amarasinghe, Jonathan Bachrach, Michael Carbin, Carlos Pacheco, Frank Sherwood, Stelios Sidiroglou, Greg Sullivan, Weng-Fai Wong, Yoav Zibin, Michael D. Ernst and Martin C. Rinard
SOSP '09 — Symposium on Operating Systems Principles
Press: Slashdot MIT News MIT Technology Review

Transactional Collection Classes
Brian D. Carlstrom, Austen McDonald, Michael Carbin, Christos Kozyrakis, and Kunle Olukotun
PPoPP '07 — Principles and Practice of Parallel Computing
Paper

Reflective Program Generation with Patterns
Manuel Fähndrich, Michael Carbin, James R. Larus
GPCE '06 — Generative Programming and Component Engineering
Paper

Using Datalog with Binary Decision Diagrams for Program Analysis
John Whaley, Dzintars Avots, Michael Carbin, Monica S. Lam
APLAS '05 — Asian Symposium Programming Languages and Systems 2005
Paper

Context-Sensitive Program Analysis as Database Queries
Monica S. Lam, John Whaley, V, Benjamin Livshits, Michael Martin, Dzintars Avots,
Michael Carbin, and Christopher Unkel
PODS '05 — Principles of Database Systems (Invited paper)
Paper

Workshop Papers


Verified Integrity Properties for Safe Approximate Program Transformations
Michael Carbin, Deokhwan Kim, Sasa Misailovic, and Martin C. Rinard
PEPM '13 — Partial Evaluation and Program Manipulation, co-located with POPL

(Relative) Safety Properties for Relaxed Appproximate Programs
Michael Carbin and Martin C. Rinard
RACES '12 — Relaxing Synchronization for Multicore and Manycore Scalability,
co-located with OOPSLA

Cryptographic Path Hardening: Hiding Vulnerabilities in Software using Cryptography
Vijay Ganesh, Michael Carbin, and Martin C. Rinard
OBT '12 — Off the Beaten Track, co-located with POPL

Theses and Technical Reports


Reasoning about Relaxed Programs
Michael Carbin, Deokwan Kim, Sasa Misailovic, Martin C. Rinard
Technical Report, MIT-CSAIL-TR-2011-050

Power-Aware Computing with Dynamic Knobs
Henry Hoffmann, Stelios Sidiroglou, Michael Carbin,
Sasa Misailovic, Anant Agarwal, and Martin Rinard
Tehcnical Report, MIT-CSAIL-TR-2010-027

Learning Effective BDD Variable Orders for BDD-Based Program Analysis
Michael Carbin
Stanford University Undergraduate Honors Thesis, May 2006
Paper

Patents


Configuration of Isolated Extensions and Device Drivers
Galen C. Hunt, James R. Larus, Manuel A. Fanndrich, Orion Hodson, David R. Tarditi, Michael Spear, Michael Carbin, Steven P. Levi, Bjarne Steensgaard
U.S. Patent Number 8,074,231. Filed: June 30, 2006. Issued: December 6, 2011

Bypass Virtualization
Thomas Joseph Purtell, Won Chun, Michael Carbin
U.S. Patent Number 8,065,687. Filed: Jan 7, 2008. Issued November 22, 2011

Bio


Michael Carbin is a Ph.D. Candidate in Electrical Engineering and Computer Science at MIT. His interests include the design of programming systems that deliver improved performance and resilience by incorporating approximate computing and self-healing.

His work on program analysis at Stanford University as an undergraduate received an award for Best Computer Science Undergraduate Honors Thesis. As a graduate student, he has received the MIT Lemelson Presidential and Microsoft Research Graduate Fellowships. His recent research on verifying the reliability of programs that execute on unreliable hardware received a best paper award at OOPSLA 2013.

Contact


: mcarbin@csail.mit.edu
: Facebook
: LinkedIn
: Michael Carbin, MIT CSAIL, 77 Massachusetts Ave, 32-G730 Cambridge, MA 02139
: Office : (617) 253-7768