Milo M. K. Martin

Associate Professor (on leave)
Computer and Information Sciences Department
University of Pennsylvania
3330 Walnut Street
Levine Hall
Philadelphia, PA 19104-6389
USA

Email: milom@cis.upenn.edu

Curriculum Vitae

Update

I am now employed by Google, and I am no longer a professor at Penn. This web page is no longer maintained, but it remains for reference and links to papers and presentations.

Research Interests

My area of expertise is computer architecture; however, my interests span many aspects of computer systems research (including compilers, security, databases, embedded systems, and networking). Specifically, my current research projects involve multiprocessor and multi-core memory systems, cache coherence protocols, transactional memory systems, shared-memory workloads, scalable processor micro-architectures, verification of concurrent hardware and software, hardware support for secure systems, and programming models for next-generation multi-core hardware architectures.

I was a faculty member of Penn's Computer Architecture and Compilers Group (ACG).

Prior Projects and Collaborators

Computational Sprinting
- Utilizing Dark Silicon to Save Energy with Computational Sprinting [IEEE Micro '13]
- With: Arun Raghavan, Laurel Emurian, Lei Shao, University of Michigan, Prof. Tom Wenisch (U of Michigan), Prof. Kevin Pipe (U of Michigan), and Prof. Marios Papaefthymiou (U of Michigan)
Hardware/compiler techniques for security and memory safety of C
- Hardware-Enforced Comprehensive Memory Safety [TopPicks '13]
- With: Santosh Nagarakatte, Jianzhou Zhao, Christian DeLozier, Peter-Michael Osera, and Prof. Steve Zdancewic
- Prior participants: Joe Devietti and Colin Blundell
Cache coherence apologetics
- Why On-Chip Cache Coherence is Here to Stay [CACM'12]
- With: Prof. Mark Hill (U of Wisconsin) and Prof. Daniel Sorin (Duke U.)
Specification of relaxed consistency models
- Axiomatic POWER [CAV'12]
- With: Sela Mador-Haim, Prof. Rajeev Alur and the Cambridge/INRIA Relaxed-Memory Concurrency group.
The verified LLVM project (Vellvm)
- Formal Verification of SSA-Based Optimizations for LLVM [PLDI'13]
- With: Jianzhou Zhao, Santosh Nagarakatte, and Prof. Steve Zdancewic
Transactional memory
- RetCon [ISCA'10] and OneTM [ISCA'07]
- With: Colin Blundell and Arun Raghavan
Performance-transparent implementations of memory consistency
- InvisiFence [ISCA'09]
- With: Colin Blundell and Prof. Tom Wenisch (U of Michigan)
Adaptive cache coherence protocols
- PATCH and Token Tenure [TACO'10, MICRO'08]
- With: Arun Raghavan and Colin Blundell
Scalable microarchitectures
- NoSQ [MICRO'06, TopPicks]
- With: Tingting Sha and her advisor Prof. Amir Roth

Seminars and Reading Groups

Emerging Computational Architectures - Fall 2007
Advanced Architecture Discussion Group - Spring 2007 - Spring 2006
Systems Lunch - Fall 2007 - Fall 2006 - Spring 2006 - Fall 2005 - Spring 2005 - Fall 2004 - Spring 2004
ACG Reading Group

Teaching

Spring 2014 - (sabbatical)
Fall 2013 - (sabbatical)
Spring 2013 - CIS 371: Digital Systems Organization and Design
Fall 2012 - CIS 501: Computer Architecture
Spring 2012 - CIS 371: Digital Systems Organization and Design
Fall 2011 - CIS 501: Computer Architecture
Spring 2011 - CIS 371: Digital Systems Organization and Design
Fall 2010 - CIS 501: Computer Architecture
Spring 2010 - CIS 534: Multicore Programming and Architecture
Fall 2009 - CIS 501: Computer Architecture
Spring 2009 - CIS 371: Digital Systems Organization and Design
Fall 2008 - CIS 501: Computer Architecture
Spring 2008 - CIS 371: Digital Systems Organization and Design
Fall 2007 - (sabbatical)
Spring 2007 - CSE 372: Digital Systems Organization and Design Lab
Fall 2006 - CSE 240: Introduction to Computer Architecture
Spring 2006 - CSE 372: Digital Systems Organization and Design Lab
Fall 2005 - CIS 501: Computer Architecture
Spring 2005 - CIS 700/008 Special Topic: Hardware Support for Security
Autumn 2004 - CSE 240: Introduction to Computer Architecture
Spring 2004 - CIS 700/002 Special Topic: Multiprocessor Computer Architecture & Server Workloads

PhD Graduates

Arun Raghavan, 2013
Computational Sprinting: Exceeding Sustainable Power in Thermally Constrained Systems
First employment: Oracle Labs
Santosh Nagarakatte, 2012
Practical Low-Overhead Enforcement of Memory Safety for C Programs
First employment: Assistant Professor at Rutgers University
Colin Blundell, 2010
Mechanisms for Unbounded, Conflict-Robust Hardware Transactional Memory
First employment: IBM Research
Current employment: Google
Sebastian Burckhardt (co-advised with Prof. Rajeev Alur), 2007
Memory Model Sensitive Analysis of Concurrent Data Types
First employment: Microsoft Research

Advice and Tips

Publications

Conference Publications

On-chip Phase Change Heat Sinks Designed for Computational Sprinting.
Lei Shao, Arun Raghavan, Laurel Emurian, Marios Papaefthymiou, Thomas Wenisch, Milo Martin, Kevin Pipe.
Proceedings of the 30th Annual Thermal Measurement, Modeling, and Management Symposium (SemiTherm), March 2014.
WatchdogLite: Hardware-Accelerated Compiler-Based Pointer Checking.
Santosh Nagarakatte, Milo M. K. Martin, Steve Zdancewic.
Proceedings of the 2014 International Symposium on Code Generation and Optimization (CGO), Feb 2014.
Syntax-Guided Synthesis.
Rajeev Alur, Rastislav Bodik, Garvit Juniwal, Milo M. K. Martin, Mukund Raghothaman, Sanjit A. Seshia, Rishabh Singh, Armando Solar-Lezama, Emina Torlak, Abhishek Udupa.
Proceedings of the 2013 Formal Methods in Computer-Aided Design (FMCAD), October 2013.
Ironclad C++: A Library-Augmented Type-Safe Subset of C++.
Christian DeLozier, Richard Eisenberg, Santosh Nagarakatte, Peter-Michael Osera, Milo M. K. Martin, Steve Zdancewic.
Proceedings of the 2013 ACM SIGPLAN International Conference on Object Oriented Programming Systems Languages & Applications (OOPSLA), October 2013.
Formal Verification of SSA-Based Optimizations for LLVM.
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2013.
TRANSIT: Specifying Protocols with Concolic Snippets.
Abhishek Udupa, Arun Raghavan, Jyotirmoy V. Deshmukh, Sela Mador-Haim, Milo M. K. Martin, and Rajeev Alur.
Proceedings of the 2013 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2013.
Computational Sprinting on a Hardware/Software Testbed (best paper award).
Arun Raghavan, Laurel Emurian, Lei Shao, Marios Papaefthymiou, Kevin P. Pipe, Thomas F. Wenisch, and Milo M. K. Martin.
Proceedings of the 18th Eighteenth International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2013.
An Axiomatic Memory Model for POWER Multiprocessors.
Sela Mador-Haim, Luc Maranget, Susmit Sarkar, Kayvan Memarian, Jade Alglave, Scott Owens, Rajeev Alur, Milo M. K. Martin, Peter Sewell, and Derek Williams.
Proceedings of Computer Aided Verification (CAV), July 2012.
Watchdog: Hardware for Safe and Secure Manual Memory Management and Full Memory Safety.
Santosh Nagarakatte, Milo M K Martin, Steve Zdancewic.
Proceedings of the 39th International Symposium on Computer Architecture (ISCA), June 2012.
Talk: pdf or pptm
Multicore Acceleration for Priority Based Schedulers for Concurrency Bug Detection .
Santosh Nagarakatte, Sebastian Burckhardt, Milo M. K. Martin, and Madan Musuvathi.
Proceedings of the 2012 ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2012.
Talk: pdf or pptm
Computational Sprinting (best paper award).
Arun Raghavan, Yixin Luo, Anuj Chandawalla, Marios Papaefthymiou, Kevin P. Pipe, Thomas F. Wenisch, and Milo M. K. Martin.
Proceedings of the 18th Symposium on High Performance Computer Architecture (HPCA), Feb 2012.
Formalizing the LLVM Intermediate Representation for Verified Program Transformations.
Jianzhou Zhao, Santosh Nagarakatte, Milo M. K. Martin, and Steve Zdancewic.
Proceedings of the 39th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages (POPL), Jan 2012.
Litmus Tests for Comparing Memory Consistency Models: How Long Do They Need to Be?.
Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin.
Proceedings of the 48th Design Automation Conference (DAC), June 2011.
Generating Litmus Tests for Contrasting Memory Consistency Models.
Sela Mador-Haim, Rajeev Alur, Milo M. K. Martin.
Proceedings of Computer-aided Verification (CAV), July 2010.
RetCon: Transactional Repair without Replay.
Colin Blundell, Arun Raghavan, and Milo M. K. Martin.
Proceedings of the 37th International Symposium on Computer Architecture (ISCA), June 2010.
Talk: pdf or ppt
CETS: Compiler Enforced Temporal Safety for C.
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic.
Proceedings of ACM SIGPLAN International Symposium on Memory Management (ISMM), June 2010.
Overcoming an Untrusted Computing Base: Detecting and Removing Malicious Hardware Automatically.
Matthew Hicks, Murph Finnicum, Samuel T. King, Milo M. K. Martin, and Jonathan M. Smith.
Proceedings of the 31st IEEE Symposium on Security and Privacy (Oakland), May 2010.
InvisiFence: Performance-Transparent Memory Ordering in Conventional Multiprocessors.
Colin Blundell, Milo M. K. Martin, and Tom Wenisch.
International Symposium on Computer Architecture (ISCA), June 2009.
Talk: pdf or pptx
SoftBound: Highly Compatible and Complete Spatial Memory Safety for C.
Santosh Nagarakatte, Jianzhou Zhao, Milo M. K. Martin, and Steve Zdancewic.
Programming Language Design and Implementation (PLDI), June 2009.
Talk: pdf or pptm
Token Tenure: PATCHing Token Counting Using Directory-Based Cache Coherence.
Arun Raghavan, Colin Blundell, and Milo M. K. Martin.
International Symposium on Microarchitecture (MICRO), November 2008.
Talk: pdf or pptx
HardBound: Architectural Support for Spatial Safety of the C Programming Language.
Joe Devietti, Colin Blundell, Milo M. K. Martin, and Steve Zdancewic.
International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), March 2008.
Talk: pdf or pptm
Video of ASPLOS presentation
Making the Fast Case Common and the Uncommon Case Simple in Unbounded Transactional Memory.
Colin Blundell, Joe Devietti, E Christopher Lewis, and Milo M. K. Martin.
International Symposium on Computer Architecture (ISCA), June 2007.
Talk: pdf or ppt
CheckFence: Checking Consistency of Concurrent Data Types on Relaxed Memory Models.
Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin.
ACM SIGPLAN Conference on Programming Language Design and Implementation (PLDI), June 2007
Talk: pdf or ppt
Source Code
NoSQ: Store-Load Communication without a Store Queue,
Tingting Sha, Milo M.K. Martin, and Amir Roth,
International Symposium on Microarchitecture (MICRO), December 2006.
Talk: pdf or ppt
Bounded Model Checking of Concurrent Data Types on Relaxed Memory Models: A Case Study,
Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin,
Proceedings of Computer-aided Verification (CAV), August 2006.
Talk: ppt
Scalable Store-Load Forwarding via Store Queue Index Prediction,
Tingting Sha, Milo M.K. Martin, and Amir Roth,
International Symposium on Microarchitecture (MICRO), November 2005.
Talk: pdf
Formal Verification and its Impact on the Snooping versus Directory Protocol Debate,
Milo M. K. Martin,
International Conference on Computer Design (ICCD), October 2005.
Talk: pdf or ppt
Improving Multiple-CMP Systems Using Token Coherence,
Michael R. Marty, Jesse D. Bingham, Mark D. Hill, Alan J. Hu, Milo M. K. Martin, and David A. Wood,
International Symposium on High Performance Computer Architecture (HPCA), February 2005.
Paper: pdf
Verifying Safety of a Token Coherence Implementation by Parametric Compositional Refinement,
Sebastian Burckhardt, Rajeev Alur, and Milo M. K. Martin,
Sixth International Conference on Verification, Model Checking and Abstract Interpretation (VMCAI), January 2005.
Extended Version: pdf
Talk: pdf or ppt
Using Speculation to Simplify Multiprocessor Design,
Daniel J. Sorin, Milo M. K. Martin, Mark D. Hill, and David A. Wood,
International Parallel and Distributed Processing Symposium (IPDPS), April 2004.
Talk: ppt
Token Coherence: Decoupling Performance and Correctness,
Milo M. K. Martin, Mark D. Hill, and David A. Wood,
International Symposium on Computer Architecture (ISCA), June 2003.
Talk: pdf or ppt
Using Destination-Set Prediction to Improve the Latency/Bandwidth Tradeoff in Shared Memory Multiprocessors,
Milo M. K. Martin, Pacia J. Harper, Daniel J. Sorin, Mark D. Hill, and David A. Wood,
International Symposium on Computer Architecture (ISCA), June 2003.
Talk: pdf or ppt
SafetyNet: Improving the Availability of Shared Memory Multiprocessors with Global Checkpoint/Recovery,
Daniel J. Sorin, Milo M. K. Martin, Mark D. Hill, and David A. Wood,
International Symposium on Computer Architecture (ISCA), May 2002.
Talk: ppt
Bandwidth Adaptive Snooping,
Milo M. K. Martin, Daniel J. Sorin, Mark D. Hill, and David A. Wood,
International Symposium on High Performance Computer Architecture (HPCA), February 2002.
Talk: pdf or ppt
Correctly Implementing Value Prediction in Microprocessors that Support Multithreading or Multiprocessing,
Milo M. K. Martin, Daniel J. Sorin, Harold W. Cain, Mark D. Hill, and Mikko H. Lipasti,
International Symposium on Microarchitecture (MICRO), December 2001.
Talk: pdf or ppt
Timestamp Snooping: An Approach for Extending SMPs,
Milo M. K. Martin, Daniel J. Sorin, Anastassia Ailamaki, Alaa R. Alameldeen, Ross M. Dickson, Carl J. Mauer, Kevin E. Moore, Manoj Plakal, Mark D. Hill, and David A. Wood,
International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS), November 2000.
Talk: pdf
Exploiting Dead Value Information,
Milo M. Martin, Amir Roth, and Charles Fischer,
International Symposium on Microarchitecture (MICRO), December 1997.
Talk: pdf

Journal Publications

Utilizing Dark Silicon to Save Energy with Computational Sprinting.
Arun Raghavan, Laurel Emurian, Lei Shao, Marios Papaefthymiou, Kevin P. Pipe, Thomas F. Wenisch, and Milo M. K. Martin.
IEEE Micro, Volume 33, Number 5, Sep-Oct 2013.
Hardware-Enforced Comprehensive Memory Safety.
Santosh Nagarakatte, Milo M K Martin, Steve Zdancewic.
IEEE Micro's "Top Picks of 2012" Issue
Volume 33, Number 3, May-June 2013.
Designing for Responsiveness with Computational Sprinting.
Arun Raghavan, Yixin Luo, Anuj Chandawalla, Marios Papaefthymiou, Kevin P. Pipe, Thomas F. Wenisch, and Milo M. K. Martin.
IEEE Micro's "Top Picks of 2012" Issue
Volume 33, Number 3, May-June 2013.
Why On-Chip Cache Coherence is Here to Stay.
Milo M. K. Martin, Mark D. Hill, Daniel J. Sorin.
Communications of the ACM (CACM), Vol. 55, Issue 7, pages 78-89, July 2012.
Token Tenure and PATCH: A Predictive/Adaptive Token-Counting Hybrid.
Arun Raghavan, Colin Blundell, and Milo M. K. Martin.
ACM Transactions on Architecture and Code Optimization, Vol. 7, No. 2, Article 6, September 2010.
NoSQ: Store-Load Communication without a Store Queue,
Tingting Sha, Milo M. K. Martin, and Amir Roth,
IEEE Micro's "Top Picks of 2006" Issue
Volume 27, Number 1, January-February 2007.
Subtleties of Transactional Memory Atomicity Semantics,
Colin Blundell, E Christopher Lewis, and Milo M. K. Martin,
Computer Architecture Letters, Volume 5, November 2006.
Token Coherence: A New Framework for Shared-Memory Multiprocessors,
Milo M.K. Martin, Mark D. Hill and David A. Wood,
IEEE Micro "Top Picks of 2003" Issue
Volume 23, Number 6, November-December 2003.
Simulating a $2M Commercial Server on a $2K PC,
Alaa R. Alameldeen, Milo M.K. Martin, Carl J. Mauer, Kevin E. Moore, Min Xu, Daniel J. Sorin, Mark D. Hill and David A. Wood,
IEEE Computer, February 2003.
Talk: ppt
Specifying and Verifying a Broadcast and a Multicast Snooping Cache Coherence Protocol,
Daniel J. Sorin, Manoj Plakal, Anne E. Condon, Mark D. Hill, Milo M. K. Martin and David A. Wood,
IEEE Transactions on Parallel and Distributed Systems, June 2002 (vol 13, number 6).
(Previously available as Dept. of Computer Sciences Technical Report CS-TR-2000-1412, March 2000.)
Online protocol examples in html
Evaluation of Few-view Reconstruction Parameters for Illicit Substance Detection Using Fast-Neutron Transmission Spectroscopy,
C. L. Fink, P. G. Humm, M. M. Martin, and B. J. Micklich,
IEEE Transactions on Nuclear Science, June 1996 (Volume 43, Issue 3, Part 2)
Evaluation of Neutron Techniques for Illicit Substance Detection,
C. L. Fink, B. J. Micklich, T. J. Yule, P. G. Humm, L. Sagalovsky, and M. M. Martin,
Nuclear Instruments and Methods in Physics Research B99 (1995), 748-752.

Newsletters, Posters, and Refereed Workshop Publications

MAMA: Mostly Automatic Management of Atomicity,
Christian DeLozier, Joseph Devietti, Milo M. K. Martin,
5th Workshop on Determinism and Correctness in Parallel Programming (WoDet), March 2014.
FeS2: A Full-system Execution-driven Simulator for x86,
Naveen Neelakantam, Colin Blundell, Joe Devietti, Milo M. K. Martin and Craig Zilles,
Poster session of the International Conference on Architectural Support for Programming Languages and Operating Systems (ASPLOS Poster), 2008.
Poster: pdf
FeS2 website and download
Multifacet's General Execution-driven Multiprocessor Simulator (GEMS) Toolset,
Milo M. K. Martin, Daniel J. Sorin, Bradford M. Beckmann, Michael R. Marty, Min Xu, Alaa R. Alameldeen, Kevin E. Moore, Mark D. Hill, and David A. Wood,
SIGARCH Computer Architecture News (CAN), Volume 22, Number 4, September 2005.
Web Site: http://www.cs.wisc.edu/gems/
Deconstructing Transactional Semantics: The Subtleties of Atomicity,
Colin Blundell, E Christopher Lewis, and Milo M.K. Martin,
Workshop on Duplicating, Deconstructing, and Debunking (WDDD), June 2005.
Talk: pdf or ppt
Evaluating Non-deterministic Multi-threaded Commercial Workloads,
Alaa R. Alameldeen, Carl J. Mauer, Min Xu, Pacia J. Harper, Milo M.K. Martin, Daniel J. Sorin, Mark D. Hill and David A. Wood,
Workshop On Computer Architecture Evaluation using Commercial Workloads (CAECW), February 2002.
Talk: pdf or ppt
Characterizing a Java Implementation of TPC-W,
Todd Bezenek, Trey Cain, Ross Dickson, Timothy Heil, Milo Martin, Collin McCurdy, Ravi Rajwar, Eric Weglarz, Craig Zilles, and Mikko Lipasti,
Workshop On Computer Architecture Evaluation Using Commercial Workloads (CAECW), January 2000.
Talk: pdf

Technical Reports

Unrestricted Transactional Memory: Supporting I/O and System Calls within Transactions,
Colin Blundell, E Christopher Lewis, and Milo M. K. Martin,
Technical Report CIS-06-09, Department of Computer and Information Science, University of Pennsylvania, Philadelphia, PA, April 2006.

Dissertation

Token Coherence, Ph.D. Dissertation, December 2003.