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.
- 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)
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)
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.
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
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
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
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
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
Reflective Program Generation with Patterns
Manuel Fähndrich, Michael Carbin, James R. Larus
GPCE '06 — Generative Programming and Component Engineering
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
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)
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
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
Stanford University Undergraduate Honors Thesis, May 2006
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
Thomas Joseph Purtell, Won Chun, Michael Carbin
U.S. Patent Number 8,065,687. Filed: Jan 7, 2008. Issued November 22, 2011
Michael started his research career as undergraduate student at Stanford,
working on BDD-based program analysis with Monica Lam and with Jim Larus at
Microsoft Research on type-safe compile-time metaprogramming for the
Operating System. His work as an undergraduate received an award for
the Best Computer Science Undergraduate Honors Thesis.
As a graduate student, Michael has worked as a MIT Lemelson Presidential and Microsoft Research Graduate Fellow with Martin Rinard on both the theory and practice of verified approximate computing and software self-healing.