I’m a principal engineer on the S3 team at Amazon Web Services. I work on the S3 Tables analytics service, open-source clients like Mountpoint for Amazon S3 and S3 Connector for PyTorch, and our backend storage systems including ShardStore. I also develop the Shuttle framework for testing concurrent Rust code at AWS and elsewhere.
Before AWS, I was a professor of computer science at the University of Texas at Austin. My research interests are in formal methods, programming languages, and systems—I’m most excited about making systems software faster and safer using automated verification and synthesis techniques. My work has received best paper awards from SOSP, OSDI, ASPLOS, and EuroSys. I have a PhD in computer science from the University of Washington.
Publications
Conference Papers
- SquirrelFS: using the Rust compiler to check file-system crash consistency. Hayley LeBlanc, Nathan Taylor, James Bornholt and Vijay Chidambaram. OSDI 2024.
- Automatic Generation of Vectorizing Compilers for Customizable Digital Signal Processors. Samuel Thomas and James Bornholt. ASPLOS 2024. Best Paper Award.
- Synthesis-Aided Crash Consistency for Storage Systems. Jacob Van Geffen, Xi Wang, Emina Torlak, and James Bornholt. ECOOP 2023.
- Chipmunk: Investigating Crash-Consistency in Persistent-Memory File Systems. Hayley LeBlanc, Shankara Pailoor, Om Saran, Isil Dillig, James Bornholt, and Vijay Chidambaram. EuroSys 2023. Best Paper Award.
- Synthesizing Fine-Grained Synchronization Protocols for Implicit Monitors. Kostas Ferles, Benjamin Sepanski, Rahul Krishnan, James Bornholt, and Isil Dillig. OOPSLA 2022.
- Using Lightweight Formal Methods to Validate a Key-Value Storage Node in Amazon S3. James Bornholt, Rajeev Joshi, Vytautas Astrauskas, Brendan Cully, Bernhard Kragl, Seth Markle, Kyle Sauri, Drew Schleit, Grant Slatton, Serdar Tasiran, Jacob Van Geffen, and Andrew Warfield. SOSP 2021. Best Paper Award.
- Vectorization for Digital Signal Processors via Equality Saturation. Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson. ASPLOS 2021.
- A Synthesis-Aided Compiler for DSP Architectures. Alexa VanHattum, Rachit Nigam, Vincent T. Lee, James Bornholt, and Adrian Sampson. LCTES 2020.
- Automatic Generation of High-Performance Quantized Machine Learning Kernels. Meghan Cowan, Thierry Moreau, Tianqi Chen, James Bornholt, and Luis Ceze. CGO 2020.
- Fixing Code That Explodes Under Symbolic Evaluation. Sorawee Porncharoenwase, James Bornholt, and Emina Torlak. VMCAI 2020.
- Scaling Symbolic Evaluation for Automated Verification of Systems Code with Serval. Luke Nelson, James Bornholt, Ronghui Gu, Andrew Baumann, Emina Torlak, and Xi Wang. SOSP 2019. Best Paper Award. Distinguished Artifact Award.
- Finding Code That Explodes Under Symbolic Evaluation. James Bornholt and Emina Torlak. OOPSLA 2018. Distinguished Artifact Award.
- Nickel: A Framework for Design and Verification of Information Flow Control Systems. Helgi Sigurbjarnarson, Luke Nelson, Bruno Castro-Karney, James Bornholt, Emina Torlak, and Xi Wang. OSDI 2018.
- Hyperkernel: Push-Button Verification of an OS Kernel. Luke Nelson, Helgi Sigurbjarnarson, Kaiyuan Zhang, Dylan Johnson, James Bornholt, Emina Torlak, and Xi Wang. SOSP 2017.
- Synthesizing Memory Models from Framework Sketches and Litmus Tests. James Bornholt and Emina Torlak. PLDI 2017.
- Push-Button Verification of File Systems via Crash Refinement. Helgi Sigurbjarnarson, James Bornholt, Emina Torlak, and Xi Wang. OSDI 2016. Best Paper Award.
- Disciplined Inconsistency with Consistency Types. Brandon Holt, James Bornholt, Irene Zhang, Dan R. K. Ports, Mark Oskin, and Luis Ceze. SoCC 2016.
- Specifying and Checking File System Crash-Consistency Models. James Bornholt, Antoine Kaufmann, Jialin Li, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. ASPLOS 2016.
- A DNA-Based Archival Storage System. James Bornholt, Randolph Lopez, Douglas M. Carmean, Luis Ceze, Georg Seelig, and Karin Strauss. ASPLOS 2016. IEEE Micro Top Picks.
- Optimizing Synthesis with Metasketches. James Bornholt, Emina Torlak, Dan Grossman, and Luis Ceze. POPL 2016.
- Hardware–Software Co-Design: Not Just a Cliché. Adrian Sampson, James Bornholt, and Luis Ceze. SNAPL 2015.
- Uncertain<T>: A First-Order Type for Uncertain Data. James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley. ASPLOS 2014. SIGPLAN Research Highlight. IEEE Micro Top Picks.
Journal Papers
- Noninterference Specifications for Secure Systems. Luke Nelson, James Bornholt, Arvind Krishnamurthy, Emina Torlak, and Xi Wang. ACM SIGOPS Operating Systems Review, vol. 54, no. 1, pp. 31–39, July 2020.
- A Taxonomy of General Purpose Approximate Computing Techniques. Thierry Moreau, Joshua San Miguel, Mark Wyse, James Bornholt, Armin Alaghi, Luis Ceze, Natalie Enright Jerger, and Adrian Sampson. IEEE Embedded Systems Letters, vol. 10, no. 1, pp. 2–5, March 2018.
- Toward a DNA-Based Archival Storage System. James Bornholt, Randolph Lopez, Douglas M. Carmean, Luis Ceze, Georg Seelig, and Karin Strauss. IEEE Micro, vol. 37, no. 3, pp. 98–104, May–June 2017.
- Uncertain<T>: Abstractions for Uncertain Hardware and Software. James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley. IEEE Micro, vol. 35, no. 3, pp. 132–143, May–June 2015.
Workshop Papers
- Scaling Program Synthesis by Exploiting Existing Code. James Bornholt and Emina Torlak. ML4PL 2015 (colocated with ECOOP 2015).
- Approximate Program Synthesis. James Bornholt, Emina Torlak, Luis Ceze, and Dan Grossman. WAX 2015 (colocated with PLDI 2015).
- REACT: A Framework for Rapid Exploration of Approximate Computing Techniques. Mark Wyse, Andre Baixo, Thierry Moreau, Bill Zorn, James Bornholt, Adrian Sampson, Luis Ceze, and Mark Oskin. WAX 2015 (colocated with PLDI 2015).
- Programming the Internet of Uncertain <T>hings. James Bornholt, Na Meng, Todd Mytkowicz, and Kathryn S. McKinley. SCAW 2015 (colocated with HPCA 2015).
- There's Something About Bayes: Effective Probabilistic Programming for the Rest of Us. James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley. APPROX 2014 (colocated with PLDI 2014).
Posters & Talks
- Uncertain<T>: A First-Order Type for Uncertain Data. James Bornholt. PLDI 2013 Student Research Competition. First Place, PLDI Student Research Competition. Second Place, ACM Student Research Competition Grand Final.
- The Model Is Not Enough: Understanding Energy Consumption in Mobile Devices. James Bornholt, Todd Mytkowicz, and Kathryn S. McKinley. Hot Chips 24, 2012.
Theses
- Optimizing the Automated Programming Stack. James Bornholt. PhD thesis, University of Washington, 2019.
- Abstractions and Techniques for Programming with Uncertain Data. James Bornholt. Honours thesis, Bachelor of Philosophy (Honours), Australian National University, 2013.