CSE Technical Reports Sorted by Technical Report Number
| TR Number |
Title |
Authors |
Date |
Pages |
| This report describes a strong connection between maximum satisfiability and minimally-unsatisfiable subformulas of any constraint system, as well as techniques for exploiting it. Focusing on CNF formulas, we explore this relationship and present novel algorithms for extracting minimally-unsatisfiable subformulas, including one that finds all such subformulas. We present experimental results showing how these can be used in counterexample-guided abstraction refinement for hardware verification, decreasing the number of iterations the process requires to verify a design. A large set of benchmarks is used to investigate the relationship between maximum satisfiability and minimally-unsatisfiable subformulas in a product configuration application. |
| In this paper, we propose Boost Logic, a logic family which relies on
voltage scaling, gate overdrive and energy recovery techniques to
achieve high energy efficiency at frequencies in the GHz range. The
key feature of our design is the use of an energy recovering ``boost'
stage to provide an efficient gate overdrive to a highly voltage
scaled logic at near threshold supply voltage. We have evaluated our
logic family using post-layout simulation of an 8-bit pipelined array
multiplier in a 0.13um CMOS process with Vth=340mV. At 1.6GHz
and a 1.3V supply voltage, the Boost multiplier dissipates 8.11pJ per
computation. Comparing results from post-layout simulations of boost
and voltage-scaled conventional multipliers, our proposed logic
achieves 68% energy savings with respect to static CMOS. Using low
Vth devices, Boost Logic has been verified to operate at
2GHz with a 1.25V voltage supply and 8.5pJ energy dissipation per
cycle. |
| The ongoing revolution in life sciences research is producing vast amounts of genetic and proteomic sequence data. Scientists want to pose increasingly complex queries on this data, but current methods for querying biological sequences are primitive and largely procedural. This limits the ease with which complex queries can be posed, and often results in very inefficient query plans. There is a growing and urgent need for declarative and efficient methods for querying biological sequence data. In this paper we introduce a system
called Periscope/SQ which addresses this need. Queries in our system are based on a well-defined extension of relational algebra. We introduce new physical operators and support for novel indexes in the database. As part of the optimization framework, we describe a new technique for selectivity estimation of string pattern matching predicates that is more accurate than previous
methods. We also describe a simple, yet highly effective algorithm to optimize sequence queries. Using a real-world application in eye genetics, we show how Periscope/SQ can be used to achieve a speedup of two orders of magnitude over existing procedural methods! |
| In this paper, we introduce WebBee, a client-proxy architecture that combines a web scraping proxy with a Java client to make a platform-independent gateway between small mobile devices, such as
mobile phones, and the vast information available on the World Wide
Web. The key technology behind WebBee is a web scraping engine that
executes "scraping scripts," a domain-specific scripting language we
designed for the purpose of fetching web pages and selectively
extracting information from them. By transmitting to and displaying
only this extracted information on the client device, WebBee gives
mobile devices with small displays and low network bandwidth clean and
quick access to web content customarily designed for desktop browsers.
With WebBee, providers do not need to tailor their contents specifically
for mobile devices. Furthermore, the use of a Java client ensures that
WebBee is a portable solution among modern mobile devices.
|
| We present an effective method for automatically selecting the
appropriate scale of shape features that are depicted when
rendering a 3D mesh in the style of a line drawing. The method
exhibits good temporal coherence when introducing and removing
lines as needed under changing viewing conditions, and it is
fast because the calculations are carried out entirely on the
graphics card. The strategy is to pre-compute a sequence of
filtered versions of the mesh that eliminate (via a signal
processing technique) shape features at progressively larger
scales. Each mesh in the sequence retains the original number
of vertices and connectivity, providing a direct correspondence
between meshes. The mesh sequence is loaded onto the graphics
card, and at run-time a vertex program interpolates positions
and curvature values between two of the meshes, depending on
distance to the camera. A pixel program then renders
silhouettes and suggestive contours to produce the line
drawing. In this way, fine shape features are depicted over
nearby surfaces, while appropriately coarse-scaled features are
depicted over more distant regions. |
| Performance accuracy is a critical but often neglected aspect of architectural performance simulators. One approach to evaluating performance accuracy is to attempt to reproduce observed performance results from a real machine. In this paper, we attempt to model the performance of a Compaq Alpha XP1000 workstation using the M5 full-system simulator. There are two novel aspects to this work. First, we simulate complex TCP/IP networking workloads and use network bandwidth as our primary performance
metric. Unlike conventional CPU-intensive applications, these workloads spend most of their
time in the operating system kernel and include significant interactions with platform hardware such as the interrupt controller and network interface device. Second, we attempt to achieve performance accuracy without extremely precise modeling of the reference hardware. Instead, we use simple generic component models and tune them to achieve appropriate bandwidths and latencies.
Overall, we were able to achieve reasonable accuracy even with our relatively imprecise model, matching the bandwidth of the real system within 15% in most cases. We also used profiling to break CPU time down into categories, and found that the simulation results correlated well with the real machine.
|
| Protecting sensitive files from a compromised system helps
administrator to thwart many attacks, discover intrusion trails,
and fast restore the system to a safe state. However, most
existing file protection mechanisms can be turned off after an
attacker manages to exploit a vulnerability to gain privileged
access. In this paper we propose SVFS, a Secure Virtual File
System that uses virtual machine technology to store sensitive
files in a virtual machine that is dedicated to providing secure
data storage, and run applications in one or more guest virtual
machines. Accesses to sensitive files must go through SVFS and are
subject to access control policies. Because the access control
policies are enforced independently in an isolated virtual
machine, intruders cannot bypass file protection by compromising a
guest VM. In addition, SVFS introduces a Virtual Remote Procedure
Call mechanism as a substitute of standard RPC to deliver better
performance in data exchanging across virtual machine boundaries.
We implemented SVFS and tested it against attacks on a guest
operating system using several available rootkits. SVFS was able
to prevent most of the rootkits from being installed, and prevent
all of them from persisting past reboot. We also compared the
performance of SVFS to the native Ext3 file system and found that
performance cost was reasonable considering the security benefits
of SVFS. Our experimental results also show VRPC does improve the
filesystem performance.
|
| In this report, we present an efficient approach to resonant system design. Our approach involves the use of resonant clocks to drive level sensitive latches in pipelined datapaths. Through judicious design of these timing elements, the energy efficiency of resonant clocking
can be obtained without performance penalties, while maintaining robust, race-free operation.
Since our approach involves driving only the timing elements with resonant clocks and places no restrictions on the type of computational logic, the method can be used with existing static CMOS
design flows. We describe our technique for two, three and four phase clock systems and present clock generation mechanisms. We also introduce the level-sensitive timing elements to be used with
these clocks and discuss how they are introduced into a datapath.
|
Technical Reports Page
|
|
