The study of programming languages is a rich field within computer science, incorporating both the abstract theoretical portions of computer science and the platform specific details. Topics studied in programming languages, chiefly compilers or interpreters, are permanent fixtures in programming that students will interact with throughout their career. These systems are, however, considerably complicated, as they must cover a wide range of functionality in order to enable languages to be created and run. The process of educating students thus requires that the demanding workload of creating one of the systems be balanced against the time and resources present in a university classroom setting. Systems building upon these fundamental systems can become out of reach when the number of preceding concepts and thus classes are taken into account. Among these is the study of just-in-time (JIT) compilers, which marry the processes of interpreters and compilers for the purposes of a flexible and fast runtime. The purpose of this thesis is to present JITed, a framework within which JIT compilers can be developed with a time commitment and workload befitting of a classroom setting, specifically one as short as ten weeks. A JIT compiler requires the development of both an interpreter and a compiler. This poses a problem, as classes teaching compilers and interpreters typically feature the construction of one of those systems as their term project. This makes the construction of both within the same time span as is usually allotted for a single system infeasible. To remedy this, JITed features a prebuilt interpreter, that provides the runtime environment necessary for the compiler portion of a JIT compiler to be built. JITed includes an interface for students to provide both their own compiler and the functionality to determine which portions of code should be compiled. The framework allows for important concepts of both compilers in general and JIT compilers to be taught in a reasonable timeframe.

One of the most difficult tasks a compiler writer faces is the construction of the instruction selector. The instruction selector is that part of the compiler that translates compiler intermediate representation (IR) into instructions for a target machine. Unfortunately, implementing an instruction selector “by hand” is a difficult, time consuming, and error prone task. The details of both the IR and target instruction set must be carefully considered in order to generate correct and efficient code. This, in turn, requires an expert in both the compiler internals as well as the target machine. Even an expert, however, can implement an instruction selector that is difficult to verify and debug. In this dissertation we describe the instruction selector problem, cover previous attempts at solving it, and identify what we believe to be the most prominent factor inhibiting their widespread adoption. This dissertation proposes a generalized approach toward generating instruction selectors automatically. In particular, we propose CISL, a common machine description language for specifying the semantics of compiler IR and target instructions, and GIST, a machine independent heuristic search procedure that can find equivalent instruction sequences between compiler IR and target instructions. CISL is an object-oriented-based language leveraging modern programming language constructs (e.g., classes, inheritance, mixins) and is capable of describing instructions for a variety of IR and target ISAs (Instruction Set Architecture). GIST leverages CISLs well-defined semantics and a canonicalization process to discover automatically instruction selector patterns: target instruction sequences that implement IR semantics. These instruction selector patterns are then generated in a compiler implementation independent format (XML). Small adapter programs use the generated instruction selector patterns to generate compiler specific implementation code. Our experiments show that instruction selector patterns can be discovered automatically and independent of a particular compiler framework or target machine. In addition, experience proved that adapter programs are easy to implement and instruction selector code is easy to generate from generated patterns. Furthermore, the generated instruction selectors are comparable in performance to the original compilers.

Due to the difficulty of obtaining formal proofs, there is increasing interest in partially or completely automating proof search in interactive theorem provers. Despite being a theorem prover with an active community and plentiful corpus of 170,000+ theorems, no deep learning system currently exists to help automate theorem proving in ACL2. We have developed a machine learning system that generates recommendations to automatically complete proofs. We show that our system benefits from the copy mechanism introduced in the context of program repair. We make our system directly accessible from within ACL2 and use this interface to evaluate our system in a realistic theorem proving environment.

No description available.

<p>The goal of this dissertation is to design a collection of techniques and tools that enable<br> the ease of programming under the traditional strong concurrency guarantees, without sacrificing the performance offered by modern distributed database systems. Our main thesis<br> is that language-centric reasoning can help developers efficiently identify and eliminate con-<br> currency anomalies in modern database programs, and we have demonstrated that it results<br> in faster and safer database programs</p>

