More Web Proxy on the site http://driver.im/

research-article

Experience report: a do-it-yourself high-assurance compiler

Authors:

Sebastian Niller,

Alwyn GoodloeAuthors Info & Claims

ACM SIGPLAN Notices, Volume 47, Issue 9

Pages 335 - 340

https://doi.org/10.1145/2398856.2364553

Published: 09 September 2012 Publication History

Abstract

Embedded domain-specific languages (EDSLs) are an approach for quickly building new languages while maintaining the advantages of a rich metalanguage. We argue in this experience report that the "EDSL approach" can surprisingly ease the task of building a high-assurance compiler. We do not strive to build a fully formally-verified tool-chain, but take a "do-it-yourself" approach to increase our confidence in compiler-correctness without too much effort. Copilot is an EDSL developed by Galois, Inc. and the National Institute of Aerospace under contract to NASA for the purpose of runtime monitoring of flight-critical avionics. We report our experience in using type-checking, QuickCheck, and model-checking "off-the-shelf" to quickly increase confidence in our EDSL tool-chain.

References

[1]

E. Axelsson, K. Claessen, M. Sheeran, J. Svenningsson, D. Engdal, and A. Persson. The design and implementation of Feldspar - an embedded language for digital signal processing. In Implementation and Application of Functional Languages, volume 6647 of LNCS, pages 121--136. Springer, 2011.

Digital Library

[2]

A. I. Baars and S. D. Swierstra. Typing dynamic typing. In Intl. Conference on Functional Programming (ICFP), pages 157--166. ACM, September 2002.

Digital Library

[3]

R. S. Boyer and J. S. Moore. MJRTY: A fast majority vote algorithm. In Automated Reasoning: Essays in Honor of Woody Bledsoe, pages 105--118, 1991.

[4]

P. Caspi, D. Pialiud, N. Halbwachs, and J. Plaice. LUSTRE: a declarative language for programming synchronous systems. In 14th Symposium on Principles of Programming Languages, pages 178--188, 1987.

Digital Library

[5]

K. Claessen and J. Hughes. QuickCheck: A lightweight tool for random testing of Haskell programs. In ACM SIGPLAN Notices, pages 268--279. ACM, 2000.

Digital Library

[6]

E. Clarke, D. Kroening, and F. Lerda. A tool for checking ANSI-C programs. In Tools and Algorithms for the Construction and Analysis of Systems (TACAS), LNCS, pages 168--176. Springer, 2004.

[7]

