Programming Languages and Compilers Commons^™

Deep Learning Recommendations For The Acl2 Interactive Theorem Prover, Robert K. Thompson, Robert K. Thompson

Master's Theses

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 …

Rasm: Compiling Racket To Webassembly, Grant Matejka

Master's Theses

WebAssembly is an instruction set designed for a stack based virtual machine, with an emphasis on speed, portability and security. As the use cases for WebAssembly grow, so does the desire to target WebAssembly in compilation. In this thesis we present Rasm, a Racket to WebAssembly compiler that compiles a select subset of the top forms of the Racket programming language to WebAssembly. We also present our early findings in our work towards adding a WebAssembly backend to the Chez Scheme compiler that is the backend of Racket. We address initial concerns and roadblocks in adopting a WebAssembly backend and …

Jited: A Framework For Jit Education In The Classroom, Caleb Watts

Master's Theses

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 …

Towards A Complete Formal Semantics Of Rust, Alexa White

Master's Theses

Rust is a relatively new programming language with a unique memory model designed to provide the ease of use of a high-level language as well as the power and control of a low-level language while preserving memory safety. In order to prove the safety and correctness of Rust and to provide analysis tools for its use cases, it is necessary to construct a formal semantics of the language. Existing efforts to construct such a semantic model are limited in their scope and none to date have successfully captured the complete functionality of the language. This thesis focuses on the K-Rust …

Rplidar A2 Accuracy, Ramiro O. Garcia

STAR Program Research Presentations

Traffic is not only a source of frustration but also a leading cause of death for people under 35 years of age. Recent research has focused on how driver assistance technology can be used to mitigate traffic fatalities and create more enjoyable commutes. In addition, self-driving vehicles can reduce fuel consumption the amount by 5% and increases the number of cars on the highway. To achieve this we need to research reliable sensors. This summer I research Rplidar A2 sensor which hopefully will be responsible for recording distance to the preceding car and helping prevent Insider Attacks or Misbehaviors of …

Design And Analysis Of An Instrumenting Profiler For Webassembly, Chandler Gifford

Master's Theses

This thesis presents the design, implementation, and analysis of WasmProf, an instrumenting profiler for WebAssembly programs. WebAssembly is a compiled language designed for use on the web that, at the time of this writing, is still being actively developed. At present, performance analysis for WebAssembly programs mostly consists of browsers’ built-in sampling profilers. These profilers work well in many cases but only give a statistical estimation of the distribution of function calls and are, therefore, not well-suited for more fine-grained analysis. The WasmProf instrumenting profiler fills this analysis gap. WasmProf is capable of tracking the number of calls made and …

Supported Programming For Beginning Developers, Andrew Gilbert

Master's Theses

Testing code is important, but writing test cases can be time consuming, particularly for beginning programmers who are already struggling to write an implementation. We present TestBuilder, a system for test case generation which uses an SMT solver to generate inputs to reach specified lines in a function, and asks the user what the expected outputs would be for those inputs. The resulting test cases check the correctness of the output, rather than merely ensuring the code does not crash. Further, by querying the user for expectations, TestBuilder encourages the programmer to think about what their code ought to do, …

An Empirical Study Of Alias Analysis Techniques, Andrew T. Tran

Master's Theses

As software projects become larger and more complex, software optimization at that scale is only feasible through automated means. One such component of software optimization is alias analysis, which attempts to determine which variables in a program refer to the same area in memory, and is used to relocate instructions to improve performance without interfering with program execution. Several alias analyses have been proposed over the past few decades, with varying degrees of precision and time and space complexity, but few studies have been conducted to compare these techniques with one another, nor to measure with program data to confirm …

Funqual: User-Defined, Statically-Checked Call Graph Constraints In C++, Andrew P. Nelson

Master's Theses

Static analysis tools can aid programmers by reporting potential programming mistakes prior to the execution of a program. Funqual is a static analysis tool that reads C++17 code ``in the wild'' and checks that the function call graph follows a set of rules which can be defined by the user. This sort of analysis can help the programmer to avoid errors such as accidentally calling blocking functions in time-sensitive contexts or accidentally allocating memory in heap-sensitive environments. To accomplish this, we create a type system whereby functions can be given user-defined type qualifiers and where users can define their own …

