Abstract
A virtual machine, which is a software layer representing an execution environment, can be placed inside another virtual machine. As virtual machines at every level in a location hierarchy compete with other processes for processing time, the computing power of a virtual machine depends on its position in this hierarchy and may change if the virtual machine moves. These effects of nested virtualization motivate the calculus of virtually timed ambients, a formal model of hierarchical locations for execution with explicit resource provisioning, introduced in this paper. Resource provisioning in this model is based on virtual time slices as a local resource. To reason about timed behavior in this setting, weak timed bisimulation for virtually timed ambients is defined as an extension of bisimulation for mobile ambients. We show that the equivalence of contextual bisimulation and reduction barbed congruence is preserved by weak timed bisimulation. The calculus of virtually timed ambients is illustrated by examples.
This is a preview of subscription content, log in via an institution to check access.
Access this chapter
Tax calculation will be finalised at checkout
Purchases are for personal use only
References
Aman, B., Ciobanu, G.: Mobile ambients with timers and types. In: Jones, C.B., Liu, Z., Woodcock, J. (eds.) ICTAC 2007. LNCS, vol. 4711, pp. 50–63. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-75292-9_4
Aman, B., Ciobanu, G.: Timers and proximities for mobile ambients. In: Diekert, V., Volkov, M.V., Voronkov, A. (eds.) CSR 2007. LNCS, vol. 4649, pp. 33–43. Springer, Heidelberg (2007). https://doi.org/10.1007/978-3-540-74510-5_7
Baeten, J.C.M., Bergstra, J.A.: Real time process algebra. Technical report CS-R 9053, Centrum voor Wiskunde en Informatica (CWI) (1990)
Baeten, J.C.M., Middelburg, C.A.: Process Algebra with Timing. Monographs in Computer Science. An EATSC series. Springer, Heidelberg (2002). https://doi.org/10.1007/978-3-662-04995-2
Ben-Yehuda, M., Day, M.D., Dubitzky, Z., Factor, M., Har’El, N., Gordon, A., Liguori, A., Wasserman, O., Yassour, B.: The turtles project: design and implementation of nested virtualization. In: Proceedings of the 9th Symposium on Operating Systems Design and Implementation (OSDI 2010), pp. 423–436. USENIX (2010)
Berger, M.: Towards abstractions for distributed systems. Ph.D. thesis, University of London, Imperial College, November 2004
Bračevac, O., Erdweg, S., Salvaneschi, G., Mezini, M.: CPL: a core language for cloud computing. In: Proceedings of the 15th International Conference on Modularity, pp. 94–105. ACM (2016)
Cardelli, L., Gordon, A.D.: Mobile ambients. Theoret. Comput. Sci. 240(1), 177–213 (2000)
Cardelli, L., Gordon, A.D.: Equational properties of mobile ambients. Math. Struct. Comput. Sci. 13(3), 371–408 (2003)
Ciobanu, G.: Interaction in time and space. ENTSC 203(3), 5–18 (2008)
Fournet, C., Gonthier, G.: A hierarchy of equivalences for asynchronous calculi. J. Logic Algebraic Program. 63(1), 131–173 (2005)
Goldberg, R.P.: Survey of virtual machine research. IEEE Comput. 7(6), 34–45 (1974)
Hennessy, M., Regan, T.: A process algebra for timed systems. Inf. Comput. 117(2), 221–239 (1995)
Honda, K., Yoshida, N.: On reduction-based process semantics. Theoret. Comput. Sci. 151(2), 437–486 (1995)
Johnsen, E.B., Schlatte, R., Tapia Tarifa, S.L.: Integrating deployment architectures and resource consumption in timed object-oriented models. J. Log. Algebraic Methods Program. 84(1), 67–91 (2015)
Lee, I., Philippou, A., Sokolsky, O.: Resources in process algebra. J. Log. Algebraic Programming 72(1), 98–122 (2007)
Merro, M., Hennessy, M.: A bisimulation-based semantic theory of safe ambients. ACM Trans. Program. Lang. Syst. 28(2), 290–330 (2006)
Merro, M., Zappa Nardelli, F.: Behavioral theory for mobile ambients. J. ACM 52(6), 961–1023 (2005)
Moller, F., Tofts, C.: A temporal calculus of communicating systems. In: Baeten, J.C.M., Klop, J.W. (eds.) CONCUR 1990. LNCS, vol. 458, pp. 401–415. Springer, Heidelberg (1990). https://doi.org/10.1007/BFb0039073
Mousavi, M.R., Reniers, M.A., Basten, T., Chaudron, M.R.V.: PARS: a process algebraic approach to resources and schedulers. In: Process Algebra for Parallel and Distributed Processing. Chapman and Hall/CRC (2008)
Murakami, M.: Congruent bisimulation equivalence of ambient calculus based on contextual transition system. In: Proceedings of the 7th International Symposium on Theoretical Aspects of Software Engineering (TASE 2013), pp. 149–152. IEEE Computer Society (2013)
Nicollin, X., Sifakis, J.: The algebra of timed processes, ATP: theory and application. Inf. Comput. 114(1), 131–178 (1994)
Sangiorgi, D., Walker, D.: The Pi-Calculus: A Theory of Mobile Processes. Cambridge University Press, Cambridge (2001)
Satoh, I., Tokoro, M.: A timed calculus for distributed objects with clocks. In: Nierstrasz, O.M. (ed.) ECOOP 1993. LNCS, vol. 707, pp. 326–345. Springer, Heidelberg (1993). https://doi.org/10.1007/3-540-47910-4_17
Vigliotti, M., Phillips, I.: Barbs and congruences for safe mobile ambients. ENTCS 66(3), 37–51 (2007)
Williams, D., Jamjoom, H., Weatherspoon, H.: The Xen-Blanket: virtualize once, run everywhere. In: Proceedings of the 7th European Conference on Computer Systems (EuroSys 2012), pp. 113–126. ACM (2012)
Author information
Authors and Affiliations
Corresponding author
Editor information
Editors and Affiliations
Rights and permissions
Copyright information
© 2017 IFIP International Federation for Information Processing
About this paper
Cite this paper
Johnsen, E.B., Steffen, M., Stumpf, J.B. (2017). A Calculus of Virtually Timed Ambients. In: James, P., Roggenbach, M. (eds) Recent Trends in Algebraic Development Techniques. WADT 2016. Lecture Notes in Computer Science(), vol 10644. Springer, Cham. https://doi.org/10.1007/978-3-319-72044-9_7
Download citation
DOI: https://doi.org/10.1007/978-3-319-72044-9_7
Published:
Publisher Name: Springer, Cham
Print ISBN: 978-3-319-72043-2
Online ISBN: 978-3-319-72044-9
eBook Packages: Computer ScienceComputer Science (R0)
