Abstract
This paper describes a rely-guarantee proof to show that Simpson’s 4-slot single-reader, single-writer ACM is Lamport atomic (as described fully in the paper). First an abstract ACM specification is proved Lamport atomic using an exhaustive assertional method. A formal model of Simpson’s 4-slot is then given and this has been proved to be a refinement of the abstract specification using Nipkow’s retrieve relation rule. Simpson’s 4-slot is then shown to be Lamport atomic using an interleaved concurrency rely-guarantee proof method for shared variable concurrency.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Similar content being viewed by others
References
Aczel, P.: On an inference rule for parallel composition. Unpublished letter to Cliff Jones (March 1983)
Angerholm, S., Bicarregui, J., Maharaj, S.: On the Verification of VDM Specifications and Refinement with PVS. In: Bicarregui, J.C. (ed.) Proof in VDM: Case Studies. FACIT. Springer, Heidelberg (1998)
Ashcroft, E.A.: Proving assertions about parallel programs. JCSS 10, 110–135 (1975)
Brooke, P., Jacob, J.L., Armstrong, J.M.: Analysis of the FourSlot Mechanism. In: Proceedings of the BCS-FACS Northern Formal Methods Workshop (1996)
Brooke, P.J.: A Timed Semantics for a Hierarchical Design Notation. PhD thesis, Department of Computer Science, University of York (April 1999)
de Roever, W.-P., et al.: Concurrency Verification: Introduction to Compositional and Noncompositional Methods. Cambridge Tracts in Theoretical Computer Science, vol. (54). Cambridge University Press, Cambridge (2001)
Formal Systems (Europe) Ltd. Failures-Divergence Refinement: The FDR 2.0 User Manual (August 1996)
Henderson, N., Paynter, S.E.: The Formal Classification and Verification of Simpson’s 4-Slot Asynchronous Communication Mechanism. In: Eriksson, L.-H., Lindsay, P.A. (eds.) FME 2002. LNCS, vol. 2391, pp. 350–369. Springer, Heidelberg (2002)
Hoare, C.A.R.: Monitors: An Operating System Structuring Concept. Communications of the ACM 17(10), 549–557 (1974)
Jones, C.B.: Development Methods for Computing Programs Including a Notion of Interference. PhD thesis, Oxford University Computing Laboratory (1981)
Jones, C.B.: Specification and Design of (Parallel) Programs. Information Processing Letters 83, 321–331 (1983)
Jones, C.B.: Tentative steps towards a development method for interfering programs. ACM Transactions an Programming Languages and Systems 5(4), 596–619 (1983)
Jones, C.B.: Systematic Software Development Using VDM, 2nd edn. International Series in Computer Science (1990)
Lamport, L.: On Interprocess Communication – Part 1: Basic Formalism. Distributed Computing 1, 77–85 (1986)
Lamport, L.: On Interprocess Communication – Part 2: Algorithms. Distributed Computing 1, 86–101 (1986)
Nipkow, T.: Non-Deterministic Data Types: Models and Implementations. Acta Informatica 22, 629–661 (1986)
Nipkow, T.: Behavioural Implementation Concepts for Nondeterministic Data Types. PhD thesis, University of Manchester (May 1987)
Owre, S., Shanker, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS Language: Version 2.3. Technical report, Computer Science Laboratory – SRI International (September 1999)
Owre, S., Shanker, N., Rushby, J.M., Stringer-Calvert, D.W.J.: PVS System Guide: Version 2.3. Technical report, Computer Science Laboratory – SRI International (September 1999)
Paynter, S.E., Henderson, N., Armstrong, J.M.: Ramifications of metastability in bit variables explored via Simpson’s 4-slot mechanism. Submitted to FACS (January 2003)
Roscoe, A.W.: The Theory and Practice of Concurrency. Prentice Hall Series in Computer Science (1998)
Rushby, J.: Model-Checking Simpson’s Four-Slot Fully Asychronous Communication Mechanism. Technical Report Issued, Computer Science Laboratory – SRI International (July 2002)
Simpson, H.R.: Fully Asynchronous Communication. In: Proceedings of the IEE Colloquium an MASCOT in Real-Time Systems (May 1987)
Simpson, H.R.: Four-Slot Fully Asynchronous Communication Mechanism. IEE Proceedings 137 Part E(1), 17–30 (1990)
Simpson, H.R.: Correctness Analysis for Class of Asynchronous Communication Mechanism. IEE Proceedings 139 Part E(1), 35–49 (1992)
Simpson, H.R.: New Algorithms for Asynchronous Communication. IEE Proceedings of Computer Digital Technology 144(4), 227–231 (1997)
Simpson, H.R.: Role Model Analysis of an Asynchronous Communication Mechanism. IEE Proceedings of Computer Digital Technology 144(4), 232–240 (1997)
Xia, F.: Supporting the MASCOT method with Petri net techniques for real- time systems development. PhD thesis, London University, King’s College (January 2000)
Xia, F., Clark, I.: Complementing the role model method with petri-net techniques in studying issues of data freshness of the four slot mechanism. Technical Report CS-TR-654, Department of Computing Science, University of Newcastle (January 1999)
Xia, F., Yakovlev, A.V., Clark, I.G., Shang, D.: Data communication in systems with heterogeneous timing. IEEE Micro 22(6) (November- December 2002)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2003 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Henderson, N. (2003). Proving the Correctness of Simpson’s 4-Slot ACM Using an Assertional Rely-Guarantee Proof Method. In: Araki, K., Gnesi, S., Mandrioli, D. (eds) FME 2003: Formal Methods. FME 2003. Lecture Notes in Computer Science, vol 2805. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-540-45236-2_15
Download citation
DOI: https://doi.org/10.1007/978-3-540-45236-2_15
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-40828-4
Online ISBN: 978-3-540-45236-2
eBook Packages: Springer Book Archive