- talks - lists.cs.princeton.edu

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

Colloquium Speaker Monday 12/13- Dan Morris
by Nicole E. Wagenblast 10 Dec '10

10 Dec '10

What Human-Computer Interaction and Medicine Can Offer Each Other Dan Morris, Microsoft Research Monday, December 13, 2010, 4:30pm Computer Science Small Auditorium, CS105 Our work sits at the intersection of Human-Computer Interaction (HCI) and Medicine. That means that 50% of what we do is applying HCI methodology to problems in medicine, so we can spend the other 50% of our time "borrowing" technologies from medicine and applying them to HCI. This talk, therefore, will focus on two topics: (a) patient-friendly medical information displays, and (b) sensing physiological signals for computer input. In the first part of the talk, I'll present our work on making electronic medical record data more useful to patients, work that spans both qualitative research ("what *should* patient interfaces look like?") and technology research ("how do we actually build that without asking doctors to spend hours explaining everything to us?"). In the second part of the talk, I'll present our work on using sensing techniques that medical science has known about for centuries (like measuring electrical muscle activity, and measuring body acoustics) to build new computer input systems. This part of the talk will have cool videos, so bring your popcorn. Dan Morris is a researcher in the Computational User Experiences group at Microsoft Research; he is interested in novel input devices, patient-facing medical technology, and computer support for music and creativity. Dan studied neurobiology as an undergraduate at Brown, and developed brain-computer interfaces: first at Brown, and later as an engineer at Cyberkinetics, Inc. His PhD thesis at Stanford focused on haptic rendering and physical simulation for virtual surgery, and his work since coming to MSR (in 2006) has included using physiological signals for input systems, designing patient-friendly information displays for hospitals, and generating automatic accompaniment for sung melodies. If you would like to see both his research talents and his (lack of) performance talents showcased in one four-minute masterpiece, search for "Microsoft Songsmith Commercial".

1 1

M Burns FPO
by Melissa Lawson 08 Dec '10

08 Dec '10

Michael Burns will present his FPO on Tuesday December 14 at 10AM in Room 402. The members of his committee are: Adam Finkelstein, advisor; Szymon Rusinkiewicz and Doug DeCarlo (Rutgers), readers; Perry Cook and Tom Funkhouser, nonreaders. A copy of his thesis, "Efficient and Comprehensible Visualization of Complex 3-D Scenes", is on display in Room 310. Everyone is invited to attend his talk.

1 0

colloquium speaker Wed. 12/8- Xiaowei Yang
by Nicole E. Wagenblast 07 Dec '10

07 Dec '10

Bootstrapping Accountability in the Internet We Have Xiaowei Yang, Duke University Wednesday December 8, 4:30pm Computer Science Building small auditorium, CS105 The lack of accountability makes the Internet vulnerable to numerous attacks, including prefix hijacking, route forgery, source address spoofing, and DoS flooding attacks. This work takes a "dirty-slate" approach to bring accountability to the present Internet with low-cost and deployable enhancements. In this talk, we will present IPA, a network architecture that uses the readily available top-level DNSSEC infrastructure and BGP to bootstrap accountability. We integrate IPA with a suite of security building blocks to combat various network-layer attacks. Our evaluation shows that IPA introduces modest overhead, is gradually deployable , and offers security incentives to early adopters. Xiaowei Yang is an assistant professor in the Department of Computer Science at Duke University. Before joining Duke, she was an assistant professor in the Department of Computer Science at the University of California at Irvine. She received a PhD in Computer Science from Massachusetts Institute of Technology, and a BE from Tsinghua University. She is a receipt of the NSF CAREER award.

1 1

R Fiebrink FPO
by Melissa Lawson 06 Dec '10

06 Dec '10

Rebecca Fiebrink will present her FPO on Monday December 13 at 1:30PM in room 402. The members of her committee are: Perry Cook, advisor; Dan Trueman and Dan Morris (Microsoft), readers; Adam Finkelstein and Ken Steiglitz, nonreaders. A copy of her thesis, "Real-Time Human Interaction with Supervised Learning Algorithms for Music Composition and Performance", is on display in Room 310. Everyone is invited to attend her talk.

1 0

M Bateni preFPO
by Melissa Lawson 06 Dec '10

06 Dec '10