Compiler Optimization Effects On Register Collisions, Jonathan S. Tan

Master's Theses

We often want a compiler to generate executable code that runs as fast as possible. One consideration toward this goal is to keep values in fast registers to limit the number of slower memory accesses that occur. When there are not enough physical registers available for use, values are ``spilled'' to the runtime stack. The need for spills is discovered during register allocation wherein values in use are mapped to physical registers. One factor in the efficacy of register allocation is the number of values in use at one time (register collisions). Register collision is affected by compiler optimizations that …

Gpumap: A Transparently Gpu-Accelerated Map Function, Ivan Pachev

Master's Theses

As GPGPU computing becomes more popular, it will be used to tackle a wider range of problems. However, due to the current state of GPGPU programming, programmers are typically required to be familiar with the architecture of the GPU in order to effectively program it. Fortunately, there are software packages that attempt to simplify GPGPU programming in higher-level languages such as Java and Python. However, these software packages do not attempt to abstract the GPU-acceleration process completely. Instead, they require programmers to be somewhat familiar with the traditional GPGPU programming model which involves some understanding of GPU threads and kernels. …

Spest – A Tool For Specification-Based Testing, Corrigan Redford Johnson

Master's Theses

This thesis presents a tool for SPEcification based teSTing (SPEST). SPEST is designed to use well known practices for automated black-box testing to reduce the burden of testing on developers. The tool uses a simple formal specification language to generate highly-readable unit tests that embody best practices for thorough software testing. Because the specification language used to generate the assertions about the code can be compiled, it can also be used to ensure that documentation describing the code is maintained during development and refactoring.

The utility and effectiveness of SPEST were validated through several exper- iments conducted with students in …

An Interactive User Interface Improves Data Visualization In R, Nathan Sweem

STAR Program Research Presentations

An interactive user interface application was created using the R statistical computing environment and the Shiny package to visualize historical data on the performance of mutual funds and exchange-traded funds (ETFs). Historical data for these funds is scraped from the Yahoo! Finance webpage. The application allows the user to analyze this historical data by category and fund family, which are also scraped from Yahoo! Finance. The application generates interactive plots to compare the performance of selected mutual funds and ETFs given the baseline and center determined by the user. The application has been modified to attentively match the data with …

Simple Macro: Addon For World Of Warcraft, Yemane Gebreyesus

Computer Engineering

This senior project was started to try and solve a problem within World of Warcraft. That particular problem is the underdeveloped default macro interface, which Simple Macro aims to remedy by creating a more user-friendly interface that is accessible by a wider audience. It employs a click through method of accessing and editing data to reduce the amount of typing necessary. The addon also has a feature to specifically help players that want to change a target in certain groups of macros all at once. The project was developed in both Lua and XML.

Conception, Design And Construction Of A Remote Wifi Vehicle Using Arduino, Clayton Broman

Physics

The scope of this senior project was to make a wireless vehicle controlled via Internet Protocol. This vehicle operates remotely and without direct line of sight. Commands are sent from a program running on a laptop and transmitted using a wireless router. Visual data is retrieved from a network camera, mounted on the vehicle, in real-time, to see where you are going.

Analyzing The Performance Of The Sofia Infrared Telescope, Sarah M. Bass, Jeffrey Van Cleve, Zaheer Ali

STAR Program Research Presentations

The Stratospheric Observatory for Infrared Astronomy (SOFIA) is an airborne near-space observatory onboard a modified Boeing 747-SP aircraft, which flies at altitudes of 45,000 ft., above 99% of the Earth’s water vapor. SOFIA contains an effective 2.5 m infrared (IR) telescope that has a dichroic tertiary mirror, reflecting IR and visible wavelengths to the science instrument (SI) and focal plane imager (FPI), respectively. To date, seven different SIs have been designed to cover a wide range of wavelengths and spectral resolutions. Since the telescope operates in the infrared, different techniques, including chopping, nodding, and dithering, are used to reduce the …

Flitecam Data Process Validation, Jesse K. Tsai, Sachindev S. Shenoy, Brent Cedric Nicklas, Zaheer Ali, William T. Reach

STAR Program Research Presentations

