Control, performance and safety in programming languages
Abstract/Contents
- Abstract
- 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.
Description
| Type of resource | text |
|---|---|
| Form | electronic; electronic resource; remote |
| Extent | 1 online resource. |
| Publication date | 2016 |
| Issuance | monographic |
| Language | English |
Creators/Contributors
| 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 |
Subjects
| 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
- Copyright
- © 2016 by David Anthony Terei
- License
- This work is licensed under a Creative Commons Attribution Non Commercial 3.0 Unported license (CC BY-NC).
Also listed in
Loading usage metrics...