Tech Reports

ULCS-03-024

Temporal Deductive Verification of Cache Coherence Protocols

Michael Fisher and Alexei Lisitsa

Abstract

Firstorder temporal logics (FOTLs) are very expressive formalisms in which we can specify, at a very natural level of abstraction, (almost) any computational system, together with its correctness conditions. This makes FOTLs ideal for formally specifying both software and hardware systems. Unfortunately, the expressiveness of FOTL also means that such logics are typically highly undecidable. Consequently, the fully automated deductive verification of FOTL specifications is not, in general, possible.

Recently, however, a tractable fragment of FOTL was identified by Hodkinson, Wolter and Zakharyashev. This fragement, termed the monodic fragment is amenable to automated proof techniques, and we have developed a number of theorem-proving systems for this fragment. In this paper, we particularly consider the use of such tractable fragments of firstorder temporal logics in the deductive verification of an important class of protocols, namely cache coherence protocols. This is the first use of monodic FOTLs in the deductive verification of reactive systems.

For each technical report listed here, copyright and all intellectual property rights remain with the respective authors. Copyright is effective from the year of publication in each case. By downloading a file from this page, you agree to use it only for purposes of research and scholarship. Any other use of this material or storage of it in any medium or its sale or distribution in any form is expressly forbidden without prior written permission from the authors concerned.