Salt & Alef: Unlocking the Power of Boolean Satisfiability

Publication Source: The 10th Annual High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, 2006

Solvers for the Boolean satisfiability problem (SAT) are an enabling technology for a diverse set of applications relevant to the HPEC community. These applications include formal verification, analysis of numerical precision for embedded pipelines, and cognitive reasoning. However, solver performance, measured in terms of speed and maximum problem size, is a limiting factor to the application of SAT to real-world problems. We are developing a constraint language, translation tool, and parallel SAT solver to significantly mitigate the impact of these limitations.
Google Scholar    Article

Alef Verification and Planning System

Publication Source: The 48th Annual Cray User Group (CUG) Technical Conference, Lugano, Switzerland, 2006

Recently, solvers for the Satisfiability problem (SAT) have become an enabling technology for diverse areas of military and commercial interest. However, solver performance, in terms of speed, maximum problem size, and efficiency, is a limiting factor to the more extensive application of this technology. This paper discusses Reservoir's SAT-based planning and verification system, Alef, which includes a compiler, intermediate language, and parallel solver for HPC hardware. 
Google Scholar    Article

SAT Solvers for Investigation of Architectures for Cognitive Information Processing

Publication Source: The High Performance Embedded Computing Workshop (HPEC), Lexington, MA, USA, September, 2006

Sponsored by DARPA in the ACIP Program, this presentation covers demand for cognitive processing, historical architectures for AI / cognitive processing, SAT solvers as a cognitive application, application specific hardware, parallelizing SAT, current performance, and architectural implications.

R-Stream 3.0: Technologies for High Level Embedded Application Mapping

Publication Source: The 8th Annual High Performance Embedded Computing (HPEC) Workshops, Lexington, MA, USA, 2004

R-Stream is a High Level Compiler being developed as part of the DARPA IPTO Polymorphous Computer Architecture Program. The compiler is targeted at the problem of mapping high performance embedded signal/knowledge processing applications. Our 2.0 version, presented as a poster at HPEC last year, will be performing application mapping via the Streaming Virtual Machine interface to low level compilers (LLC). This presentation will focus on the implementation and architecture of the high level compiler (HLC). In particular, we will present the performance results and insights from our 2.0 version of our Integrated Radar Tracker (IRT) running simulated on the reference Polymorphous Computer Architecture (PCA). The performance results will be accompanied by details of the application transformations that 2.0 will be performing, including granularity selection, high level streaming transformations, and the manner in which we integrate the data parallel front end of IRT with the more task/thread parallel back end. Furthermore, we expect to be able to provide insight into the benefits and limitations of some aspects of the morphware software architecture, in particular the phased HLC/LLC compilation structure, the SVM interface, and the abstraction of architectures into the Streaming Machine Model (SMM) and Hierarchical Machine Model (HMM). We may further be able to accompany this with some performance results for the application mapped to commercial architectures that are emerging with similarities to the PCA architecture class.
Google Scholar    Article

Dynamic Optimization in the Mainframe World

Publication Source: The 4th Workshop on Feedback-Directed and Dynamic Optimization (FDDO-4), Austin, TX, USA

The OOCT system implements dynamic optimization within a software emulation of Fujitsu's K series mainframe architecture. OOCT compiles the instructions of the traditional K series operating system called ASP. The combined requirements of running below the OS and operating in a mainframe product restrict the features of OOCT on the one hand while providing opportunities for unusual optimizations and implementation techniques on the other. We describe the system structure to show where tradeoffs were made, providing details on some of the unusual features. We highlight the adaptive features of OOCT for balancing and delaying CPU load. Finally, we describe a set of lessons taken away from our experience with mainframe emulation.
Google Scholar    Article

1 22 23 24