Software is intertwined in our daily lives: it manages sensitive personal information, allows us to connect with our peers, and controls devices like planes, cars, etc. Recent years have seen a surge in the adoption of a new kind of software system that uses Machine Learning and Artificial Intelligence due to an abundance of data. Owing to the ubiquitous nature, the security and reliability of these systems are paramount. However, due to these systems’ complex nature, they are fragile and suffer from design and implementation flaws that make them unreliable. Unfortunately, building systems with provable guarantees is still a niche domain and remains largely unapproachable for the software development community, since these techniques require significant investment in terms of time and effort. In this dissertation, I present verification techniques that ease the manual burden required to build reliable software and machine learning systems. The proposed techniques leverage specifications in the form of input/output examples and program synthesis techniques to ensure system correctness. I present the first approach that reduces the general lemma synthesis problem to a data-driven program synthesis problem, for easing the proof burden in a foundational verification setting. I then present an extension to this data-driven synthesis approach that expands the class of lemmas that can be synthesized. I conclude with the first counterexample-guided verification approach that can provably enforce correctness properties in Neural Networks.

Safe languages provide programming abstractions, like type and memory safety, to improve programmer productivity. Unfortunately, in the domain of concurrent programming, mainstream safe languages instead choose to adopt complex and error-prone semantics by default in the name of performance. A memory consistency model defines the possible values that a shared-memory read may return in a multithreaded programming language. Languages today like Java and Julia have adopted a relaxed (or weak) memory model that is designed to admit most traditional compiler optimizations and obviate the need for hardware fences on most shared-memory accesses. The downside, however, is that programmers are exposed to a complex and unintuitive semantics and must carefully declare certain variables as volatile in order to enforce program orderings that are necessary for proper behavior. Not only does this performance-by-default approach conflict with the design philosophy of “safe” languages, but also surprisingly, very little is actually known about the practical performance cost of a stronger memory model.

In this thesis, I define the safe-by-default and performant-by-choice volatile-by-default semantics for Java and other JVM-based languages. volatile-by-default provides sequential consistency (SC) by default, while still allows expert programmers to avoid fence overheads on performance-critical libraries. I present VBD-HotSpot and VBDA-HotSpot, modifications of Oracle’s HotSpot JVM that enforce the volatile-by-default semantics on Intel X86 hardware and ARM hardware. I then present a novel speculative technique to optimize language-level SC. Finally, I have implemented an SC enforcing Julia compiler that guarantees SC for Julia by default. Through evaluations of the above projects, I show that it is possible to measure the practical cost of strong and simple semantics for concurrent programming, and with optimizations, it is possible to have a simpler semantics for concurrent programming at a reasonable cost for certain languages.

Although the program verification community has developed several techniques for analyzing software and formally proving their correctness, these techniques are too sophisticated for end users and require significant investment in terms of time and effort. In this dissertation, I present techniques that help programmers easily formalize the initial requirements for verifying their programs — specifications and inductive invariants. The proposed techniques leverage ideas from program synthesis and statistical learning to automatically generate these formal requirements from readily available program-related data, such as test cases, execution traces etc. I detail three of these data-driven learning techniques – FlashProfile and PIE for specification learning, and LoopInvGen for invariant learning.

I conclude with some principles for building robust synthesis engines, which I learned while refining the aforementioned techniques. Since program synthesis is a form of function learning, it is perhaps unsurprising that some of the fundamental issues in program synthesis have also been explored in the machine learning community. I study one particular phenomenon — overfitting. I present a formalization of overfitting in program synthesis, and discuss two mitigation strategies, inspired by existing techniques.

Cloud computing has become an essential part of our computing infrastructure. In this model, data and programs are hosted in (often third-party) data centers that provide APIs for data access and running large-scale computations. It is used in almost all major internet services companies and increasingly being considered by other organizations to host their data and run analytics. However several challenges lie in its full-scale adoption, chief among them being security, performance and correctness. Security is important as both client data and computations need to be sent to third-party data centers. Performance is important as cloud computing involves several development iterations, each running on large-scale data. Correctness is critical as cloud frameworks are complex distributed systems serving billions of users every day.