Mohammad Hossein Bateni will present his preFPO on Monday December 13 at 10:30AM in Room 302 (note room!). The members of his committee are: Moses Charikar, advisor; Sanjeev Arora and MohammadTaghi Hajiaghayi (UMCP), readers; Bernard Chazelle and Rob Schapire, nonreaders. Everyone is invited to attend his talk. His abstract follows below. -------------------------- Grouping a set of items into clusters according to their similarities is called clustering. It is now a common technique in widely different applications in, e.g., bioinformatics, data mining, machine learning, and social network analysis. Considerable effort has been put into study of the clustering techniques in recent years. In this thesis, we introduce a new clustering paradigm, in which items to be classified are vertices of a graph. Vertices have their own budgets and the goal is to cluster them such that the cost of (connections in) each cluster can be payed by the budget of its participants. Furthermore, we want vertices in different clusters be in some sense far from each other. We propose and analyze algorithms for two similar problems in this paradigm. The resulting guarantees lead to resolution of several network design questions. We improve the approximation ratio for prize-collecting Steiner tree and TSP. In addition, we present polynomial-time approximation schemes (PTAS's) for planar Steiner forest, planar multiway cut, and planar prize-collecting Steiner tree. The talk is based on joint works with Aaron Archer, MohammadTaghi Hajiaghayi, Howard Karloff, Philip Klein, Daniel Marx, and Claire Mathieu.

1 0

A Badam preFPO
by Melissa Lawson 06 Dec '10

06 Dec '10

Anirudh Badam will present his preFPO on Monday December 13th at 2.30PM in Room 401 (note room!). The members of his committee are: Vivek Pai, advisor; Mike Freedman and Jennifer Rexford, readers; David Walker and Andrea LaPaugh, non-readers. Everyone is invited to attend his talk. His abstract follows below. ------------------------------ "On Scaling the Memory-Storage Boundary" In this work, we examine approaches for addressing the growing gap between the main memory of today's systems and their storage layers. The ever increasing amount of data and the need to access more of it quickly has magnified the gap between the main memory and the traditional secondary storage devices. The limited memory capacity of servers coupled with the limits of RAM density imposes a large premium on obtaining high in-memory hit-rates that are vital for today's servers. In this thesis, we focus on two new methods to bridge this gap: we create new approaches to increase the indexing efficiency of secondary storage using current main memory limits, and we also develop techniques to better integrate new high-speed storage technologies like flash memory based solid state drives (SSD) and phase change memory (PCM) into the memory hierarchy. In both cases, we can increase effective memory/storage capacity and cost effectiveness by at least an order of magnitude. First, we present the design and implementation of HashCache, an efficient hash table representation that can be used as an index for web-proxy caches, WAN accelerators, data deduplicators, and memory object caches. HashCache presents a flat, pointer-less, space-efficient and tlb-optimized hash table implementation. Using HashCache, systems can increase the amount of secondary storage that can be indexed for the same amount of main memory by up to 20 times. We also present the design and implementation of SSDAlloc, which augments RAM with new high-density, high-performance and non-volatile memory technologies. We specifically focus on hybrid RAM/SSD settings and we believe that our techniques will be equally useful in hybrid RAM/PCM settings. Using these new memory technologies via the swap-layer, which works at a page granularity, can decrease the performance and reliability of these memories, owing to their well-known limited lifetime issues. Similarly, using these memories via a filesystem/object-store interface would need intrusive application modifications. Our technique eliminates these intrusive modifications while providing high performance and reliability by managing the SSD and the RAM at an object granularity entirely via virtual memory. SSDAlloc uses the SSD as a log-structured object store and the RAM as a compact object cache while the application operates via the page-granular virtual memory. Finally, we demonstrate the benefits of SSDAlloc by developing a HashCache based memory object cache in a hybrid RAM/SSD setting using SSDAlloc. The same system built using SSDAlloc performs up to 17.1 times better when compared to the one built with the SSD as a swap-layer, and up to 3.5 times better when compared to the one built with the SSD as a log-structured swap-layer. Additionally, the system built using SSDAlloc writes up to 32 times less data when compared to both the SSD-swap based systems while requiring only a few code modifications.

1 0

Colloquium Speaker Sep Kamvar- Wed. Dec. 1
by Nicole E. Wagenblast 29 Nov '10

29 Nov '10

The Challenges (and Joys!) of Personalizing Web Search Sep Kamvar, Stanford University Wednesday, December 1, 2010, 4:30pm Computer Science Small Auditorium, CS105 The personalization of search results has long been seen as an important strategic direction for search engines. However, it was not until the past few years where personalized search was possible at scale. In this talk, I will talk about the algorithms that made web-scale personalized search possible. I will discuss some special characteristics of the structure of the web (and the eigenstructure of the web matrix), and describe the computational techniques used to exploit this structure to compute of PageRank much faster than by standard methods. The resulting speed allowed the computation of an individualized ranking for every user on the web, resulting in a dramatic improvement in search relevance. Sep Kamvar is a consulting professor of Computational and Mathematical Engineering at Stanford University. His research focuses on personal and social models for search. >From 2003 to 2007, Sep was the head of personalization at Google. Prior to Google, he was founder and CEO of Kaltix, a personalized search company that was acquired by Google in 2003. Sep is the author of two books and over 40 technical publications and patents in the fields of search and social computing. He is on the technical advisory boards of several companies, including Aardvark, Etsy, and Hunch. His artwork has been exhibited at the Museum of Modern Art in New York, the Victoria and Albert Musem in London, and the National Museum of Contemporary Art in Athens.

1 1