- talks - lists.cs.princeton.edu

Alex Iriza will present his Master's thesis talk on Thursday, September 10, 2015 at 1:30pm in CS 401
by Nicki Gotsis 09 Sep '15

09 Sep '15

Alex Iriza will present his Master's thesis talk on Thursday, September 10, 2015 at 1:30pm in CS 401. The members of his committee are Jérémie Lumbroso (adviser) and Bob Sedgewick (co-adviser). Everyone is invited to attend his talk. His abstract follows below. Title: Enumeration and random generation of unlabeled classes of graphs: a practical study of cycle pointing and the dissymmetry theorem Abstract: Our work studies the enumeration and random generation of unlabeled combinatorial classes of unrooted graphs. While the technique of vertex pointing provides a straightforward procedure for analyzing a labeled class of unrooted graphs by first studying its rooted counterpart, the existence of nontrivial symmetries in the unlabeled case causes this technique to break down. Instead, techniques such as the dissymmetry theorem (of Otter) and cycle pointing (of Bodirsky et al.) have emerged in the unlabeled case, with the former providing an enumeration of the class and the latter providing both an enumeration and an unbiased sampler. In this work, we extend the power of the dissymmetry theorem by showing that it in fact provides a Boltzmann sampler for the class in question. We then present an exposition of the cycle pointing technique, with a focus on the enumeration and random generation of the underlying unpointed class. Finally, we apply cycle pointing to enumerate and implement samplers for the classes of distance-hereditary graphs and three-leaf power graphs.

1 0

Joey Dodds will present his FPO "Computation Improves Interactive Symbolic Execution" on Thursday, 9/10/2015 at 10am in CS 302
by Nicki Gotsis 01 Sep '15

01 Sep '15

Joey Dodds will present his FPO, "Computation Improves Interactive Symbolic Execution," on Thursday, 9/10/2015 at 10:00 AM, CS 302. The members of his committee are: Andrew Appel (adviser); Readers: David Walker, Jesper Bengtson(IT University of Copenhagen); Nonreaders: Sharad Malik, Aarti Gupta A copy of his thesis is available in Room 310. Everyone is invited to attend his talk. The talk title and abstract follow below: ________________________________________________________ "Computation Improves Interactive Symbolic Execution" As it becomes more prevalant throughout our lives, correct software is more important than it has ever been before. Verifiable C is an expressive Hoare logic (higher-order impredicative concurrent separation logic) for proving functional correctness of C programs. The program logic is foundational—it is proved sound in Coq w.r.t. the operational semantics of CompCert Clight. Users apply the program logic to C programs using semiautomated tactics in Coq, but these tactics are very slow. This thesis shows how to make an efficient (yet still foundational) symbolic executor based on this separation logic by using computational reflection in several different ways. Our execution engine is able to interact gracefully with the user by reflecting application-specific proof goals back to the user for interactive proof—necessary in functional correctness proofs where there is almost always domain-specific reasoning to be done. We use our “mostly sound” type system, computationally efficient finite-map data structures, and the MirrorCore framework for computationally reflected logics. Measurements show a 40× performance improvement.

1 1

lunch talk Tue Sep 1 on "Building efficient network dataplanes in software"
by Jennifer Rexford 31 Aug '15

31 Aug '15

Speaker: Luigi Rizzo, from Universita` di Pisa Title: Building efficient network dataplanes in software Date/time: 12pm lunch and 12:30-1:30pm talk, Tuesday September 1 Location: CS 402 Abstract: In this talk we give a survey of solutions -- and especially, discuss the underlying design principles -- that we developed in recent years to achieve extremely high packet processing rates in commodity operating systems, for both bare metal and virtual machines. By using simple abstractions, and resisting the temptation to design systems around performant but constraining assumptions, we have been able to build a very flexible framework that addresses the speed and latency communication requirements of both bare metal and virtual machines up to the 100 Gbit/s range. Our goal is not to provide the fastest framework in the universe, but one that is easy to use and rich of features (and still, amazingly fast), to taking away concerns on the dataplane's speed from (reasonable) network applications. Our NETMAP framework, opensource and BSD licensed, runs on 3 OSes (FreeBSD, Linux, Windows); provides access to NICs, host stack, virtual switches and point-to-point channels (netmap pipes), running between 20 and over 100Mpps on software ports, and saturating NICs with just a single core (reported up to 45 Mpps on recent 40G nics); achieves bare-metal speed on VMs thanks to a virtual passthrough mode (available for Qemu and bhyve); and can be used with no modifications by libpcap clients. Bio: Luigi Rizzo is an associate professor at the Universita` di Pisa. He has worked on network emulation, high performance networking, packet scheduling, multicast and reliable multicast. He is a long time contributor to FreeBSD, for which he has developed several subsystems including the dummynet network emulator, the ipfw firewall, and the netmap framework. He has been program committe member for for sigcomm, conext, infocom, nsdi, Usenix ATC, ANCS and other conferences, as well as PC chair for Sigcomm 2009 and Conext 2014, ANCS 2016, and general chair for Sigcomm 2006. Luigi has been a frequent visiting researcher at various institutions including ICSI/UC Berkeley, Google Mountain View, Intel Research Cambridge, Intel Research Berkeley.