In this dissertation, I argue that program analysis techniques can help address the above key challenges of cloud computing. I describe three projects that illustrate different aspects of the solution space: MrCrypt is a system that uses static analysis to guarantee data confidentiality in cloud computations by using homomorphic encryption schemes. Vega is a library that significantly improves incremental performance by rewriting modified workflows to use previously computed results. Kuai is a distributed, enumerative model checker that verifies correctness in Software Defined Networks, the networking layer used by many data centers.

The driver linac of the proposed Rare Isotope Accelerator(RIA) requires a great variety of high intensity, high charge state ion beams. In order to design and to optimize the low energy beam line optics of the RIA front end,we have developed a new parallel three-dimensional model to simulate the low energy, multi-species ion beam formation and transport from the ECR ion source extraction region to the focal plane of the analyzing magnet. A multisection overlapped computational domain has been used to break the original transport system into a number of each subsystem, macro-particle tracking is used to obtain the charge density distribution in this subdomain.The three-dimensional Poisson equation is solved within the subdomain and particle tracking is repeated until the solution converges. Two new Poisson solvers basedon a combination of the spectral method and the multigrid method have been developed to solve the Poisson equation in cylindrical coordinates for the beam extraction regionand in the Frenet-Serret coordinates for the bending magnet region. Some test examples and initial applications will also be presented.

In this paper, we present a three-dimensional model for self-consistently modeling ion beam formation from plasma ion sources and transporting in low energy beam transport systems. A multi-section overlapped computational domain has been used to break the original transport system into a number of weakly coupled subsystems. Within each subsystem, macro-particle tracking is used to obtain the charge density distribution in this subdomain. The three-dimensional Poisson equation is solved within the subdomain after each particle tracking to obtain the self-consistent space-charge forces and the particle tracking is repeated until the solution converges. Two new Poisson solvers based on a combination of the spectral method and the finite difference multigrid method have been developed to solve the Poisson equation in cylindrical coordinates for the straight beam transport section and in Frenet-Serret coordinates for the bending magnet section. This model can have important application in design and optimization of the low energy beam line optics of the proposed Rare Isotope Accelerator (RIA) front end.

Despite the rapid increase in mobile web traffic, page loads still fall short of user performance expectations. Numerous solutions have attempted to optimize the web performance, however, these state-of-the-art techniques are either ineffective or impractical in real-world settings due to complexity or deployment challenges. Inspired by mobile apps which provide faster user-perceived performance, we target two significant bottlenecks in the page load process; First, clients have to suffer multiple round trips and server processing delays to fetch the page's main HTML; during this time, a browser cannot display any visual content which frustrates users. Next, these pages include large amounts of JavaScript code in order to offer users a dynamic experience. These scripts often make pages slow to load, partly due to a fundamental inefficiency in how browsers process JavaScript content which fails to leverage the multiple CPU cores that are readily available even on low-end phones. We pursue a programmatic approach that works on legacy web pages and unmodified browsers. We built two fully-automatic systems that are complementary to each other and each optimizes one of the above contributors to slow page loads: Fawkes and Horcrux. Fawkes leverages our measurement study finding that 75% of HTML content remains unchanged across page loads spread 1 week apart. With Fawkes, web servers extract static, cacheable HTML templates (e.g., layout templates) for their pages offline. Upon client request, the static template is sent back to the client immediately and is rendered while dynamic content (e.g., news headlines) is generated which expresses the updates required to transform those rendered templates into the latest page versions. Fawkes reduces the startup delays incurred during the fetch of page's HTML and improves interactivity metrics such as Speed Index and Time-to-first-paint by 46% and 64% at the median in warm cache settings; results are 24% and 62% in cold cache settings. Our second system, Horcrux addresses the client-side computation overheads through offline analysis of all the JavaScript code on the server-side to conservatively identify the page state across all loads of the page. Horcrux's JavaScript scheduler then uses this information to judiciously parallelize JavaScript execution on the client-side while ensuring correctness, accounting for the non-determinism intrinsic to web page loads, and the constraints placed by the browser's API for parallelism. Horcrux reduces median browser computation delays by 31-44% and page load times by 18-37%.