Department of Computer Sciences

1999 ACL2 Workshop

March 29 - March 31, 1999

Single-Threaded Objects

To support efficient execution of certain kinds of models, especially models of microprocessors, ACL2 provides ``single-threaded 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.

Slides (use "Landscape" when in ghostview)

J Moore

Last updated March 1999
Computer Sciences Department
University of Texas at Austin