1 0

Siemens talks next week: 12-1:30pm Tue Aug 25 on cybersecurity, 12-1:30pm Thu Aug 27 on engineering complex systems
by Jennifer Rexford 22 Aug '15

22 Aug '15

Two talks this coming week from Siemens in Princeton Siemens Corporation Summer Lunch & Learn Series Tuesday, August 25, Noon-1:30 PM EQuad, Room J223 Cyber Security and its impact on Siemens & Corporate Technology Lunch will be provided Benjamin Collar, Head of Research Group – Cyber Security Americas is a dynamic engineering executive who excels in developing teams and individuals. As head of cyber-security research at Siemens Corporate Technology, Benjamin leads a team of security experts who execute and support the security strategy of the Siemens operating companies. He is a strong advocate for cyber-security and privacy within the company as well as in the public. Ben is constantly seeking new ways to break barriers and challenge the status quo as he creatively drives results across organizational boundaries. Thursday, August 27, Noon-1:30 PM EQuad, Room J201 Engineering Complex Systems – Fun with Large Spatial, Temporal, Fidelity, and Parameter Spaces Lunch will be provided Dr. Arquimedes Canedo is a Principal Key Expert Scientist at Siemens Corporate Technology in Princeton, NJ. Arqui is very passionate about developing technologies for multi-disciplinary and multi-scale design, engineering, and simulation of complex systems. This talk aims at motivating graduate students, from all backgrounds, to develop ideas that will help to develop the next-generation engineering tools for complex systems. He will introduce some of the problems associated with modern engineering with a few real-world examples that illustrate the need for better tools for integrating multi-disciplinary systems. He will also present some of the research efforts at Siemens Corporate Technology in the area of industrial Automation and Control. Arqui will share his own experience on working at Siemens Corporate Technology. About Siemens Siemens Corporation is a U.S. subsidiary of Siemens AG, a global technology powerhouse that has stood for engineering excellence, innovation, quality, reliability and internationality for more than 165 years. For more than 30 years, Siemens Corporation, Corporate Technology (CT) have been developing breakthroughs in science and emerging technologies. Corporate Technology (CT), is comprised of more than 300 of the world’s most talented scientists, engineers and technical experts from over two dozen countries. Cross-functional research teams bring together a broad range of technical and business expertise from different disciplines. We have US locations in Princeton, NJ, Berkeley, CA and Charlotte, NC.

1 0

Joshua Kroll will present his FPO, "Accountable Algorithms" on Friday, August 21, 2015 at 11am in Sherrerd Hall 306.
by Nicki Gotsis 12 Aug '15

12 Aug '15

Joshua Kroll will present his FPO, "Accountable Algorithms" on Friday, August 21, 2015 at 11am in Sherrerd Hall 306. The members of his committee are: Readers: Arvind Narayanan, Matthew Green (Johns Hopkins University) Examiners: Edward Felten (adviser), Andrew Appel, and Nicholas Feamster A copy of his thesis is available in Room 310. Everyone is invited to attend his talk.

1 0

EE Seminar - August 10, 2015, 11:00 am, E-Quad B205 - Prof. Gernot Heiser
by Nicole E. Wagenblast 30 Jul '15

30 Jul '15

SeminarLogo.jpg Speaker: Prof. Gernot Heiser University of New South Wales Title: Towards Principled Temporal Isolation in the Operating System Date: Monday, August 10, 2015 Time: 11:00 a.m. Room: E-Quad, Room B205 Host: Prof. Ruby Lee Abstract: Spatial isolation, i.e. controlling memory access, forms the basis of protection in operating systems. However, this is neither sufficient for ensuring safe operation of real-time systems, nor for ensuring confidentiality. It must be complemented by temporal isolation, i.e. preventing a process from unduly influencing the execution speed of another process. Most operating systems provide very poor temporal isolation if any. Exceptions are systems designed to support a narrow class of applications (either hard real-time systems or separation kernels for security-critical uses), which also tend to have high overheads or force low system utilisation. The formally-verified seL4 microkernel is a general-purpose high-assurance platform that is intended to support a wide range of uses, including highly performance-sensitive mobile systems, (safety) multi-criticality systems and (security-critical) cross-domain solutions. We are therefore after mechanisms that provide strong temporal isolation where needed, but avoid overheads where not. The talk will discuss present work in progress on simple kernel mechanisms that will allow us to achieve those goals. Biography: Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at UNSW, and leads the Software Systems Research Group at NICTA, Australia’s National Centre of Excellence for ICT Research. He joined NICTA at its creation in 2002, and before that was a full-time member of academic staff at UNSW from 1991. His past work included the Mungi single-address-space operating system (OS), several un-broken records in IPC performance, and the best-ever reported performance for user-level device drivers. More recently he led the team at NICTA which produced the world’s first formal proof of functional correctness of a protected general-purpose operating-system kernel, the first published sound worst-case execution time analysis of a protected OS kernel, and the synthesis of high-performance device drivers. In 2006, Gernot with a number of his students founded Open Kernel Labs, to market secure virtualization technology for embedded systems. The company’s OKL4 operating system, a descendent of L4 kernels developed by his group at UNSW and NICTA, is deployed in billions of mobile devices, and now ships on the security processor of all iOS devices. Open Kernel Labs was sold to General Dynamics in August 2012.

