Mark R. Tuttle
Principal Engineer
Amazon Web Services
27 Melcher Street
Boston, MA 02210
tuttle@acm.org
8 Melanie Lane
Arlington, MA 02474
(781) 648-1106
mrtuttle@alum.mit.edu
Experience: My resume and an overview of work before Intel.
Education:
PhD, Massachusetts Institute of Technology, computer science, 1989
MS, Massachusetts Institute of Technology, computer science, 1987
BS, University of Nebraska-Lincoln, with highest distinction, math and computer science, 1984
Research Interests:
Distributed and parallel systems; fault-tolerance, scalability, and reliability; specification, verification, and testing tools and methodology; algorithms; theory.
Refereed conference publications:
- Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Model checking boot code from AWS data centers. Formal Methods in System Design, 57(1):34–52, July 2021.
- Nathan Chong, Byron Cook, Jonathan Eidelman, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Code-level model checking in the software development workflow at Amazon Web Services. Software – Practice and Experience, 51(4):772–797, January 2021.
- Nathan Chong, Byron Cook, Konstantinos Kallas, Kareem Khazem, Felipe R. Monteiro, Daniel Schwartz-Narbonne, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Code-level model checking in the software development workflow. In Gregg Rothermel and Doo-Hwan Bae, editors, Proceedings of the 42nd International Conference on Software Engineering, Software Engineering in Practice (ICSE’20), pages 11–20. ACM, July 2020.
- Byron Cook, Kareem Khazem, Daniel Kroening, Serdar Tasiran, Michael Tautschnig, and Mark R. Tuttle. Model Checking Boot Code from AWS Data Centers. In Hana Chockler and Georg Weissenbacher, editors, Proceedings of the 30th International Conference on Computer Aided Verification (CAV 2018), LNCS 10982, pp. 467–486, 2018.
- Oleksandr Bazhaniuk, John Loucaides, Lee Rosenbaum, Mark R. Tuttle, and Vincent Zimmer. Excite: Symbolic execution for BIOS security. In Proceedings of the 9th Annual USENIX Workshop on Offensive Technologies (WOOT ’15), August 2015.
- Raghudeep Kannavara, Christopher J. Havlicek, Bo Chen, Mark R. Tuttle, Kai Cong, Sandip Ray, Fei Xie. Challenges and Opportunities with Concolic Testing. In Proceedings of the National Aerospace Electronics Conference – Ohio Innovation Summit (NAECON-OIS 2015), IEEE, June 2015.
- Mark R. Tuttle and Amit Goel. Protocol proof checking simplified with SMT. In Proceedings of the 11th Annual IEEE International Symposium on Network Computing and Applications (NCA), August 2012.
- Amit Goel, Sava Krstic, Rebekah Leslie, and Mark R. Tuttle. SMT-based system verification with DVF. In Proceedings of the 10th Annual International Workshop on Satisfiability Modulo Theories (SMT Workshop), Manchester, June 2012.
- Maurice Herlihy, Yoram Moses, and Mark R. Tuttle. Transforming worst-case optimal solutions for simultaneous tasks into all-case optimal solutions. In Proceedings of the 30th Annual ACM Symposium on Principles of Distributed Computing (PODC), pages 231-238, June 2011.
- John O’Leary, Murali Talupur, and Mark R. Tuttle. Protocol verification using flows: An industrial experience. In Proceedings of the 9th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 172-179, November 2009.
- John O’Leary, Bratin Saha, and Mark R. Tuttle. Model checking transactional memory with Spin. In Proceedings of the 29th International Conference on Distributed Computing Systems (ICDCS), pages 335-342, June 2009.
- Murali Talupur and Mark R. Tuttle. Going with the flow: Parameterized verification using message flows. In Proceedings of the 8th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 69-76, November 2008. (Examples) Best paper award.
- John O’Leary, Bratin Saha, Mark R. Tuttle. Brief Announcement: Model checking transactional memory with Spin. In Proceedings of the 27th Annual ACM Symposium on Principles of Distributed Computing (PODC), page 424, August 2008.
- David James, Tim Leonard, John O’Leary, Murali Talupur, and Mark R. Tuttle. Brief Announcement: Extracting models from design documents with Mapster. In Proceedings of the 27th Annual ACM Symposium on Principles of Distributed Computing (PODC), page 456, August 2008.
- Noga Alon, Chen Avin, Michal Koucky, Gady Kozma, Zvi Lotker, and Mark R. Tuttle. Many random walks are faster than one. In Proceedings of the 20th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA), pages 119-128, June 2008.
- John O’Leary, Bratin Saha, and Mark R. Tuttle, Model checking transactional memory. ETAPS Workshop on Designing Correct Circuits (DCC), April 2008.
- Murali Talupur, Sava Krstic, John O’Leary, and Mark R. Tuttle. Parametric Verification of Industrial Cache Protocols. ETAPS Workshop on Designing Correct Circuits (DCC), April 2008.
- Ariel Cohen, John W. O’Leary, Amir Pnueli, Mark R. Tuttle, and Lenore D. Zuck. Verifying Correctness of Transactional Memories. In Proceedings of the 7th International Conference on Formal Methods in Computer-Aided Design (FMCAD), pages 37-44, November 2007.
- Zvi Lotker, Boaz Patt-Shamir, and Mark R. Tuttle. Publish and perish: Definition and analysis of an n-person publication impact game. In Proceedings of the 18th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA), pages 11-18, August 2006.
- Zvi Lotker, Boaz Patt-Shamir, and Mark Tuttle. Brief Announcement: Timing games and shared memory. In Proceedings of the 19th International Symposium on Distributed Computing (DISC), pages 507-508, September 2005.
- Baruch Awerbuch, Yossi Azar, Zvi Lotker, Boaz Patt-Shamir, and Mark Tuttle. Collaborate with strangers to find own preferences. In Proceedings of the 17th Annual ACM Symposium on Parallel Algorithms and Architectures (SPAA), pages 263-269, July 2005.
- Baruch Awerbuch, Boaz Patt-Shamir, David Peleg, and Mark Tuttle. Adaptive collabortion in peer-to-peer systems. In Proceedings of the 25th IEEE International Conference on Distributed Computing Systems (ICDCS), pages 71-80, June 2005.
- Baruch Awerbuch, Boaz Patt-Shamir, David Peleg, and Mark Tuttle. Improved recommendation systems. In Proceedings of the 16th Annual ACM-SIAM Symposium on Discrete Algorithms (SODA), pages 1174-1183, January 2005.
- Maurice Herlihy, Sergio Rajsbaum, and Mark Tuttle. An axiomatic approach to computing the connectivity of synchronous and asynchronous systems. In Proceedings of the Sixth Workshop on Geometric and Topological Methods in Concurrency and Distributed Computing (GETCO), Electronic Notes in Theoretical Computer Science. Elsevier, October 2004.
- Baruch Awerbuch, Boaz Patt-Shamir, David Peleg, and Mark Tuttle. Collaboration of untrusting peers with changing interests. In Proceedings of the 5th ACM Conference on Electronic Commerce (EC), pages 112-119, May 2004.
- Sandip Ray, John Matthews, and Mark Tuttle. Certifying compositional model checking algorithms in ACL2. In Proceedings of the 4th International Workshop on the ACL2 Theorem Prover and Its Applications (ACL2), July 2003.
- David Lomet and Mark Tuttle. A theory of redo recovery. In Proceedings of the ACM SIGMOD International Conference on Management of Data, pages 397-406. ACM, June 2003.
- Leslie Lamport, John Matthews, Mark Tuttle, and Yuan Yu. Specifying and verifying systems with TLA+. In Proceedings of the Tenth ACM SIGOPS European Workshop: Can we really depend on an OS?, pages 45-48, September 2002.
- Maurice Herlihy, Sergio Rajsbaum, and Mark Tuttle. A new synchronous lower bound for set agreement. In Proceedings of the 15th International Conference on Distributed Computing (DISC), volume 2180 of Lecture Notes in Computer Science, pages 136-150. Springer-Verlag, October 2001.
- Maurice Herlihy, Sergio Rajsbaum, and Mark Tuttle. An overview of synchronous message-passing and topology. In Proceedings of the Workshop on Geometry and Topology in Concurrency Theory (GETCO), volume NS-00-3 of Basic Research in Computer Science Notes Series. Department of Computer Science, University of Aarhus, August 2000.
- Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark Tuttle, and Yuan Yu. Cache coherence verification with TLA+. In Proceedings of the World Congress On Formal Methods In The Development Of Computing Systems, FM’99, Industrial Panel, volume 1709 of Lecture Notes in Computer Science, page 1871, September 1999.
- David B. Lomet and Mark R. Tuttle. Logical logging to extend recovery to new domains. In Alex Delis, Christos Faloutsos, and Shahram Ghandeharizadeh, editors, Proceedings of the ACM SIGMOD International Conference on Management of Data, pages 73-84. ACM, June 1999.
- Maurice Herlihy, Sergio Rajsbaum, and Mark R. Tuttle. Unifying synchronous and asynchronous message-passing models. In Proceedings of the 17th Annual ACM Symposium on Principles of Distributed Computing, pages 133-142. ACM, June 1998.
- David Lomet and Mark R. Tuttle. Redo recovery after system crashes. In Umesh Dayal, Peter Gray, and Shojiro Nishio, editors, Proceedings of the 21st International Conference on Very Large Data Bases, pages 457-468. Morgan Kaufmann, September 1995.
- Soma Chaudhuri and Mark R. Tuttle. Fast increment registers. In Gerard Tel and Paul Vitanyi, editors, Proceedings of the 8th International Workshop on Distributed Algorithms, volume 857 of Lecture Notes in Computer Science, pages 74-88. Springer-Verlag, Berlin, October 1994.
- Soma Chaudhuri, Maurice Herlihy, Nancy Lynch, and Mark R. Tuttle. A tight lower bound for k-set agreement. In Proceedings of the 34th IEEE Symposium on Foundations of Computer Science, pages 206-215. IEEE, November 1993.
- Soma Chaudhuri, Maurice Herlihy, Nancy Lynch, and Mark R. Tuttle. A tight lower bound for processor coordination. In Proceedings of the 3rd International Workshop on Responsive Computer Systems, pages 4-15, September 1993.
- Martin Abadi and Mark R. Tuttle. A semantics for a logic of authentication. In Proceedings of the 10th Annual ACM Symposium on Principles of Distributed Computing, pages 201-216. ACM, August 1991.
- Michael Merritt, Francesmary Modugno, and Mark R. Tuttle. Time-constrained automata. In J. C. M. Baeten and J. F. Groote, editors, Proceedings of the Second International Conference on Concurrency Theory (Concur’91), volume 527 of Lecture Notes in Computer Science, pages 408-423. Springer-Verlag, Berlin, August 1991.
- Gil Neiger and Mark R. Tuttle. Common knowledge and consistent simultaneous coordination. In J. van Leeuwen and N. Santoro, editors, Proceedings of the 4th International Workshop on Distributed Algorithms, volume 486 of Lecture Notes in Computer Science, pages 334-352. Springer-Verlag, September 1990.
- Maurice P. Herlihy and Mark R. Tuttle. Wait-free computation in message-passing systems. In Proceedings of the 9th Annual ACM Symposium on Principles of Distributed Computing, pages 347-362. ACM, August 1990.
- Joseph Y. Halpern and Mark R. Tuttle. Knowledge, probability, and adversaries. In Proceedings of the 8th Annual ACM Symposium on Principles of Distributed Computing, pages 103-118. ACM, August 1989.
- Joseph Y. Halpern, Yoram Moses, and Mark R. Tuttle. A knowledge-based analysis of zero knowledge. In Proceedings of the 20th ACM Symposium on Theory of Computing, pages 132-147. ACM, May 1988.
- Nancy A. Lynch and Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. In Proceedings of the 6th Annual ACM Symposium on Principles of Distributed Computing, pages 137-151. ACM, August 1987.
- Yoram Moses and Mark R. Tuttle. Programming simultaneous actions using common knowledge. In Proceedings of the 27th IEEE Symposium on Foundations of Computer Science, pages 208-221. IEEE, October 1986.
Refereed journal publications:
- Noga Alon, Chen Avin, Michal Koucky, Gady Kozma, Zvi Lotker, and Mark R. Tuttle. Many random walks are faster than one. Combinatorics, Probability and Computing, 20(4):481-502, July 2011.
- Maurice Herlihy, Sergio Rajsbaum, and Mark R. Tuttle. An axiomatic approach to computing the connectivity of synchronous and asynchronous systems. Electronic Notes in Theoretical Computer Science, 230:79-102, March 2009.
- Zvi Lotker, Boaz Patt-Shamir, and Mark R. Tuttle. A game of timing and visibility. Games and Economic Behavior, 62(2): 643-660, March 2008, doi 10.1016/j.geb.2007.04.006.
- Baruch Awerbuch, Yossi Azar, Zvi Lotker, Boaz Patt-Shamir, and Mark R. Tuttle. Collaborate with strangers to find own preferences. Theory of Computing Systems, 42(1):27-41, January 2008, doi 10.1007/s00224-007-9016-7.
- Rajeev Joshi, Leslie Lamport, John Matthews, Serdar Tasiran, Mark Tuttle, and Yuan Yu. Checking cache-coherence protocols with TLA+. Formal Methods in System Design: Special Issue on Industrial Applications, 22(2):125-131, March 2003.
- Maurice Herlihy, Sergio Rajsbaum, and Mark R. Tuttle. An overview of synchronous message-passing and topology. Electronic Notes in Theoretical Computer Science, 39(2):1-17, 2001.
- Soma Chaudhuri, Maurice Herlihy, Nancy Lynch, and Mark R. Tuttle. Tight bounds for k-set agreement. Journal of the ACM, 47(5):912–943, September 2000.
- Soma Chaudhuri, Maurice Herlihy, and Mark R. Tuttle. Wait-free implementations in message-passing systems. Theoretical Computer Science, 220(1):211-245, June 1999.
- Joseph Y. Halpern and Mark R. Tuttle. Knowledge, probability, and adversaries. Journal of the ACM, 40(4):917-962, September 1993.
- Gil Neiger and Mark R. Tuttle. Common knowledge and consistent simultaneous coordination. Distributed Computing, 6(3):181-192, 1993.
- Nancy A. Lynch and Mark R. Tuttle. An introduction to input/output automata. CWI-Quarterly, 2(3):219-246, September 1989. Also available as MIT Technical Memo MIT/LCS/TM-373.
- Yoram Moses and Mark R. Tuttle. Programming simultaneous actions using common knowledge. Algorithmica, 3(1):121-169, 1988.
Book chapters:
- David Lomet and Mark R. Tuttle. Redo recovery after system crashes. In Vijay Kumar and Meichun Hsu, editors, Recovery Mechanisms in Database Systems, pages 101-124. Prentice Hall, Upper Saddle River, New Jersey, 1999.
Technical reports:
- Soma Chaudhuri, Maurice Herlihy, Nancy Lynch, and Mark R. Tuttle. Tight bounds for k-set agreement. Technical Report 98/4, DEC Cambridge Research Lab, May 1998.
- Soma Chaudhuri, Maurice Herlihy, and Mark R. Tuttle. Wait-free implementations in message-passing systems. Technical Report 98/5, DEC Cambridge Research Lab, May 1998.
Theses:
- Mark R. Tuttle. Hierarchical correctness proofs for distributed algorithms. Master’s thesis, Massachusetts Institute of Technology, Laboratory for Computer Science, April 1987. Available as MIT Technical Report MIT/LCS/TR-387.
- Mark R. Tuttle. Knowledge and Distributed Computation. PhD thesis, Massachusetts Institute of Technology, Laboratory for Computer Science, May 1990. Available as MIT Technical Report MIT/LCS/TR-477.
Unpublished manuscripts:
- Leslie Lamport, Mark Tuttle, and Yuan Yu. The wildfire verification challenge problem. July 2000.
- Homayoon Akhiani, Damien Doligez, Paul Harter, Leslie Lamport, Joshua Scheid, Mark Tuttle, and Yuan Yu. TLA+ verification of cache coherence protocols. February 1999.
- Hagit Attiya and Mark R. Tuttle. Bounds for slotted l-exclusion. Technical memo, MIT, February 1989.
- Mark R. Tuttle. A game-theoretic characterization of eventual common knowledge. Technical memo, MIT, October 1988
Patents:
- David B. Lomet and Mark R. Tuttle. “Database computer system using logical logging to extend recovery.” US Patent 6,978,279, December 20, 2005.
- David B. Lomet and Mark R. Tuttle. “Logical logging to extend recovery.” US Patent 7,509,351, March 24, 2009.
- Boaz Patt-Shamir, Mark Rogers Tuttle, and Eytan Adar. “Computer method and apparatus for collaborative web searches.” US Patent 8,312,003, November 13, 2012.
- Baruch Awerbuch, Boaz Patt-Shamir, David Peleg, Mark Tuttle. Improved recommendation systems. Application pending, December 2004.
Invited Talks:
- Reasoning about distributed computation. Computer Science and Engineering 40th Anniversary Distinguished Alumni Talks, University of Nebraska – Lincoln, September 2008.
- Analyzing Cache Coherence with TLA+. Workshop on Formal Specification and Verification Methods for Shared Memory Systems at International Conference on Formal Methods in Computer-Aided Design (FMCAD), October 2000.
- Using TLA+ at COMPAQ. TLA+ User Group Meeting at World Congress On Formal Methods In The Development Of Computing Systems (FM), September, 1999.
- Unifying synchronous and asynchronous message-passing models. Computer Science Colloquium series, Brown University, March 1999.
- Lower bounds for agreement. Mathematics and Statistics Colloquium series, University of Nebraska-Lincoln, May 1997.
- A tight lower bound for k-set agreement. Computer Science Colloquium series, Dartmouth University, January 1995.
- Build models, not logics. Panel, Computer Security Foundations Workshop, June 1993.
- How fast are wait-free concurrent objects? POCS Seminar Series, MIT Laboratory for Computer Science, April 1993.
Recognition:
- Best paper award at Formal Methods in Computer-Aided Design (FMCAD), 2008.
- Danny Dolev (Hebrew University) recognized two papers as among the most highly cited papers ever published in the ACM conference Principles of Distributed Computing in his keynote talk at PODC’s 25th Anniversary Celebration, 2006.
- Young Alumni Achievement Award, University of Nebraska-Lincoln, May 1997
- National champion, ACM National Scholastic Programming Competition, University of Nebraska-Lincoln team, 1983