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.
This is a preview of subscription content, log in via an institution.
Buying options
Tax calculation will be finalised at checkout
Purchases are for personal use only
Learn about institutional subscriptionsReferences
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