1 0

11am Mon Aug 10 talk in E-Quad B205 on principled temporal isolation in operating systems
by Jennifer Rexford 30 Jul '15

30 Jul '15

> From: "Lori A. Bailey" <lbailey(a)Princeton.EDU> > Subject: EE Seminar - August 10, 2015, 11:00 am, E-Quad B205 - Prof. Gernot Heiser > Date: July 30, 2015 at 11:42:49 AM EDT > To: ee-seminar(a)Princeton.EDU > Reply-To: "Lori A. Bailey" <lbailey(a)Princeton.EDU> > > > Speaker: Prof. Gernot Heiser > University of New South Wales > Title: Towards Principled Temporal Isolation in the Operating System > Date: Monday, August 10, 2015 > Time: 11:00 a.m. > Room: E-Quad, Room B205 > Host: Prof. Ruby Lee > > Abstract: Spatial isolation, i.e. controlling memory access, forms the basis of protection in operating systems. However, this is neither sufficient for ensuring safe operation of real-time systems, nor for ensuring confidentiality. It must be complemented by temporal isolation, i.e. preventing a process from unduly influencing the execution speed of another process. Most operating systems provide very poor temporal isolation if any. Exceptions are systems designed to support a narrow class of applications (either hard real-time systems or separation kernels for security-critical uses), which also tend to have high overheads or force low system utilisation. > > The formally-verified seL4 microkernel is a general-purpose high-assurance platform that is intended to support a wide range of uses, including highly performance-sensitive mobile systems, (safety) multi-criticality systems and (security-critical) cross-domain solutions. We are therefore after mechanisms that provide strong temporal isolation where needed, but avoid overheads where not. The talk will discuss present work in progress on simple kernel mechanisms that will allow us to achieve those goals. > > > Biography: Gernot Heiser is Scientia Professor and John Lions Chair of Operating Systems at UNSW, and leads the Software Systems Research Group at NICTA, Australia’s National Centre of Excellence for ICT Research. He joined NICTA at its creation in 2002, and before that was a full-time member of academic staff at UNSW from 1991. His past work included the Mungi single-address-space operating system (OS), several un-broken records in IPC performance, and the best-ever reported performance for user-level device drivers. More recently he led the team at NICTA which produced the world’s first formal proof of functional correctness of a protected general-purpose operating-system kernel, the first published sound worst-case execution time analysis of a protected OS kernel, and the synthesis of high-performance device drivers. > > In 2006, Gernot with a number of his students founded Open Kernel Labs, to market secure virtualization technology for embedded systems. The company’s OKL4 operating system, a descendent of L4 kernels developed by his group at UNSW and NICTA, is deployed in billions of mobile devices, and now ships on the security processor of all iOS devices. Open Kernel Labs was sold to General Dynamics in August 2012. > > > > > > . > >

1 0

Haipeng Luo will present his Pre FPO on July 27, 2015 at 2pm in CS 401
by Nicki Gotsis 27 Jul '15

27 Jul '15

