Madan Musuvathi

关于

I am a Partner Research Manager at Microsoft Research (opens in new tab) managing the Research in Software Engineering (opens in new tab) group. I truly believe in integrating methods and ideas from different research areas. My research interests span programming languages, formal methods, systems, high-performance computing, machine learning, and their various subfields including parallelism and concurrency, model checking, verification, program analysis, program synthesis, theorem proving, satisfiability modulo theories, compilers, and testing. Tools and methods from my research are used by software developers at Microsoft and elsewhere.

Research Thrusts

Performance Abstractions for ML Systems

I am working on disciplined programming abstractions for generating high-performance compute and communication GPU kernels, bringing together techniques from high-performance computing, compilers, and program synthesis.

• Synthesis of communication collectives: We proposed a general mechanism to precisely capture the latency/bandwidth tradeoff in communication collectives and demonstrated how to synthesize collective algorithms in the pareto-optimal frontier [PPoPP ’21]. We use constraint solvers to automatically synthesize optimal algorithms [NSDI ’23] and compiler + runtime to build efficient communication kernels [ASPLOS ’23]. Cutom communication kernels generated this way [MSCCL] have been used in production at Microsoft and elsewhere. Recent work [MSCCL++] is integrated into AMD’s RCCL library of communication kernels.
• Performance abstractions for compute kernels: We are building efficient programming abstractions that enable fine-grained overlapping of compute and communication kernels [CGO ’24, ASPLOS ’22]. The long-term research goal is to build performance-preserving high-level language programming language for specifying GPU kernels without compromising performance and eliminate the need for custom CUDA programming.

Safe Natural Programming & LLMs for Software Engineering

With the advent of LLMs, there is a trend towards programming with natural language (aka vibe coding). While this is exciting, our research bet is that we need to move towards safe natural programming, where the programmer is completely protected from programming language abstractions (code writing/reviewing, code-level debugging/testing) just as safe programming languages protect programmers from assembly language abstractions. We have been working towards this ambitious research agenda determining how to formalize intents specified in natural language, synthesize programs from such formal specifications, both correctly and performantly – as bugs (both correctness and performance bugs) break abstractions. We have made initial progress towards using LLMs for intent formalization [ICSE ’24, ICSE ’24], specification generation [EMNLP ’23, HotOS ’23], bug finding [SOSP ’24], and code optimization [CGO ’25].

Concurrency Verification and Testing

Large scale systems are concurrent, asynchronous, and distributed. I have developed techniques to systematically test and find race conditions at scale. This stream of work required combining systematic exploration techniques of model checking with disciplined insights from how systems are built. The tools that I have developed are in use at Microsoft and elsewhere to find thousands of race conditions.

• Probabilistic delay injection: Practitioners have long observed that inserting random delays flushes out race conditions. We formalized this insight into PCT, a randomized algorithm with probabilistic guarantees for finding race conditions [ASPLOS ’10, PLDI ’12]. The work combines practical insights on the structure of concurrency bugs with classical results from dimension theory of partial-ordered sets to effectively cover orderings in concurrent executions. To the best of my knowledge, this algorithm (along with its derivatives) is the only known technique to improve upon random delay injection in finding bugs.
• Data race detection: Insights from PCT lead to efficient techniques for data-race detection and thread-safety violation detection with near-zero runtime overhead [OSDI ’10, RV ’12, SOSP ’19, EuroSys ’23]. These techniques have found widespread use within Microsoft finding thousands of bugs. Syzkaller (opens in new tab) uses these techniques today (through KCSAN) to find hundreds of bugs in Linux.
• Model Checking & Context-Bounded Exploration: This work developed scalable ways to apply model checking/systematic state-space exploration to real systems [OSDI ’02, NSDI ’04, OSDI ’04]. A key technique required scalability was to bound the search towards bugs, while providing progressive notions of coverage [PLDI ’07, PLDI ’08, OSDI ’08, ICSE ’09]. We also developed, for the first time, the notions of concurrency unit-testing [TACAS ’10, SIGCSE ’11, IEEE Software ’11] when the prevailing notion was that concurrency testing is only amenable in the large as stress tests.

