December 2007 - talks - lists.cs.princeton.edu

talk at 11am on routing-protocol convergence by Pierre Francois
by Jennifer Rexford 14 Dec '07

14 Dec '07

TALK ANNOUNCEMENT: Title: BGP convergence in much less than a second Speaker: Pierre Francois, Universite Catholique de Louvain Date: 11:00am on Friday December 14 Location: CS room 402 Abstract -------- This talk will about recent improvements to the Border Gateway Protocol, the routing protocol used by Internet Service Providers to exchange routing information to provide Internet-wide connectivity. It will show how a fast recovery of connectivity can now be achieved in the case of a link or node failure within an ISP network. We will emphasize that most business cases allow a local BGP recovery (convergence) in case of failure, i.e. a convergence where inter-domain path exploration is actually not required to recover the connectivity after a failure. We will show that although convergence could be local, iBGP deployements do not favor the propagation of alternate paths within an ISP network, which artificially lead to transient lack of connectivity, disclosed to neighboring peers. We will then turn to router implementation issues that could not allow a fast convergence of BGP due to the scaling factors of BGP Reaching sub-second convergence of BGP will however be shown possible by first allowing a better propagation of alternate paths within ISP networks, and second enable the recent improvements to BGP router implementations and to Forwarding Information Bases designs.

1 0

F Perry preFPO
by Melissa M Lawson 13 Dec '07

13 Dec '07

Frances Perry will present her preFPO on Wednesday December 19 at 10:30 AM in Room 402. The members of her committee are: David Walker, advisor; Andrew Appel and David Tarditi (Microsoft), readers; David August and Margaret Martonosi, nonreaders. A copy of her abstract follows below. Everyone is invited to attend her talk. Formal Reasoning about Transient Faults My thesis research focuses on guaranteeing that software is reliable in the presence of transient faults. A transient fault occurs when an energetic particle strikes a chip and causes a change in state in the processor. These faults do not cause permanent damage, but they may affect the computation that is currently executing. Transient faults have been shown to be the cause of crashes at major companies, and current technology trends, such as decreasing transistor size, will make future processors much more susceptible. Researchers in architecture and compilers have already developed a number of different solutions using software, hardware or a combination of the two. The general approach of all these solutions is to duplicate computations and check for consistency between the copies. Unfortunately, generating correct fault-tolerant code is difficult, and there has been very little research on verifying these techniques. Testing is rarely sufficient because full coverage would require testing all combinations of features in conjunction with all combinations of faults. Along with colleagues, I designed a new type system that guarantees that faulty executions of a well-typed program are identical to non-faulty executions up to the point where a fault is detected. We use a hybrid hardware-software solution in which an added hardware queue buffers the stores from the original computation and only writes them to memory if the duplicate computation agrees. Faults can occur at any point and randomly modify a register or queue value. The assembly-level type system tracks information about the two computations which we use to rigorously prove that well-typed programs satisfy reliability properties. We use these reliability properties to show that all executions containing a single fault will always detect the fault before the difference from non-faulty versions becomes observable. More recently, I designed a typed system for reasoning about software solutions for control-flow faults. Control-flow faults arise when a fault causes a jump or branch instruction to transfer control to an unexpected code address. Current software solutions can detect most, but not all, control-flow faults. I formally analyzed a subset of these solutions that can detect any fault that causes incorrect control transfers between basic blocks. Similarly to the previous work, this is accomplished by using a type system to track reliability properties. However, the type system contains new techniques that allow it to reason soundly even when code transfers to an unexpected location and continues executing. Here, I proved that executions with a single fault will visit at most one incorrect block before the fault is detected.

1 0

M Hibbs FPO
by Melissa M Lawson 13 Dec '07

13 Dec '07

Matt Hibbs will present his FPO on Thursday December 20 at 2PM in Icahn Labs Room 280. The members of his committee are; Olga Troyanskaya, advisor; Tom Funkhouser and Kai Li, readers; David Botstein (Genomics) and Leonid Kruglyak (Mol Bio), nonreaders. A copy of his thesis, "Analysis and Visualization of Large-Scale Gene Expression Microarray Compendia" is on display in Room 310. Everyone is invited to attend his talk.

