Abstract
Sharing between B constructs is limited, both on the specification and the implementation level. The limitations stem from the single writer/multiple readers paradigm, restricted visibility of shared variables, and structural constraints to prevent interference. As a consequence, applications with inherent sharing requirements have to either be described as large monolithic constructs or be underspecified, leading to a loss of modularity respectively certain desirable properties being unprovable.
We propose a new compositional symmetric shared access mechanism based on roles describing rely/guarantee conditions. The mechanism provides for multiple writers on shared constructs, visibility of shared variables in the accessors’ invariants, and controlled aliasing. Use is uniform in machines, refinements, and implementations. Sharing is compositional: all proof obligations are local and do not require knowledge of the other accessors’ specifications, let alone their or the shared construct’s implementation.
Soundness of the mechanism is established by flattening.
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
Martìn Abadi and Leslie Lamport. Conjoining specifications. ACM Transactions on Programming Languages and Systems, 17(3):507–534, 1995.
J. R. Abrial. The B Book: Assigning Programs to Meanings. Cambridge University Press, 1996.
R. Back and J. von Wright. Trace refinement of action systems. In CONCUR 94, pages 367–384. LNCS 836, Springer Verlag, 1994.
J. A. Bergstra, J. Heering, and P. Klint. Module algebra. Journal of the ACM, 37(2): 335–372, 1990.
Didier Bert, Marie-Laure Potet, and Yann Rouzaud. A study on components and assembly primitives in B. In Proceedings of the first B conference, pages 47–62, 3 rue du Maréchal Joffre, BP 34103, 44041 Nantes Cedex 1, 1996. IRIN Institut de recherche en informatique de Nantes.
Martin Büchi. The B Bank. In Emil Sekerinski and Kaisa Sere, editors, Program Development by Refinement: Case Studies Using the B Method, chapter 4, pages 115–180. Springer Verlag, 1998. http://www.abo.fi/~mbuechi/publications/BBook.html.
Pierre Collette. Application of the composition principle to UNITY-like specifications. In Proceedings of TAPSOFT 93, pages 230–242. LNCS 668, Springer Verlag, 1993.
Willem-Paul de Roever. The quest for compositionality—a survey of assertion-based proof systems for concurrent programs, part I: Concurrency based on shared variables. In F.J. Neuhold and G. Chroust, editors, Proceedings of the IFIP Working Conference “The role of abstract models in computer science”, pages 181–205. North-Holland, 1985.
J.S. Fitzgerald and C. B. Jones. Modularizing the formal description of a database system. In VDM’90: VDM and Z-Formal Methods in Software Development, pages 189–210. LNCS 428, Springer Verlag, 1990.
N. Francez and I. Forman. Interacting Processes: A Multiparty Approach to Coordinated Distributed Programming. ACM Press, 1996.
Nissim Francez and Amir Pnueli. A proof method for cyclic programs. Acta Informatica, 9: 133–157, 1978.
Peter Grønning, Thomas Qvist Nielsen, and Hans Henrik Løvengreen. Refinement and composition of transition-based rely-guarantee specifications with auxiliary variables. In Proceedings of the 10th Conference on Foundations of Software Technology and Theoretical Computer Science, pages 332–348. LNCS 472, Springer Verlag, 1990.
I. J. Hayes and L. P. Wildman. Towards libraries for Z. In J. P. Bowen and J. E. Nicholls, editors, Z User Workshop: Proceedings of the Seventh Annual Z User Meeting, Workshops in Computing. Springer Verlag, 1993.
Richard Helm, Ian M. Holland, and Dipayan Gangopadhyay. Contracts: Specifying behavioral compositions in object-oriented systems. In Proceedings of OOPSLA/ECOOP’ 90, pages 169–180, 1990.
Cliff B. Jones. Specification and design of (parallel) programs. In Proceedings of IFIP’83, pages 321–332. North Holland, 1983.
Cliff B. Jones. Accomodating interference in the formal design of concurrent object-based programs. Formal Methods in System Design, 8(2):105–122, March 1996.
Leslie Lamport. The temporal logic of actions. ACM Transactions of Programming Languages and Systems, 16(3):872–923, 1994.
Kevin Lano. Integrating formal and structured methods in object-oriented system development. In S.J. Goldsack and S.J.H. Kent, editors, Formal Methods and Object Technology. Springer Verlag, 1996.
J. Misra and M. Chandy. Proofs of networks of processes. IEEE Software Engineering, 7(4):417–426, 1981.
S. Owicki and D. Gries. An axiomatic proof technique for parallel programs. Acta Informatica, 6:319–340, 1976.
Marie-Laure Potet and Yann Rouzaud. Composition and refinement in the B-method. In Proceedings of the second B conference, pages 46–65. LNCS 1393, Springer Verlag, 1998.
Emil Sekerinski and Kaisa Sere, editors. Program Develoment by Refinement: Case Studies Using the B Method. FACIT. Springer Verlag, 1998.
Kaisa Sere and Marina Waldén. Data refinement of remote procedures. In Proceedings of TACS 97, pages 267–294. LNCS 1281, Springer Verlag, 1997.
Ketil Stølen. Development of Parallel Programs on Shared Data-Structures. PhD thesis, University of Manchester, 1990. Available as technical report UMCS-91-1-1.
Qiwen Xu. On compositionality in refining concurrent systems. In J. He, J. Cooke, and P. Wallis, editors, Proceedings of the BCS FACS 7th Refinement Workshop. Electronic Workshops in Computing, Springer Verlag, 1996.
Qiwen Xu, Antonio Cau, and Pierre Collette. On unifying assumption-commitment style proof rules for concurrency. In Proceedings of CONCUR 94, pages 267–282. LNCS 836, Springer Verlag, 1994.
Qiwen Xu, Willem-Paul de Roever, and Jifeng He. The rely-guarantee method for verifying shared variable concurrent programs. Formal Aspects of Computing, 9(2):149–174, 1997.
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 1999 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Büchi, M., Back, R. (1999). Compositional Symmetric Sharing in B. In: Wing, J.M., Woodcock, J., Davies, J. (eds) FM’99 — Formal Methods. FM 1999. Lecture Notes in Computer Science, vol 1708. Springer, Berlin, Heidelberg. https://doi.org/10.1007/3-540-48119-2_25
Download citation
DOI: https://doi.org/10.1007/3-540-48119-2_25
Published:
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-540-66587-8
Online ISBN: 978-3-540-48119-5
eBook Packages: Springer Book Archive