Article

Single-Threaded Objects in ACL2

Authors:

Robert S. Boyer,

J. Strother MooreAuthors Info & Claims

PADL '02: Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages

Pages 9 - 27

Published: 19 January 2002 Publication History

Abstract

ACL2 is a first-order applicative programming language based on Common Lisp. It is also a mathematical logic for which a mechanical theorem-prover has been implemented in the style of the Boyer-Moore theorem prover. The ACL2 system is used primarily in the modeling and verification of computer hardware and software, where the executability of the language allows models to be used as prototype designs or "simulators." To support efficient execution of certain kinds of models, especially models of microprocessors, ACL2 provides "singlethreaded objects," structures with the usual "copy on write" applicative semantics but for which writes are implemented destructively. Syntactic restrictions insure consistency between the formal semantics and the implementation. The design of single-threaded objects has been influenced both by the need to make execution efficient and the need to make proofs about them simple. We discuss the issues.

References

[1]

E. Barendsen and S. Smetsers. Uniqueness typing for functional languages with graph rewriting semantics. In Mathematical Structures in Computer Science 6 , pages 579-612. 1996.

[2]

R. S. Boyer and J S. Moore. A Computational Logic . Academic Press, New York, 1979.

[3]

R. S. Boyer and J S. Moore. A Computational Logic Handbook, Second Edition . Academic Press, New York, 1997.

[4]

J.-Y. Girard. Linear logic. In Theoretical Computer Science , volume 50, pages 1-102. 1987.

[5]

D. Greve, M. Wilding, and D. Hardin. High-speed, analyzable simulators. In Kaufmann et al. {9}, pages 113-136.

[6]

David A. Greve. Symbolic simulation of the JEM1 microprocessor. In G. Gopalakrishnan and P. Windley, editors, Formal Methods in Computer-Aided Design - FM-CAD , LNCS 1522. Springer-Verlag, 1998.

[7]

David Hardin, Matthew Wilding, and David Greve. Transforming the theorem prover into a digital design tool: From concept car to off-road vehicle. In Alan J. Hu and Moshe Y. Vardi, editors, Computer-Aided Verification - CAV '98 , volume 1427 of Lecture Notes in Computer Science . Springer-Verlag, 1998. See URL http://pobox.com/users/hokie/docs/concept.ps.

[8]

P. Hudak. Continuation-based mutable abstract data types, or how to have your state and munge it too. Technical Report YaleU/DCS/RR-914, Department of Computer Science, Yale University, July 1992.

[9]

M. Kaufmann, P. Manolios, and J S. Moore, editors. Computer-Aided Reasoning: ACL2 Case Studies . Kluwer Academic Press, 2000.

[10]

M. Kaufmann, P. Manolios, and J. S. Moore. Computer-Aided Reasoning: An Approach . Kluwer Academic Press, 2000.

[11]

Matt Kaufmann and J. Moore. A precise description of the acl2 logic. In http://www.cs.utexas.edu/users/moore/publications/km97a.ps.Z. Department of Computer Sciences, University of Texas at Austin, 1997.

[12]

J. S. Moore. Rewriting for symbolic execution of state machine models. In Computer-Aided Verification - CAV'01 , volume 2102 of Lecture Notes in Computer Science . Springer-Verlag, 2001. See URL http://www.cs.utexas.edu/users/moore/publications/nu-rewriter.

[13]

G. Plotkin. Call-by-name, call-by-value, and the ¿-calculus. In Theoretical Computer Science , volume 1, pages 125-159. 1975.

[14]

D. Schmidt. Detecting global variables in denotational specifications. ACM Trans. Prog. Lang , 7:299-310, 1985.

[15]

G. L. Steele, Jr. Common Lisp The Language, Second Edition . Digital Press, 30 North Avenue, Burlington, MA 01803, 1990.

[16]

W. Stoye. Message-based functional operating systems. 6(3):291-311, 1986.

[17]

P. Wadler. Monads for functional programming. In Advanced Functional Programming . Springer Verlag, LNCS 925, 1995.

[18]

P. Wadler. How to declare an imperative. ACM Computing Surveys , 29(3):240-263, September 1997.

Cited By

