arXiv subjects

Bodhisatwa Chatterjee

Publications and source records attributed to Bodhisatwa Chatterjee.

4 recordsLinked to original sources

arXiv2026

ProofWright: Towards Agentic Formal Verification of CUDA

Large Language Models (LLMs) are increasingly used to automatically generate optimized CUDA kernels, substantially improving developer productivity. However, despite rapid generation, these kernels often contain subtle correctness bugs and lack formal safety guarantees. Runtime testing is inherently unreliable - limited input coverage and reward hacking can mask incorrect behavior - while manual formal verification is reliable but cannot scale to match LLM output rates, creating a critical validation bottleneck. We present ProofWright, an agentic verification framework that bridges this gap by integrating automated formal verification with LLM-based code generation. ProofWright provides end-to-end guarantees of memory safety, thread safety, and semantic correctness for LLM-generated CUDA kernels. On KernelBench L1, ProofWright verifies safety properties for 74% of generated kernels, uncovers subtle correctness errors missed by conventional testing, and establishes semantic equivalence for a class of element-wise kernels. With a modest overhead of 3 minutes per kernel, ProofWright demonstrates that scalable, automated formal verification of LLM-generated GPU code is feasible - offering a path toward trustworthy high-performance code generation without sacrificing developer productivity.

cs.SE↗

arXiv2026

Phaedrus: Predicting Dynamic Application Behavior with Lightweight Generative Models and LLMs

Application profiling is essential for software optimization tasks such as code layout and memory placement, where optimization decisions depend on program behavior. However, modern applications exhibit significant input-dependent variability, limiting the effectiveness of conventional profiling approaches that rely on a single representative execution. We present Phaedrus, a compiler-assisted deep learning framework that predicts dynamic program behavior across diverse execution instances, with a focus on dynamic function call prediction. These predicted call sequences are used to guide input-specific compiler optimizations, enabling code specialization without requiring program execution. Phaedrus introduces two complementary techniques. Application Behavior Synthesis (Dynamis) is a profile-less approach in which large language models infer dynamic behavior directly from source code and static compiler analysis, bypassing traditional profiling. Application Profile Generalization (Morpheus) employs generative models trained on compressed and augmented Whole Program Path (WPP) function profiles to predict application behavior for unseen inputs. Experimental results show that Phaedrus accurately identifies frequently executed and runtime-dominated hotspot functions, covering up to 85-99% of total execution time. Using these predictions, Phaedrus enables superior profile-guided optimizations, achieving an average performance improvement of 6% (upto 25%) and a binary size reduction of 5.19% (upto 19%), without executing the target program. Additionally, Phaedrus reduces WPP function profile sizes by up to $10^{7} \times $.

cs.SE↗

arXiv2022

Effective Cache Apportioning for Performance Isolation Under Compiler Guidance

With a growing number of cores in modern high-performance servers, effective sharing of the last level cache (LLC) is more critical than ever. The primary agenda of such systems is to maximize performance by efficiently supporting multi-tenancy of diverse workloads. However, this could be particularly challenging to achieve in practice, because modern workloads exhibit dynamic phase behaviour, which causes their cache requirements & sensitivities to vary at finer granularities during execution. Unfortunately, existing systems are oblivious to the application phase behavior, and are unable to detect and react quickly enough to these rapidly changing cache requirements, often incurring significant performance degradation. In this paper, we propose Com-CAS, a new apportioning system that provides dynamic cache allocations for co-executing applications. Com-CAS differs from the existing cache partitioning systems by adapting to the dynamic cache requirements of applications just-in-time, as opposed to reacting, without any hardware modifications. The front-end of Com-CAS consists of compiler-analysis equipped with machine learning mechanisms to predict cache requirements, while the back-end consists of proactive scheduler that dynamically apportions LLC amongst co-executing applications leveraging Intel Cache Allocation Technology (CAT). Com-CAS's partitioning scheme utilizes the compiler-generated information across finer granularities to predict the rapidly changing dynamic application behaviors, while simultaneously maintaining data locality. Our experiments show that Com-CAS improves average weighted throughput by 15% over unpartitioned cache system, and outperforms state-of-the-art partitioning system KPart by 20%, while maintaining the worst individual application completion time degradation to meet various Service-Level Agreement (SLA) requirements.

cs.PL↗

arXiv2021

Compiler-Guided Throughput Scheduling for Many-core Machines

Typical schedulers in multi-tenancy environments make use of reactive, feedback-oriented mechanisms based on performance counters to avoid resource contention but suffer from detection lag and loss of performance. In this paper, we address these limitations by exploring the utility of predictive analysis through dynamic forecasting of applications' resource-heavy regions during its execution. Our compiler framework classifies loops in programs and leverages traditional compiler analysis along with learning mechanisms to quantify their behaviour. Based on the predictability of their execution time, it then inserts different types of beacons at their entry/exit points. The information produced by beacons in multiple processes is aggregated and analyzed by the proactive scheduler to respond to the anticipated workload requirements. For throughput environments, we develop a framework that demonstrates high-quality predictions and improvements in throughput over CFS by 76.78% on an average and up to 3.2x on Amazon Graviton2 Machine on consolidated workloads across 45 benchmarks.

cs.DC↗