PurPL Retreat 2020
This is the first annual retreat of the Purdue Center for Programming Principles and Software Systems (PurPL), following the inaugural kick-off symposium in 2019.
Due to the ongoing Covid-19 pandemic, the event will be held in a virtual format. Pre-recorded talks by PurPL faculty, students, and industry partners are available for offline-viewing below. Q&A and discussion sessions will be held via Zoom on August 31th (PurPL affiliates and invited participants only).
Pre-Recorded Talks
|
Taurus: A Data Plane for In-Network Machine Learning (AI, Networks)
Muhammad Shahbaz AbstractEmerging applications-cloud computing, the internet of things, and augmented/virtual reality-need responsive, available, secure, ubiquitous, and scalable datacenter networks. Network management currently uses simple, per-packet, data-plane heuristics (e.g., ECMP and sketches) under an intelligent, millisecond-latency control plane that runs data-driven performance and security policies. However, to meet users' quality-of-service expectations in a modern data center, networks must operate intelligently at line rate. In this paper, we present Taurus, an intelligent data plane capable of machine-learning inference at line rate. Taurus adds custom hardware based on a map-reduce abstraction to programmable network devices, such as switches and NICs; this new hardware uses pipelined and SIMD parallelism for fast inference. Our evaluation of a Taurus-enabled switch ASIC, supporting several real-world benchmarks, shows that Taurus operates three orders of magnitude faster than a server-based control plane, while increasing area by 24% and latency, on average, by 178 ns. On the long road to self-driving networks, Taurus is the equivalent of adaptive cruise control: deterministic rules steer flows, while machine learning tunes performance and heightens security. Bio: https://mshahbaz.gitlab.io/files/bio.pdf |
|
Efficient Practical Secure Computation: Real-world Applications (internal - click to log in) (PL, Crypto)
Hemanta Maji AbstractSecure multi-party computation enables mutually distrusting parties to compute securely over their private data. Such privacy requirements go a long way in building end-user confidence and may even be legally mandated in specific scenarios. After over three decades of highly influential research, secure computation protocols for real-world applications are finally nearing deployment. This talk considers the representative task of securely computing the proximity of two secret trajectories. Parties are interested in finding whether their trajectories get close to each other or not, and disclosing no additional information. Next, the talk elaborates on appropriately encoding real-world applications, like privacy-preserving contact tracing, collision detection, enforcing no-fly zones, and congestion detection in traffic, as particular instances of this general secure computation task. |
|
Regexes gone wrong: Improving Software Security Through Empiricism (Security, SE)
James Davis AbstractRegular expressions are a fundamental tool in computing. They are used in virtually every context, from the IDE to the web stack to spreadsheets and genomic analysis. Software engineers struggle to use them properly. One regex area of particular concern is regex-based denial of service (REDOS). Regexes are used for input sanitization; regexes are implemented with exponential worst-case complexity. The combination can expose web services to REDOS. I discuss some of my work on this problem, combining quantitative and qualitative empirical software engineering to measure the problem, with a bit of automata theory to resolve REDOS in a backwards-compatible way. Jamie is an Assistant Professor at Purdue ECE |
|
Cryptographic Automation (internal - click to log in) (Crypto)
Christina Garman AbstractThis talk will focus on some of my thoughts on how we can use cryptographic automation to remove the human element from the deployment and analysis of cryptographic systems, as well as ideas on tools that could be built to help design and securely deploy new and complex cryptographic systems while preventing insecurities from happening. I will briefly discuss two areas of interest to my current research, zero knowledge proofs and anonymous credentials. Christina Garman is an assistant professor in the Department of Computer Science at Purdue University. Her research interests focus largely on practical and applied cryptography. More specifically, her work has focused on the security of deployed cryptographic systems from all aspects, including the evaluation of real systems, improving the tools that we have to design and create them, and actually creating real, deployable systems. She is also one of the co-founders of ZCash, a startup building a cryptocurrency based on Zerocash. |
|
Programming with Proofs for High-assurance Systems
Nikhil Swamy (Microsoft Research) AbstractProgramming critical systems with proofs, a long-standing goal of computer science, is beginning to come within reach of modern programming languages and proof assistants. I provide a brief overview of recent accomplishments in this space, related to work in the F* proof assistant and Project Everest, one of its flagship applications. Programs developed in F* with proofs of correctness are now deployed in wide variety of settings, ranging from Microsoft Windows and Hyper-V, Microsoft Azure, the Linux kernel, Firefox, mbedTLS, and several others production systems. |
|
AIRCoP: Abstract IR for Comprehensive Parallelization (PL, Systems, ML) Fei Wang (advisor: Tiark Rompf) AbstractThere exist a myriad of parallelization paradigms for training machine learning models, including data parallelism, model parallelism, attribute parallelism, and pipeline parallelism. No paradigm is strictly superior; for best results, tools must be able to harness the power of many different paradigms and even support their combined usage. Thus far, however, machine learning frameworks and libraries individually only support small subsets of these paradigms: extending them with new parallelization strategies is difficult due to the large engineering effort involved in modifying complex runtimes and code generation backends. As a result, machine learning researchers and practitioners frequently need to port their models to different frameworks to experiment with different parallelization strategies. In this paper, we show that a large set of parallel training paradigms can be viewed as computation graph transformations and thus unified within a framework-agnostic compilation phase that does not require deep backend integration. We categorize parallel training paradigms into spatial partitioning for each operator, pipelined execution for each module, and memory-conserving primitives for both intermediate tensors and trainable parameters. We design a set of concise and expressive annotations that guide the transformation of sequential models to explicit parallel programs. The transformation procedure is presented formally as Abstract IR for Comprehensive Parallelization (AIRCoP), both for clarity and to demonstrate correctness. As a proof-of-concept, we implement AIRCoP, which can be used with any framework backend that supports basic parallel executions on multiple devices. We present an evaluation of the TensorFlow backend with 4 GPUs in order to highlight the performance benefits of flexible parallel strategies, providing up to a 20% increase in training throughput. Fei Wang is a 5th year Ph.D candidate at Purdue University Computer Science Department, working with Prof. Tiark Rompf |
|
Architecting Intermediate Layers for Efficient Composition in End-to-End Data Science Pipelines (PL, Systems, ML)
Supun Abeysinghe (advisor: Tiark Rompf) AbstractDeploying cutting edge machine learning (ML) models at scale requires ingesting data from various sources and preprocessing data in various ways. Today, this preprocessing is typically implemented using separate tools like Pandas or Spark that then feed into ML frameworks like PyTorch or TensorFlow. While all these systems go to great lengths to optimize performance for their specific workloads, significant performance is lost when used in combination, due to conversions between incompatible internal data formats and the general inability to perform optimizations across systems. A key idea to remove these bottlenecks is to reorganize existing frameworks (or their front-ends) around a common intermediate layer (IR) which enables cross-optimization and eradicates conversion overheads. We present Flern, the first intermediate-layer integration between systems that are best-of-breed individually and also represents a new state-of-the-art for integration. Supun is a second-year Ph.D. student in Computer Science at Purdue University. His research interests lie at the intersection of compilers and machine learning. Specifically, utilizing generative programming techniques to build efficient ML systems. |
|
Towards Full Dependent Types in Scala (internal - click to log in) (PL, Theory)
Oliver Bracevac (post-doc with Tiark Rompf) AbstractScala combines strong typing, object-oriented/functional programming, and first-class modules into a single language design. For a long time, the soundness of Scala's type system, especially of path-dependent types, remained an open issue, which was eventually settled by the dependent object types (DOT) calculus as its foundational model, together with its mechanized soundness proof. However, DOT has proven to be difficult to extend, still leaving a large semantic gap between the full Scala language and its foundation. In this talk, I will argue for building Scala's foundation on top of type theory in the sense of Martin-Löf, which is well-understood, and includes dependent types in their most general form. This step promises a streamlined language design, and opens up Scala for certified programming in the league of proof assistants, such as Coq. Furthermore, I outline peaceful coexistence between a rigorous logical sublanguage for theorem proving and a general-purpose programming language. Oliver is a postdoctoral researcher at Purdue University, collaborating with Prof. Tiark Rompf. He has been working at the intersection of programming languages and systems research. His goal is to explore new ways of programming complex systems, to make them simpler, safer, and faster. His contributions span the areas of functional programming, type theory, verification, distributed/reactive programming, as well as stream/event processing. |
|
Combining Context-Aware Neural Translation Models using Ensemble for Program Repair (AI, Program Repair)
Thibaud Lutellier (advisor: Lin Tan) AbstractThibaud is a PhD student at the University of Waterloo, advised by Lin Tan (https://ece.uwaterloo.ca/~tlutelli/) |
|
Metaprogramming for Program Analyzers (PL, Systems)
Guannan Wei (advisor: Tiark Rompf) AbstractBuilding correct, performant and flexible program analyzers is hard. In this talk, I will present our study on applying metaprogramming to improve the construction, performance and flexibility of program analyzers. Two instances covered are abstract interpreters for functional languages and symbolic execution engines for imperative languages. The recipe can be summarized as 1) deriving program analyzers from its concrete definitional interpreter, 2) turning the program analyzer to a staged analyzer (compiler) via staging and the 1st Futamura projection, which generates low-level code and eliminates interpretation overhead, and 3) finally use type and effect systems to model and abstract over the behavior of analyzer, which improves flexibility by modularly interpreting the effects, such as nondeterminism. Guannan is a fourth year doctoral student in computer science at Purdue University, advised by Professor Tiark Rompf. His research area is programming languages, especially with interests in functional programming, type systems, program analysis and metaprogramming. |
|
Secure Evalution of Vectorized Random Forests (internal - click to log in) (Compilers, Crypto, ML)
Raghav Malik (advisor: Milind Kulkarni) AbstractAs the demand for machine learning--based inference increases in tandem with concerns about privacy, there is a growing recognition of the need for secure machine learning, in which secret models can be used to classify private data without the model or data being leaked. Fully Homomorphic Encryption (FHE) allows for arbitrary computation to be done over encrypted data without having to decrypt it first, and therefore provides the building blocks we need to create such systems. While such computation is often orders of magnitude slower than its plaintext counterpart, the ability of FHE cryptosystems to do ciphertext packing-that is, encrypting an entire vector of plaintexts such that operations are evaluated elementwise on the vector-helps ameliorate this overhead through parallelization. This effectively creates a SIMD architecture where computation can be vectorized for more efficient evaluation. Most recent research in this area has focused on applying these techniques to neural network models. Decision forests are a type of machine learning model that excel in applications with categorical data, but their inherent sequential dependences make them difficult to vectorize in an FHE setting. In this paper we present an approach to restructure decision forests in a way that severs the dependences within each tree, thus making the secure evaluation of the forest easier to vectorize as well as parallelize. We also present a framework, SEVR, that automates this restructuring process and compiles decision forest models into vectorized FHE programs that perform inference over the model. We evaluate SEVR by using it to compile and execute several synthetic microbenchmarks as well as real-world models trained on open source data. We find that although execution time largely scales linearly with model size, the reshaped model is highly parallelizable, resulting in performance on large models that exceeds prior results. Raghav is a PhD student at Purdue University, advised by Professor Milind Kulkarni. |
|
Problems and Opportunities in Training Deep-Learning Software Systems: An Analysis of Variance (internal - click to log in) (AI, Empirical Study, Software Systems)
Hung Pham (advisor: Lin Tan) AbstractDeep learning (DL) training algorithms utilize nondeterminism to improve models’ accuracy and training efficiency. Hence, multiple identical training runs (e.g., identical training data, algorithm, and network) produce different models with different accuracy and training time. In addition to these algorithmic factors, DL libraries (e.g., TensorFlow and cuDNN) introduce additional variance(referred to as implementation-level variance) due to parallelism, optimization, and floating-point computation. This work is the first to study the variance of DL systems and the awareness of this variance among researchers and practitioners. Our experiments on three datasets with six popular networks show large overall accuracy differences among identical training runs. Even after excluding weak models, the accuracy difference is still 10.8%. In addition, implementation-level factors alone cause the accuracy difference across identical training runs to be up to 2.9%, the per-class accuracy difference to be up to 52.4%, and the training time to convergence difference to be up to 145.3%. All core(TensorFlow, CNTK, and Theano) and low-level libraries exhibit implementation-level variance across all evaluated versions. Our researcher and practitioner survey shows that 83.8% of the901 participants are unaware of or unsure about any implementation-level variance. In addition, our literature survey shows that only 19.5±3% of papers in recent top software engineering (SE), AI, and systems conferences use multiple identical training runs to quantify the variance of their DL approaches. This paper raises awareness of DL variance and directs SE researchers to challenging tasks such as creating deterministic DL libraries for debugging and improving the reproducibility of DL software and results. |
Neural-Symbolic Modeling for Natural Language Discourse (NLP, Neural-Symbolic Modeling, Probabilistic Logic)
Maria Leonor Pacheco (advisor: Dan Goldwasser)
AbstractBuilding models for realistic natural language tasks requires dealing with long texts and accounting for complicated structural dependencies. Neural-symbolic representations have emerged as a way to combine the reasoning capabilities of symbolic methods, with the expressiveness of neural networks. However, most of the existing frameworks for combining neural and symbolic representations have been designed for classic relational learning tasks that work over a universe of symbolic entities and relations. We present DRAIL, an open-source declarative framework for specifying deep relational models using probabilistic logic, designed to support a variety of NLP scenarios. Our framework supports easy integration with expressive language encoders, and provides an interface to study the interactions between representation, inference and learning. |
|
Reconciling Enumerative and Deductive Program Synthesis (PL, Synthesis)
Yanjun Wang (advisor: Xiakong Qiu) Abstract"Syntax-guided synthesis (SyGuS) aims to find a program satisfying semantic specification as well as user-provided structural hypotheses. There are two main synthesis approaches: enumerative synthesis, which repeatedly enumerates possible candidate programs and checks their correctness, and deductive synthesis, which leverages a symbolic procedure to construct implementations from specifications. Neither approach is strictly better than the other: automated deductive synthesis is usually very efficient but only works for special grammars or applications; enumerative synthesis is very generally applicable but limited in scalability. In this paper, we propose a cooperative synthesis technique for SyGuS problems with the conditional linear integer arithmetic (CLIA) background theory, as a novel integration of the two approaches, combining the best of the two worlds. The technique exploits several novel divide-and-conquer strategies to split a large synthesis problem to smaller subproblems. The subproblems are solved separately and their solutions are combined to form a final solution. The technique integrates two synthesis engines: a pure deductive component that can efficiently solve some problems, and a height-based enumeration algorithm that can handle arbitrary grammar. We implemented the cooperative synthesis technique, and evaluated it on a wide range of benchmarks. Experiments showed that our technique can solve many challenging synthesis problems not possible before, and tends to be more scalable than state-of-the-art synthesis algorithms." Yanjun is a fourth year Ph.D student in Electrical and Computer Engineering at Purdue University, advised by Prof. Xiaokang Qiu. |
|
Snek: Overloading Python Semantics via Virtualization (PL, Systems, ML)
James Decker (advisor: Tiark Rompf) AbstractHigh performance computing libraries implemented in Python often require users to define problems in two forms of computations: those which will be executed in Python; and those which will be executed by a highly-optimized downstream kernel, often implemented in a lower-level language. This pattern can be seen in computation graphs in deep learning libraries (e.g., TensorFlow) and numerical computing frameworks (e.g., JAX), defining symbolic constraints for SMT solvers (e.g., Z3Py), and many other domains. Expressions which must be (eventually) evaluated by the corresponding kernel are expressed using domain-specific syntax in the form of API calls, even if there exist similar constructs in Python, such as control flow expressions. In this talk, we will discuss the use of "language virtualization," essentially an advanced form of operator overloading in which language primitives are redefined as virtual methods able to be overridden by a given frameworks. This allows frameworks to construct symbolic expressions which include any expression in Python, including control flow. We implement our virtualization framework as a system called Snek which represents the first type-driven multi-stage programming framework for a dynamic language, without requiring extra-linguistic mechanisms. We further demonstrate the ability to quickly and easily provide new semantics for Python constructs, while matching or surpassing performance of hand-written code targeting a given back-end. James is a fifth year PhD candidate in Computer Science at Purdue University studying with Tiark Rompf. James is interested in programming languages and compilers as they relate to high performance computing, with an emphasis on machine learning applications on nontraditional architectures. |
|
PolyRec: Composable, Sound Transformations of Nested Recursion and Loops (Compilers, PL)
Kirshanthan Sundararajah (advisor: Milind Kulkarni) AbstractScheduling transformations reorder a program’s operations to improve locality and/or parallelism. The polyhedral model is a general framework for composing and applying instancewise scheduling transformations for loop-based programs, but there is no analogous framework for recursive programs. This work presents an approach for composing and applying scheduling transformations—like inlining, interchange, and code motion—to nested recursive programs. This paper describes the phases of the approach—representing dynamic instances, composing and applying transformations, reasoning about correctness—and shows that these techniques can verify the soundness of composed transformations. Kirshanthan is a PhD student in School of Electrical and Computer Engineering at Purdue University advised by Milind Kulkarni. He is interested in Compilers, Programming Languages and High Performance Computing with an emphasis on optimizing irregular programs. |
|
A Hybrid Model for Learning Embeddings and Logical Rules Simultaneously from Knowledge Graphs (ML, Knowledge Graph Mining, Hybrid Learning Methods)
Susheel Suresh (advisor: Jennifer Neville) AbstractThe problem of knowledge graph (KG) reasoning has been widely explored by traditional rule-based systems and more recently by knowledge graph embedding methods. While logical rules can capture deterministic behavior in a KG they are brittle and mining ones that infer facts beyond the known KG is challenging. Probabilistic embedding methods are effective in capturing global soft statistical tendencies and reasoning with them is computationally efficient. While embedding representations learned from rich training data are expressive, incompleteness and sparsity in real-world KGs can impact their effectiveness. We aim to leverage the complementary properties of both methods to develop a hybrid model that learns both high-quality rules and embeddings simultaneously. Our method uses a cross feedback paradigm wherein, an embedding model is used to guide the search of a rule mining system to mine rules and infer new facts. These new facts are sampled and further used to refine the embedding model. Experiments on multiple benchmark datasets show the effectiveness of our method over other competitive standalone and hybrid baselines. We also show its efficacy in a sparse KG setting and finally explore the connection with negative sampling. Susheel is a third year PhD student in Computer Science at Purdue advised by Prof. Jennifer Neville working towards relational learning and reasoning |
