CSE Technical Reports Sorted by Technical Report Number
| TR Number | Title | Authors | Date | Pages |
| CSE-TR-506-05 | From Max-SAT to Min-UNSAT: Insights and Applications | Liffiton, Andraus and Sakallah | February, 2005 | 7 |
| 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. |
| CSE-TR-507-05 | Boost Logic: A High Speed Energy Recovery Circuit Family | Sathe, Ziesler and Papaefthymiou | February, 2005 | 15 |
| 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. |
| CSE-TR-508-05 | Towards Declarative Querying for Biological Sequences | Tata, Patel, Friedman and Swaroop | March, 2005 | 15 |
| 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! |
| CSE-TR-509-05 | On the Design and Implementation of a Proxy-Based Architecture for Web Access on Mobile Devices | Upatkoon, Wang and Jamin | April, 2005 | 10 |
| 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. |
| CSE-TR-510-05 | Multi-scale Line Drawings from 3D Meshes | Alex Ni, Kyuman Jeong, Seungyong Lee, and Lee Markosian | July, 2005 | 6 |
| 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. |
| CSE-TR-511-05 | Performance Validation of Network-Intensive Workloads on a Full-System Simulator | Ali G. Saidi, Nathan L. Binkert, Lisa R. Hsu, and Steven K. Reinhardt | July, 2005 | 10 |
| 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. |
| CSE-TR-512-05 | Towards Protecting Sensitive Files in a Compromised System | Xin Zhao, Kevin Borders, and Atul Prakash | September, 2005 | 18 |
| 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. |
| CSE-TR-513-05 | Resonant System Design with Coarse Grained Pipelines | Visvesh S. Sathe and Marios C. Papaefthymiou | September, 2005 | 7 |
| 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