Control, performance and safety in programming languages

Placeholder Show Content


Type safety and memory safety are the foundations of most modern programming languages. They assure that a large and important class of bugs simply cannot occur. When type and memory safety are combined with powerful mechanisms to control the functionality of code, such as module systems and monads, abstractions that may have otherwise required modifications to the language can be built. For example security mechanisms for both trusted and untrusted code, such as sandboxes and information flow control mechanisms, can be built and deployed as simple language-level libraries. However, all general purpose programming languages provide features that allow type and memory safety to be violated. For instance, Java has the sun.misc.Unsafe class, Go the unsafe package, and Haskell the System.IO.Unsafe module. These features exist for three reasons. First, they give developers greater control, for example, allowing interoperability with foreign code and hardware. Secondly, developers often use these unsafe features to implement higher performance code than they could otherwise, such as custom memory allocators. Finally, unsafe features are often exposed as an implementation artifact by the language and runtime system implementers, used by trusted parts of the standard library to implement safe abstractions for general consumption. These unsafe features are obviously useful and are widely used by developers, however, they cause three major problems. Firstly, they reintroduce all the possible bugs that type and memory safety remove, Secondly, they break a developer's and static analyzer's ability to reason cleanly about code. Third, they allow language abstractions to be violated, preventing security mechanism being implemented as simple libraries. This thesis explores solutions to the problem of allowing but controlling developer access to unsafe features in programming languages such that code can still be reasoned about and invariants enforced. It looks at it in two parts. First, we describe Safe Haskell, a language mechanism for controlling the use of unsafe features by developers. Secondly, we investigate the use of unsafe features and their use in violating memory safety for performance gains. We describe two novel language mechanisms, M3 and Blade, that open up the memory management subsystem of safe languages without giving up either memory or type safety.


Type of resource text
Form electronic; electronic resource; remote
Extent 1 online resource.
Publication date 2016
Issuance monographic
Language English


Associated with Terei, David
Associated with Stanford University, Department of Computer Science.
Primary advisor Mazières, David (David Folkman), 1972-
Thesis advisor Mazières, David (David Folkman), 1972-
Thesis advisor Aiken, Alexander
Thesis advisor Engler, Dawson R
Advisor Aiken, Alexander
Advisor Engler, Dawson R


Genre Theses

Bibliographic information

Statement of responsibility David Terei.
Note Submitted to the Department of Computer Science.
Thesis Thesis (Ph.D.)--Stanford University, 2016.
Location electronic resource

Access conditions

© 2016 by David Anthony Terei
This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).

Also listed in

Loading usage metrics...