Abstract
Distributed and concurrent object-oriented systems are difficult to analyze due to the complexity of their concurrency, communication, and synchronization mechanisms. The future mechanism extends the traditional method call communication model by facilitating sharing of references to futures. By assigning method call result values to futures, third party objects may pick up these values. This may reduce the time spent waiting for replies in a distributed environment. However, futures add a level of complexity to program analysis, as the program semantics becomes more involved.
This paper presents a model for asynchronously communicating objects, where return values from method calls are handled by futures. The model facilitates invariant specifications over the locally visible communication history of each object. Compositional reasoning is supported, as each object may be specified and verified independently of its environment. A kernel object-oriented language with futures inspired by the ABS modeling language is considered. A compositional proof system for this language is presented, formulated within dynamic logic.
Supported by the EU project FP7-231620 HATS: Highly Adaptable and Trustworthy Software using Formal Models (http://www.hats-project.eu) and COST Action IC0701.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
Preview
Unable to display preview. Download preview PDF.
References
Agha, G., Frølund, S., Kim, W., Panwar, R., Patterson, A., Sturman, D.: Abstraction and modularity mechanisms for concurrent computing. IEEE Parallel Distributed Technology: Systems Applications 1(2), 3–14 (1993)
Ahern, A., Yoshida, N.: Formalising Java RMI with explicit code mobility. Theoretical Computer Science 389(3), 341–410 (2007)
Falkner, K., Coddington, P.D., Oudshoorn, M.J.: Implementing asynchronous remote method invocation in Java. In: Proc. PART 1999 (November 1999)
Morandi, B., Bauer, S.S., Meyer, B.: SCOOP – A Contract-Based Concurrent Object-Oriented Programming Model. In: Müller, P. (ed.) LASER Summer School 2007/2008. LNCS, vol. 6029, pp. 41–90. Springer, Heidelberg (2010)
Ábrahám, E., Grabe, I., Grüner, A., Steffen, M.: Behavioral interface description of an object-oriented language with futures and promises. Journal of Logic and Algebraic Programming 78(7), 491–518 (2009)
Ahrendt, W., Dylla, M.: A system for compositional verification of asynchronous objects. Science of Computer Programming (2010)
Alpern, B., Schneider, F.B.: Defining liveness. IPL 21(4), 181–185 (1985)
Baker Jr., H.G., Hewitt, C.: The incremental garbage collection of processes. In: Proc. 1977 Symposium on Artificial Intelligence and Programming Languages, pp. 55–59. ACM (1977)
Beckert, B., Hähnle, R., Schmitt, P.H. (eds.): Verification of Object-Oriented Software: The KeY Approach. LNCS (LNAI), vol. 4334. Springer, Heidelberg (2007)
Broy, M., Stølen, K.: Specification and Development of Interactive Systems. Monographs in Computer Science. Springer (2001)
Clavel, M., Durán, F., Eker, S., Lincoln, P., Martí-Oliet, N., Meseguer, J., Talcott, C.: All About Maude - A High-Performance Logical Framework. LNCS, vol. 4350. Springer, Heidelberg (2007)
Dahl, O.-J.: Can program proving be made practical?. In: Les Fondements de la Programmation. Institut de Recherche d’Informatique et d’Automatique, Toulouse, France, pp. 57–114 (1977)
Dahl, O.-J.: Object-oriented specifications. In: Research Directions in Object-Oriented Programming, pp. 561–576. MIT Press, Cambridge (1987)
Dahl, O.-J.: Verifiable Programming. International Series in Computer Science. Prentice Hall (1992)
Dahl, O.-J., Owe, O.: Formal methods and the RM-ODP. Research Report 261, Dept. of Informatics, University of Oslo, Norway (1998)
de Boer, F.S., Clarke, D., Johnsen, E.B.: A Complete Guide to the Future. In: De Nicola, R. (ed.) ESOP 2007. LNCS, vol. 4421, pp. 316–330. Springer, Heidelberg (2007)
Din, C.C., Dovland, J., Johnsen, E.B., Owe, O.: Observable behavior of distributed systems: Component reasoning for concurrent objects. Journal of Logic and Algebraic Programming 81(3), 227–256 (2012)
Din, C.C., Dovland, J., Owe, O.: An approach to compositional reasoning about concurrent objects and futures. Research Report 415, Dept. of Informatics, University of Oslo (2012), http://folk.uio.no/crystald/rr415.pdf
Dovland, J., Johnsen, E.B., Owe, O.: Verification of concurrent objects with asynchronous method calls. In: Proc. SwSTE 2005, pp. 141–150. IEEE Press (2005)
Halstead Jr., R.H.: Multilisp: a language for concurrent symbolic computation. ACM Trans. Program. Lang. Syst. 7(4), 501–538 (1985)
Full ABS Modeling Framework, Deliverable 1.2 of project FP7-231620 (HATS) (March 2011), http://www.hats-project.eu
Hoare, C.A.R.: Communicating Sequential Processes. International Series in Computer Science. Prentice Hall (1985)
International Telecommunication Union. Open Distributed Processing - Reference Model parts 1–4. Technical report, ISO/IEC, Geneva (1995)
Jeffrey, A., Rathke, J.: Java JR: Fully Abstract Trace Semantics for a Core Java Language. In: Sagiv, M. (ed.) ESOP 2005. LNCS, vol. 3444, pp. 423–438. Springer, Heidelberg (2005)
Johnsen, E.B., Owe, O.: Object-Oriented Specification and Open Distributed Systems. In: Owe, O., Krogdahl, S., Lyche, T. (eds.) From OO to FM (Dahl Festschrift). LNCS, vol. 2635, pp. 137–164. Springer, Heidelberg (2004)
Johnsen, E.B., Owe, O.: An asynchronous communication model for distributed concurrent objects. Software and Systems Modeling 6(1), 35–58 (2007)
Liskov, B.H., Shrira, L.: Promises: Linguistic support for efficient asynchronous procedure calls in distributed systems. In: Proc. PLDI 1988. ACM Press (1988)
Meseguer, J.: Conditional rewriting logic as a unified model of concurrency. Theoretical Computer Science 96, 73–155 (1992)
Soundararajan, N.: Axiomatic semantics of communicating sequential processes. ACM TOPLAS 6(4), 647–662 (1984)
Soundararajan, N.: A proof technique for parallel programs. Theoretical Computer Science 31(1-2), 13–29 (1984)
Yonezawa, A., Briot, J.-P., Shibayama, E.: Object-oriented concurrent programming in ABCL/1. In: Proc. OOPSLA 1986. Sigplan Notices, vol. 21(11), pp. 258–268 (1986)
Author information
Authors and Affiliations
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2012 Springer-Verlag Berlin Heidelberg
About this paper
Cite this paper
Din, C.C., Dovland, J., Owe, O. (2012). Compositional Reasoning about Shared Futures. In: Eleftherakis, G., Hinchey, M., Holcombe, M. (eds) Software Engineering and Formal Methods. SEFM 2012. Lecture Notes in Computer Science, vol 7504. Springer, Berlin, Heidelberg. https://doi.org/10.1007/978-3-642-33826-7_7
Download citation
DOI: https://doi.org/10.1007/978-3-642-33826-7_7
Publisher Name: Springer, Berlin, Heidelberg
Print ISBN: 978-3-642-33825-0
Online ISBN: 978-3-642-33826-7
eBook Packages: Computer ScienceComputer Science (R0)