VLDB 2026 Research / reviewers in the wild / expert
Sorav Bansal
dblp:97/6573
· DBLP profile ↗
25ranked-venue papers
8as first author
3since 2021 · last 2024
0009-0004-2006-9635ORCID · corroborated
Domains — the database's venue-derived domains; a paper can count in several
Software engineering, systems software and programming languages · 13 · 3 first-author · 3 since 2021Systems, architecture and hardware · 8 · 2 first-author · 1 since 2021Computer networks · 5 · 4 first-authorArtificial intelligence and machine learning · 1Databases, data management, data science and information retrieval · 1 · 1 first-authorHuman-computer interaction and ubiquitous computing · 1Theory of computation · 1
| Year | Publication | Venue | Position |
|---|---|---|---|
| 2024 | Modeling Dynamic (De)Allocations of Local Memory for Translation ValidationabstractEnd-to-End Translation Validation is the problem of verifying the executable code generated by a compiler against the corresponding input source code for a single compilation. This becomes particularly hard in the presence of dynamically-allocated local memory where addresses of local memory may be observed by the program. In the context of validating the translation of a C procedure to executable code, a validator needs to tackle constant-length local arrays, address-taken local variables, address-taken formal parameters, variable-length local arrays, procedure-call arguments (including variadic arguments), and the alloca () operator. We provide an execution model, a definition of refinement, and an algorithm to soundly convert a refinement check into first-order logic queries that an off-the-shelf SMT solver can handle efficiently. In our experiments, we perform blackbox translation validation of C procedures (with up to 100+ SLOC), involving these local memory allocation constructs, against their corresponding assembly implementations (with up to 200+ instructions) generated by an optimizing compiler with complex loop and vectorizing transformations. Abhishek Rose, Sorav Bansal |
Proc. ACM Program. Lang. | 2 |
| 2023 | StaticPersist: Compiler Support for PMEM Programming
Sorav Bansal |
VMCAI | 1 |
| 2022 | Automatic Generation of Debug Headers through BlackBox Equivalence CheckingabstractModern compiler optimization pipelines are large and complex, and it is rather cumbersome and error-prone for compiler developers to preserve debugging information across optimization passes. An optimization can add, remove, or reorder code and variables, which makes it difficult to associate the generated code statements and values with the source code statements and values. Moreover recent proposals for automatic generation of optimizations (e.g., through search algorithms) have not previously considered the preservation of debugging information.We demonstrate the application of a blackbox equivalence checker to automatically populate the debugging information in the debug headers of the optimized executables compiled from C programs. A blackbox equivalence checker can automatically compute equivalence proofs between the original source code and the optimized executable code without the knowledge of the exact transformations performed by the compiler/optimizer. We present an algorithm that uses these formal equivalence proofs to improve the executable’s debugging headers. We evaluate this approach on benchmarks derived from the Testsuite of Vectorizing Compilers (TSVC) compiled through three different compilers: GCC, ClangLLVM, and ICC. We demonstrate significant improvements in the debuggability of the optimized executable code in these experiments. The benefits of these improvements can be transparently realized through any standard debugger, such as GDB, to debug the updated executable. Vaibhav Kiran Kurhe, Pratik Karia, Shubhani Gupta, Abhishek Rose, Sorav Bansal |
CGO | 5 |
| 2020 | OOElala: order-of-evaluation based alias analysis for compiler optimizationabstractIn C, the order of evaluation of expressions is unspecified; further for expressions that do not involve function calls, C semantics ensure that there cannot be a data race between two evaluations that can proceed in either order (or concurrently). We explore the optimization opportunity enabled by these non-deterministic expression evaluation semantics in C, and provide a sound compile-time alias analysis to realize the same. Our algorithm is implemented as a part of the Clang/LLVM infrastructure, in a tool called OOElala. Our experimental results demonstrate that the untapped optimization opportunity is significant: code patterns that enable such optimizations are common; the enabled transformations can range from vectorization to improved instruction selection and register allocation; and the resulting speedups can be as high as 2.6x on already-optimized code. Ankush Phulia, Vaibhav Bhagee, Sorav Bansal |
PLDI | 3 |
| 2020 | Counterexample-guided correlation algorithm for translation validationabstractAutomatic translation validation across the unoptimized intermediate representation (IR) of the original source code and the optimized executable assembly code is a desirable capability, and has the potential to compete with existing approaches to verified compilation such as CompCert. A difficult subproblem is the automatic identification of the correlations across the transitions between the two programs' respective locations. We present a counterexample-guided algorithm to identify these correlations in a robust and scalable manner. Our algorithm has both theoretical and empirical advantages over prior work in this problem space. Shubhani Gupta, Abhishek Rose, Sorav Bansal |
Proc. ACM Program. Lang. | 3 |
| 2019 | HawkEye: Efficient Fine-grained OS Support for Huge PagesabstractEffective huge page management in operating systems is necessary for mitigation of address translation overheads. However, this continues to remain a difficult area in OS design. Recent work on Ingens uncovered some interesting pitfalls in current huge page management strategies. Using both page access patterns discovered by the OS kernel and fine-grained data from hardware performance counters, we expose problematic aspects of current huge page management strategies. In our system, called HawkEye/Linux, we demonstrate alternate ways to address issues related to performance, page fault latency and memory bloat; the primary ideas behind HawkEye management algorithms are async page pre-zeroing, de-duplication of zero-filled pages, fine-grained page access tracking and measurement of address translation overheads through hardware performance counters. Our evaluation shows that HawkEye is more performant, robust and better-suited to handle diverse workloads when compared with current state-of-the-art systems. Ashish Panwar, Sorav Bansal, K. Gopinath |
ASPLOS | 2 |
| 2018 | Effective Use of SMT Solvers for Program Equivalence Checking Through Invariant-Sketching and Query-Decomposition
Shubhani Gupta, Aseem Saxena, Anmol Mahajan, Sorav Bansal |
SAT | 4 |
| 2018 | Automatic Verification of Intermittent Systems
Manjeet Dahiya, Sorav Bansal |
VMCAI | 2 |
| 2017 | Black-Box Equivalence Checking Across Compiler Optimizations
Manjeet Dahiya, Sorav Bansal |
APLAS | 2 |
| 2017 | The Unicorn Runtime: Efficient Distributed Shared Memory Programming for Hybrid CPU-GPU ClustersabstractProgramming hybrid CPU-GPU clusters is hard. This paper addresses this difficulty and presents the design and runtime implementation of Unicorn-a parallel programming model for hybrid CPU-GPU clusters. In particular, this paper proves that efficient distributed shared memory style programing is possible and its simplicity can be retained across CPUs and GPUs in a cluster, minus the frustration of dealing with race conditions. Further, this can be done with a unified abstraction, avoiding much of the complication of dealing with hybrid architectures. This is achieved with the help of transactional semantics (on shared global address spaces), deferred bulk data synchronization, workload pipelining and various communication and computation scheduling optimizations. We describe the said abstraction, our computation and communication scheduling system and report its performance on a few benchmarks like Matrix Multiplication, LU Decomposition and 2D FFT. We find that parallelization of coarse-grained applications like matrix multiplication or 2D FFT using our system requires only about 30 lines of C code to set up the runtime. The rest of the application code is regular single CPU/GPU implementation. This indicates the ease of extending parallel code to a distributed environment. The execution is efficient as well. When multiplying two square matrices of size 65, 536 χ 65,536, Unicornachieves a peak performance of 7.88 TFlop/s when run over a cluster of 14 nodes with each node equipped with two Tesla M2070 GPUs and two 6-core Intel Xeon 2.67 GHz CPUs, connected over a 32Gbps Infiniband network. In this paper, we also demonstrate that the Unicorn programming model can be efficiently used to implement high level abstractions like MapReduce. We use such an extension to implement PageRank and report its performance. For a sample web of 500 million web pages, our implementation completes a page rank iteration in about 18 seconds (on average) on a 14-node cluster. Tarun Beri, Sorav Bansal, Subodh Kumar 0001 |
IEEE Trans. Parallel Distributed Syst. | 2 |
| 2015 | A Scheduling and Runtime Framework for a Cluster of Heterogeneous Machines with Multiple AcceleratorsabstractWe present a runtime system for simple and efficient programming of CPU+GPU clusters. The programmer focuses on core logic, while the system undertakes task allocation, load balancing, scheduling, data transfer, etc. Our programming model is based on a shared global address space, made efficient by transaction style bulk-synchronous semantics. This model broadly targets coarse-grained data parallel computation particularly suited to multi-GPU heterogeneous clusters. We describe our computation and communication scheduling system and report its performance ona few prototype applications. For example, parallelization of matrix multiplication or 2D FFT using our system requires the regular CPU/GPU implementations and about 30 lines of additional C code to set up the runtime. Our runtime system achieves a performance of 5.61 TFlop/s while multiplying two square matrices of 1.56 billion elements each over a 10-nodecluster with 20 GPUs. This performance is possible due toa number of critical optimizations working in concert. These include perfecting, pipelining, maximizing overlap between computation and communication, and scheduling efficiently across heterogeneous devices of vastly different capacities. Tarun Beri, Sorav Bansal, Subodh Kumar 0001 |
IPDPS | 2 |
| 2015 | Improving Remote Desktopping Through Adaptive Record/ReplayabstractAccessing the display of a computer remotely, is popularly called remote desktopping. Remote desktopping software installs at both the user-facing client computer and the remote server computer; it simulates user's input events at server, and streams the corresponding display changes to client, thus providing an illusion to the user of controlling the remote machine using local input devices (e.g., keyboard/mouse). Many such remote desktopping tools are widely used. We show that if the remote server is a virtual machine (VM) and the client is reasonably powerful (e.g., current laptop and desktop grade hardware), VM deterministic replay capabilities can be used adaptively to significantly reduce the network bandwidth consumption and server-side CPU utilization of a remote desktopping tool. We implement these optimizations in a tool based on Qemu/KVM virtualization platform and VNC remote desktopping platform. Our tool reduces VNC's network bandwidth consumption by up to 9x and server-side CPU utilization by up to 56% for popular graphics-intensive applications. On the flip side, our techniques consume higher CPU/memory/disk resources at the client. The effect of our optimizations on user-perceived latency is negligible. Shehbaz Jaffer, Piyus Kedia, Sorav Bansal |
VEE | 3 |
| 2013 | Efficient virtualization on embedded power architecture® platformsabstractPower Architecture® processors are popular and widespread on embedded systems, and such platforms are increasingly being used to run virtual machines. While the Power Architecture meets the Popek-and-Goldberg virtualization requirements for traditional trap-and-emulate style virtualization, the performance overhead of virtualization remains high. For example, workloads exhibiting a large amount of kernel activity typically show 3-5x slowdowns over bare-metal. Aashish Mittal, Dushyant Bansal, Sorav Bansal, Varun Sethi |
ASPLOS | 3 |
| 2013 | Variable and thread bounding for systematic testing of multithreaded programsabstractPrevious approaches to systematic state-space exploration for testing multi-threaded programs have proposed context-bounding and depth-bounding to be effective ranking algorithms for testing multithreaded programs. This paper proposes two new metrics to rank thread schedules for systematic state-space exploration. Our metrics are based on characterization of a concurrency bug using v (the minimum number of distinct variables that need to be involved for the bug to manifest) and t (the minimum number of distinct threads among which scheduling constraints are required to manifest the bug). Our algorithm is based on the hypothesis that in practice, most concurrency bugs have low v (typically 1-2) and low t (typically 2-4) characteristics. We iteratively explore the search space of schedules in increasing orders of v and t. We show qualitatively and empirically that our algorithm finds common bugs in fewer number of execution runs, compared with previous approaches. We also show that using v and t improves the lower bounds on the probability of finding bugs through randomized algorithms. Systematic exploration of schedules requires instrumenting each variable access made by a program, which can be very expensive and severely limits the applicability of this approach. Previous work has avoided this problem by interposing only on synchronization operations (and ignoring other variable accesses). We demonstrate that by using variable bounding (v) and a static imprecise alias analysis, we can interpose on all variable accesses (and not just synchronization operations) at 10-100x less overhead than previous approaches. Sandeep Bindal, Sorav Bansal, Akash Lal |
ISSTA | 2 |
| 2013 | Fast dynamic binary translation for the kernelabstractDynamic binary translation (DBT) is a powerful technique with several important applications. System-level binary translators have been used for implementing a Virtual Machine Monitor [2] and for instrumentation in the OS kernel [10]. In current designs, the performance overhead of binary translation on kernel-intensive workloads is high. e.g., over 10x slowdowns were reported on the syscall nanobenchmark in [2], 2-5x slowdowns were reported on lmbench microbenchmarks in [10]. These overheads are primarily due to the extra work required to correctly handle kernel mechanisms like interrupts, exceptions, and physical CPU concurrency. Piyus Kedia, Sorav Bansal |
SOSP | 2 |
| 2008 | Binary Translation Using Peephole Superoptimizers
Sorav Bansal, Alex Aiken |
OSDI | 1 |
| 2006 | Automatic generation of peephole superoptimizersabstractPeephole optimizers are typically constructed using human-written pattern matching rules, an approach that requires expertise and time, as well as being less than systematic at exploiting all opportunities for optimization. We explore fully automatic construction of peephole optimizers using brute force superoptimization. While the optimizations discovered by our automatic system may be less general than human-written counterparts, our approach has the potential to automatically learn a database of thousands to millions of optimizations, in contrast to the hundreds found in current peephole optimizers. We show experimentally that our optimizer is able to exploit performance opportunities not found by existing compilers; in particular, we show speedups from 1.7 to a factor of 10 on some compute intensive kernels over a conventional optimizing compiler. Sorav Bansal, Alex Aiken |
ASPLOS | 1 |
| 2006 | Energy Efficiency and Capacity for TCP Traffic in Multi-Hop Wireless Networks
Sorav Bansal, Rajeev Shorey, Archan Misra |
Wirel. Networks | 1 |
| 2004 | Design and Analysis of a Cooperative Medium Access Scheme for Wireless Mesh NetworksabstractThis paper presents the detailed design and performance analysis of MACA-P, a RTS/CTS based MAC protocol, that enables simultaneous transmissions in wireless mesh networks. The IEEE 802.11 DCF MAC prohibits any parallel transmission in the neighborhood of either a sender or a receiver (of an ongoing transmission). MACA-P is a set of enhancements to the 802.11 MAC that allows parallel transmissions in situations when two neighboring nodes are either both receivers or transmitters, but a receiver and a transmitter are not neighbors. The performance of MACA-P in terms of system throughput is obtained through a simulation of the protocol using ns and is compared with the 802,11 RTS/CTS MAC. Experiments with the base MACA-P protocol reveal the need for certain enhancements, especially to avoid the drawbacks associated with attempts at parallel transmissions in scenarios where such parallelism is not feasible. Studies with the enhanced MACA-P protocol also demonstrate how significant performance gains in wireless mesh network performance may be realized if the radio transceiver behavior is modified in tandem with the MAC protocol. Arup Acharya, Archan Misra, Sorav Bansal |
BROADNETS | 3 |
| 2004 | CAR: Clock with Adaptive Replacement
Sorav Bansal, Dharmendra S. Modha |
FAST | 1 |
| 2004 | Performance of TCP and UDP protocols in multi-hop multi-rate wireless networksabstractAn interesting feature of IEEE 802.11 wireless LAN cards is that they support multiple transmission modes. For example, the 802.11b cards support four transmission modes of I, 2, 5.5 and 11 Mbps, whereas, the 802.11a cards support eight transmission modes, up to a maximum of 54 Mbps. In this paper, we study layer four protocols over multi-rate multi-hop wireless networks and attempt to answer the question whether higher bandwidth links necessarily outperform lower bandwidth links in these networks. We examine this question by taking into account the transport layer protocols such as the TCP and UDP. While network capacity is a topic of active interest in the research community, a comparative study of the ad hoc network throughput at the different link bandwidths has not been made. We then propose a bandwidth-based ad hoc routing protocol and look at how to integrate QoS with routing. Sorav Bansal, Rajeev Shorey, Arzad Alam Kherani |
WCNC | 1 |
| 2003 | MACA-P: A MAC for Concurrent Transmissions in Multi-Hop Wireless NetworksabstractThis paper presents the initial design and performance study of MACA-P, a RTS/CTS based MAC protocol that enables simultaneous transmissions in multihop ad-hoc wireless networks. Providing such low-cost multihop and high performance wireless access networks is an important enabler of pervasive computing. MACA-P is a set of enhancements to the 802.11 DCF that allows parallel transmissions in many situations when two neighboring nodes are either both receivers or both transmitters, but a receiver and a transmitter are not neighbors. Like 802.11, MACA-P contains a contention-based reservation phase prior to data transmission. However, the data transmission is delayed by a control phase interval, which allows multiple sender-receiver pairs to synchronize their data transfers, thereby avoiding collisions and improving system throughput. Arup Acharya, Archan Misra, Sorav Bansal |
PerCom | 3 |
| 2003 | Comparing the routing energy overheads of ad-hoc routing protocolsabstractWe use simulations to study the comparative routing overheads of three ad-hoc routing protocols, namely AODV, DSDV and DSR. In contrast to earlier studies, we focus exclusively on the energy consumption and not on other metrics such as the number of routing packets. In particular, we study the 'range effects' of the three protocols, i.e., how changes to the transmission power and transmission radius affect the overall energy consumed by routing-related packets. Due to the broadcast nature of the wireless medium, the energy spent in packet receptions is almost as important as the transmission power; using the number of transmissions as an indicator of the routing overhead can thus be fairly misleading. Our studies show that the energy overhead of the three protocols varies with the transmission power in distinct and non-obvious ways. Sorav Bansal, Rajeev Shorey, Archan Misra |
WCNC | 1 |
| 2002 | The capacity of multi-hop wireless networks with TCP regulated trafficabstractWe study the dependence of the capacity of multi-hop wireless networks on the transmission range of nodes in the network with TCP regulated traffic. Specifically, we examine the sensitivity of the capacity to the speed of the nodes and the number of TCP connections in an ad hoc network. By incorporating the notion of a minimal acceptable QoS metric (loss) for an individual session, we argue that the QoS-aware capacity is a more accurate model of the TCP-centric capacity of an ad-hoc network. We study the dependence of capacity on the source application (Telnet or FTP) and on the choice of the ad-hoc routing protocol (ad-hoc on-demand distance vector - AODV, dynamic source routing - DSR or destination-sequenced distance vector - DSDV). We conclude that persistent and non-persistent traffic behave quite differently in an ad-hoc network. Sorav Bansal, Rajeev Shorey, Shobhit Chugh, Anurag Goel, Archan Misra |
GLOBECOM | 1 |
| 2002 | Energy Efficiency and Throughput for TCP Traffic in Multi-Hop Wireless NetworksabstractWe study the performance metrics associated with TCP-regulated traffic in multi-hop wireless networks that use a common physical channel (e.g., IEEE 802.11). In contrast to earlier analyses, we focus simultaneously on two key operating metrics - the energy efficiency and the session throughput. Using analysis and simulations, we show how these metrics are strongly influenced by the radio transmission range of individual nodes. Due to tradeoffs between the individual packet transmission energy and the likelihood of retransmissions, the total energy consumption is a convex function of the number of hops (and hence, of the transmission range). On the other hand, the TCP session throughput decreases supra-linearly with a decrease in the transmission range. In certain scenarios, the overall network capacity can then be a concave function of the transmission range. Based on our analysis of the performance of an individual TCP session, we finally study how parameters such as the node density and the radio transmission range affect the overall network capacity under different operating conditions. Our analysis shows that capacity metrics at the TCP layer behave quite differently than corresponding idealized link-layer metrics. Sorav Bansal, Archan Misra, Ashu Razdan, Rajeev Shorey |
INFOCOM | 3 |