Fall 2000 Abstracts

Sponsored by Salomon Smith Barney

 

Friday October 27, 2000
Speaker: Micha Sharir, Tel Aviv University
Title: Combinatorics of Arrangements - Recent Progress
Abstract: Arrangements of curves and surfaces have been a major topic of study in computational and combinatorial geometry for more than 15 years. The field has progressed from analysis of two-dimensional arrangements in the 80's and early 90's to analysis of arrangements in three and higher dimensions. The progress included sharp bounds on the complexity of lower envelopes, single cells, zones, vertical decompositions, as well as finding many applications of these bounds to diverse areas, such as motion planning and geometric optimization.

In the past couple of years more progress has been made on various major problems in the combinatorics of arrangements, and the purpose of this talk is to survey some of this progress. The main topics that I will survey are:

  • The k-set problem: A lot of new results have been obtained, starting with Dey's improved bound for k-sets in the plane, and including an improved bound in 3 dimensions, an improved lower bound in the plane, connection between k-sets and deep results in the theory of polytopes, and improved bounds on levels in arrangements of curves.
  • Incidences between points and curves: I will survey recent progress on this problem, including improved bounds for incidences between points and circles and several related problems. I will also mention new results concerning bounds on the number of k-simplices spanned by a point set in d dimensions that are congruent to a fixed simplex.
  • Union of geometric objects: Several new results have been obtained recently, including near-quadratic bounds on the complexity of the union of cylinders in 3-space, union of equal cubes in 3-space, union of fat convex bodies in the plane, and more.
Friday November 10, 2000
Speaker: Alan Fekete, University of Sydney
Title: Making Snapshot Isolation Serializable
Abstract: Snapshot Isolation (SI) is a multi-version concurrency control algorithm. SI is attractive because it never delays read operations, not even when concurrent writes are occurring. SI has been implemented by Microsoft Exchange and Oracle (with certain variations), and it provides an isolation level that avoids many of the common concurrency anomalies. SI does not guarantee serializability, however. Like most protocols that fail to guarantee serializabiliy, SI can lead to arbitrarily serious violations of integrity constraints. Fortunately there are applications where the program logic guarantees that only serializable executions can take place, one example being the TPC-C benchmark.

We present a new theory with which the DBA can examine the program logic of the application to achieve one of the following two goals:

  1. To verify that only serializable executions will occur when running on a DBMS which has SI as its concurrency control algorithm.
  2. If 1 fails, to modify the application programs so that such serializability will be guaranteed.

Our goal is to bring concurrency safety to the many applications running on systems with SI as the concurrency control mechanism.

Friday November 17, 2000
Speaker: Demetri Terzopoulos, University of Toronto
Title: Artificial Animals (and Humans): From Physics to Intelligence
Abstract: I will present research spanning the fields of computer graphics, computer vision, and artificial life, an emerging discipline that bridges computational science and biological science. We have created physics-based virtual worlds inhabited by realistic "artificial animals". Our synthetic fauna possess muscle-actuated bodies, sensors, and brains with motor, perception, and behavior centers. Artificial animals - including, of course, artificial humans - are of interest in computer graphics because they are self-animating characters that dramatically advance the state of the art of production animation and interactive games. As biomimetic autonomous agents situated in realistic virtual worlds, artificial animals also foster a deeper, computationally oriented understanding of biological information processing. For example, they enable a new paradigm for computer vision research which exploits virtual reality. I will demonstrate virtual animals and humans perceptually navigating their dynamic 3D worlds, their foveated eyes controlled by active vision algorithms that analyze afferent retinal image streams. Artificial animals are furthermore valuable to the study of learning and cognition in living systems. I will show how they can master muscle-actuated locomotion and learn advanced motor skills guided by sensory perception. Finally, knowledge representation and reasoning formalisms from artificial intelligence support the cognitive mind of "Homo sapiens syntheticus". A multimedia presentation will render this talk accessible to all.
Friday December 1, 2000
Speaker: George Necula, U. C. Berkeley
Title: Oracle-Based Checking of Untrusted Software
Abstract: Proof-carrying code (PCC) has been proposed as a general mechanism that allows the receiver of an untrusted program to check the program's compliance with certain key safety policies, such as type safety or disciplined resource management. To make this possible the program comes accompanied by an easy-to-check proof of compliance; this leaves to the receiver the easy task of proof checking. One of the major applications of PCC to date has been to instrument a Java compiler to produce proofs of type safety along with the optimized machine code. This enables a Java client to combine the speed of compiled code with the safety checking of bytecode, all in a slim package consisting mostly of a machine code parser and a proof checker.

In this talk we review the basic motivation and design of a PCC infrastructure for Java and then we focus on novel aspects of the design that enabled us to scale to Java programs up to 100,000 lines. First, we observed that actual proofs of Java type safety can be very large even though they are quite shallow in mathematical content. This motivated us to develop a variant of PCC in which the proof checker is replaced by a non-deterministic theorem prover, which is simple yet quite powerful. The proof is then replaced by a sequence of bits acting as an oracle that the prover uses to resolve its non-deterministic choices. If the oracle guides the prover to success then the code is accepted.

There are many advantages to this oracle-based design of PCC, most notable of which being that the size of oracles adapts naturally to the complexity of the property being checked. In the particular case of proofs of type safety for assembly language programs obtained from Java source programs, the oracles are only 15% of the size of machine code, which is more than an order of magnitude smaller than the corresponding proofs. We will conclude the presentation with a discussion of a number of other design and engineering choices that were necessary to achieve scalability.
Friday February 2, 2001
Speaker: Jon Bentley, Bell Laboratories
Title: Cache-Conscious Algorithms and Data Structures
Abstract: Computer architects are magicians: they make us believe the ludicrous proposition that 50-nanosecond RAM can keep up with 1-nanosecond processors. Most of the time, we fall for their cruel hoax because of the wonder of caches: small, fast memories that apparently give us huge volume at low cost and fast speed. Most programmers receive the benefits of caches without worrying about the mechanism. Cache-conscious software design takes caching into account, and thereby speeds up some programs. This talk shows how cache-conscious algorithms and data structures can achieve speedups of up to an order of magnitude across a wide variety of machines.
Friday February 9, 2001
Speaker: Fred B. Schneider, Cornell University
Title: The Design and Deployment of COCA
Abstract: COCA is a fault-tolerant and secure on-line certification authority that has been built and deployed both in a local area network and in the Internet. Replication is used to achieve availability; proactive recovery with threshold cryptography is used for digitally signing certificates in a way that defends against mobile adversaries which attack, compromise, and control one replica for a limited period of time before moving on to another. Relatively weak assumptions characterize environments in which COCA's protocols will execute correctly. No assumption is made about execution speed and message delivery delays; channels are expected to exhibit only intemittent reliability; and up to 1/3 of COCA's servers may be faulty or compromised. The result is a system with inherent defenses to denial of service attacks because, by their very nature, weak assumptions are difficult for attackers to invalidate. Moreover, COCA also introduces a novel form of caching (for results of expensive cryptographic operations) that blunts replay attacks.

 

Distinguished Lecture Series


Campus Events