May 2014 - talks - lists.cs.princeton.edu

David Shue FPO Monday, May 12, 2014 at 1pm in 402 Computer Science
by Nicki Gotsis 05 May '14

05 May '14

David Shue will present his FPO on Monday, May 12, 2014 at 1pm in 402 Computer Science. The members of his committee are Michael Freedman, advisor; Jennifer Rexford and Anees Shaikh (Google), readers; and Vivek Pai and Margaret Martonosi, nonreaders. A copy of his thesis, "Multi-tenant Resource Allocation For Shared Cloud Storage" is available in room 310. Everyone is invited to attend his talk. Nicki Gotsis Graduate Coordinator Room 310, Computer Science (609) 258-5387 ngotsis(a)cs.princeton.edu

1 0

Speaker: Thomas Dreibholz, Thursday May 8 at 3pm in 301
by Andy Bavier 05 May '14

05 May '14

Everyone is invited to attend this talk. Thomas Dreibholz (Simula Research Laboratory) Thursday, May 8, 3pm Computer Science 301 The NorNet Testbed for Multi-Homed Systems -- Introduction and Status Multi-homing denotes the simultaneous connection of endpoints to multiple Internet Service Providers (ISP). That is, such endpoints should remain reachable even when some of the ISPs have problems. Besides the redundancy aspect, multi-homing can also make load sharing by multi-path transport possible, i.e. increasing the application throughput by utilizing multiple paths simultaneously. The growing need for and deployment of multi-homed applications makes large-scale testing and evaluation in realistic Internet setups necessary. For instance, different paths can have very different characteristics with regard to bandwidth, packet loss rate, congestion, delay and jitter. Therefore, the Simula Research Laboratory is building up the NorNet testbed, which is an open platform for such experiments. NorNet consists of two parts, the wireless part NorNet Edge as well as the wired part NorNet Core, providing researchers the possibility to use programmable, multi-homed nodes at different locations in Norway as well as at some international sites. This talk gives an overview over the NorNet testbed, with a special focus on the usage of the PlanetLab/Linux Containers-based software that is used to run NorNet Core. NorNet homepage: https://www.nntb.no

1 0

Scott Erickson will present his MSE thesis talk on Thursday, May 8th, 2014 at 1:30pm in room 302
by Nicki Gotsis 05 May '14

05 May '14

Scott Erickson will present his MSE thesis talk on Thursday, May 8th, 2014 at 1:30pm in room 302 of the Computer Science Building. His committee is: Michael Freedman, adviser and Vivek Pai as reader. Everyone is invited to attend his talk. His abstract follows below. --------------------------- Abstract: There are an increasing number of users consuming more and more data through mobile apps on their carrier’s metered 3G and 4G connections. However, a certain percentage of this traffic is duplicated, and is thus wasteful. If this duplicated data were to be eliminated, consumers could use their data connections more comfortably while lightening the load on the network. This work presents a system that deduplicates HTTP traffic, and experimentally evaluates its performance. Nicki Gotsis Graduate Coordinator Room 310, Computer Science (609) 258-5387 ngotsis(a)cs.princeton.edu

1 0

Gordon Stewart: Pre-FPO talk announcement (5/12 at 9:30 in Room 302)
by Nicki Gotsis 05 May '14

05 May '14

Gordon Stewart will present his Pre-FPO on Monday, May 12 at 9:30am in Room 302 in the Computer Science Building. The members of his committee are: Andrew Appel (advisor); Zhong Shao and David Walker (readers); David August and Sharad Malik (nonreaders). Everyone is invited to attend his talk. The talk title and abstract follow below: ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Title: Verified Separate Compilation for C ~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~~ Verified separate compilation is the process of independently translating a program's components in a way that preserves correctness of the program as a whole. In the most general case, a verified separate compiler supports heterogeneous source programs, in which some modules are in C or another high-level language while others are written in a lower-level language like x86 assembly, as is common in systems software such as operating systems. A verified separate compiler in this context is one that preserves the behavior of the entire source program, comprising the C and x86 modules, when the C code is compiled to assembly. Separate compilation has numerous practical benefits. It speeds up development cycles by enabling re-compilation of just those source modules that have been edited by the programmer. It enables shared libraries---separately compiled modules mapped at runtime into the virtual address spaces of multiple processes. It promotes modularity in the large, by enabling programmers to write applications containing logically distinct translation units, each composed at a different level of abstraction or even in a different programming language altogether. But perhaps equally important are applications of verified separate compilers to /modular verification/, the act of reasoning independently about each module in a program (with respect to specifications of the other modules) in order to prove whole program correctness. A modular verification approach means the programmer can break the task of proving correctness of large programs into smaller, more manageable steps: First provide specifications of the modules that form the program, then prove independently of each module that the module meets its specification. When modules proved correct in this way are compiled by a semantics-preserving separate compiler, one gets not only that each module is translated correctly to assembly and then machine code, but also that the target whole program---linked and running on the machine---has the same behavior as the source whole program about which the programmer proved a correctness specification. The result is an end-to-end system: Whole program properties proved modularly at the source level are true also of the whole program that results from separate compilation and linking. In this thesis, I present techniques that address the verified separate compilation problem in the context of C-like languages. My work extends state-of-the-art verified compilers for C such as CompCert (http://compcert.inria.fr/)---the correctness proof of which is currently limited to whole programs---to support verified separate compilation. Major results of the thesis are the proof of a separate compilation theorem for C and the novel semantics of inter-language linking on which the statement of the separate compilation theorem depends. I also address applications to verified compilation of coarse-grained concurrent programs, revealing surprising connections between separate compilation and concurrency in the process. To validate the separate compilation result, I show that it supports modular verification of source programs in the Verified Software Toolchain program logic for C (http://vst.cs.princeton.edu/).

1 0

Adrian Soviani's FPO has been rescheduled to 12pm on Friday May 2
by Joseph Crouthamel 02 May '14

02 May '14

Adrian Soviani's FPO has been rescheduled to 12pm on Friday May 2 in Room 402. The members of his committee are: JP Singh, advisor; Kai Li and David August, readers; Brian Kernighan and Andrea LaPaugh, nonreaders. A copy of his thesis, "A Hybrid SPMD - Coarse Grain Dataflow Parallel Programming Model" is available in Room 310. Everyone is invited to attend his talk. Nicki Gotsis Graduate Coordinator Room 310, Computer Science (609)258-5387 ngotsis(a)cs.princeton.edu

2 1