The bedrock structured programming system
We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining character...
| Main Author: | |
|---|---|
| Format: | Article |
| Language: | English |
| Published: |
Association for Computing Machinery (ACM)
2021
|
| Online Access: | https://hdl.handle.net/1721.1/135766 |
| _version_ | 1826194694400376832 |
|---|---|
| author | Chlipala, A |
| author_facet | Chlipala, A |
| author_sort | Chlipala, A |
| collection | MIT |
| description | We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. The abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language; but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack. |
| first_indexed | 2024-09-23T10:00:16Z |
| format | Article |
| id | mit-1721.1/135766 |
| institution | Massachusetts Institute of Technology |
| language | English |
| last_indexed | 2024-09-23T10:00:16Z |
| publishDate | 2021 |
| publisher | Association for Computing Machinery (ACM) |
| record_format | dspace |
| spelling | mit-1721.1/1357662022-03-29T20:51:33Z The bedrock structured programming system Chlipala, A We report on the design and implementation of an extensible programming language and its intrinsic support for formal verification. Our language is targeted at low-level programming of infrastructure like operating systems and runtime systems. It is based on a cross-platform core combining characteristics of assembly languages and compiler intermediate languages. From this foundation, we take literally the saying that C is a "macro assembly language": we introduce an expressive notion of certified low-level macros, sufficient to build up the usual features of C and beyond as macros with no special support in the core. Furthermore, our macros have integrated support for strongest postcondition calculation and verification condition generation, so that we can provide a high-productivity formal verification environment within Coq for programs composed from any combination of macros. Our macro interface is expressive enough to support features that low-level programs usually only access through external tools with no formal guarantees, such as declarative parsing or SQL-inspired querying. The abstraction level of these macros only imposes a compile-time cost, via the execution of functional Coq programs that compute programs in our intermediate language; but the run-time cost is not substantially greater than for more conventional C code. We describe our experiences constructing a full C-like language stack using macros, with some experiments on the verifiability and performance of individual programs running on that stack. 2021-10-27T20:29:12Z 2021-10-27T20:29:12Z 2013-01-01 2019-05-13T17:18:03Z Article http://purl.org/eprint/type/ConferencePaper https://hdl.handle.net/1721.1/135766 en https://dl.acm.org/citation.cfm?id=2500592 ACM SIGPLAN Notices Creative Commons Attribution-Noncommercial-Share Alike http://creativecommons.org/licenses/by-nc-sa/4.0/ application/pdf Association for Computing Machinery (ACM) MIT web domain |
| spellingShingle | Chlipala, A The bedrock structured programming system |
| title | The bedrock structured programming system |
| title_full | The bedrock structured programming system |
| title_fullStr | The bedrock structured programming system |
| title_full_unstemmed | The bedrock structured programming system |
| title_short | The bedrock structured programming system |
| title_sort | bedrock structured programming system |
| url | https://hdl.handle.net/1721.1/135766 |
| work_keys_str_mv | AT chlipalaa thebedrockstructuredprogrammingsystem AT chlipalaa bedrockstructuredprogrammingsystem |