A Mechanically Checked Proof of a
Multiprocessor Result via a Uniprocessor View, J Moore, February, 1998.
This paper presents an ACL2 proof that an n-processor concurrent system
implements a non-blocking counter. This paper illustrates one method for
dealing with concurrency and nondeterminism in ACL2, by formalizing a
compositional semantics for a shared-memory concurrent system. ( ACL2 script).
An ACL2 Proof of Write Invalidate Cache
Coherence, J Moore, in A. J. Hu and M. Y. Vardi (eds.) Computer Aided
Verification: 10th International Conference, CAV '98, Springer-Verlag
LNCS 1427, pp. 29-38, 1998. This paper presents a pedagogical example of
the use of ACL2. An extremely simple cache coherence property is formalized
and proved. The intended contribution of the paper is not in the realm of
cache coherence -- the problem dealt with here is far too simple for that --
but in demonstrating the ACL2 in a simple modeling project and in one
approach to concurrency. (ACL2
Scripts)
Interactive
Consistency in ACL2, Bill Young, Computational Logic, Inc., March,
1997. This paper presents an ACL2 translation of Rushby's PVS improvement
to Bevier and Young's Nqthm formalization of the Pease, Shostak and Lamport
Oral Messages (“Byzantine Generals”) problem.
