- talks - lists.cs.princeton.edu

Y Zhu preFPO
by Melissa Lawson 23 Feb '11

23 Feb '11

Yaping Zhu will present her preFPO on Tuesday March 1 at 10:30AM in Room 402. The members of her committee are: Jen Rexford, advisor; Vivek Pai and Aman Shaikh (AT&T Labs Research), readers; Mike Freedman and Andrea LaPaugh, nonreaders. Everyone is invited to attend her talk. Her abstract follows below. -------------------------------------- Minimizing Wide-area Performance Disruptions in Inter-domain Routing Abstract The Internet is the platform for most of our communications needs today. However, network changes like routing changes or congestion lead to performance disruptions, which would affect the user experience. Therefore, minimizing performance disruptions is crucial, and network operators have to react and fix the problems. Diagnosing wide-area performance disruptions is challenging: first, each network has limited visibility into the root cause of performance disruptions, requiring network operators to collect and analyze measurements of routing and traffic data; second, there are so many potential factors which might lead to performance disruptions, and these factors are usually interdependent with each other. Thus, the network diagnosis is usually done in an ad-hoc manner, and there are no formalized ways to define metrics and classify the performance disruption according to the causes. The thesis conducts two case studies to diagnose wide-area performance disruptions from the perspectives of a large tier-1 ISP and a large CDN: i) From the ISP's perspective, we designed and implemented a system that tracks inter-domain route changes at scale and in real time. Our system could be used as the building block for many diagnosis scenarios for the ISPs. ii) From the CDN's perspective, we focus on diagnosing wide-area network changes which caused latency increases to access the services in the CDN. We proposed a method for automatically classifying large increases of latency, and evaluated our techniques on one month of measurement data to identify major sources of high latency for a large CDN. Stepping back from the protocol designer's perspective, we refactor the inter-domain routing protocol BGP (Border Gateway Protocol), based on the lessons learned from the case studies: first, since each network only has limited visibility and control within its own network and the neighbors, we propose to select a route only based on the next- hop AS. second, the BGP protocol is not designed with operational challenges of performance and security in mind. Thus, there are many proposals to add additional BGP attributes and satisfy the operational needs. These proposals make the protocol and configuration complicated and error-prone, and make it difficult for network operators to diagnose problems. Instead, we argue to separate the performance and security requirements out of the protocol. Our proposal of next-hop BGP simplifies the protocol, and has the benefits of fast convergence, incentive compatibility, and easier support for multi-path routing.

1 0

Colloquium Speaker Aleksander Madry- Feb 23
by Nicole E. Wagenblast 21 Feb '11

21 Feb '11

Electrical Flows and Laplacian Systems: A New Tool for Graph Algorithms Aleksander Madry, Massachusetts Institute of Technology Wednesday, February 23rd, 4:30pm Computer Science Small Auditorium, CS105 In recent years, the emergence of massive computing tasks that arise in context of web applications and networks has made the need for efficient graph algorithms more pressing than ever. In particular, it lead us to focus on reducing the running time of the algorithms to make them as fast as possible, even if it comes at a cost of reducing the quality of the returned solution. This motivates us to expand our algorithmic toolkit to include techniques capable of addressing this new challenge. In this talk, I will describe how treating a graph as a network of resistors and relating the combinatorial properties of the graph to the electrical properties of the resulting circuit provides us with a powerful new set of tools for the above pursuit. As an illustration of their applicability, I will use these ideas to develop a new technique for approximating the maximum flow in capacitated, undirected graphs that yields the asymptotically fastest-known algorithm for this problem. Aleksander is a PhD candidate in Computer Science at MIT, advised by Michel Goemans and Jonathan Kelner. His research focuses on algorithmic graph theory, i.e. design and analysis of very efficient (approximation) algorithms for fundamental graph problems. He also enjoys investigating topics in combinatorial optimization - especially the ones involving dealing with uncertainty.

1 1

Colloquium speaker, Nick Feamster, Wed. Feb. 16th
by Nicole E. Wagenblast 15 Feb '11

