Distributed systems form the foundation of our society's infrastructure. Complex distributed protocols and algorithms are used in enterprise storage systems, distributed databases, large-scale planetary systems, and sensor networks. Errors in these protocols translate to denial of service to some clients, potential loss of data, and even monetary losses. Unfortunately, it is notoriously difficult to develop reliable high-performance distributed systems that run over asynchronous networks, such as the Internet. Even if a distributed system is based on a well-understood distributed algorithm, its implementation can contain coding bugs and errors arising from complexities of realistic distributed environments.

This talk describes CrystalBall, a new approach for developing and deploying distributed systems. In CrystalBall, nodes predict distributed consequences of their actions, and use this information to detect and avoid errors. Each node continuously runs a state exploration algorithm on a recent consistent snapshot of its neighborhood and predicts possible future violations of specified safety properties. We describe a new state exploration algorithm, consequence prediction, which explores causally related chains of events that lead to property violation. Using CrystalBall, we identified new bugs in mature Mace implementations of a random overlay tree, BulletPrime content distribution system, and the Chord distributed hash table. Furthermore, we show that if the bug is not corrected during system development, CrystalBall is effective in steering the execution away from inconsistent states at run-time, with low false negative rates.

The Internet is afflicted by unwelcome "requests", defined broadly as claims on a scarce resource, such as a server's CPU (in the case of spurious traffic whose purpose is to deny service) or a human's attention (in the case of spam). Traditional responses to these problems apply heuristics: they try to identify "bad" requests based on their content (e.g., in the way that spam filters analyze an email's text). This talk argues that heuristics are inherently gameable and that defenses should instead aim to allocate resources proportionally to all clients (so if, say, 10% of the requesters of some scarce resource are "bad", those clients should be limited to 10% of the resources).

To meet this goal, this talk presents two systems. The first is a denial-of-service mitigation in which clients are encouraged to automatically send *more* traffic to a besieged server. The "good" clients can thereby compete equally with the "bad" ones. The second is a distributed system for enforcing per-sender email quotas to control spam. This system scales to a workload of millions of requests per second, tolerates arbitrary faults in its constituent hosts, and resists a variety of attacks. It achieves this fault-tolerance despite storing only one copy (roughly) of any given datum and, ultimately, does a fairly large job with fairly little mechanism.

Database replication has received a lot of attention during the last decade. This wave of research has concentrated on how to obtain scalable database replication. This talk will be devoted to the most recent advances on how to attain scalable database replication contributed by the Distributed Systems Lab (LSD) at Universidad Politenica de Madrid. It will address the most important bottlenecks that limit scalability such as isolation level, degree of replication, recovery, and engineering issues. The talk will cover techniques to overcome these bottlenecks. Special emphasis will be put on the role of snapshot isolation as enabling factor of large scalability to overcome the scalability limit of serializability. The talk will also cover other techniques building upon snapshot isolation to overcome other scalability bottlenecks such as partial replication.

The inclusion of OpenJDK 6 into the core of Fedora, Debian, OpenSuse and Ubuntu has enabled millions of GNU/Linux users to easily obtain the latest version of the Java SE platform. This has changed the packaging landscape for Java software, since ISVs and distro builders can now rely on the Java platform being available out of the box. Planned enhancements to the Java programming language aim to further simplify packaging by making Java software more modular and more explicit about its dependencies.

In this talk, I will present FlightPath, a novel peer-to-peer streaming application that provides a highly reliable data stream to a dynamic set of peers. FlightPath offers a more stable stream than previous works by several orders of magnitude. I will explain the techniques we use to maintain such stability despite peers that act maliciously and selfishly.

More broadly, this talk will discuss the core of FlightPath's success: approximate equilibria. I will highlight how these equilibria let us rigorously design incentives to limit selfish behavior, yet also provide the flexibility to build practical systems. Specifically, I will show how we use epsilon-Nash equilibria to engineer a live streaming system to use bandwidth efficiently, absorb flash crowds, adapt to sudden peer departures, handle churn, and tolerate malicious activity.

The Scala language (http://www.scala-lang.org/) aims to unify object-oriented and functional programming, while maintaining full interoperability with the Java language. However, while Scala has been under active development since 2003, there has yet to be a satisfactory formal model of Scala. There are several calculi that come close, but all have discrepancies in expressive power, some are lacking complete proofs, and some are unsound.

In this talk, I will give a short introduction to Scala, review several calculi that fall short of providing a formal model of Scala, and give an overview of the calculus I have been developing, Scala Classic, that will help fill this gap in the foundations of Scala.

We describes a flexible and easily extensible predicate abstraction-based approach to the verification of STL usage, and observe the advantages of verifying programs in terms of high-level data structures rather than low-level pointer manipulations. We formalize the semantics of the STL by means of a Hoare-style axiomatization. The verification requires an operational model conservatively approximating the semantics given by the C++ standard. Our results show advantages (in terms of errors detected and false positives avoided) over previous attempts to analyze STL usage.

This talk introduces the Checker Framework, which supports adding pluggable type systems to the Java language in a backward-compatible way. A type system designer defines type qualifiers and their semantics, and a compiler plug-in enforces the semantics. Programmers can write the type qualifiers in their programs and use the plug-in to detect or prevent errors. The Checker Framework is useful both to programmers who wish to write error-free code, and to type system designers who wish to evaluate and deploy their type systems.

The Checker Framework includes new Java syntax for expressing type qualifiers; declarative and procedural mechanisms for writing type-checking rules; and support for flow-sensitive local type qualifier inference and for polymorphism over types and qualifiers. The Checker Framework is well-integrated with the Java language and toolset.

We have evaluated the Checker Framework by writing 5 checkers and running them on over 600K lines of existing code. The checkers found real errors, then confirmed the absence of further errors in the fixed code. The case studies also shed light on the type systems themselves.

Model-based development of adaptive embedded systems is an approach to deal with the increased complexity adaptation imposes on system design. Integrating formal verification techniques into this design process providesmeans to rigorously prove critical properties. However, most verification tools are based on foundational models, e.g. automata, unable to express intuitive notions used in model-based development appropriately. Furthermore, automatic methods such as model checking are only efficiently applicable to systems of limited sizes due to the state-explosion problem. Our approach to alleviate these problems uses a semantics-based integrationof model-based development and formal verification for adaptive embedded systems allowing to capture design-level models at a high level of abstraction. Verification complexity induced by the applied modelling concepts is reduced by verified model transformations. These transformations include model slicing, data domain abstractions and compositional reasoning techniques. The overall approach as well as the model transformations have been evaluated together with the development of an adaptive vehicle stability control syste

In this talk, I will present my recent work on the Expandable Network Disk (END). END aggregates storage on a cluster of machines into a single virtual disk. END's main goals are to offer good performance during normal operation, and to resume operation quickly after changes in the cluster, specifically machine crashes, reboots, and additions.

END achieves these goals using a two-layer design, in which storage ``bricks'' hold two kinds of information. The lower layer stores replicated immutable ``chunks'' of data, each indexed by a unique key. The upper layer maps each block address to the key of its current content; each mapping is held on two bricks using primary-backup replication. This separation allows END flexibility in where it stores chunks and thus efficiency: it writes new chunks to bricks chosen for speed, it moves only address mappings (not data) when bricks fail and recover, it fully replicates new writes when a brick is unavailable, and it uses chunks on a recovered brick without risk of staleness.

The END prototype's write throughput on a cluster of 16 PC-based bricks is 150 MByte/s with 2x replication, about 70% of the aggregate throughput of the underlying hardware. END continues after a single brick failure, re-incorporates a rebooting brick, and expand to include a new brick after a few seconds of reduced performance during each change. (Joint work with Robert Morris.)

Seemingly fundamental limitations in hardware manufacturing are driving an industry-wide move away from speedy but complex single core processors towards simpler but massively parallel many-core processors. The job of discovering parallelism (and hence achieving performance) on these new chips is left to software: that is, the programmers and their tools. Parallel programming has traditionally been a specialty area requiring extensive expertise, and non-deterministic concurrency introduces vast new classes of exceptionally difficult to eliminate bugs. In short, the job of programming becomes much harder on many-core processors. In order for programmers to cope successfully with these challenges, the software tools used to program many-core processors must take a giant leap forward. Specifically, programming abstractions and languages must be designed to allow programmers to easily express parallelism in a way that is scalable, performant, and most of all, correct. This talk discusses the problem in more detail, and describes two projects aimed at supporting this goal. The Pillar implementation language is a C-like high level compiler target language intended to provide the key sequential and concurrent constructs needed to efficiently implement task-parallel languages, while the Ct language is a system for exploiting the key area of data-parallelism using ideas from functional programming. Together, these two systems provide a foundation upon which a wide variety of abstractions and languages for expressing parallelism can be built.

We study the application of modular static analysis to prove program safety and detection of program errors. In particular, we shall consider imperative programs that rely on numerical invariants.

To handle the challenges of disjunctive analyses, we introduce the notion of affinity to characterize how closely related is a pair of disjuncts. Finding related elements in the conjunctive (base) domain allows the formulation of precise hull and widening operators lifted to the disjunctive (powerset extension of the) base domain. We have implemented a static analyzer based on the disjunctive polyhedral analysis where the relational domain and the proposed operators can progressively enhance precision at a reasonable cost. Our second objective is to support either a proof of the absence of bugs in the case of a valid program or bug finding in the case of a faulty program. We propose a dual static analysis that is designed to track concurrently two over-approximations: the success and the failure outcomes. Due to the concurrent computation of outcomes, we can identify two significant input conditions: a never-bug condition that implies safety for inputs that satisfy it and a must-bug condition that characterizes inputs that lead to true errors in the execution of the program.

Kurzweil says, computers will enable people to live forever and doctors will be doing backup of your memories by late 2030. This talk is not about that, yet. Instead, the remarkable drop in disk costs makes it possible and attractive to retain past application states and store them for a long time for "time-travel". A still open question is how to best organize long-lived past state storage? Split snapshots are a recent approach to virtualized past states that is attractive for several reasons. Split snapshots are persistent, can be taken with high-frequency, and theyare transactionally consistent. Unmodified database application code can run against them. Like no other approach, they provide low-cost discriminated garbage collection of unneeded snapshots, a useful feature in long-lived systems. Lastly, compared to a temporal database, split snapshots are significantly simpler and more general since they virtualize disk blocks rather than logical records.

Several novel techniques underly split snapshots. An extended recovery invariant allows to create consistent copy-on-write snapshots without blocking, a new kind of persistent index provides fast snapshot access, and a new snapshot storage organization incrementally garbage collects selected copy-on-write snapshots without copying and without creating disk-fragmentation. Measurements of a prototype system indicate that the new techniques are efficient and scalable, imposing minimal ($4\%$) performance penalty on a storage system, on expected common workloads. (Joint work with Ross Shaull and Hao Xu)

Despite its increasing importance in our lives, the Internet remains insecure and its global properties unknown. Spam, phishing, and Denial of Service (DoS) attacks have become common, while global properties as basic as the router-connectivity graph continue to elude researchers. Further, these two problems are inter-related: curtailing abuse exposes gaps in knowledge of the Internet's underlying structure, and studying the underlying structure exposes new techniques to curtail abuse. My research leverages this insight by working on both securing and understanding the Internet.

In this talk, I first discuss my work in securing the Internet by describing Opt-Ack, a DoS attack on the network using optimistic acknowledgments. With this attack, malicious TCP receivers "optimistically" acknowledge packets they did not receive and cause unwitting TCP senders to flood the network. Using Opt-Ack, the resulting traffic flood is hundreds to millions of times the attacker's true bandwidth. I demonstrate randomly skipped segments, an efficient and incrementally deployable solution to the Opt-Ack attack.

Second, I describe my work in understanding the Internet with DisCarte, a constraint-solving system that infers the Internet router-connectivity graph. DisCarte uses disjunctive logic programming to cross-validate topology information from TTL-limited traceroute probes and the often ignored IP Record Route option against observed network engineering practices. Compared to previous techniques, router-connectivity graphs produced by DisCarte are more accurate and contain more features.

D Frama-C is a framework dedicated to build static analyzers for C programs and make them cooperate to achieve better results. One important component of this cooperation is the ANSI/ISO C Specification Language (ACSL), a JML-like language allowing to formally specify the behavior of C functions and statements. The analyses can indeed generate verification conditions as ACSL formulas that will be taken as input by the other ones (and hopefully discharged at some point). This talk will first present the existing Frama-C analyses. Then, we will have a look at the main ACSL constructions. Last, we will show how these constructions can be used for the specification of existing code, and how Frama-C could be extended to deal with C++.

How did you use the Internet today? The answer to this question has significantly evolved in the last decade. Ten years ago, we were browsing simple websites with text and images, and communicating via instant messaging and emails. In addition to these applications, today's users are engaging in on-demand video streaming, multimedia conferencing, and sharing files from software updates to personal music, and as a result transferring large volumes of data (of the order of Mbytes) more frequently than ever. Hence, bulk data transfers at the core of these applications are becoming increasingly important and are expected to provide high throughput and efficiency. Contrary to these expectations, however, our study of file sharing networks confirms previous observations that bulk data transfers are slow and inefficient, motivating the need to rethink their design. In this talk, I will present my approach to address a prominent performance bottleneck for these bulk data transfers: Lack of sufficient sources of data to download from. My work addresses this challenge by (1) exploiting network peers that serve files similar to the file being downloaded, and (2) by coupling all the available network resources with similar data on the local disk of a receiver. My talk will also highlight the system design and implementation for the above solutions. For example, I will discuss handprinting, a novel and efficient algorithmic technique to locate the additional similar network peers with only a constant overhead. Finally, a transfer system that simultaneously benefits from disk and network is required to work well across a diverse range of operating environments and scenarios resulting from varying network and disk performance. I will present the design principles for an all-weather transfer system that adapts to a wide spectrum of operating conditions by monitoring resource availability.

The Internet has seen a tremendous growth since its inception four decades ago. With its increasing importance, there has been a growing emphasis on improving the reliability of the infrastructure. One approach to delivering such reliability is for design engineers, network administrators and researchers to stress test potential solutions against a wide variety of deployment scenarios. For instance, web hosting services would wish to ensure that they can deliver target levels of performance and availability under a range of conditions. Similarly, Internet Service Providers (ISPs) would benefit from understanding future growth in traffic demands at individual routers in its network as a function of emerging applications and expanding user base.

I argue that one of the key ingredients required to carry out such studies is a deep understanding of Internet traffic characteristics. This talk will try to uncover some of the mysteries surrounding Internet traffic, including its rich structure. I will thus describe the principles and key insights that led to the development of the Swing traffic generator. Swing is the first tool to reproduce realistic and responsive Internet-like traffic in a testbed. Starting from observing packets across a given link, Swing automatically extracts parameters for its detailed multi-level model. It then uses this model to generate live traffic that looks qualitatively similar to the original traffic. More interestingly, Swing provides the user with meaningful knobs to project traffic demands into the future. This includes changing assumptions about user popularity of applications, planned upgrades to the network as well as change in the semantics of applications.

Type inference is a key component of modern, statically typed, functional programming languages, such as Caml and Haskell. It allows programmers to omit many excessive---and in some cases all---type annotations from programs.

A different key component of modern programming languages is polymorphism. However, languages with polymorphism typically have ad-hoc restrictions on where and what kind of polymorphic types may occur. Supporting ``first-class'' polymorphism, by lifting those restrictions, is obviously desirable, but it is hard to achieve without sacrificing type inference.

In this talk I will explain the difficulties with type inference for first-class polymorphism, give a historic roadmap of the research on this topic, and present a new type system for first-class polymorphism that improves on earlier proposals: it is an extension of ML type inference; it has a simple, declarative specification; typeability is robust to program transformations; and the specification enjoys a sound, complete and decidable type inference algorithm.

This is joint work with Stephanie Weirich and Simon Peyton Jones.

Computer games and virtual worlds present the next frontier in digital entertainment and social interaction. An important aspect of computer games is the artificial intelligence (AI) of non-player characters. To create interesting AI in games today, we can create complex, dynamic behavior for a very small number of characters, but neither the game engines nor the style of AI programming enables intelligent behavior that scales to a very large number of non-player characters. I will talk about modeling game AI as a data management problem, providing a scalable framework for games with a huge number of non-player characters. I will also discuss applications of this idea to crowd simulations. I will conclude with scalability challenges for Massively Multiplayer Online Games and collaborative environments.

This talk describes joint work with Alan Demers, Christoph Koch, and Walker White.

Network-enabled mobile devices are quickly becoming ubiquitous in the lives of ordinary people, but current technologies for providing ubiquitous global *connectivity* between these devices still require experts to set up and manage. Users must allocate and maintain global domain names in order to connect to their devices globally via DNS, they must allocate a static IP address and run a home server to use Mobile IP or set up a virtual private network, they must configure firewalls to permit desired remote access traffic while filtering potentially malicious traffic from unknown parties, and so on. This model of "management by experts" works for organizations with administrative staff, but is infeasible for most consumers who wish to set up and manage their own personal networks.

The Unmanaged Internet Architecture (UIA) is a suite of design principles and experimental protocols that provide robust, efficient global connectivity among mobile devices while relying for configuration only on simple, intuitive management concepts. UIA uses "personal names" rather than traditional global names as handles for accessing personal devices remotely. Users assign these personal names via an ad hoc device introduction process requiring no central allocation. Once assigned, personal names bind securely to the global identities of their target devices independent of network location. Each user manages one namespace, shared among all the user's devices and always available on each device. Users can also name other users to share resources with trusted acquaintances. Devices with naming relationships automatically arrange connectivity when possible, both in ad hoc networks and using global infrastructure when available. We built a prototype implementation of UIA that demonstrates the utility and feasibility of these design principles. The prototype includes an overlay routing layer that leverages the user's social network to provide robust connectivity in spite of network failures and asymmetries such as NATs, a new transport protocol implementing a novel stream abstraction that more effectively supports the highly parallelized and media-oriented applications demanded on mobile devices, and a flexible security framework based on proof-carrying authorization (PCA) that provides "plug-in" interoperability with existing secure naming and authentication systems.

Bryan Ford is a faculty candidate

The expressive power of functional and object-oriented languages derives in part from their higher-orderness: through closures and objects, code becomes data. This talk focuses on meeting the challenges that such power poses for static analysis and its clients. (To make the talk more accessible, a brief history of the higher-order analysis is included.)

Since its discovery in the 1980s, higher-order control-flow analysis (CFA) has enabled many critical program optimizations, such as flow-directed inlining and static virtual-method resolution. Over the past two decades, much research in higher-order analysis focused on improving the speed and precision of CFA. Despite frequent encounters with the limits of CFAs, little progress had been made in moving beyond them, as measured by the kinds of optimizations made possible and the kinds of questions made answerable.

The key limitation of CFAs is the inherently coarse approximation that they inflict upon environment structure. This talk centers on my development of environment analysis---techniques which break through these limitations of twenty years standing. Of particular note is that these techniques evade the cost/precision tradeoff usually found in program analyses: compared to previous techniques, they provide improvements in both power and precision, yet also reduce the cost of the compile-time analysis in practice. Using environment analysis as a foundation, my recent work on logic-flow analysis has continued to expand the reach of higher-order analysis beyond optimization and into realms such as security and verification.

Matthew Might is a faculty candidate

Making the right model assumptions is crucial in developing robust and efficient computing systems. The ability of a model to solve distributed computing problems is primarily defined by the /synchrony assumptions/ the model makes. Given that many problems in distributed computing are impossible to solve in the asynchronous way, it is very important to determine the minimal synchrony assumptions that are sufficient to solve a given problem. These assumptions can be conveniently encapsulated in the /weakest failure detector/ abstraction.

In this talk, I will focus on defining the "weakest failure detector ever": the failure detector that is strong enough to circumvent /some/ asynchronous impossibility and, at the same time, necessary to circumvent /any/ asynchronous impossibility. In this context, I will consider the /geometrical/ approach, based on modeling a system state of as a high-dimensional geometrical object, and a distributed computation as an evolution of this object in space. This approach has been shown instrumental in characterizing the class of tasks solvable in /asynchronous/ systems. I will argue that applying these ideas to /partially synchronous/ systems may lead to automatic derivations of the weakest failure detectors for various distributed computing problems, and, eventually, to establishing a theory of distributed computational complexity.

The large and constantly growing Internet routing table size is a longstanding problem that leads to increased convergence time, increased boot time, and costly equipment upgrades. The problem exists for both VPN and global routing tables, and there is concern that IPv4 address space exhaustion over the next few years may lead to an increasingly fragmented address space, poor aggregation, and therefore a increase in the rate of routing table size. To address these issues, the IETF is working hard on new protocols that will shrink routing tables. In this talk, we present a way to shrink routing tables, easily by an order of magnitude or more, without any new protocols. The idea behind our approach, called Virtual Aggregation, is to partition the address space into large Virtual Prefixes, each of which is delegated to a tunneled virtual network composed of a fraction of ISP routers. Virtual Aggregation can be used independently by a single ISP, or cooperatively among a group of ISPs. This talk describes how Virtual Aggregation can be configured and deployed, and gives performance results based on measurements made at a Tier-I ISP.