Intuitionistic type theory is a widely-used framework for constructive mathematics and computer programming. Martin-Lof's meaning explanations justify the rules of type theory by defining types as classifications of programs according to their behaviors. Recently, researchers noticed that the rules of type theory also admit homotopy-theoretic models, and subsequently extended type theory with constructs inspired by these models: higher inductive types and Voevodsky's univalence axiom. Although such higher-dimensional type theories have proved useful for homotopy-theoretic reasoning, they lack a computational interpretation.

In this proposal, I describe a modification of the meaning explanations that accounts for higher-dimensional types as classifications of higher-dimensional programs. I aim to extend these cubical meaning explanations with additional features inspired by other higher-dimensional and computational type theories, and explore the programming applications of higher-dimensional programs.

Thesis Committee:
Robert Harper (Chair)
Jeremy Avigad
Karl Crary
Daniel R. Licata (Wesleyan University)
Todd Wilson (California State University, Fresno)

Copy of Proposal Summary

In this talk, we will discuss the classic bipartite matching problem in the online setting, first introduced in the seminal work of Karp, Vazirani and Vazirani (STOC '90). Specifically, we consider the problem for the well-studied class of regular graphs. Matching in this class of graphs was studied extensively in the offline setting. In the online setting, an optimal deterministic algorithm, as well as efficient algorithms under stochastic input assumptions were known. In this work, we present a novel randomized algorithm with competitive ratio tending to one on this family of graphs, under adversarial arrival order. Our main result is an algorithm which achieves competitive ratio 1-O(\sqrt{\log d} / \sqrt{d}) in expectation on d-regular graphs, and thus the problem becomes easier for randomized algorithms as d increases (for deterministic algorithms, the optimal competitive ratio is known to decrease as d increases, and tends to 1-1/e).

In contrast, we show that all previously-known online algorithms, such as the generally worst-case optimal RANKING algorithm of Karp et al., are restricted to a competitive ratio strictly bounded away from one, even as d grows. Moreover, we show the converge rate of our algorithm's competitive ratio to one is nearly tight, as no algorithm achieves competitive ratio better than 1-O(1 / \sqrt{d}). Finally, we show that our algorithm yields a similar competitive ratio with high probability, as well as guaranteeing each offline vertex a probability of being matched tending to one.

Joint work with Ilan R. Cohen (Hebrew University of Jerusalem).

Machine learning (ML) methods are used to analyze data which are collected from various sources. As the problem size grows, we turn to distributed parallel computation to complete ML training in a reasonable amount of time. However, naive parallelization of ML algorithms often hurts the effectiveness of parameter updates due to the dependency structure among model parameters, and a subset of model parameters often bottlenecks the completion of ML algorithms due to the uneven convergence rate. In this proposal, I propose two efforts: 1) STRADS that improves the training speed in an order of magnitude and 2) STRADS-AP that makes parallel ML programming easier.

In STRADS, I will first present scheduled model-parallel approach with two specific scheduling schemes: 1) model parameter dependency checking to avoid updating dependent parameters concurrently; 2) parameter prioritization to give more update chances to the parameters far from its convergence point. To efficiently run the scheduled model-parallel in a distributed system, I implement a prototype framework called STRADS. STRADS improves the parameter update throughput by pipelining iterations and overlapping update computations with network communication for parameter synchronization. With ML scheduling and system optimizations, STRADS improves the ML training time by an order of magnitude. However, these performance gains are at the cost of extra programming burden when writing ML schedules. In STRADS-AP, I will present a high-level programming library and a system infrastructure that automates ML scheduling. The STRADS-AP library consist of three programming constructs: 1) a set of distributed data structures (DDS); 2) a set of functional style operators; and 3) an imperative style loop operator. Once an ML programmer writes an ML program using STRADS-AP library APIs, the STRADS-AP runtime automatically parallelizes the user program over a cluster ensuring data consistency.

Thesis Committee:
Garth A. Gibson (Co-chair)
Eric P. Xing (Co-chair)
Phillip B. Gibbons
Joseph E. Gonzalez (University of California, Berkeley)

