zbMATH — the first resource for mathematics

Virtually timed ambients: a calculus of nested virtualization. (English) Zbl 1381.68205
Summary: Nested virtualization enables a virtual machine, which is a software layer representing an execution environment, to be placed inside another virtual machine. Nested virtual machines form a location hierarchy where virtual machines at every level in the hierarchy compete with other processes at that level for processing time. With nested virtualization, the computing power of a virtual machine depends on its position in this hierarchy and may change if the virtual machine moves. This paper introduces the calculus of virtually timed ambients, a formal model of hierarchical locations for execution with explicit resource provisioning, motivated by these effects of nested virtualization. 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. Simulation with time relaxation is defined to express that a system is slower than another system up to a given time bound. The calculus of virtually timed ambients is illustrated by examples.

68Q85 Models and methods for concurrent and distributed computing (process algebras, bisimulation, transition nets, etc.)
PDF BibTeX Cite
Full Text: DOI
[1] Aman, B.; Ciobanu, G., Mobile ambients with timers and types, (Jones, C. B.; Liu, Z.; Woodcock, J., Proc. 4th International Colloquium on Theoretical Aspects of Computing, ICTAC’07, Lecture Notes in Computer Science, vol. 4711, (2007), Springer), 50-63 · Zbl 1147.68586
[2] Aman, B.; Ciobanu, G., Timers and proximities for mobile ambients, (Diekert, V.; Volkov, M. V.; Voronkov, A., Proc. 2nd International Symposium on Computer Science in Russia, CSR’07, Lecture Notes in Computer Science, vol. 4649, (2007), Springer), 33-43 · Zbl 1188.68202
[3] Baeten, J. C.M.; Bergstra, J. A., Real time process algebra, (1990), Centrum voor Wiskunde en Informatica (CWI), Technical Report CS-R 9053 · Zbl 0719.68020
[4] Baeten, J. C.M.; Middelburg, C. A., Process algebra with timing, Monographs in Computer Science, An EATSC Series, (2002), Springer · Zbl 1021.68063
[5] 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, (Proc. 9th USENIX Symposium on Operating Systems Design and Implementation, OSDI 2010, (2010), USENIX Association), 423-436
[6] Berger, M., Towards abstractions for distributed systems, (Nov. 2004), University of London, Imperial College, PhD Thesis
[7] Bidinger, P.; Stefani, J., The kell calculus: operational semantics and type system, (Najm, E.; Nestmann, U.; Stevens, P., Proc. 6th International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS 2003, Lecture Notes in Computer Science, vol. 2884, (2003), Springer), 109-123 · Zbl 1253.68235
[8] Bračevac, O.; Erdweg, S.; Salvaneschi, G.; Mezini, M., CPL: a core language for cloud computing, (Proc. 15th International Conference on Modularity, MODULARITY 2016, (2016), ACM), 94-105
[9] Cardelli, L.; Gordon, A. D., Mobile ambients, (Nivat, M., Proceedings of FoSSaCS ’98, Lecture Notes in Computer Science, vol. 1378, (1998), Springer), 140-155
[10] Cardelli, L.; Gordon, A. D., Equational properties of mobile ambients, Math. Struct. Comput. Sci., 13, 3, 371-408, (2003) · Zbl 1085.68099
[11] Cavaliere, M.; Sburlan, D., Time-independent P systems, (Mauri, G.; Paun, G.; Pérez-Jiménez, M. J.; Rozenberg, G.; Salomaa, A., Proc. 5th International Workshop on Membrane Computing, WMC’04, Lecture Notes in Computer Science, vol. 3365, (2004), Springer), 239-258 · Zbl 1117.68355
[12] Choe, Y.; Lee, M., δ-calculus: process algebra to model secure movements of distributed mobile processes in real-time business applications, (23rd European Conference on Information Systems, ECIS 2015, Münster, Germany, May 26-29, 2015, (2015))
[13] Ciobanu, G., Interaction in time and space, Electron. Notes Theor. Comput. Sci., 203, 3, 5-18, (May 2008)
[14] Ciobanu, G.; Prisacariu, C., Timers for distributed systems, Electron. Notes Theor. Comput. Sci., 164, 3, 81-99, (2006)
[15] Fournet, C.; Gonthier, G., A hierarchy of equivalences for asynchronous calculi, J. Log. Algebraic Program., 63, 1, 131-173, (2005) · Zbl 1066.68088
[16] Goldberg, R. P., Survey of virtual machine research, IEEE Comput., 7, 6, 34-45, (1974)
[17] Hennessy, M.; Regan, T., A process algebra for timed systems, Inf. Comput., 117, 2, 221-239, (1995) · Zbl 0826.68068
[18] Honda, K.; Yoshida, N., Replication in concurrent combinators, (Hagiya, M.; Mitchell, J. C., TACS, Lecture Notes in Computer Science, vol. 789, (1994), Springer), 786-805 · Zbl 0942.03510
[19] Honda, K.; Yoshida, N., On reduction-based process semantics, Theor. Comput. Sci., 151, 2, 437-486, (1995) · Zbl 0871.68122
[20] 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) · Zbl 1304.68029
[21] Johnsen, E. B.; Steffen, M.; Stumpf, J. B., A calculus of virtually timed ambients, (Phillip, James; Roggenbach, Markus, Postproceedings of the 23rd International Workshop on Algebraic Development Techniques, WADT 2016, Lecture Notes in Computer Science, vol. 10644, (2017), Springer Verlag), in press
[22] Lee, I.; Philippou, A.; Sokolsky, O., Resources in process algebra, J. Log. Algebraic Program., 72, 1, 98-122, (2007) · Zbl 1121.68081
[23] Lüttgen, G.; Vogler, W., Bisimulation on speed: worst-case efficiency, Inf. Comput., 191, 2, 105-144, (June 2004)
[24] Merro, M.; Hennessy, M., A bisimulation-based semantic theory of safe ambients, ACM Trans. Program. Lang. Syst., 28, 2, 290-330, (2006)
[25] Merro, M.; Zappa Nardelli, F., Behavioral theory for mobile ambients, J. ACM, 52, 6, 961-1023, (Nov. 2005)
[26] Milner, R., The polyadic pi-calculus: A tutorial, (1991), Technical Report, Logic and Algebra of Specification
[27] Milner, R.; Sangiorgi, D., Barbed bisimulation, (Kuich, W., Proceedings of ICALP ’92, Lecture Notes in Computer Science, vol. 623, (1992), Springer), 685-695
[28] Moller, F.; Tofts, C., A temporal calculus of communicating systems, (Baeten, J. C.M.; Klop, J. W., Proc. 1st International Conference on Concurrency Theory, CONCUR’90, Lecture Notes in Computer Science, vol. 458, (1990), Springer), 401-415
[29] Mousavi, M. R.; Reniers, M. A.; Basten, T.; Chaudron, M. R.V., PARS: a process algebraic approach to resources and schedulers, (Alexander, M.; Gardner, W., Process Algebra for Parallel and Distributed Processing, (2008), Chapman and Hall/CRC)
[30] Murakami, M., Congruent bisimulation equivalence of ambient calculus based on contextual transition system, (Proc. 7th International Symposium on Theoretical Aspects of Software Engineering, TASE 2013, (2013), IEEE Computer Society), 149-152
[31] Nicollin, X.; Sifakis, J., The algebra of timed processes, ATP: theory and application, Inf. Comput., 114, 1, 131-178, (1994) · Zbl 0811.68093
[32] Paun, G.; Rozenberg, G.; Salomaa, A., The Oxford handbook of membrane computing, (2010), Oxford University Press · Zbl 1237.68001
[33] Sangiorgi, D., Introduction to bisimulation and coinduction, (2012), Cambridge University Press · Zbl 1252.68008
[34] Sangiorgi, D.; Walker, D., The pi-calculus: A theory of mobile processes, (2001), Cambridge University Press · Zbl 0981.68116
[35] Satoh, I.; Tokoro, M., A timed calculus for distributed objects with clocks, (Nierstrasz, O. M., Proc. 7th European Conference on Object-Oriented Programming, ECOOP’93, (1993), Springer), 326-345
[36] Vigliotti, M.; Phillips, I., Barbs and congruences for safe mobile ambients, Electron. Notes Theor. Comput. Sci., 66, 3, 37-51, (2007)
[37] Williams, D.; Jamjoom, H.; Weatherspoon, H., The xen-blanket: virtualize once, run everywhere, (Proc. 7th European Conference on Computer Systems, EuroSys’12, (2012), ACM), 113-126
This reference list is based on information provided by the publisher or from digital mathematics libraries. Its items are heuristically matched to zbMATH identifiers and may contain data conversion errors. It attempts to reflect the references listed in the original paper as accurately as possible without claiming the completeness or perfect precision of the matching.