John Fiskio-Lasseter: Research Overview

Papers (Peer-Reviewed)

Technical Reports and Unpublished Manuscripts

Other Useful Things

Details

Xiaofang Zhang, Michal Young, and John H. E. F. Lasseter. Refining code-design mapping with flow analysis. Foundations of Software Engineering, 2004 ACM Symposium (SIGSOFT '04), pages 231-240. ACM PR., 2004.

Abstract We address the problem of refining and completing a partially specified high-level design model and a partially-defined mapping from source code to design model. This is related but not identical to tasks that have been automated with a variety of reverse engineering tools to support software modification tasks. We posited that set-based flow analysis algorithms would provide a convenient and powerful basis for refining an initial rough model and partial mapping, and in particular that the ability to compute fixed points of set equations would be useful in propagating constraints on the relations among the model, the mapping, and facts extracted from the implementation. Here we report our experience applying this approach to a modest but realistic example problem. We were successful in expressing a variety of useful transformations very succinctly as flow equations, and the propagation of recursively-defined constraints was indeed useful in refining the mapping from implementation to model. On the other hand, our experience highlights remaining challenges to make this an attractive approach for general use. Special measures are required to identify and remove inconsistent constraints before they propagate through a system. Also, while the required flow equations are succinct, they are also rather opaque; it is not obvious how their expressive power might be preserved in a more accessible notation.

John H. E. F. Lasseter. Toolkits for the Automatic Construction of Data Flow Analyzers. Technical Report CIS-TR-04-03, University of Oregon, 2003.

Abstract

This position paper surveys the developments in the state of the art of data flow analysis construction tools, from those designed for integration with production compilers to those designed as pure research systems. Although this work is not primarily an account of data flow analysis itself, nor of data flow frameworks, the structure of every existing flow analysis toolkit is based on one data flow framework or another. Specifically, the design and implementation of a DFA construction tool involves consideration of three crucial problems: the underlying data flow framework, the modeling of program execution via a flow graph, and the specification of a generic solution algorithm for the supported class of data flow problems. We opt here for a conceptual rather than historical presentation; the discussion is structured according to the kinds of problems that face the designers of generation tools, with the features of existing systems serving as illustrations.

Xiaofang Zhang, John Fiskio-Lasseter, and Michal Young. Flow analyses for abstraction of architectural structure and behavior. Technical Report CIS-TR-03-01, University of Oregon, 2003.

Abstract Architectural analysis for style checking and transformations can include analysis of gross structure (topology) together with analysis of behavior. In this paper, we investigate such integrated analyses in the context of C2-style architectures. We apply flow analysis in a novel way to the structure and behavior of C2-style message bus architectures to discover groups of components that can be condensed into a single ``virtual component.'' The combined analysis can be expressed in the form of flow equations interpreted by a generic flow analysis toolkit which treats all relations - those that describe the structure of the system and those that describe its behavior - uniformly.

John Fiskio-Lasseter and Michal Young. Flow equations as a generic programming tool for manipulation of attributed graphs. ACM SIGPLAN-SIGSOFT Workshop on Program Analysis for Software Tools and Engineering (PASTE'02), pages 69-76. ACM Pr., 2002.

Abstract The past three decades have seen the creation of several tools that extract, visualize, and manipulate graph-structured representations of program information. To facilitate interconnection and exchange of information between these tools, and to support the prototyping and development of new tools, it is desirable to have some generic support for the specification of graph transformations and exchanges between them.

GenSet is a generic programmable tool for transformation of graph-structured data. The implementation of theGenSet system and the programming paradigm of its language are both based on the view of a directed graph as a binary relation. Rather than use traditional relational algebra to specify transformations, however, we opt instead for the more expressive class of flow equations. Flow equations -- or, more generally, systems of simultaneous fixpoint equations -- have seen fruitful applications in several areas, including data and control flow analysis, formal verification, and logic programming. In GenSet, they provide the fundamental construct for the programmer to use in defining new transformations.

John Fiskio-Lasseter and Amr Sabry. Putting operational techniques to the test: a syntactic theory for behavioral Verilog. Third International Workshop on Higher Order Operational Techniques in Semantics, 1999, pages 32-49. ENTCS Vol. 26. Elsevier, 1999.

Abstract We present a syntactic theory for the behavioral subset of the Verilog Hardware Description Language. Due to the complexity of the language, the construction of this theory represents a serious test of the suitability of syntactic operational techniques for reasoning about industrial languages. Overall, we have found that these techniques are rather robust but with a few caveats. Our theory formalizes the simulation cycle explicitly, exposes a number of ambiguities and inconsistencies in the language reference manual (LRM), and is the most accurate known description of this subset of Verilog, with respect to the LRM. The syntactic theory has been used to automatically derive a simulator for Verilog.

John Fiskio-Lasseter. A Formal Description of Behavioral Verilog Based on Axiomatic Semantics. Tech. Rep. TR-98-04, University of Oregon, Computer and Information Science Department. 1998

Abstract Reasoning about hardware designs written in Verilog is problematic, in large part because of the lack of a formal semantics for the language. The behavioral aspects of many constructs within the language are unclear, even with the existence now of an official language standard. As a result, a program may contain many subtleties which can be overlooked without careful analysis, and which may not even appear, depending on the implementation of the simulator that is used. In this thesis, we present a formal description of a large subset of behavioral Verilog, based on axiomatic semantics. Our primary contribution is an explicit formalization of the Verilog simulation cycle. In addition, we discuss some of the constructs that pose particular challenges to formal description, and offer axiomatic descriptions of these constructs that appear to match the behavior of the leading simulation packages.

This paper is my MS Thesis, although I have improved its appearance from the less-than-attractive formatting that was a consequence of the graduate school's archival requirements.

In retrospect, my choice of notation was really terrible in this work. The HOOTS paper is much shorter and much more readable, although a lot of the details are omitted there.

johnfl@cs.uoregon.edu
Last modified: Mon Oct 14 12:24:55 PDT 2002