Memory Consistency

I have long been an ardent proponent of simple easy-to-understand consistency models, despite academics and practitioners alike do not seem to appreciate the benefits :). Consistency models involve a tradeoff between easy-to-measure performance and hard-to-measure programmability. So, relaxed consistency models (for CPUs, GPUs, and distributed systems) abound where alleged performance improvements come from a complete lack of concern for programmability. In a series of papers, I advocated the case for sequential consistency and showed that well-designed systems can implement SC efficiently [PLDI ’10, PLDI ’11, ASPLOS ’11, ISCA ’12, IEEE Micro ’13, SNAPL ’15, PPoPP ’17, PLDI ’19, TOPLAS ’21]. To quantify the programmability cost of relaxed consistency models, I studied the increased cost/complexity of program verification [CAV ’08, POPL ’10, CC ’10, ESOP ’12, ESOP ’12]

Other

• Parallel Algorithms: I worked on using symbolic reasoning to break dependences in sequential computations [ASPLOS ’14, PPoPP ’14, CACM ’16, TOPC ’16,
• Machine Learning: I worked on improved algorithms and systems for classical machine learning [ICML ’15, ICASSP ’16, VLDB ’15, IPDPS ’18, IPDPS’21, MLSys ’21]
• Compilers for Fully Homomorphic Encryption: I worked on compilers for fully homomorphic encryption computations [PLDI ’20, PLDI ’19]
• Satisfiability Modulo Theories: I worked on a theorem prover called Zap [LPAR ’05], a precursor to the now popular Z3 theorem prover. I developed improved decision procedures [IJCAR ’06, PDPAR ’05], improved quantifier reasoning [TACAS ’05], modular generation of interpolants [CADE ’05], and cover algorithms [ESOP ’08]

Honors and Awards

• CAV Award 2023 for the introduction of context-bounded analysis and its applications to systematic testing of concurrent programs.
• PPoPP Best Paper Award 2021: Synthesizing Optimal Collective Algorithms
• SOSP Best Paper Award 2019: Efficient and Scalable Thread-Safety Violation Detection — Finding thousands of concurrency bugs during testing.
• CACM Research Highlight 2015: Parallelizing dynamic programming through rank convergence
• SIGPLAN Research Highlight 2015: Parallelizing dynamic programming through rank convergence
• OSDI Best Paper Award 2004: Using Model Checking to Find Serious File System Errors

Keynotes and Invited Talks

• Kahlert Distinguished Lecture Series, Univ. of Utah 2024: Safe Natural Programming
• LCPC 2019: Cryptographic Computations need Compilers
• EPFL Seminar 2017: Beyond the Embarrassingly Parallel – New Languages, Compilers, and Runtimes
• PPoPP-HPCA-CGO Joint Keynote 2016: Beyond the Embarrassingly Parallel – New Languages, Compilers, and Runtimes
• ISMM 2013: Safety-first Approach to Memory Consistency Models

Professional Service

Bio

Madan Musuvathi is a Partner Research Manager at Microsoft Research managing the RiSE group that focuses on research in programming languages, formal methods, systems, high-performance computing, and machine learning. His research has produced several software reliability and performance-engineering tools that are widely used within Microsoft and other companies. He received the CAV award in 2023 for his fundamental contributions to the field of computer-aided verification. He has won distinguished paper awards at several conferences including PPoPP ’21, SOSP ’19, and OSDI ‘04. One of his co-advisees won the 2012 ACM SIGPLAN Outstanding Doctoral Dissertation Award. He co-chaired the Program Committee of PPoPP ’26 and ASPLOS ’24. He received his Ph.D. from Stanford University.