About
Hi! I am a fourth year Ph.D. student in Trishul group at the University of Texas at Austin, working with Prof. Swarat Chaudhuri. I work in the area of programming languages, formal methods with applications to quantum computing. I am currently working on using automata-theoretic approaches for efficient representations of Boolean functions.
I recently interned at Google in the P4-Based Automated Reasoning (P4-BAR) group to scale the performance of their tool by optimizing the symbolic execution pipeline. Prior to pursuing Ph.D., I worked at Google India (2020-21) where I worked in the Google Ads team and Microsoft India (2019-2020) where I worked in Azure Compute team.
I graduated from Indian Institute of Technology Madras in 2019 with a Dual Degree (Bachelor’s and Master’s) in Computer Science. I was advised by Prof. V Krishna Nandivada. My final year thesis work was on Graph Coloring using GPUs.
Papers
-
Weighted Context-Free-Language Ordered Binary Decision Diagrams
@
OOPSLA 24
Abstract
Over the years, many variants of Binary Decision Diagrams (BDDs) have been developed to address the deficiencies of vanilla BDDs. A recent innovation is the Context-Free-Language Ordered BDD (CFLOBDD), a hierarchically structured decision diagram, akin to BDDs enhanced with a procedure-call mechanism, which allows substructures to be shared in ways not possible with BDDs. For some functions, CFLOBDDs are exponentially more succinct than BDDs. Unfortunately, the multi-terminal extension of CFLOBDDs, like multi-terminal BDDs, cannot efficiently represent functions of type B^n -> D, when the function’s range has many different values. This paper addresses this limitation through a new data structure called Weighted CFLOBDDs (WCFLOBDDs). WCFLOBDDs extend CFLOBDDs using insights from the design of Weighted BDDs (WBDDs) – BDD-like structures with weights on edges. We show that WCFLOBDDs can be exponentially more succinct than both WBDDs and CFLOBDDs.
-
Context-Free-Language Ordered Binary Decision Diagrams
@
(TOPLAS) 24
Abstract
This paper presents a new compressed representation of Boolean functions, called CFLOBDDs (for Context-Free-Language Ordered Binary Decision Diagrams). They are essentially a plug-compatible alternative to BDDs (Binary Decision Diagrams), and hence useful for representing certain classes of functions, matrices, graphs, relations, etc. in a highly compressed fashion. CFLOBDDs share many of the good properties of BDDs, but–in the best case–the CFLOBDD for a Boolean function can be exponentially smaller than any BDD for that function. Compared with the size of the decision tree for a function, a CFLOBDD–again, in the best case–can give a double-exponential reduction in size. They have the potential to permit applications to (i) execute much faster, and (ii) handle much larger problem instances than has been possible heretofore. CFLOBDDs are a new kind of decision diagram that go beyond BDDs (and their many relatives). The key insight is a new way to reuse sub-decision-diagrams: components of CFLOBDDs are structured hierarchically, so that sub-decision-diagrams can be treated as standalone ‘‘procedures’’ and reused. We applied CFLOBDDs to the problem of simulating quantum circuits, and found that for several standard problems the improvement in scalability–compared to simulation using BDDs–is quite dramatic. In particular, the number of qubits that could be handled using CFLOBDDs was larger, compared to BDDs, by a factor of 128x for GHZ; 1,024x for BV; 8,192x for DJ; and 128x for Grover’s algorithm. (With a 15-minute timeout, the number of qubits that CFLOBDDs can handle are 65,536 for GHZ, 524,288 for BV; 4,194,304 for DJ; and 4,096 for Grover’s Algorithm.)
-
Symbolic Quantum Simulation with Quasimodo
@
CAV 23
Abstract
The simulation of quantum circuits on classical computers is an important problem in quantum computing. Such simulation requires representations of distributions over very large sets of basis vectors, and recent work has used symbolic data-structures such as Binary Decision Diagrams (BDDs) for this purpose. In this tool paper, we present Quasimodo, an extensible, open-source Python library for symbolic simulation of quantum circuits. Quasimodo is specifically designed for easy extensibility to other backends. Quasimodo allows simulations of quantum circuits, checking properties of the outputs of quantum circuits, and debugging quantum circuits. It also allows the user to choose from among several symbolic data-structures – both unweighted and weighted BDDs, and a recent structure called Context-Free-Language Ordered Binary Decision Diagrams (CFLOBDDs) – and can be easily extended to support other symbolic data-structures.
-
Graph Coloring using GPUs
@
Euro-Par 2019 19
Abstract
Graph coloring is a widely studied problem that is used in a variety of applications, such as task scheduling, register allocation, eigenvalue computations, social network analysis, and so on. Many of the modern day applications deal with large graphs (with millions of vertices and edges) and researchers have exploited the parallelism provided by multi-core systems to efficiently color such large graphs. GPUs provide a promising parallel infrastructure to run large applications. In this paper, we present new schemes to efficiently color large graphs on GPUs.
We extend the algorithm of Rokos et al. to efficiently color graphs using GPUs. Their approach has to continually resolve conflicts for color assignment. We present a data driven variation of their algorithm and use an improved scheme for conflict resolution. We also propose two optimizations for our algorithm to reduce both the execution time and memory requirements. We have evaluated our scheme (called SIRG) against the NVIDIA cuSPARSE library and the work of Chen et al., and show that SIRG runs significantly faster: geomean 3.42× and 1.76×, respectively. We have also compared SIRG against the scheme of Rokos et al. for CPUs and show that SIRG performs faster on most input graphs: geomean 10.37×.