Abstract
As part of the development of a new real-time operating system, an asynchronous communication mechanism, for use between applications, has been implemented in a programming language with an advanced static type system. This mechanism is designed to provide desired properties of asynchronicity, coherency and freshness. We used the features of the type system, including linear and dependent types, to represent and partially prove that the implementation safely upheld coherency and freshness. We believe that the resulting program code forms a good example of how easily linear and dependent types can be applied in practice to prove useful properties of low-level concurrent systems programming, while leaving no traces of runtime overhead.
This research is supported partly by NSF grant CCF-1018601.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
Similar content being viewed by others
References
Alkassar, E., Hillebrand, M.A., Leinenbach, D., Schirmer, N.W., Starostin, A.: The Verisoft Approach to Systems Verification. In: Shankar, N., Woodcock, J. (eds.) VSTTE 2008. LNCS, vol. 5295, pp. 209–224. Springer, Heidelberg (2008)
ARM Limited. ARM Architecture Reference Manual, ARMv7-A and ARMv7-R edition (2011)
Bershad, B.N., Savage, S., Pardyak, P., Sirer, E.G., Fiuczynski, M., Becker, D., Eggers, S., Chambers, C.: Extensibility, Safety and Performance in the SPIN Operating System. In: Proceedings of the Fifteenth ACM Symposium on Operating Systems Principles, pp. 267–284 (1995)
Blume, M., et al.: Standard ML of New Jersey (2009), http://www.smlnj.org/
Cardelli, L., et al.: Modula-3 report (revised). Technical report, Digital Equipment Corp. (now HP Inc.) (November 1989), http://www.hpl.hp.com/techreports/Compaq-DEC/SRC-RR-52.html
Chen, C., Xi, H.: Combining Programming with Theorem Proving. In: ICFP 2005: Proceedings of the Tenth ACM SIGPLAN International Conference on Functional Programming, pp. 66–77. ACM Press (2005)
Danish, M.: Terrier OS, http://www.github.com/mrd/terrier
de Moura, L., Bjørner, N.: Z3: An Efficient SMT Solver. In: Ramakrishnan, C.R., Rehof, J. (eds.) TACAS 2008. LNCS, vol. 4963, pp. 337–340. Springer, Heidelberg (2008)
Elphinstone, K., Heiser, G.: From L3 to seL4 What Have We Learnt in 20 Years of L4 Microkernels? In: Proceedings of the Twenty-Fourth ACM Symposium on Operating Systems Principles, SOSP 2013, pp. 133–150. ACM, New York (2013)
Fu, G.: Design and Implementation of an Operating System in Standard ML. Master’s thesis, University of Hawaii (August 1999), http://www2.hawaii.edu/~esb/prof/proj/hello/
Hallgren, T., Jones, M.P., Leslie, R., Tolmach, A.: A principled approach to operating system construction in Haskell. SIGPLAN Not. 40(9), 116–128 (2005)
Henderson, N., Paynter, S.E.: The formal classification and verification of Simpson’s 4-slot asynchronous communication mechanism. Springer, Heidelberg (2002)
Hohmuth, M., Tews, H.: The VFiasco approach for a verified operating system. In: Proceedings of the 2nd ECOOP Workshop on Programming Languages and Operating Systems (2005), http://www.cs.ru.nl/H.Tews/Plos-2005/ecoop-plos-05-letter.pdf
Hunt, G.C., Laru, J.R.: Singularity: Rethinking the Software Stack. In: ACM SIGOPS Operating System Review, vol. 41, pp. 37–49. Association for Computing Machinery (April 2007)
Klein, G., Elphinstone, K., Heiser, G., et al.: seL4: Formal verification of an OS kernel. In: Proceedings of the 22nd ACM Symposium on Operating Systems Principles, Big Sky, MT, USA (October 2009)
Lamport, L.: On interprocess communication. Distributed Computing 1-2, 77–101 (1986)
Paulson, L.C.: Isabelle. LNCS, vol. 828. Springer, Heidelberg (1994)
Peyton-Jones, S., Marlow, S., et al.: The Glasgow Haskell Compiler, http://www.haskell.org/ghc/
Rushby, J.: Model checking Simpson’s four-slot fully asynchronous communication mechanism. Computer Science Laboratory–SRI International, Tech. Rep. Issued (2002)
Simpson, H.R.: Four-slot fully asynchronous communication mechanism. In: IEE Proceedings, vol. 137, Pt. E, No. 1. IEE (January 1990)
Simpson, H.R.: Correctness analysis for class of asynchronous communication mechanisms. IEE Proceedings E (Computers and Digital Techniques) 139, 35–49 (1992)
Simpson, H.R.: Role model analysis of an asynchronous communication mechanism. In: Computers and Digital Techniques, IEE Proceedings, vol. 144, pp. 232–240. IET (1997)
Torvalds, L., et al.: Linux, http://www.linuxfoundation.org/
Wadler, P.: A taste of linear logic. In: Borzyszkowski, A.M., Sokolowski, S. (eds.) MFCS 1993. LNCS, vol. 711, pp. 185–210. Springer, Heidelberg (1993), http://dx.doi.org/10.1007/3-540-57182-5_12
Xi, H., et al.: The ATS language, http://www.ats-lang.org/
Zhu, D., Xi, H.: Safe Programming with Pointers through Stateful Views. In: Hermenegildo, M.V., Cabeza, D. (eds.) PADL 2004. LNCS, vol. 3350, pp. 83–97. Springer, Heidelberg (2005)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2014 Springer International Publishing Switzerland
About this paper
Cite this paper
Danish, M., Xi, H. (2014). Using Lightweight Theorem Proving in an Asynchronous Systems Context. In: Badger, J.M., Rozier, K.Y. (eds) NASA Formal Methods. NFM 2014. Lecture Notes in Computer Science, vol 8430. Springer, Cham. https://doi.org/10.1007/978-3-319-06200-6_12
Download citation
DOI: https://doi.org/10.1007/978-3-319-06200-6_12
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-06199-3
Online ISBN: 978-3-319-06200-6
eBook Packages: Computer ScienceComputer Science (R0)