The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library. / Thesis / Doctor of Philosophy (PhD) / The invention of Hardware Description Languages has given hardware designers access to powerful methods of abstraction and organization, previously only available to software developers. A high-powered means of examining properties such as reliability, correctness and safety is the creation of formal, mathematical proofs of correctness. One approach to this is the modelling of the artifact in the logic of some deductive system, such as the higher order logic of the Prototype Verification System (PVS). The ambition of this work is to demonstrate a mechanism by which a class of hardware descriptions may be used to generate such models automatically. We further demonstrate the utility of said models, using them to demonstrate non-trivial correctness properties. We also present a method of generating hardware descriptions, logical models, and proofs from a class of tabular specifications. The language on which this method operates is Bluespec SystemVerilog (BSV), a high-level hardware description language notable for its elegant semantics. The target platform of our translation is the Prototype Verification System (PVS), which features a highly automatic theorem-proving system. The translation algorithm is discussed at length, including the reconciliation of BSV's action-oriented semantic and the Kripke semantics employed by our chosen model in PVS. Five case studies demonstrate our methodology. In studies one and two, function blocks of the IEC 61131-3 Annex F library are verified against tabular specifications, or generated from the same. The remaining case studies are based on the Shakti RISC-V implementation of the RapidIO subsystem. Our final case study demonstrates progress towards the verification of highly abstract and complex properties over the entire translatable subset of the RapidIO library.

There is a great number of programming languages and they follow various paradigms such as imperative, functional, or logic programming among the major ones and various methodologies such as structured approach or object-oriented or object-centered approach. A memory management design of a programming language is one of the most important features to help facilitate reliable design. There are two wide-spread approaches in memory management: manual memory management and automatic memory management, known as Garbage Collection (GC for short). Recently, a third approach to memory management called Ownership has emerged. Ownership management is adapted in two recent languages Rust and Swift. Rust follows a deterministic syntax-driven memory management depending on static ownership rules implemented and enforced by the rustc compiler. Though the Rust approach eliminates to a high degree memory problems such as memory leak, dangling pointer and use after free, it has a steep learning costs. Swift also implements ownership concept in Automatic Reference Counting ARC. Though the ownership concept is adapted in Swift, it is not a memory safe language because of possibility of strong reference cycles. In this research, a demonstration of the ownership in Rust and Swift will be discussed and illustrated, followed by analysis of the consequences of memory issues related to each design. The comparison of Rust and Swift is based on ownership, memory safety, usability and programming paradigm in each language. As an illustration, an experiment to compare the elapsed times of two different structures and their algorithms, Binary Tree and Array are presented. The results illustrate and compare the performances of the same programs written in Rust, Swift, C, C++, and Java. / Thesis / Master of Science (MSc)