Goel SHunt W(2013)Automated Code Proofs on a Formal Model of the X86Revised Selected Papers of the 5th International Conference on Verified Software: Theories, Tools, Experiments - Volume 816410.1007/978-3-642-54108-7_12(222-241)Online publication date: 17-May-2013
https://dl.acm.org/doi/10.1007/978-3-642-54108-7_12
Hardin DHardin SRay SRussinoff D(2009)Efficient, formally verifiable data structures using ACL2 single-threaded objects for high-assurance systemsProceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications10.1145/1637837.1637853(100-105)Online publication date: 11-May-2009
https://dl.acm.org/doi/10.1145/1637837.1637853
Hardin D(2008)Considerations in the design and verification of microprocessors for safety-critical and security-critical applicationsProceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design10.5555/1517424.1517425(1-8)Online publication date: 17-Nov-2008
https://dl.acm.org/doi/10.5555/1517424.1517425
Show More Cited By

Single-Threaded Objects in ACL2
1. Theory of computation

Recommendations

An Integration of HOL and ACL2
FMCAD '06: Proceedings of the Formal Methods in Computer Aided Design

A link between the ACL2 and HOL4 proof assistants is described. This allows each system to be deployed smoothly within a single formal development. Several applications are being considered: using ACL2's execution environment for simulating HOL models; ...
An embedding of the ACL2 logic in HOL
ACL2 '06: Proceedings of the sixth international workshop on the ACL2 theorem prover and its applications

We describe an embedding of the ACL2 logic into higher-order logic. An implementation of this embedding allows ACL2 to be used as an oracle for higher-order logic provers.
A Formalization of Powerlist Algebra in ACL2

In Misra (ACM Trans Program Lang Syst 16(6):1737---1767, 1994), Misra introduced the powerlist data structure, which is well suited to express recursive, data-parallel algorithms. Moreover, Misra and other researchers have shown how powerlists can be ...

Comments

Please enable JavaScript to view thecomments powered by Disqus.

Information & Contributors

Information

Published In

cover image Guide Proceedings

PADL '02: Proceedings of the 4th International Symposium on Practical Aspects of Declarative Languages

January 2002

350 pages

ISBN:354043092X

Publisher

Springer-Verlag

Berlin, Heidelberg

Publication History

Published: 19 January 2002

Qualifiers

Article

Contributors

Other Metrics

View Article Metrics

Bibliometrics & Citations

Bibliometrics

Article Metrics

7
Total Citations
View Citations
0
Total Downloads

Downloads (Last 12 months)0
Downloads (Last 6 weeks)0

Reflects downloads up to 12 Nov 2024

Other Metrics

View Author Metrics

Citations

Cited By

Goel SHunt W(2013)Automated Code Proofs on a Formal Model of the X86Revised Selected Papers of the 5th International Conference on Verified Software: Theories, Tools, Experiments - Volume 816410.1007/978-3-642-54108-7_12(222-241)Online publication date: 17-May-2013
https://dl.acm.org/doi/10.1007/978-3-642-54108-7_12
Hardin DHardin SRay SRussinoff D(2009)Efficient, formally verifiable data structures using ACL2 single-threaded objects for high-assurance systemsProceedings of the Eighth International Workshop on the ACL2 Theorem Prover and its Applications10.1145/1637837.1637853(100-105)Online publication date: 11-May-2009
https://dl.acm.org/doi/10.1145/1637837.1637853
Hardin D(2008)Considerations in the design and verification of microprocessors for safety-critical and security-critical applicationsProceedings of the 2008 International Conference on Formal Methods in Computer-Aided Design10.5555/1517424.1517425(1-8)Online publication date: 17-Nov-2008
https://dl.acm.org/doi/10.5555/1517424.1517425
Théry LHanrot G(2007)Primality proving with elliptic curvesProceedings of the 20th international conference on Theorem proving in higher order logics10.5555/1792233.1792257(319-333)Online publication date: 10-Sep-2007
https://dl.acm.org/doi/10.5555/1792233.1792257
Moore JZhang Q(2005)Proof pearlProceedings of the 18th international conference on Theorem Proving in Higher Order Logics10.1007/11541868_24(373-384)Online publication date: 22-Aug-2005
https://dl.acm.org/doi/10.1007/11541868_24
Moore J(2002)Functional formal methodsACM SIGPLAN Notices10.1145/583852.58149037:9(123-123)Online publication date: 17-Sep-2002
https://dl.acm.org/doi/10.1145/583852.581490
Moore JWand MPeyton Jones S(2002)Functional formal methodsProceedings of the seventh ACM SIGPLAN international conference on Functional programming10.1145/581478.581490(123-123)Online publication date: 4-Oct-2002
https://dl.acm.org/doi/10.1145/581478.581490

View Options

View options

Get Access

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

Media

Figures

Other

Tables

View Table of Contents