FLITECAM Data Processing Validation

Many of the challenges that come from working with astronomical imaging arise from the reduction of raw data into scientifically meaningful data. First Light Infrared Test CAMera (FLITECAM) is an infrared camera operating in the 1.0–5.5 μm waveband on board SOFIA (Stratospheric Observatory For Infrared Astronomy). Due to the significant noise from the atmosphere and the camera itself, astronomers have developed many methods to reduce the effects of atmospheric and instrumental emission. The FLITECAM Data Reduction Program (FDRP) is a program, developed at SOFIA Science Center, subtracts darks, removes flats, and dithers images.

This project contains …

Senior Project Report - Doctest, Stephen Weessies

Computer Engineering

DocTest is a program that, simply put, allows a programmer or user to document STANAG 4586 (a standard for unmanned aerial vehicle interoperability) messages and test the vehicle system at Lockheed Martin [5]. The program is extensible to allow for further development aiding our software team to do what they do best and not get bogged down in tedious but necessary documentation. DocTest is also used to aid in testing, keeping track of the issues and bugs found and creating a document that captures each issue so an issue is not missed or forgotten. This program was made for use …

Cuda Web Api Remote Execution Of Cuda Kernels Using Web Services, Massimo J. Becker

Master's Theses

Massively parallel programming is an increasingly growing field with the recent introduction of general purpose GPU computing. Modern graphics processors from NVIDIA and AMD have massively parallel architectures that can be used for such applications as 3D rendering, financial analysis, physics simulations, and biomedical analysis. These massively parallel systems are exposed to programmers through in- terfaces such as NVIDIAs CUDA, OpenCL, and Microsofts C++ AMP. These frame- works expose functionality using primarily either C or C++. In order to use these massively parallel frameworks, programs being implemented must be run on machines equipped with massively parallel hardware. These requirements limit …

Functional Reactive Musical Performers, Justin M. Phillips

Master's Theses

Computers have been assisting in recording, sound synthesis and other fields of music production for quite some time. The actual performance of music continues to be an area in which human players are chosen over computer performers. Musical performance is an area in which personalization is more important than consistency. Human players play with each other, reacting to phrases and ideas created by the players that they are playing with. Computer performers lack the ability to react to the changes in the performance that humans perceive naturally, giving the human players an advantage over the computer performers.

This thesis creates …

Max Flow Spill Code Placement Algorithm Implemented In Gcc 4.4.3, Stephen Robert Beard

Computer Engineering

The placement of spill code plays an important role in the register allocator of an optimizing compiler. Many computer architectures possess a register linkage convention that dictates which registers are preserved across function calls and which are not. This project addresses the problem of optimizing spill code that is associated with register linkage conventions.

This algorithm was created by Dr. Chris Lupo and is described in the paper Beyond Register Allocation: a Novel Algorithm for Spill-Code Placement. The algorithm was implemented for GCC 2.5.7 for a PA-RISC architecture [4]. The work in this project will involve porting the existing code …

Automation In Cs1 With The Factoring Problem Generator, Joshua B. Parker

Master's Theses

As the field of computer science continues to grow, the number of students enrolled in related programs will grow as well. Though one-on-one tutoring is one of the more effective means of teaching, computer science instructors will have less and less time to devote to individual students. To address this growing concern, many tools that automate parts of an instructor’s job have been proposed. These tools can assist instructors in presenting concepts and grading student work, and they can help students learn to program more effectively. A growing group of intelligent tutoring systems attempts to tie all of this functionality …

Post Register Allocation Spill Code Optimization, Christopher Lupo, Kent Wilken

Computer Science and Software Engineering

A highly optimized register allocator should provide an efficient placement of save/restore code for procedures that contain calls. This paper presents a new approach to placing callee-saved save and restore instructions that generalizes Chow's shrink-wrapping technique (Chow 1988). An efficient, profile-guided, hierarchical spill code placement algorithm is used to analyze the structure of a procedure to calculate the minimum dynamic execution count locations to place callee-saved save and restore code. The algorithm is implemented in the Gnu Compiler Collection and has been tested on the SPEC CPU2000 Integer Benchmark suite. Results show that the technique reduces the number of dynamic …