<p> </p> <p>Distributed agreement-based systems use common distributed agreement protocols such as leader election and consensus as building blocks for their target functionality—processes in these systems may need to agree on a leader, on the members of a group, on owners of locks, or on updates to replicated data. Such distributed agreement-based systems are common and potentially permit modular, scalable verification approaches that mimic their modular design. Interestingly, while there are many verification efforts that target agreement protocols themselves, little attention has been given to distributed agreement-based systems that build on top of these protocols. </p> <p>In this work, we aim to develop a fully-automated, modular, and usable parameterized verification approach for distributed agreement-based systems. To do so, we need to overcome the following challenges. First, the fully automated parameterized verification problem, i.e, the problem of algorithmically checking if the system is correct for any number of processes, is a well-known <em>undecidable </em>problem. Second, to enable modular verification that leverages the inherently-modular nature of these agreement-based systems, we need to be able to support <em>abstractions </em>of agreement protocols. Such abstractions can replace the agreement protocols’ implementations when verifying the overall system; enabling modular reasoning. Finally, even when the verification is fully automated, a system designer still needs assistance in <em>modeling </em>their distributed agreement-based systems. </p> <p>We systematically tackle these challenges through the following contributions. </p> <p>First, we support efficient, decidable verification of distributed agreement-based systems by developing a computational model—the GSP model—for reasoning about distributed (agreement-based) systems that admits decidability and <em>cutoff </em>results. Cutoff results enable practical verification by reducing the parameterized verification problem to the verification problem of a system with a fixed, finite number of processes. The GSP model supports generalized communication primitives and global guards, both of which are essential to enable abstractions of agreement protocols. </p> <p>Then, we address the usability and modularity aspects by developing a framework, QuickSilver, tailored for modeling and modular parameterized verification of distributed agreement-based systems. QuickSilver provides an intuitive domain-specific language, called Mercury, that is equipped with two agreement primitives capable of abstracting away agreement protocols when modeling agreement-based systems; enabling modular verification. QuickSilver extends the decidability and cutoff results of the GSP model to provide fully automated, efficient parameterized verification for a large class of systems modeled in Mercury. </p> <p>Finally, we leverage synthesis techniques to further enhance the usability of our approach and propose Cinnabar, a tool that supports synthesis of distributed agreement-based systems with efficiently-decidable parameterized verification. Cinnabar allows a system de- signer to provide a sketch of their Mercury model and uses a counterexample-guided synthesis procedure to search for model completions that both belong to the efficiently-decidable fragment of Mercury and are correct. </p> <p>We evaluate our contributions on various interesting distributed agreement-based systems adapted from real-world applications, such as a data store, a lock service, a surveillance system, a pathfinding algorithm for mobile robots, and more. </p>

The rise of parallel programming languages, as a result of processors' flattening clock frequencies, has lead to further use of high-level parallel pattern-based programming framework such as SkePU. SkePU provides a sequential high-level interface connected to different back-ends, or a hybrid of several, which reduces the time required to learn several new programming languages. Although this high-level interface introduces a new problem, an abstraction layer from the user to what code is being executed. To make SkePU programs easier to analyze this thesis implements a performance visualization tool for SkePU. The conducted literature study found that there currently exists very few performance visualization tools that cater specifically towards skeleton programming languages. This thesis evaluates usability of the implemented tool by conducting a survey and a user study with participants whom are very familiar with SkePU. The choice of evaluation method is in itself critically evaluated, as is the design choices made, and results are presented with an accompanying discussion as to how those results were derived.

The problem of this study was to develop and fieldtest a microcomputer assisted instruction program to teach simple microcomputer language acquisition. Four instruments were designed and pilot tested for use in the research. The first instrument was a survey designed to determine the complexity of the Applesoft BASIC commands. The second instrument was a survey to determine the frequency with which the Applesoft BASIC commands are used by Intermediate Microcomputer Users. The third instrument was an Exit Interview to determine how the Beginning Microcomputer Users felt about the instructional program and the presentation of the instruction. The fourth instrument, a Criterion Performance Test, was used to determine how well the instruction in the MAI program was transmitted to Beginning Microcomputer Users. The subjects involved in this study included three Expert Microcomputer Users, thirty Intermediate Microcomputer Users, and 24 Beginning Microcomputer Users. The experts were used to identify the Applesoft BASIC commands which are essential to Beginning Users, and to prioritize the commands. The intermediates were used to identify the frequency of use of each of the BASIC commands. Five of the intermediates were also used to test the instructional program for sequencing and appropriateness of instruction. The beginners were used for two separate purposes. Three sets of three subjects each were used to point out weaknesses in the instructional program so that they could be overcome. Fifteen beginners were used to test the final instructional program to determine whether it transmitted the desired information. Four research questions were posed in this study. These questions were answered based upon the findings. Fifteen BASIC commands and special characters were identified as essential to beginners in order for them to use the microcomputer adequately. Nine programmed instruction techniques were identified as suitable for use in microcomputer assisted instruction. One hundred and eighty-eight of the 257 revision suggestions were incorporated into program changes. Upon completion of the formative evaluation process, the instructional program was improved so that all subjects in the field test were able to demonstrate mastery of at least 70 percent of the behaviors which the program taught. / Ed. D.