Abstract
In this paper we propose a methodology for verifying the sequential consistency of caching algorithms. The scheme combines times-tamping and an auxiliary history table to construct a serial execution ‘matching’ any given execution of the algorithm. We believe that this approach is applicable to an interesting class of sequentially consistent algorithms in which the buffering of cache updates allows stale values to be read from cache. We illustrate this methodology by verifying the high level specifications of the lazy caching and ring algorithms.
Chapter PDF
Similar content being viewed by others
Keywords
These keywords were added by machine and not by the authors. This process is experimental and the keywords may be updated as the learning algorithm improves.
References
S. V. Adve and K. Gharachorloo. Shared memory consistency models: A tutorial. Technical Report 9512, Rice University, 1995.
Y. Afek, G. Brown, and M. Merrit. Lazy caching. ACM Transactions on Programming Languages and Systems, 15(1):182–205, 1993.
R. Alur, K. L. McMillan, and D. Peled. Model checking of correctness conditions for concurrent objects. In MICS’96:219–228, 1996.
T. Arons. Homepage. http://www.wisdom.weizmann.ac.il/~tamarah/caching/.
E. Brinksma. Cache consistency by design. Dist. Comp., 12:61–74, 1999.
W. W. Collier. Reasoning about Parallel Architectures. Prentice Hall, 1992.
A. E. Condon, M. D. Hill, M. Plakal, and D. J. Sorin. Lamport clocks: Reasoning about shared-memory correctness. Technical Report CS-TR-1367, University of Wisconsin, Madison, 1998.
A. E. Condon, M. D. Hill, M. Plakal, and D. J. Sorin. Lamport clocks: Verifying a directory cache-coherence protocol. In Proc. 10th ACM Symp. Parallel Algorithms and Architectures (SPAA), 1998.
J. Davies and G. Lowe. Using CSP to verify sequential consistency. Dist. Comp., 12:91–103, 1999.
G. Delzanno. Automatic verification of parametrized cache coherence protocols. CAV’00:53–68, 2000.
D. L. Dill and S. Park. Verification of FLASH cache coherence protocol by aggregation of distributed transactions. In SPAA’96:288–296, 1996.
D. L. Dill and S. Park. Verification of cache coherence protocols by aggregation of distributed transactions. In Theory of Computing Systems. 1998.
Distributed Computing, Volume 12Number 2/3, 1999.
M. Dubois and F. Pong. Verification techniques for cache coherence protocols. ACM Computing Surveys, 29(1):82–126, 1997.
R. Gerth. Sequential consistency and the lazy caching algorithm. Dist. Comp., 12:57–59, 1999.
S. Graf. Characterization of a sequentially consistent memory and verification of a cache memory by abstraction. Dist. Comp., 12:75–90, 1999.
R. Ghughal, G. Gopalakrishnan, A. Mokkedem, and R. Nalumasu. The ‘test model-checking’ approach to the verification of formal memory models of multiprocessors. CAV’98:376–464, 1998.
M. Glusman and S. Katz. Mechanizing proofs of computation equivalence. CAV’99:354–367, 1999.
T. Henzinger, S. Qadeer, and S. K. Rajamani. Verifying sequential consistency on shared-memory multiprocessor systems. CAV’99:301–315, 1999.
W. Janssen, M. Poel, and J. Zwiers. The compositional approach to sequential consistency and lazy caching. Dist. Comp., 12:105–127, 1999.
R. Jonsson, A. Pnueli, and C. Rump. Proving refinement using transduction. Dist. Comp., 12:129–149, 1999.
P. Ladkin, L. Lamport, B. Olivier, and D. Roegel. Lazy caching in TLA. Dist. Comp., 12:151–174, 1999.
L. Lamport. Time, clocks and the ordering of events. Communications of the ACM, 21(7):558–565, 1978.
L. Lamport. How to make a multiprocessor computer that correctly executes multiprocess programs. IEEE Transactions on Computers, C-82(9):690–691, 1979.
L. Lamport. The temporal logic of actions. ACM Trans. Prog. Lang. Sys., 16(3):872–923, May 1994.
R. S. Lazic. A Sematic Study of Data Independed with Appliations to Model Checking. PhD thesis, Oxford University Computing Laboratory, 1999.
S. Owre, J. M. Rushby, N. Shankar, and M. K. Srivas. A tutorial on using PVS for hardware verification. TPCD’94:258–279, 1994.
J. Stoy, X. Shen, and Arvind. Proofs of correctness of cache-coherence protocols. In Formal Methods Europe, FME’01, Springer-Verlag, 2001.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2001 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Arons, T. (2001). Using Timestamping and History Variables to Verify Sequential Consistency. In: Berry, G., Comon, H., Finkel, A. (eds) Computer Aided Verification. CAV 2001. Lecture Notes in Computer Science, vol 2102. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-44585-4_42
Download citation
DOI: https://doi.org/10.1007/3-540-44585-4_42
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-42345-4
Online ISBN: 978-3-540-44585-2
eBook Packages: Springer Book Archive