Haipeng Luo will present his Pre FPO on July 27, 2015 at 2pm in CS 401. The committee members are Robert Schapire (adviser); Elad Hazan and Readers: Satyen Kale (Yahoo Labs); and Non-readers: Sanjeev Arora, Barbara Engelhardt Everyone is invited to attend his talk. The talk title and abstract follow below: Title: Optimal and Adaptive Online Learning Online learning is one of the important and well-established learning models in the area of machine learning. Generally speaking, the goal of online learning is to make a sequence of accurate predictions â€œon the flyâ€ when interacting with the environment. Online learning has been extensively studied in recent years, and has also become of great interest to practitioners due to its applicability to large scale applications such as advertisement placement and recommendation systems. Existing online learning algorithms, however, are not always directly applicable in practice, because they usually rely on sophisticated tuning of parameters that gives sound theoretical guarantees but hardly works in practice. In this thesis, our main focus is thus to design practical and ready-to-use online learning algorithms that are parameter-free and work simultaneously under different patterns of data as well as different evaluation criteria. Our main contributions are new optimal and adaptive algorithms for the following three online learning problems: 1. We study the classic problem of online learning by combining expert advice with several new and challenging goals. By converting the problem into a â€œdrifting gameâ€ and analyzing the approximate minimax optimal solutions, we propose a new parameter-free algorithm called AdaNormalHedge. Our algorithm is the first one that achieves several desirable objectives simultaneously, including learning from unknown or even infinite number of experts, competing with a sequence of unknown competitors, and achieving much better performance when dealing with easy problems, while still ensuring worst case robustness in difficult situations. Our results lead to significant improvements in several applications, such as predicting almost as well as the best pruning tree of a decision tree. 2. The second problem we study is online boosting. Boosting is one of the central methodology in machine learning that studies the task of combining weak rule-of-thumbs into a strong learning algorithm. While it is well-studied in the offline batch setting, there is very few work on the theory of online boosting. We thus develop a set of optimal and adaptive online boosting algorithms, some that achieve arbitrarily small error under a novel notion of weak online learnability, and the others which converge to the best possible achieved by the linear combination of weak learners. Experiments on benchmark data are conducted to show that our new algorithms indeed improve upon previous work. 3. The last problem we investigate is online learning without knowing the actual time horizon, which is yet another important feature for a practical algorithm. Previously, different techniques have been used, such as the so-called â€œdoubling trickâ€ which is unfortunately inelegant and wasteful. We formalize this problem as a game and study the exact minimax optimal solutions. We first prove that learning with unknown time horizon is strictly harder, and then propose a simple minimax optimal algorithm for a special case. Based on this special case, we further develop a new algorithm for the general case which, although not being exact optimal, enjoys a better performance guarantee compared to previous work.

2 2

Taewook Oh will present his FPO on Tuesday, 7/28/2015 at 9:30am, 401 Computer Science
by Nicki Gotsis 20 Jul '15

20 Jul '15

Taewook Oh will present his FPO, "AUTOMATIC EXPLOITATION OF INPUT PARALLELISM, on Tuesday, 7/28/2015 at 9:30am, 401 Computer Science The members of his committee are Prof. David August (advisor); Readers: Prof. Brian Kernighan, Prof. Scott Mahlke (Univ. of Michigan) ; Non-readers: Prof. Andrew Appel, Prof. Sharad Malik (ELE). A copy of his thesis is available in Room 310. Everyone is invited to attend his talk.

1 0

today: 11am talk on measuring Internet quality of experience
by Jennifer Rexford 20 Jul '15

20 Jul '15

Speaker: Renata Teixeira, Inria Paris-Rocquencourt Title: HostView: Measuring Internet quality of experience on end-hosts Date/time: 11:00am-12:00pm Monday July 20 Location: CS 402 Abstract: There is much interest recently in doing automated performance diagnosis on user laptops or desktops. One interesting aspect of performance diagnosis that has received little attention is the user perspective on performance. To conduct research on both end-host performance diagnosis and user perception of network and application performance, we designed an end-host data collection tool, called HostView. HostView not only collects network, application and machine level data, but also gathers feedback directly from users. User feedback is obtained via two mechanisms, a system-triggered questionnaire and a user-triggered feedback form, that for example asks users to rate the performance of their network and applications. This talk will describe our experience with the first deployment of HostView. Using data from 40 users, we articulate the challenges in this line of research, and report on initial findings in correlating user data to system-level data. We then describe our more recent efforts in conducting an in-depth study with twelve users in France to guide our design of the next version of HostView and of methods to infer user context and activities. This is joint work with Diana Joumblatt, Jaideep Chandrashekar, Nina Taft, Anna-Kaisa Pietilainen, George Rosca, Peter Tolmie, Tom Rodden, Tom Lodge, Richard Motier. This work is funded in part by the EU FP7 User-Centric Networking project, Grant No. 611001. Bio: Renata Teixeira received the Ph.D. degree in computer science from the University of California, San Diego, in 2005. During her Ph.D. studies, she worked on Internet routing at the AT&T Research. She was a researcher with the Centre National de la Recherche Scientifique (CNRS) at LIP6, UPMC Sorbonne Universites, Paris, France from 2006 to 2013. She joined Inria Paris-Rocquencourt as senior researcher in October 2013. She was a visiting scholar at UC Berkeley/ICSI in 2011. Her research interests are in measurement, analysis, and management of data networks. She has authored more than 60 papers in this area. Renata is vice-chair of ACM SIGCOMM. She is a member of the steering committee of the ACM Internet Measurement Conference and has been active in the program committees of ACM SIGCOMM, ACM IMC, ACM CoNEXT, PAM, IEEE INFOCOM, among others.

1 0