Este trabalho apresenta um conjunto de contribuiçõoes teóricas e metodológicas para o projeto e a implementação de linguagens de programação, utilizando o autômato adaptativo como dispositivo formal para sua definição. A especificação completa de uma linguagem de programação envolve desde a compreensão adequada de princípios e fundamentos comuns entre todas as linguagens de programação, transparentes ao programador, até as suas formas e características externas. Embora muitos modelos e notações possam ser utilizados na formalização de diferentes aspectos envolvidos no projeto e na implementação das linguagens de programação, o autômato adaptativo demonstra alta aplicabilidade e adequação para uma definição completa da linguagem, sem a necessidade do uso de diferentes notações. Demonstra-se como os autômatos adaptativos podem ser utilizados como uma metalinguagem unificada para especificar todas as componentes relevantes da definição formal da linguagem de programação, tais como: análise léxica, reconhecimento da sintaxe livre de contexto e manipulação de alguns aspectos dependentes de contexto da linguagem - declaração e uso de nomes simb´olicos, semântica estática, declaração e expansão de macros, entre outros. São apresentados os conceitos relacionados, e descrito os aspectos mais importantes da formalização proposta. Para isso, utiliza-se uma linguagem imperativa simplificada, sobre a qual é acoplado um mecanismo de extensão para torná-la extensÍvel. / This work presents a set of theoretical and methodological contributions to the design and implementation of programming languages, using the adaptive automaton as device for its formal definition. The complete specification of a programming language involves proper understanding of principles and common ground between all the programming languages, transparent to the programmer, and forms and external characteristics. Although many models and notations can be used to formalize different aspects involved in the design and implementation of programming languages, the adaptive automaton shows high applicability and suitability to full definition of the language, without the need to use distincts notations. It is shown how the adaptive automata can be used as a unified metalanguage to specify all the relevant components of the formal definition of programming language, such as lexical analysis, sintax contextfree recognition and handling of context-dependent aspects of language - declaration and use of symbolic names, static semantics, definition and expansion of macros, and others. Concepts are shown and the most important aspects are described of the this formal proposal. A simple imperative language is used, on which is attached an extension mechanism to make it extensible.

Thesis. 1976. Ph.D.--Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. / Microfiche copy available in Archives and Engineering. / Vita. / Bibliography: leaves 188-193. / Ph.D.

Thesis. 1975. Ph.D.--Massachusetts Institute of Technology. Dept. of Electrical Engineering and Computer Science. / Bibliography: leaves 187-189. / Ph.D.

This thesis describes the Drag language. Drag is a general purpose, gradually typed, lexically scoped, and multi-paradigm pro- gramming language. The essence of Drag is to build the abstract syntax trees of the programs directly and interactively. Our work includes the language specification and a prototype program. The language specification focuses on the syntax, the semantic model, and the type system. The prototype consists of an interactive editor and a compiler that targets several plat- forms, among which we focus on the LLVM platform in this thesis.

LARs (Line Associative Registers) are very wide tagged registers, used for both register-wide SWAR (SIMD Within a Register )operations and scalar operations on arbitrary fields. LARs include a large data field, type tags, source addresses, and a dirty bit, which allow them to not only replace both caches and registers in the conventional memory hierarchy, but improve on both their functions. This thesis details a LAR-based architecture, and describes the design of a compiler which can generate code for a LAR-based design. In particular, type conversion, alignment, and register allocation are discussed in detail.

The Planguages project is the birthplace of the Planguage programmingapproach, which is designed to alleviate the task of writing parallelprograms and harness massively parallel computers and networks of workstations. Planguage has two existing translators, Parallel C (PC) and Pfortran,which is used for their base languages, C and Fortran77. The translatorswork with MPI (Message Passing Interface) for communications. SOS(ipStreams, Overlapping and Shortcutting), a function library that supportsthe three named functionalities, can be used to further optimize parallel algorithms. This project is the next step in the continuing project of updatingthe PC Compiler. The goal is to test the viability of using “shortcutting”functions. Parallel programs with the ability to shortcut can be generatedby the updated version of the PC Compiler. In addition, this project introducesthe ability of the PC Compiler to translate a race condition intoa non-deterministic solution. This document explores different phases of the project in detail. Thefollowing phases are included: software design, algorithm design, analysis,and results. The deliverables, source code, and diagrams are included asAppendices.