Copy of  Proposal Summary

The identification of anomalies and communities of nodes in real-world graphs has applications in widespread domains, from the automatic categorization of wikipedia articles or websites to bank fraud detection. While recent and ongoing research is supplying tools for the analysis of simple unlabeled data, it is still a challenge to find patterns and anomalies in large labeled datasets such as time evolving networks. What do real communities identified in big networks look like? How can we find sources of infections in bipartite networks? Can we predict who is most likely to join an online discussion on a given topic?

We model interaction networks using appropriate matrix and tensor representations in order to gain insights into these questions. We incorporate edge attributes, such as timestamps in phone-call networks or airline codes in flight networks, and complex node side-information, such as who-retweets-whom in order to understand who uses a given hashtag on Twitter. We provide three major contributions:

1. Hyperbolic communities: Our exploration of real communities provides novel theoretical ideas regarding their structure, and we show how typical long-tail degree distributions can be leveraged to create efficient algorithms on problems that seem to suffer from quadratic explosion.
2. Anomaly detection: Novel distributed algorithms that identify problematic nodes whose influence can only be detected on their neighbors, validated through the analysis of data breaches in bank transactions.
3. Forecasting: New techniques that forecast network evolution by incorporating contextual side-information and the evolution of independent community structures.

Leveraging these techniques, we explore massive datasets such as networks with billions of credit card transactions, Twitter graphs with over 300 million interactions and phone-call networks with over 50 million phone-calls.

Thesis Committee:
Christos Faloutsos (Co-Chair)
Pedro Ribeiro (Co-Chair)
William Cohen
Aarti Singh
Tina Eliassi-Rad (Northeastern University)
Beatriz Santos (University of Aveiro)
Alexandre Francisco (University of Lisbon)

Join the students in the Cognitive Robotics class, who will be demoing their final projects.  All welcomed.

This class uses Anki's new Cozmo robot: the first truly affordable vision-based mobile manipulator. Anki was founded in 2010 by three CMU Robotics PhD students: Boris Sofman, Mark Palatucci, and Hanns Tappeiner. The company has received $208 million in venture funding; Marc Andreesen serves on their board.

Faculty:  David Touretzky

An optimization problem seeks to minimize or maximize the value of an objective function subject to a set of equality and inequality constraints. Many applications in science and engineering often require solving optimization problems, with matrices possibly appearing in the objective function, the constraints set or both. Although most of these problems can be solved exactly using polynomial time algorithms, these algorithms are too slow to deal with the large size of modern datasets and the matrices obtained by the latter.  In practice, fast approximate algorithms, that are designed by carefully trading the accuracy of a solution with the runtime complexity, are preferred to slow exact algorithms. This talk will introduce linear sketching and highlight how it can be used to obtain fast approximate algorithms for least squares regression, least absolute deviations regression and low rank approximation.

Presented in Partial Fulfillment of the CSD Speaking Skills Requirement

In today's datacenters, storage and network resources are shared to lower costs and achieve better utilization, but how does one meet tail latency performance goals in these shared environments? Workloads exhibit different behaviors (e.g., burstiness, load) and can have different latency requirements. Furthermore, storage and networks each exhibit unique performance characteristics that make it hard to provide latency guarantees. For example, in SSD storage devices, writes are slower than reads, while in networks, packets traverse a series of queues and congest with different workloads at each queue.

In this talk, I will describe my thesis work on meeting tail latency goals when sharing storage and networks. Our work looks at the problem from the perspective of scheduling policies, admission control, and workload placement. In particular, we implement new policies and mechanisms for controlling the congestion between multiple workloads of varying burstiness. Our system is unique in that it incorporates mathematically grounded techniques such as Deterministic Network Calculus (DNC) and Stochastic Network Calculus (SNC) to guarantee tail latency. In fact, we are the first to implement SNC in a computer system.

Thesis Committee:
Mor Harchol-Balter (Chair)
Gregory R. Ganger
David G. Andersen
Michael A. Kozuch (Intel Labs)
Arif Merchant (Google)


Subscribe to CSD