An operational approach to computer system specification using applicative high-order logic.
Item
-
Title
-
An operational approach to computer system specification using applicative high-order logic.
-
Identifier
-
AAI9304677
-
identifier
-
9304677
-
Creator
-
Jin, Ti.
-
Contributor
-
Adviser: Stanley Habib
-
Date
-
1992
-
Language
-
English
-
Publisher
-
City University of New York.
-
Subject
-
Computer Science
-
Abstract
-
The objective of this thesis is to present and demonstrate the concept of applying an applicative high order logic to a fully-operational specification for complex computer system design and early implement-free simulation. Two realms are literally involved in this research. First, a Process-oriented, Applicative, Interpretable Specification Language, short for "PAISLey," is proposed. An applicative specification serves as an operating paradigm to embody an automatic test and check of design correctness, system consistency, to carry out faithfully an instance-free design simulation, gather significant performance measurements, and so forth. A variety of examples spanning many abstract levels of computer architecture have been exhibited to illuminate how well these subjects can be undertaken.;Secondly, we introduce a newly developed hierarchical cache organization for a tightly-coupled multi-processor system using a single shared memory. A small and fast set-associative memory, which functions as a write multi-buffer, is placed between the main memory and the private caches of local processors in order to resolve the cache coherence, shorten the write through latency, and then reduce memory bus traffic. We name it a Write Look-Ahead Buffer, or a WLAB. Two generic configurations of this Write Look-Ahead Buffer regarding local caches are discussed. The structure and size of the Write Look-Ahead Buffer will significantly affect the system performance. Several possible cache coherence protocols based on the WLAB organization are also addressed because the selection of the coherence strategy exerts instant effects on its performance.;A considerably large portion of this dissertation is devoted to producing the PAISLey specification for the WLAB cache system. Trace simulation of the WLAB cache system using the PAISLey specification is carried over on SUN SPARC II workstations. A large volume of analytic data is collected directly from running the WLAB specification. Through this exploration of PAISLey to the WLAB cache system, we manifest and verify our original concept of consigning applicative high order logic specifications to the operational computer system description and instance-free simulation.
-
Type
-
dissertation
-
Source
-
PQT Legacy CUNY.xlsx
-
degree
-
Ph.D.