1 0

Talk Today
by Ginny Hogan 12 Dec '07

12 Dec '07

Shaz Qadeer, Microsoft Research, will present his talk, "Taming Concurrency: A Program Verification Perspective", 4:15pm Computer Science room 105 -

1 0

11am Fri Dec 14 talk on routing-protocol convergence by Pierre Francois
by Jennifer Rexford 10 Dec '07

10 Dec '07

TALK ANNOUNCEMENT: Title: BGP convergence in much less than a second Speaker: Pierre Francois, Universite Catholique de Louvain Date: 11:00am on Friday December 14 Location: CS room 402 Abstract -------- This talk will about recent improvements to the Border Gateway Protocol, the routing protocol used by Internet Service Providers to exchange routing information to provide Internet-wide connectivity. It will show how a fast recovery of connectivity can now be achieved in the case of a link or node failure within an ISP network. We will emphasize that most business cases allow a local BGP recovery (convergence) in case of failure, i.e. a convergence where inter-domain path exploration is actually not required to recover the connectivity after a failure. We will show that although convergence could be local, iBGP deployements do not favor the propagation of alternate paths within an ISP network, which artificially lead to transient lack of connectivity, disclosed to neighboring peers. We will then turn to router implementation issues that could not allow a fast convergence of BGP due to the scaling factors of BGP Reaching sub-second convergence of BGP will however be shown possible by first allowing a better propagation of alternate paths within ISP networks, and second enable the recent improvements to BGP router implementations and to Forwarding Information Bases designs.

1 0

Speaker Wednesday -
by Ginny Hogan 10 Dec '07

10 Dec '07

Shaz Qadeer, Microsoft Research, will present his talk "Taming Concurrency: A Program Verification Perspective" Wednesday Dec 12th at 4:15 pm Computer Science Room 105 -

1 0

Wed. Dec 12th: Shaz Qadeer: "Taming Concurrency: A Program Verification Perspective"
by David Walker 07 Dec '07

07 Dec '07

December 12th (next Wednesday) Shaz Qadeer from Microsoft research is visiting Princeton. He is an expert in analysis of concurrent programs and will be giving a distinguished lecture entitled "Taming Concurrency: A Program Verification Perspective". If you would like to meet with him (faculty or students), please pick a timeslot on Wednesday and put yourself on his schedule by editing this file: ~dpw/qadeer His abstract and bio are list below. Thanks, Dave ********************************************************** * Taming Concurrency: A Program Verification Perspective * * Shaz Qadeer * * Microsoft Research * ********************************************************** Concurrency, as a basic primitive for software construction, is more relevant today than ever before, primarily due to the multi-core revolution. General-purpose software applications must find ways to exploit concurrency explicitly in order to take advantage of multiple cores. However, experience has shown that explicitly parallel programs are difficult to get right. To deliver compelling software products in the multi-core era, we must improve our ability to reason about concurrency. Generalizing well-known sequential reasoning techniques to concurrent programs is fundamentally difficult because of the possibility of interference among concurrently-executing tasks. In this lecture, I will present reduction and context-bounding, two ideas that alleviate the difficulty of reasoning about interference by creating a simpler view of a concurrent execution than an interleaving of thread instructions. Reduction reduces interference by making a sequence of instructions in a thread appear as a single atomic instruction; it allows the programmer to view an execution as a sequence of large atomic instructions. Context-bounding reduces interference by focusing on executions with a small number of context switches; it allows the programmer to view an execution as a sequence of large thread contexts. I will present the theory behind these two approaches and their realization in a number of program verification tools I have developed over the years. Bio: Shaz Qadeer is a researcher in the Software Reliability Research group at Microsoft Research. The goal of his research is to develop tools for improving the productivity of programmers. He has worked on many program verification tools, spanning the range from run-time verification to model checking to static analysis, with an emphasis on tools for concurrent programs. Shaz received his Ph.D. at UC Berkeley and worked at Compaq Systems Research Center before joining Microsoft Research.

1 0