15 Feb '11

Challenges and Opportunities for Tomorrow's Networks Nick Feamster, Georgia Tech Wednesday, February 16 , 4:30pm Computer Science Building, Small Auditorium, 105 The Internet is the underlying fabric for nearly all of our day-to-day communication; it is an undeniable success. More than a billion people around the world now have Internet access, and that number is projected to at least double in the next 10 years. The Internet is seeing increasing penetration in various resource-challenged environments, both in this country and abroad. These new frontiers for networking offer exciting opportunities, but they also pose serious challenges. Internet attacks are proliferating. Networks are becoming increasingly complex and difficult to troubleshoot. More than 20 countries around the world censor at least some Internet content. Our personal and private data is falling into the hands of a few large content providers. The performance of networks in homes, and how humans interact with them, are both poorly understood. These coming challenges will require us to think differently about networking: a discipline that has focused almost exclusively on performance must begin thinking more about people. In this talk, I will take a retrospective view of some important networking innovations over the past 10 years, surveying some solutions we and others have developed to improve the Internet's security, manageability and availability. I will then take a look forward at new challenges, and argue that to solve the most pressing problems for networking today, we must draw on techniques from a broad range of areas, including policy, economics, programming languages and human-computer interaction. Nick Feamster is an assistant professor in the College of Computing at Georgia Tech. He received his Ph.D. in Computer science from MIT in 2005, and his S.B. and M.Eng. degrees in Electrical Engineering and Computer Science from MIT in 2000 and 2001, respectively. His research focuses on many aspects of computer networking and networked systems, including the design, measurement, and analysis of network routing protocols, network operations and security, and anonymous communication systems. In December 2008, he received the Presidential Early Career Award for Scientists and Engineers (PECASE) for his contributions to cybersecurity, notably spam filtering. His honors also include a Sloan Research Fellowship, the NSF CAREER award, Technology Review's TR35 award, the IBM Faculty Fellowship, and award papers at SIGCOMM 2006, the NSDI 2005 conference, Usenix Security 2002 and Usenix Security 2001.

1 1

Colloquium Speaker, Mark Braverman, Tuesday Feb 15
by Nicole E. Wagenblast 14 Feb '11

14 Feb '11

Average-case solutions to hard problems Mark Braverman , University of Toronto Tuesday, February 15, 2011- 4:30pm Computer Science, 105 Many important computational problems are affected by various computational barriers that make them intractable in the worst case. In spite of this, it is often possible to get around these barriers and produce useful, if not optimal solutions for most instances of the problem. I will use several examples from my work to illustrate how considering an average or a typical case of the problem can be used to produce useful algorithms and mechanisms. The first example deals with the problem of assigning medical graduates to residency programs in the presence of married couples. The problem of finding a stable matching between residency programs and doctors without couples is solved by the famous Gale-Shapley algorithm. In the presence of couples, such a matching may not exist, and it is NP-hard to determine whether it exists or not. Still, in a large random market we show how to find a good stable outcome with high probability. The second example deals with aggregating noisy comparison signals, such as sport competition results, into a ranking most consistent with the observed signals. The worst-case version of the problem, known as the Minimum Feedback Arcset problem is NP-hard. We give an efficient algorithm for the average-case version of the problem.

1 0

Physics Colloquium-"Computer vision and optics in the study of fine art"
by Andrew W. Appel 04 Feb '11

04 Feb '11

1 0

S Jafarpour preFPO
by Melissa Lawson 04 Feb '11

04 Feb '11