Behavioral synthesis is the process of compiling an Electronic System Level (ESL) design to a register-transfer level (RTL) implementation. ESL specifications define the design functionality at a high level of abstraction (e.g., with C/C++ or SystemC), and thus provide a promising approach to address the exacting demands to develop feature-rich, optimized, and complex hardware systems within aggressive time-to-market schedules. Behavioral synthesis entails application of complex and error-prone transformations during the compilation process. Therefore, the adoption of behavioral synthesis highly depends on our ability to ensure that the synthesized RTL conforms to the ESL description. This dissertation provides an end-to-end scalable equivalence checking support for behavioral synthesis. The major challenge of this research is to bridge the huge semantic gap between the ESL and RTL descriptions, which makes the direct comparison of designs in ESL and RTL difficult. Moreover, a large number and a wide variety of aggressive transformations from front-end to back-end require an end-to-end scalable checking framework. This dissertation provides an end-to-end scalable equivalence checking support for behavioral synthesis. The major challenge of this research is to bridge the huge semantic gap between the ESL and RTL descriptions, which makes the direct comparison of designs in ESL and RTL difficult. Moreover, a large number and a wide variety of aggressive transformations from front-end to back-end require an end-to-end scalable checking framework. A behavioral synthesis flow can be divided into three major phases, including 1) front-end : compiler transformations, 2) scheduling: assigning each operation a clock cycle and satisfying the user-specified constraints, and 3) back-end : local optimizations and RTL generation. In our end-to-end and incremental equivalence checking framework, we check each of the three phases one by one. Firstly, we check the front-end that consists of a sequence of compiler transformations by decomposing it into a series of checks, one for each transformation applied. We symbolically explore paths in the input and output programs of each transformation, and check whether the input and output programs have the same observable behavior under the same path condition. Secondly, we validate the scheduling transformation by checking the preservation of control and data dependencies, and the preservation of I/O timing in the user-specified scheduling mode. Thirdly, we symbolically simulate the scheduled design and the generated RTL cycle by cycle, and check the equivalence of each mapped variables. We also develop several key optimizations to make our back-end checker scale to real industrial-strength designs. In addition to the equivalence checking framework, we also present an approach to detecting deadlocks introduced by parallelization of RTL blocks that are connected by synthesized interfaces with handshaking protocols. To demonstrate the efficiency and scalability of our framework, we evaluated it on transformations applied by a behavioral synthesis tool to designs from the C-based CHStone and SystemC-based S2CBench benchmarks. Based on the evaluation results, our front-end checker can efficiently validate more than 75 percent of the total of 1008 compiler transformations applied to designs from the CHStone benchmark, taking an average time of 1.5 seconds per transformation. Our scheduling checker can validate control-data dependencies and I/O timing of all designs from S2CBench benchmark. Our back-end checker can handle designs with more than 32K lines of synthesized RTL from the CHStone benchmark, which demonstrates the scalability of the checker. Furthermore, our checker found several bugs in a commercial tool, underlining both the importance of formal equivalence checking and the effectiveness of our approach.

This thesis describes TeaBag, which is a debugger for functional logic computations. TeaBag is an accessory of a virtual machine currently under development. A distinctive feature of this machine is its operational completeness of computations, which places novel demands on a debugger. This thesis describes the features of TeaBag, in particular the handling of non-determinism, the ability to control nondeterministic steps, to remove context information, to toggle eager evaluation, and to set breakpoints on both functions and terms. This thesis also describes TeaBag's architecture and its interaction with the associated virtual machine. Finally, some debugging sessions of defective programs are presented to demonstrate TeaBag's ability to locate bugs. A distinctive feature of TeaBag is how it presents non-deterministic trace steps of an expression evaluation trace to the user. In the past expression evaluation traces were linearized via backtracking. However, the presence of backtracking makes linear traces difficult to follow. TeaBag does not present backtracking to the user. Rather TeaBag presents the trace in two parts. One part is the search space which has a tree structure and the other part is a linear sequence of steps for one path through the search space.

Abstract not available

The object-oriented community is paying increasing attention to techniques for object instance encapsulation and alias protection. Formal techniques for modular verification of programs at the level of objects are being developed hand in hand with type systems and static analysis techniques for restricting the structure of runtime object graphs. Ownership type systems have provided a sound basis for such structural restrictions by being able to statically represent an extensible object ownership hierarchy. However, such structural restrictions may potentially have limitations on cases when more flexible reference structures are desired. In this thesis, we present a different encapsulation technique, called Effect Encapsulation, which confines side effects rather than object references. With relaxed restriction on reference structure, it is able to express certain common object-oriented patterns which cannot be expressed in Ownership Types. From this basis, we also describe a model of Object Validity --- a framework for reasoning about object invariants. Such a framework can track the effect and dependency of method calls on object invariants within an ownership-based type system, even in the presence of re-entrant calls. Moreover, we present an access control technique for protecting object instances. Combined with context variance, the resulting type system allows for a more flexible and useful access control policy, hence is capable of expressing more object-oriented patterns.