Milo M. K. Martin

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

Email: milom@cis.upenn.edu
Office Phone: (215) 746-2972

Curriculum Vitae

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'm the faculty leader of Penn's Computer Architecture and Compilers Group (ACG).

Current Projects and Collaborators

Computational sprinting
- Recent result: Computational Sprinting [HPCA'12] (best paper award recipient)
- With: Arun Raghavan, Prof. Tom Wenisch (U of Michigan), Prof. Kevin Pipe (U of Michigan), and Prof. Marios Papaefthymiou (U of Michigan)
Cache coherence apologetics
- Recent result: Why On-Chip Cache Coherence is Here to Stay [CACM'12]
- With: Prof. Mark Hill (U of Wisconsin) and Prof. Daniel Sorin (Duke U.)
Hardware/software techniques for security and memory safety of C
- Recent result: Watchdog [ISCA'12]
- With: Santosh Nagarakatte, Jianzhou Zhao, Christian DeLozier, Peter-Michael Osera, and Prof. Steve Zdancewic
- Prior participants: Joe Devietti and Colin Blundell
Specification of relaxed consistency models
- Recent result: Axiomatic POWER [CAV'12]
- With: Sela Mador-Haim, Prof. Rajeev Alur and the Cambridge/INRIA Relaxed-Memory Concurrency group.
The verified LLVM project (Vellvm)
- Recent result: Formalizing the LLVM Intermediate Representation [POPL'12]
- With: Jianzhou Zhao, Santosh Nagarakatte, and Prof. Steve Zdancewic

Prior Projects and Collaborators

Transactional memory
- RetCon [ISCA'10] and OneTM [ISCA'07]
- With: Colin Blundell and Arun Raghavan
Adaptive cache coherence protocols
- PATCH and Token Tenure [TACO'10, MICRO'08]
- With: Arun Raghavan and Colin Blundell
Performance-transparent implementations of memory consistency
- InvisiFence [ISCA'09]
- With: Colin Blundell and Prof. Tom Wenisch (U of Michigan)
Scalable microarchitectures
- With: Tingting Sha and her advisor Prof. Amir Roth
- NoSQ [MICRO'06, TopPicks]

Software Releases

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

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

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

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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
Talk: pdf or pptm
Source Code
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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
Paper: pdf
Talk: pdf or ppt
Additional Information
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.
Paper: pdf
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.
Paper: pdf
Talk: ppt
Additional Information
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
Extended Version: pdf
Talk: pdf or ppt
Additional Information
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
Talk: pdf
Exploiting Dead Value Information,
Milo M. Martin, Amir Roth, and Charles Fischer,
International Symposium on Microarchitecture (MICRO), December 1997.
Paper: pdf
Talk: pdf

Journal Publications

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.
Paper: pdf
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.
Paper: pdf
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.)
Paper: pdf
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)
Paper: pdf
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

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.
Paper: pdf
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.
Paper: pdf
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.
Paper: pdf
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
Project Page: html

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.