Sina Jafarpour will present his preFPO on Friday February 11 at 2PM in Room 402. The members of his committee are: Robert Calderbank; advisor, Rob Schapire and Ingrid Daubechies (Duke); readers, and David Blei and Amit Singer (PACM and Math); non-readers. Everyone is invited to attend his talk. His abstract follows below. --------------------------------------------- Title: Deterministic Compressed Sensing The central goal of compressed sensing is to capture attributes of a signal using very few measurements. The initial publications by Donoho and by Candes and Tao have been followed by applications to image compression, data streaming, medical signal processing, digital communication and many others. The emphasis has been on random sensing but the limitations of this framework include performance guarantees, storage requirements, and computational cost. This talk will describe two deterministic alternatives. The first is based on expander graphs. We show that by reformulating signal reconstruction as a zero-sum game we can efficiently recover any sparse vector. We also demonstrate resilience to Poisson noise. The second is based on error correcting codes. We show that deterministic sensing matrices based on second order Reed Muller codes optimize average case performance. We also describe a very simple algorithm, one-step thresholding, that succeeds where more sophisticated algorithms, developed in the context of random sensing, fail completely. The talk is based on joint work with Waheed Bajwa, Robert Calderbank, Volkan Cevher, Marco Duarte, Zachary Harmany, Stephen Howard, Maxim Raginsky, Rob Schapire, and Rebecca Willett.

1 0

M Carroll FPO
by Melissa Lawson 20 Jan '11

20 Jan '11

Melissa Carroll will present her FPO on Wednesday January 26 at 2:30PM in Room 402. The members of her committee are: Rob Schapire, advisor; Ken Norman (PSY) and Irina Rish (IBM), readers; David Blei and Peter Ramadge (ELE), nonreaders. A copy of her thesis, "FMRI "Mind Readers": Sparsity, Spatial Structure, and Reliability", is on display in Room 310. Everyone is invited to attend her talk.

1 0

G Stewart General Exam
by Melissa Lawson 12 Jan '11

12 Jan '11

Gordon Stewart will present his research seminar/general exam on Wednesday January 19 at 2PM in Room 402. The members of his committee are: Andrew Appel 9advisor), David Walker, and David August. Everyone is invited to attend his talk, and those faculty wishing to remain for the oral exam following are welcome to do so. His abstract and reading list follow below. ----------------------------------- Abstract ======== Soundness proofs of program logics such as Hoare logics and type systems are often made easier by decorating the operational semantics with information that is useful in the proof. However, modifying the operational semantics to carry around such information can make it more difficult to show that the operational semantics corresponds to what actually occurs on a real machine. In this work we present a program logic framework targeting operational semantics in Curry-style--that is, operational semantics without proof decora- tions such as separation algebras, share models, and step indexes. Although we target Curry-style operational semantics, our framework permits local reason- ing via the frame rule and retains expressive assertions in the program logic. Soundness of the program logic is derived mechanically from simple properties of primitive commands and expressions. We demonstrate our framework by deriving a separation logic for the model of a core imperative programming language with external function calls. We also apply our framework in a more realistic setting in the soundness proof of a separation logic for CompCert's Cminor. Our proofs are machine-checked in Coq. Research Papers =============== [Appel and Blazy 2007] A. W. Appel and S. Blazy. Separation logic for small- step Cminor. In 20th Intl Conference on Theorem Proving in Higher-Order Logics, pages 5-21, 2007. [Calcagno et al. 2007] C. Calcagno, P. W. O'Hearn, and H. Yang. Local ac- tion and abstract separation logic. In LICS'07: Proceedings of the 22nd Annual IEEE Symposium on Logic in Computer Science, pages 366-378, 2007. ISBN 0-7695-2908-9. doi: http://dx.doi.org/10.1109/LICS.2007.30. [Dockins et al. 2009] R. Dockins, A. Hobor, and A. W. Appel. A fresh look at separation algebras and share accounting. In The 7th Asian Symposium on Programming Languages and Systems. Springer ENTCS, 2009. URL http://msl.cs.princeton.edu/fresh-sa.pdf. [Lahiri 2008] S. Lahiri, S. Qadeer. Back to the future: revisiting precise program verification using SMT solvers. In POPL'08: Proceedings of the 35th annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 2008. [Lerner 2003] S. Lerner, T. Millstein, and C. Chambers. Automatically Proving the Correctness of Compiler Optimizations. In PLDI'03: Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, 2003. [Leroy 2009] X. Leroy. Formal verification of a realistic compiler. Communica- tions of the ACM, 52(7):107-115, 2009. [Leroy and Blazy 2008] X. Leroy and S. Blazy. Formal verification of a C-like memory model and its uses for verifying program transformations. J. Au- tomated Reasoning, 41(1):1-31, 2008. [Necula 1997] G. Necula. Proof-Carrying Code. In POPL'97: Proceedings of the 24th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, 1997. [Parkinson 2010] M. Parkinson. The next 700 separation logics. In G. Leavens, P. O'Hearn, and S. Rajamani, editors, Verified Software: Theories, Tools, Experiments, volume 6217 of Lecture Notes in Computer Science, pages 169-182. Springer Berlin / Heidelberg, 2010. [Parkinson et al. 2006] M. Parkinson, R. Bornat, and C. Calcagno. Variables as resource in Hoare logics. Proc. of 21st Annual IEEE Symp. on Logic in Computer Science, 0:137-146, 2006. ISSN 1043-6871. [Reynolds 2002] J.C. Reynolds. Separation Logic: a Logic for Shared Mutable Data Structures. In LICS'02: Proceedings of the 17th Annual IEEE Symposium on Logic in Computer Science, pages 55 - 74, 2002. Textbooks ========= [Pierce 2002] B. Pierce. Types and Programming Languages. 2002. [Winskell 1993] G. Winskell. The Formal Semantics of Programming Languages (Chapters 1-7). 1993.

