 
|
 |
2004
. 2003
. 2002 . 2001
. 2000
. 1999
. 1998
. 1997
. 1996
. 1995
. 1994
. 1993
. 1992
. 1991
. 1990
MS-CIS-04-01
Stephen Tse and Steve Zdancewic
MS-CIS-04-02
An Efficient XPath Streaming Processor
Yi Chen, Susan B. Davidson and Yifeng
Zheng
MS-CIS-04-03
The Design of Synchronization Mechanisms
for Peer-to-Peer Massively Multiplayer Games
Honghui Lu,Björn Knutsson, Margaret Delap,
John Fiore, Baohua Wu
MS-CIS-04-04
A Formal Analysis of Some Properties
of Kerberos 5 Using MSR
Frederick Butler(1), Iliano Cervesato(2),
Aaron D. Jaggard(3), and Andre Scedrov(4)
(1)Dept. of Mathematics, UPenn,(2)ITT Industries, Inc.,(3)Dept.
of Mathematics, Tulane, (4)Depts. of Mathematics and CIS, UPenn
MS-CIS-04-05
HSIF semantics
Oleg Sokolsky, Insup Lee, Rajeev Alur
We present semantics for HSIF, a language for exchanging hybrid
systems models between modeling and analysis tools. Unlike most
other interchange formats, HSIF is intended for the exchange of
formal objects. Therefore, the primary concern in developing HSIF
is to preserve behavior of the exchanged models and a precise semantic
definition is thus necessary. HSIF models are collections of hybrid
automata that communicate via shared variables. The concurrency
model is chosen to respect dependencies between variables.
MS-CIS-04-06
Low-Overhead Debugging with DISE
Marc L. Corliss, E Christopher Lewis, and Amir Roth
MS-CIS-04-07
Andrew I. Schein and Lyle H. Ungar
MS-CIS-04-08
Bayesian Example Selection using
BaBiES
Andrew I. Schein, S. Ted Sandler
and Lyle H. Ungar
Active learning is widely used to select which examples from
a pool
should be labeled to give best results
when learning predictivemodels. It is, however, sometimes
desirable to choose examples beforeany labeling or machine learning
has occurred. The optimal experimentaldesign literature
has many theoretically attractive optimality criteria for example
selection,but most are intractable when working with large numbers
of predictive features. We present the BaBiES criterion,an
approximation of Bayesian A-optimal design for linear regressionusing
binary predictors, which is both simple and extremely fast.
Empirical evaluations demonstrate that, in spite of selecting
all examples prior to learning, BaBiES is competitive with standard
active learningmethods for a variety of document classification
tasks.
MS-CIS-04-09
Amir Roth
A store queue (SQ) is a critical component of the load execution
machinery. High ILP processors require high load execution bandwidth,
but providing high bandwidth SQ access is difficult. Address
banking, which works well for caches, conflicts with age-ordering
which is required for
the SQ and multi-porting exacerbates the latency of the associative
searches that load execution requires.
In this paper, we present a new high-bandwidth load-store
unit design that exploits the predictability of forwarding behavior.
To start with, a simple predictor filters loads that are not
likely to require forwarding from accessing the SQ enabling
a reduction in the number of associative ports. A subset
of the loads that do not access the SQ are re-executed prior
to retirement to detect over-aggressive filtering and train
thepredictor. A novel adaptation of a Bloom filter keeps the
re-execution
subset minimal. Next, the same predictor filters stores that
don't forward values to nearby loads from the SQ enabling a
substantial capacity reduction. To enable this optimization
and maintain in-order store retirement, we add a second SQ that
contains all stores, but only to retirement and Bloom filter
management; this queue is large but isn't associatively searched.
Finally, to boost both load and store filtering and to handle
programs with heavy forwarding bandwidth requirements we add
a second, address-banked forwarding structure that handles "easy"
forwarding instances, leaving the globally-ordered SQ to handle
only "tricky" cases. Our design does not directly address load
queue scalability, but does dovetail with a recent proposal
that also uses re-execution to tackle this issue.
Performance simulations on SPEC2000 and MediaBench benchmarks
show that our design comes within 2% (7% in the worst case)
of the performance of an ideal multi-ported SQ, using only a
16-entry queue with a single associative lookup port.
MS-CIS-04-10
Ameesh Makadia and Kostas Daniilidis
Robotic navigation
algorithms increasingly make use of the panoramic field of view
provided by omnidirectional images toassist with localization
tasks. Since the images taken by a particular class of
omnidirectional sensors can be mapped to the sphere, the problem
of attitude estimation arising from 3D motions of the camera
can be treated as a problem of estimating the camera motion
between spherical images. This problem has traditionally been
solved by tracking points or features between images.
However, there are many natural scenes where the features cannot
be tracked with confidence. We present an algorithm that
uses image features to estimate ego-motion without explicitly
searching for correspondences. We formulate the problem
as a correlation of functions defined on the product of spheres
(S^2 x S^2) which are acted upon by elements of the direct product
group (SO(3) x SO(3)). We efficiently compute this correlation
and obtain our solution using the spectral information of functions
in (S^2 x S^2).
MS-CIS-04-11
A Design for Type-Directed Programming
in Java (Extended Version)
Stephanie Weirich
and Liang Huang
MS-CIS-04-12
Timothee Cour, Jianbo Shi
Image segmentation is often treated as an unsupervised task.
Segmentation by human, in contrast, relies heavily on memory
to produce an object-like clustering, through a mechanism of
controlled hallucination. This paper presents a learning algorithm
for memory-driven object segmentation and recognition. We propose
a general spectral graph learning algorithm based on gradient
descent in the space of graph weight matrix using derivatives
of eigenvectors. The gradients are efficiently computed using
the theory of implicit functions. This algorithm effectively
learns a graph network capable of memorizing and retrieving
multiple patterns given noisy inputs. We demonstrate the validity
of this approach on segmentation and recognition tasks, including
geometric shape extraction, and hand-written digit recognition.
MS-CIS-04-13
Calin Belta, Volkan Isler and George
J. Pappas
In this paper we present a theoretical and computational
framework for automatic generation of provably correct control
laws for planar robots in polygonal environments. Using triangulation
and
discrete abstractions, we map continuous
motion planning and control problems to computationally
inexpensive finite statetransition systems. In this framework,
powerful discrete and/or probabilistic planning algorithms
in topologically complicated environments can be seamlessly
linked to automatic generation of control laws for robots
with non-trivial kinematics or dynamics and control bounds.
While the algorithms that we developed are quite general,
we focus on fully-actuated kinematic robots with velocity
bounds, double integrators with velocity and acceleration
bounds, and (under-actuated) unicycles with forward and
turning speed bounds.
MS-CIS-04-14
Seeing Through Water
Alexei Efros, Volkan Isler, Jianbo
Shi and Mirko Visontai
We consider the problem of recovering an underwater image
distorted by surface waves. A large amount of video
data of the distorted image is acquired and the problem
is posed in terms of understanding the statistics
of local patches in the image
plane.This challenging reconstruction task can be formulated
as a manifold learning problem, such that the center of
the manifold is the image of the undistorted patch.
To compute the center, we present a new technique to estimate
global distances on the manifold.Our technique achieves
robustness through convex flow computations and solves
the ``leakage" problem inherent in recent manifold embedding
techniques.
MS-CIS-04-15
Combinators
for Bi-Directional Tree Transformations: A Linguistic
Approach to the View Update Problem
Nathan Foster,
Michael B. Greenwald, Jonathan T. Moore, Benjamin
C. Pierce, and Alan Schmitt
MS-CIS-04-16
Stephen Tse and Steve Zdancewic
This paper presents the design
of a programming language that supports information-flow
security policies and certificate-based declassification.
The language uses monadic information-flow annotations
in the style of Abadi et al.'s dependency core calculus,
and has an effects system and fixpoints. The type system
conflates security concepts such as labels, principals,
and privileges with abstract types, allowing a uniform
treatment of lattice structures throughout the language.
Myers' and Liskov's decentralized label model is encoded
using type constructors that describe confidentiality
and integrity policies, and label refinements and principal
groups follow naturally from intersection and union types.
Singleton types, combined with bounded universal and existential
quantifications connect the type system with public-key
infrastructures whose digital certificates provide authorization
for privileged operations such as declassification. These
features allow specification of security policies in term
of dynamic entities such as run-time user identities and
file access permissions.
Besides showing that the language is sound, we present
a security theorem that generalizes standard noninterference
to account for information flows introduced by declassification.
Although this result gives only a coarse approximation
to the information potentially leaked, it captures our
intuitions about certificate-based declassification.
MS-CIS-04-17
Stephen Tse
Programs written in a typed
language are guaranteed to satisfy the safety properties
of the type system without runtime checks. A type system
for an intermediate language allows static verification
of safety properties independent of source languages,
and opens up opportunities for advanced compiler optimizations.
This paper surveys three major intermediate languages:
Java bytecode, typed assembly language and proof-carrying
code. Java bytecode requires minimal type annotation but
sophisticated verification algorithms. Typed assembly
language permits low-level constructs such as registers
and instruction blocks, yet still enforces control-flow
safety and memory safety. Proof-carrying code provides
a general framework for any safety properties definable
in a
meta-logical framework.
We motivate the use of typed intermediate languages, illustrate
the type systems of the three languages mentioned above
with examples, and compare their tradeoffs of expressiveness
versus complexity. Additionally, we assess the impact
of the three languages and identify research directions
for future work.
MS-CIS-04-18
Discovering
Communities through Information Structure and Dynamics:
A Review of Recent Research
Nick Montfort
MS-CIS-04-19
Andrew McGregor
This report presents algorithms for finding large matchings
in the streaming model. In this model, applicable when dealing
with massive graphs, edges are streamed-in in some arbitrary order
rather than residing in randomly accessible memory. For epsilon>0,
we achieve a 1/(1+epsilon) approximation for maximum cardinality
matching and a 1/(2+epsilon) approximation to maximum weighted
matching. Both algorithms use a constant number of passes.
MS-CIS-04-20
Compositional Real-Time Scheduling
Framework
Insik Shin and Insup
Lee
MS-CIS-04-21
Hanna M. Wallach
MS-CIS-04-22
Marcelo Siqueira, Longin J. Latecki,
Jean Gallier
A 3D binary digital image is said to be well-composed
if and only if the set of points in the faces shared by the
voxels of foreground and background points of the image is a
surface in R3. Well-composed images enjoy important topological
and geometric properties; in particular, there is only one type
of connected component in any well-composed image, as 6-, 14-,
18-, and 26-connected components are equal. This implies that
several algorithms used in computer vision, computer graphics,
and image processing become simpler. For example, thinning algorithms
do not suffer from the irreducible thickness problem if the
image is well-composed. In this report, we introduce a new randomized
algorithm for making 3D binary digital images that are not well-composed
into well-composed ones, analyze its time complexity, and present
experimental evidence of its effectiveness when faced with practical
medical imaging data. We also introduce a new approach to extract
simplicial surfaces from 3D binary images, which is based on
our algorithm for making 3D binary digital images well-composed.
We show that the extraction of simplicial surfaces from well-composed
images using the Marching Cubes (MC) algorithm or some octree-based
algorithms can be simplified, as only six out of the fourteen
canonical configurations of cube-isosurface intersection can
occur. Moreover, the continuous analog of the digital boundary
of the input well-composed image and the MC surface are guaranteed
to be topologically equivalent.
MS-CIS-04-23
XTATIC is a lightweight extension of C# offering native support
for statically typed XML processing. XML trees are built-in
values in XTATIC, and static analysis of the trees created and
manipulated by programs is part of the ordinary job of the typechecker.
"Tree grep" pattern matching is used to investigate
and transform XML trees.
XTATIC's surface syntax and type system are tightly integrated
with those of C#. Beneath the hood, however, an implemention
of XTATIC must address a number of issues common to any language
supporting a declarative style of XML processing (e.g., XQUERY,
XSLT, XDUCE, CDUCE, XACT, XEN, etc.). In particular, it must
provide representations for XML tags, trees, and textual data
that use memory efficiently, support efficient pattern matching,
allow maximal sharing of common substructures, and permit seperate
compilation. We analyze these representation choices in detail
and describe the solutions used by the XTATIC complier.
MS-CIS-04-24
The Xtatic Experience
Vladimir Gapeyev, Michael Y. Levin, Benjamin C. Pierce, and
Alan Schmitt
XTATIC is a lightweight extension of C# with
native support for statically typed XML processing. It features
XML trees in built-in values, a refined type system based on
regular types in the style of XDUCE, and "tree
grep" - style regular patterns for traversing
and manipulating XML.
Previous papers on XTATIC have reported results on a number
of specific technical issues: basic theoretical properties of
an idealized core language, novel compilation algorithms for
regular pattern matching, and efficient runtime support for
XML procesing in the style encouraged by XTATIC. The aim of
the present paper is to discuss XTATIC - less formally and more
holistically - from the perspective of language design. We survey
the most significant issues we faced in the design process and
evaluate the choices we have made in addressing them.
MS-CIS-04-25
Paths into Patterns
Vladimir Gapeyev and Benjamin C. Pierce
The XML Path Language (XPATH) is an industry
standard notation for addressing parts of an XML document. It
is supported by many XML processing libraries and has been used
as the foundation for several dedicated XML processing languages.
Regular patterns, an alternative way of investigating and destructing
XML documents, were first proposed in the XDUCE language and
feature in a number of its descendants.
The processing styles offered by XPATH and by regular patterns
are each quite convenient for certain sorts of tasks, and the
designer of a future XML processing language might well like
to provide both. The designer might wonder, however, to what
extent these mechanisms can be based on a common foundation.
Can one be implemented by translating it into the other? Can
aspects of both be combined into a single notation?
As a first step toward addressing these questions, we show in
this paper that a language closely related to the "downward
axis" fragment of XPATH can be accurately translated into
ambiguous XDUCE-style regular patterns with a "collect
all matches" interpretation.
MS-CIS-04-26
MS-CIS-04-27
A Bisimulation for Type Abstraction and Recursion
Eijiro Sumii and Benjamin C. Pierce
MS-CIS-04-28
The effectiveness of static code optimizations--including
static optimizations performed "just-in-time"--is
limited by some basic constraints: (i) a limited number of logical
registers, (ii) a function-or region-bounded optimization scope,
and (iii) the requirement that transformations be valid along
all possible paths.
RENO is a modified MIPS-R10000 style register renaming mechanism
augmented with physical register reference counting that uses
map-table "short-circuiting" to implement dynamic
versions of several well-known static optimizations: move elimination,
common subexpression elimination, register allocation, and constant
folding. Because it implements these optimizations dynamically,
RENO can overcome some of the limitations faced by static compilers
and apply optimizations where static compilers cannot. RENO
has many more registers at its disposal--the entire physical
register file. Its optimizations naturally cross function or
any other compilation region boundary. And RENO performs optimizations
along the dynamic path without being impacted by other, non-taken
paths. If the dynamic path proves incorrect due to mispeculations,
RENO optimizations are naturally rolled back along with the
code they optimize.
MS-CIS-04-29
A high-bandwidth, low-latency load-store unit
is a critical component of a dynamically scheduled processor.
Unfortunately, it is also one of the most complex and non-scalable
components. Recently, several researchers have proposed techniques
that simplify the core load-store unit and improve its scalability
in exchange for the in-order pre-retirement re-execution of
some subset of the loads in the program..We call such techniques
load/store optimizations. One recent optimization attacks load
queue (LQ) scalability by replacing the expensive associative
search that is used to enforce intra- and inter- thread ordering
with load re-execution. A second attacks store queue (SQ) scalability
by speculatively filtering some load accesses and some store
entries from it. The speculatively accessed, speculatively populated
SQ can be made smaller and faster, but load re-execution is
required to verify the speculation. A third uses a hardware
table to identify redundant loads and skip their execution altogether.
Redundant load elimination is highly accurate but not 100%,
so re-execution is needed to flag false eliminations.
Unfortunately, the inherent benefits of load/store
optimizations are mitigated by re-execution itself. Re-execution
contends for cache bandwidths with store retirement, and serializes
load re-execution with subsequent store retirement. If a particular
technique requires a sufficient number of load re-executions,
the cost of these re-executions will outweigh the benefits of
the technique entirely and may even produce drastic slowdowns.
This is the case for the SQ technique.
Store Vulnerability Window (SVW) is a new mechanism
that reduces the re-execution requirements of a given load/store
optimization significantly, by an average of 85% across the
three load/store optimizations we study. This reduction relieves
cache port contention and removes many of the dynamic serialization
events that contribute the bulk of re-execution's cost, and
allows these techniques to perform up to their full potential.
For the scalable SQ optimization, this means the chnace to perform
at all. Without SVW, this technique posts significant slowdowns.
SVW is a simple scheme based on monotonic store sequence numbering
and a novel application of Bloom Filtering. The cost of an effective
SVW implementation is a 1KB buffer and an 2B field per LQ entry.
MS-CIS-04-30
Efficient Algorithms for k-best Deductive
Parsing
Liang Huang and David Chiang (Univ. of Maryland, College Park)
MS-CIS-04-31
Efficiently Storing and Extracting Phylogenetic
Trees for Simulation
Susan B. Davidson, Junhyong Kim and Yifeng Zheng
MS-CIS-04-32
Recent years have seen rapidly growing interest
in the development of networks of multiple unmanned aerial vehicles
(U.A.V.s), as aerial sensor networks for the purpose of coordinated
monitoring, surveillance, and rapid emergency response. This
has triggered a great deal of research in higher levels of planning
and control, including collaborative sensing and exploration,
synchronized motion planning, and formation or cooperative control.
In this paper, we describe our recently developed experimental
testbed at the University of Pennsylvania, which consists of
multiple, fixed-wing UAVs. We describe the system architecture,
software and hardware components, and overall system integration.
We then derive high-fidelity models that are validated with
hardware-in-the-loop simulations and actual experiments. Our
models are hybrid, capturing not only the physical dynamics
of the aircraft, but also the mode switching logic that supervises
lower level controllers. We conclude with a description of cooperative
control experiments involving two fixed-wing UAVs.
|
|
|