Compiling Gallina to go for the FSCQ file system
Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017.
| Main Author: | |
|---|---|
| Other Authors: | |
| Format: | Thesis |
| Language: | eng |
| Published: |
Massachusetts Institute of Technology
2018
|
| Subjects: | |
| Online Access: | http://hdl.handle.net/1721.1/113460 |
| _version_ | 1826206724980211712 |
|---|---|
| author | Ziegler, Daniel (Daniel M.) |
| author2 | Nickolai Zeldovich and M. Frans Kaashoek. |
| author_facet | Nickolai Zeldovich and M. Frans Kaashoek. Ziegler, Daniel (Daniel M.) |
| author_sort | Ziegler, Daniel (Daniel M.) |
| collection | MIT |
| description | Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017. |
| first_indexed | 2024-09-23T13:37:16Z |
| format | Thesis |
| id | mit-1721.1/113460 |
| institution | Massachusetts Institute of Technology |
| language | eng |
| last_indexed | 2024-09-23T13:37:16Z |
| publishDate | 2018 |
| publisher | Massachusetts Institute of Technology |
| record_format | dspace |
| spelling | mit-1721.1/1134602019-04-10T14:00:22Z Compiling Gallina to go for the FSCQ file system Ziegler, Daniel (Daniel M.) Nickolai Zeldovich and M. Frans Kaashoek. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Massachusetts Institute of Technology. Department of Electrical Engineering and Computer Science. Electrical Engineering and Computer Science. Thesis: M. Eng., Massachusetts Institute of Technology, Department of Electrical Engineering and Computer Science, 2017. This electronic version was submitted by the student author. The certified thesis is available in the Institute Archives and Special Collections. Cataloged from student-submitted PDF version of thesis. Includes bibliographical references (pages 85-87). Over the last decade, systems software verification has become increasingly practical. Many verified systems have been written in the language of a proof assistant, proved correct, and then made runnable using code extraction. However, due to the rigidity of extraction and the overhead of the target languages, the resulting code's CPU performance can suffer, with limited opportunity for optimization. This thesis contributes CoqGo, a proof-producing compiler from Coq's Gallina language to Go. We created Go', a stylized semantics of Go which enforce linearity, and implemented proof-producing compilation tactics from Gallina to Go' plus a straightforward translation from Go' to Go. Applying a prototype of CoqGo, we compiled a system call in the FSCQ file system, with minimal changes to FSCQ's source code. Taking advantage of the increased control given by CoqGo, we implemented three optimizations, bringing the system call's CPU performance to 19% faster than the extracted version. by Daniel Ziegler. M. Eng. 2018-02-08T15:58:38Z 2018-02-08T15:58:38Z 2017 2017 Thesis http://hdl.handle.net/1721.1/113460 1020286380 eng MIT theses are protected by copyright. They may be viewed, downloaded, or printed from this source but further reproduction or distribution in any format is prohibited without written permission. http://dspace.mit.edu/handle/1721.1/7582 87 pages application/pdf Massachusetts Institute of Technology |
| spellingShingle | Electrical Engineering and Computer Science. Ziegler, Daniel (Daniel M.) Compiling Gallina to go for the FSCQ file system |
| title | Compiling Gallina to go for the FSCQ file system |
| title_full | Compiling Gallina to go for the FSCQ file system |
| title_fullStr | Compiling Gallina to go for the FSCQ file system |
| title_full_unstemmed | Compiling Gallina to go for the FSCQ file system |
| title_short | Compiling Gallina to go for the FSCQ file system |
| title_sort | compiling gallina to go for the fscq file system |
| topic | Electrical Engineering and Computer Science. |
| url | http://hdl.handle.net/1721.1/113460 |
| work_keys_str_mv | AT zieglerdanieldanielm compilinggallinatogoforthefscqfilesystem |