1 0

W Josephson FPO
by Melissa Lawson 04 Jan '11

04 Jan '11

William Josephson will present his FPO on Tuesday January 11 at 2:30 PM in Room 302 (note Room!) The members of his committee are: Kai Li, advisor; Jen Rexford and Brian Kernighan, readers; Mike Freedman and Doug Clark, nonreaders. A copy of his thesis, "A Direct-Access File System for a New Generation of Flash Memory", is on display in Room 310. Everyone is invited to attend his talk.

1 0

S Ihm preFPO
by Melissa Lawson 13 Dec '10

13 Dec '10

Sunghwan Ihm will present his preFPO on Friday December 17 at 2PM in Room 401 (note room!) The members of his committee are: Vivek Pai, advisor; Jen Rexford and Larry Peterson, readers; Mike Freedman and Andrea LaPaugh, nonreaders. Everyone is invited to attend his talk. His abstract follows below. ---------------------- Title: Understanding and Improving Modern Web Traffic Caching As Web sites move from relatively static displays of simple pages to rich media applications with heavy client-side interaction, the nature of the resulting Web traffic changes as well. At the same time, Web traffic also increases due to the popularity of social networking, video streaming, file-hosting sites, and consolidation of existing applications to the Web. Understanding the nature of these changes grows more difficult without a better characterization of the underlying traffic, which is necessary to improve response time, analyze caching effectiveness, and to design intermediary systems, such as firewalls, security analyzers, and reporting/management systems. Unfortunately, while the Web has been studied heavily in the past, we still have little understanding of today's Web - what has been changed, and what we can do better about it. In this thesis, we revisit the previous issues with today's Web, focusing on characterizing traffic and developing a new caching technique which outperforms previous approaches. Specifically, we analyze five years (2006-2010) of real Web traffic from a globally-distributed proxy system, which captures the browsing behavior of over 50,000 users. Using this data set, we also develop a new page detection algorithm that is better suited for the modern Web page interactions, and investigate the redundancy of this traffic, using both traditional object-level caching as well as content-based approaches. Among many findings, we observe a huge potential benefit of the content-based caching approach in today's Web - the byte hit rate is almost twice larger than that of the traditional object-level caching approach. Motivated by the promising benefit of content-based caching, we also develop Wanax, a scalable and flexible wide-area network (WAN) accelerator. It uses a novel multiresolution chunking (MRC) scheme that provides high compression rates and high disk performance for a variety of content, while using much less memory than existing approaches. Wanax exploits the design of MRC to perform intelligent load shedding to maximize throughput even when running on resource-limited shared platforms. Finally, Wanax exploits mesh network environments, instead of just the star topologies common in enterprise branch offices.

1 0