P. E. Dagand, A. Baumann, and T. Roscoe. Filet-o-Fish: practical and dependable domain-specific languages for OS development. In Proceedings of the Fifth Workshop on Programming Languages and Operating Systems (PLOS '09), pages 1--5. ACM, 2009.

Digital Library

[8]

B. Dutertre and L. D. Moura. The Yices SMT solver. Technical report, SRI, 2006.

[9]

J. Gao, M. Heimdahl, and E. Van Wyk. Flexible and extensible notations for modeling languages. In Fundamental Approaches to Software Engineering (FASE), volume 4422 of LNCS, pages 102--116. Springer Verlag, March 2007.

Digital Library

[10]

A. Gill. Type-safe observable sharing in Haskell. In Proceedings of the 2009 ACM SIGPLAN Haskell Symposium, September 2009.

Digital Library

[11]

A. Goodloe and L. Pike. Monitoring distributed real-time systems: A survey and future directions. Technical Report NASA/CR-2010-216724, NASA Langley Research Center, July 2010.

[12]

N. Halbwachs and P. Raymond. Validation of synchronous reactive systems: from formal verification to automatic testing. In ASIAN'99, Asian Computing Science Conference. LNCS 1742, Springer, December 1999.

Digital Library

[13]

T. Hawkins. Controlling hybrid vehicles with Haskell. Presentation. Commercial Users of Functional Programming (CUFP), 2008. Available at http://cufp.galois.com/2008/schedule.html.

[14]

T. Kahsai, Y. Ge, and C. Tinelli. Instantiation-based invariant discovery. In 3rd NASA Formal Methods Symposium, volume 6617 of LNCS, pages 192--207. Springer, 2011.

Digital Library

[15]

D. Leijen and E. Meijer. Domain specific embedded compilers. In Domain-Specific Languages Conference. USENIX, 1999.

Digital Library

[16]

X. Leroy. Formal verification of a realistic compiler. Communications of the ACM, 52: 107--115, July 2009.

Digital Library

[17]

J. S. Moore, editor. Special Issue on System Verification: Journal of Automated Reasoning, volume 5, 1989.

Digital Library

[18]

B. Pagano, O. Andrieu, T. Moniot, B. Canou, E. Chailloux, P. Wang, P. Manoury, and J.-L. Colao. Experience report: using Objective Caml to develop safety-critical embedded tools in a certification framework. In G. Hutton and A. P. Tolmach, editors, International Conference on Functional Programming (ICFP), pages 215--220. ACM, 2009.

Digital Library

[19]

L. Pike, M. Shields, and J. Matthews. A verifying core for a cryptographic language compiler. In Proceedings of the 6th Intl. Workshop on the ACL2 Theorem Prover and its Applications, pages 1--10. ACM, 2006.

Digital Library

[20]

L. Pike, S. Niller, and N. Wegmann. Runtime verification for ultra-critical systems. In Proceedings of the 2nd Intl. Conference on Runtime Verification, LNCS. Springer, September 2011.

Digital Library

[21]

L. Sassaman, M. L. Patterson, S. Bratus, and A. Shubina. The Halting problems of network stack insecurity. ;login: The USENIX Magazine, 36 (6), December 2011.

[22]

T. Schrijvers, S. Peyton Jones, M. Sulzmann, and D. Vytiniotis. Complete and decidable type inference for GADTs. In International Conference on Functional Programming (ICFP), ICFP '09, pages 341--352. ACM, 2009.

Digital Library

[23]

D. Terei, S. Marlow, S. P. Jones, and D. Mazières. Safe haskell. In Proceedings of the Haskell Symposium, 2012.

Digital Library

[24]

X. Yang, Y. Chen, E. Eide, and J. Regehr. Finding and understanding bugs in C compilers. In Programming Language Design and Implementation (PLDI), pages 283--294. ACM, 2011.

Digital Library

Cited By

Scott RDodds MPerez IGoodloe ADockins R(2023)Trustworthy Runtime Verification via Bisimulation (Experience Report)Proceedings of the ACM on Programming Languages10.1145/36078417:ICFP(305-321)Online publication date: 31-Aug-2023
https://doi.org/10.1145/3607841
Gill ASculthorpe NDawson JEskilson AFarmer AGrebe MRosenbluth JScott RStanton J(2015)The remote monad design patternACM SIGPLAN Notices10.1145/2887747.280431150:12(59-70)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2887747.2804311
Gill ASculthorpe NDawson JEskilson AFarmer AGrebe MRosenbluth JScott RStanton JLippmeier B(2015)The remote monad design patternProceedings of the 2015 ACM SIGPLAN Symposium on Haskell10.1145/2804302.2804311(59-70)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804302.2804311
Show More Cited By

Index Terms

Experience report: a do-it-yourself high-assurance compiler
1. General and reference
  1. Cross-computing tools and techniques
    1. Reliability
2. Software and its engineering
  1. Software organization and properties
    1. Extra-functional properties
      1. Software reliability

Recommendations

Experience report: a do-it-yourself high-assurance compiler
ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming

Embedded domain-specific languages (EDSLs) are an approach for quickly building new languages while maintaining the advantages of a rich metalanguage. We argue in this experience report that the "EDSL approach" can surprisingly ease the task of building ...
Modular language implementation in Rascal - experience report

All software evolves, and programming languages and programming language tools are no exception. And just like in ordinary software construction, modular implementations can help ease the process of changing a language implementation and its dependent ...
Experience report: using hackage to inform language design
HASKELL '10

Hackage, an online repository of Haskell applications and libraries, provides a hub for programmers to both release code to and use code from the larger Haskell community. We suggest that Hackage can also serve as a valuable resource for language ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image ACM SIGPLAN Notices

ACM SIGPLAN Notices Volume 47, Issue 9

ICFP '12

September 2012

368 pages

ISSN:0362-1340

EISSN:1558-1160

DOI:10.1145/2398856

Issue’s Table of Contents

ICFP '12: Proceedings of the 17th ACM SIGPLAN international conference on Functional programming
September 2012
392 pages
ISBN:9781450310543
DOI:10.1145/2364527
General Chair:
Peter Thiemann
University of Freiburg, Germany
,
Program Chair:
Robby Findler
Northwestern University, USA

Copyright © 2012 ACM.

Permission to make digital or hard copies of all or part of this work for personal or classroom use is granted without fee provided that copies are not made or distributed for profit or commercial advantage and that copies bear this notice and the full citation on the first page. Copyrights for components of this work owned by others than ACM must be honored. Abstracting with credit is permitted. To copy otherwise, or republish, to post on servers or to redistribute to lists, requires prior specific permission and/or a fee. Request permissions from [email protected]

Publisher

Association for Computing Machinery

New York, NY, United States

Publication History

Published: 09 September 2012

Published in SIGPLAN Volume 47, Issue 9

Check for updates

Author Tags

Qualifiers

Research-article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

15
Total Citations
View Citations
298
Total Downloads

Downloads (Last 12 months)3
Downloads (Last 6 weeks)1

Reflects downloads up to 11 Dec 2024

Other Metrics

View Author Metrics

Citations

Cited By

Scott RDodds MPerez IGoodloe ADockins R(2023)Trustworthy Runtime Verification via Bisimulation (Experience Report)Proceedings of the ACM on Programming Languages10.1145/36078417:ICFP(305-321)Online publication date: 31-Aug-2023
https://doi.org/10.1145/3607841
Gill ASculthorpe NDawson JEskilson AFarmer AGrebe MRosenbluth JScott RStanton J(2015)The remote monad design patternACM SIGPLAN Notices10.1145/2887747.280431150:12(59-70)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2887747.2804311
Gill ASculthorpe NDawson JEskilson AFarmer AGrebe MRosenbluth JScott RStanton JLippmeier B(2015)The remote monad design patternProceedings of the 2015 ACM SIGPLAN Symposium on Haskell10.1145/2804302.2804311(59-70)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804302.2804311
Perez IGoodloe ADedden F(2024)Runtime Verification in Real-Time with the Copilot Language: A TutorialFormal Methods10.1007/978-3-031-71177-0_27(469-491)Online publication date: 13-Sep-2024
https://doi.org/10.1007/978-3-031-71177-0_27
Hertz BLuppen ZRozier K(2021)Integrating Runtime Verification into a Sounding Rocket Control SystemNASA Formal Methods10.1007/978-3-030-76384-8_10(151-159)Online publication date: 19-May-2021
https://doi.org/10.1007/978-3-030-76384-8_10
Basin DDardinier THeimes LKrstić SRaszyk MSchneider JTraytel D(2020)A Formally Verified, Optimized Monitor for Metric First-Order Dynamic LogicAutomated Reasoning10.1007/978-3-030-51074-9_25(432-453)Online publication date: 1-Jul-2020
https://dl.acm.org/doi/10.1007/978-3-030-51074-9_25
Goodloe A(2016)Challenges in High-Assurance Runtime VerificationLeveraging Applications of Formal Methods, Verification and Validation: Foundational Techniques10.1007/978-3-319-47166-2_31(446-460)Online publication date: 5-Oct-2016
https://doi.org/10.1007/978-3-319-47166-2_31
Gill ASculthorpe NDawson JEskilson AFarmer AGrebe MRosenbluth JScott RStanton J(2015)The remote monad design patternACM SIGPLAN Notices10.1145/2887747.280431150:12(59-70)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2887747.2804311
Gill ASculthorpe NDawson JEskilson AFarmer AGrebe MRosenbluth JScott RStanton JLippmeier B(2015)The remote monad design patternProceedings of the 2015 ACM SIGPLAN Symposium on Haskell10.1145/2804302.2804311(59-70)Online publication date: 30-Aug-2015
https://dl.acm.org/doi/10.1145/2804302.2804311
Laurent JGoodloe APike L(2015)Assuring the GuardiansRuntime Verification10.1007/978-3-319-23820-3_6(87-101)Online publication date: 15-Nov-2015
https://doi.org/10.1007/978-3-319-23820-3_6
Show More Cited By

View Options

Login options

Check if you have access through your login credentials or your institution to get full access on this article.

Full Access

Get this Publication

View options

PDF

View or Download as a PDF file.

eReader

View online with eReader.

Media

Figures

Other

Tables

View Issue’s Table of Contents