Dynamic structural operational semantics.

*(English)*Zbl 1431.68061Summary: We introduce Dynamic Structural Operational Semantics (DSOS or Dynamic SOS) as a framework for describing semantics of programming languages that include dynamic software upgrades, i.e., for upgrading software code during run-time. DSOS is built on top of the Modular SOS of P. Mosses, with an underlying category theory formalization. The idea of Dynamic SOS is to bring out the essential differences between dynamic upgrade constructs and program execution constructs. The important feature of Modular SOS (MSOS) that we exploit in DSOS is the sharp separation of the program execution code from the additional (data) structures needed at run-time. In DSOS we aim to achieve the same modularity and decoupling for dynamic software upgrades. This is partly motivated by the long term goal of having machine-checkable proofs for general results like type safety.

We exemplify Dynamic SOS on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus.

As a side contribution we define a general encapsulating construction on Modular SOS useful in situations where a form of encapsulation of the execution is needed. We use encapsulation to give modular semantics to the concurrent object-oriented programming language Creol with active objects and asynchronous method invocations.

We exemplify Dynamic SOS on two languages supporting dynamic software upgrades, namely the C-like Proteus, which supports updating of variables, functions, records, or types at specific program points, and Creol, which supports dynamic class upgrades in the setting of concurrent objects. Existing type analyses for software upgrades can be done on top of DSOS too, as we illustrate for Proteus.

As a side contribution we define a general encapsulating construction on Modular SOS useful in situations where a form of encapsulation of the execution is needed. We use encapsulation to give modular semantics to the concurrent object-oriented programming language Creol with active objects and asynchronous method invocations.

##### Keywords:

modular structural operational semantics; dynamic software updates; dynamic class upgrades; Proteus; Creol; concurrent objects
PDF
BibTeX
XML
Cite

\textit{C. Johansen} and \textit{O. Owe}, J. Log. Algebr. Methods Program. 107, 79--107 (2019; Zbl 1431.68061)

Full Text:
DOI

##### References:

[1] | Abadi, Martin; Cardelli, Luca, A Theory of Objects, (2012), Springer Science & Business Media · Zbl 0876.68014 |

[2] | Abadi, Martín; Plotkin, Gordon D., A model of cooperative threads, (Shao, Zhong; Pierce, Benjamin C., 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 36th ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL, (2009), ACM), 29-40 · Zbl 1315.68079 |

[3] | Abadi, Martín; Plotkin, Gordon D., A model of cooperative threads, Log. Methods Comput. Sci., 6, 4, (2010) · Zbl 1202.68105 |

[4] | Aceto, Luca; Bloom, Bard; Vaandrager, Frits W., Turning SOS rules into equations, Inf. Comput., 111, 1, 1-52, (1994) · Zbl 0822.68059 |

[5] | Aceto, Luca; Fokkink, Wan J.; Verhoef, Chris, Structural operational semantics, (Bergstra, Jan A.; Ponse, Alban; Smolka, Scott A., Handbook of Process Algebra, (2001), Elsevier), chapter 3 · Zbl 1062.68074 |

[6] | Aceto, Luca; Ingólfsdóttir, Anna; Reza Mousavi, Mohammad; Reniers, Michael A., Algebraic properties for free!, Bull. Eur. Assoc. Theor. Comput. Sci., 99, 81-103, (2009) · Zbl 1188.68200 |

[7] | Agha, Gul; Mason, Ian A.; Smith, Scott F.; Talcott, Carolyn L., A foundation for actor computation, J. Funct. Program., 7, 1, 1-72, (1997) · Zbl 0870.68091 |

[8] | Ajmani, Sameer; Liskov, Barbara; Shrira, Liuba, Modular software upgrades for distributed systems, (Dave, Thomas, 20th European Conference on Object-Oriented Programming. 20th European Conference on Object-Oriented Programming, ECOOP. 20th European Conference on Object-Oriented Programming. 20th European Conference on Object-Oriented Programming, ECOOP, Lecture Notes in Computer Science, vol. 4067, (2006), Springer), 452-476 |

[9] | Armstrong, Joe, Programming Erlang: Software for a Concurrent WorldPragmatic Bookshelf, (2013) |

[10] | Armstrong, Joe; Virding, Robert; Wikström, Claes; Williams, Mike, Concurrent Programming in ERLANG, (1996), Prentice Hall · Zbl 0869.68026 |

[11] | Barendregt, Henk, The Lambda Calculus: Its Syntax and Semantics, Studies in Logic and the Foundations of Mathematics, vol. 103, (1981), North-Holland · Zbl 1267.03034 |

[12] | Bierman, Gavin M.; Parkinson, Matthew J.; UpgradeJ, James Noble, Incremental typechecking for class upgrades, (Vitek, Jan, 22nd European Conference on Object-Oriented Programming. 22nd European Conference on Object-Oriented Programming, ECOOP. 22nd European Conference on Object-Oriented Programming. 22nd European Conference on Object-Oriented Programming, ECOOP, Lecture Notes in Computer Science, vol. 5142, (2008), Springer), 235-259 |

[13] | Boyapati, Chandrasekhar; Liskov, Barbara; Shrira, Liuba; Moh, Chuang-Hue; Richman, Steven, Lazy modular upgrades in persistent object stores, (Crocker, Ron; Steele, Guy L., ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications. ACM SIGPLAN Conference on Object-Oriented Programming Systems, Languages and Applications, OOPSLA, (2003), ACM), 403-417 |

[14] | Cardelli, Luca; Gordon, Andrew D., Mobile ambients, Theor. Comput. Sci., 240, 1, 177-213, (2000) · Zbl 0954.68108 |

[15] | Chalub, Fabricio; Braga, Christiano, Maude MSOS tool, Proceedings of the 6th International Workshop on Rewriting Logic and Its Applications. Proceedings of the 6th International Workshop on Rewriting Logic and Its Applications, WRLA 2006. Proceedings of the 6th International Workshop on Rewriting Logic and Its Applications. Proceedings of the 6th International Workshop on Rewriting Logic and Its Applications, WRLA 2006, Electron. Notes Theor. Comput. Sci., 176, 4, 133-146, (2007) |

[16] | Churchill, Martin; Mosses, Peter D., Modular bisimulation theory for computations and values, (Pfenning, Frank, 16th International Conference on Foundations of Software Science and Computation Structures. 16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS. 16th International Conference on Foundations of Software Science and Computation Structures. 16th International Conference on Foundations of Software Science and Computation Structures, FOSSACS, Lecture Notes in Computer Science, vol. 7794, (2013), Springer), 97-112 · Zbl 1260.68261 |

[17] | Churchill, Martin; Mosses, Peter D.; Reza Mousavi, Mohammad, Modular semantics for transition system specifications with negative premises, (D’Argenio, Pedro R.; Melgratti, Hernán C., 24th International Conference on Concurrency Theory. 24th International Conference on Concurrency Theory, CONCUR. 24th International Conference on Concurrency Theory. 24th International Conference on Concurrency Theory, CONCUR, Lecture Notes in Computer Science, vol. 8052, (2013), Springer), 46-60 · Zbl 1390.68465 |

[18] | Churchill, Martin; Mosses, Peter D.; Sculthorpe, Neil; Torrini, Paolo, Reusable components of semantic specifications XII, Trans. Aspect-Oriented Softw. Dev., 12, 132-179, (2015) |

[19] | Clavel, Manuel; Durán, Francisco; Eker, Steven; Lincoln, Patrick; Martı-Oliet, Narciso; Meseguer, José; Quesada, José F., Maude: specification and programming in rewriting logic, Theor. Comput. Sci., 285, 2, 187-243, (2002) · Zbl 1001.68059 |

[20] | de Boer, Frank S.; Clarke, Dave; Broch Johnsen, Einar, A complete guide to the future, (de Nicola, Rocco, Proc. 16th European Symposium on Programming. Proc. 16th European Symposium on Programming, ESOP’07. Proc. 16th European Symposium on Programming. Proc. 16th European Symposium on Programming, ESOP’07, Lecture Notes in Computer Science, vol. 4421, (2007), Springer-Verlag), 316-330 |

[21] | Drossopoulou, Sophia; Damiani, Ferruccio; Dezani-Ciancaglini, Mariangiola; Giannini, Paola, More dynamic object re-classification: Fickle \({}_{I I}\), ACM Trans. Program. Lang. Syst., 24, 2, 153-191, (2002) |

[22] | Flanagan, Cormac; Felleisen, Matthias, The semantics of future and an application, J. Funct. Program., 9, 1, 1-31, (1999) · Zbl 0926.68075 |

[23] | Fokkink, Wan; van Glabbeek, Rob J.; de Wind, Paulien, Compositionality of Hennessy-Milner logic by structural operational semantics, Theor. Comput. Sci., 354, 3, 421-440, (2006) · Zbl 1088.68094 |

[24] | Gebler, Daniel; Goriac, Eugen-Ioan; Reza Mousavi, Mohammad, Algebraic meta-theory of processes with data, (Borgström, Johannes; Luttik, Bas, Proc. 20th Int. Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics. Proc. 20th Int. Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics, EXPRESS/SOS. Proc. 20th Int. Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics. Proc. 20th Int. Workshop on Expressiveness in Concurrency and 10th Workshop on Structural Operational Semantics, EXPRESS/SOS, Electronic Proceedings in Theoretical Computer Science (EPTCS), vol. 120, (2013)), 63-77 |

[25] | Halstead, Robert H., Multilisp: a language for concurrent symbolic computation, ACM Trans. Program. Lang. Syst., 7, 4, 501-538, (1985) · Zbl 0581.68037 |

[26] | Harel, David; Kozen, Dexter; Tiuryn, Jerzy, Dynamic Logic, (2000), MIT Press · Zbl 0976.68108 |

[27] | Hennessy, Matthew, A Distributed Pi-Calculus, (2007), Cambridge University Press · Zbl 1125.68082 |

[28] | Hennessy, Matthew; Riely, James, Resource access control in systems of mobile agents, Inf. Comput., 173, 1, 82-120, (2002) · Zbl 1009.68081 |

[29] | Hewitt, Carl; Bishop, Peter; Steiger, Richard, A universal modular ACTOR formalism for artificial intelligence, (Nilsson, Nils J., 3rd International Joint Conference on Artificial Intelligence. 3rd International Joint Conference on Artificial Intelligence, IJCAI, (1973), William Kaufmann), 235-245 |

[30] | Holzmann, Gerard J., The Spin Model Checker, (2003), Addison-Wesley |

[31] | Hüttel, Hans, Transitions and Trees: An Introduction to Structural Operational Semantics, (2010), Cambridge Univ. Press · Zbl 1197.68052 |

[32] | Johnsen, Einar Broch; Owe, Olaf, An asynchronous communication model for distributed concurrent objects, (2nd International Conference on Software Engineering and Formal Methods. 2nd International Conference on Software Engineering and Formal Methods, SEFM, (2004), IEEE Computer Society Press), 188-197 · Zbl 1278.68067 |

[33] | Johnsen, Einar Broch; Owe, Olaf, Inheritance in the presence of asynchronous method calls, (38th Hawaii International Conference on System Sciences. 38th Hawaii International Conference on System Sciences, HICSS-38, (2005), IEEE Computer Society) · Zbl 1143.68356 |

[34] | Johnsen, Einar Broch; Owe, Olaf, An asynchronous communication model for distributed concurrent objects, Softw. Syst. Model., 6, 1, 39-58, (2007) |

[35] | Broch Johnsen, Einar; Owe, Olaf; Clarke, Dave; Bjork, Joakim, A formal model of service-oriented dynamic object groups, Sci. Comput. Program., 115-116, 3-22, (2016) |

[36] | Broch Johnsen, Einar; Owe, Olaf; Simplot-Ryl, Isabelle, A dynamic class construct for asynchronous concurrent objects, (Steffen, Martin; Zavattaro, Gianluigi, 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems. 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS’05. 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems. 7th IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS’05, Lecture Notes in Computer Science, vol. 3535, (2005), Springer), 15-30 |

[37] | Karami, Farzane; Owe, Olaf; Ramezanifarkhani, Toktam, An evaluation of interaction paradigms for active objects, J. Log. Algebraic Methods Program., 103, 154-183, (2019) · Zbl 1417.68023 |

[38] | Klein, Casey; Clements, John; Dimoulas, Christos; Eastlund, Carl; Felleisen, Matthias; Flatt, Matthew; McCarthy, Jay A.; Rafkind, Jon; Tobin-Hochstadt, Sam; Findler, Robert Bruce, Run your research: on the effectiveness of lightweight mechanization, (39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages. 39th Annual ACM SIGPLAN-SIGACT Symposium on Principles of Programming Languages, POPL ’12, (2012), ACM), 285-296 |

[39] | Lehman. Programs, Meir M., Life cycles, and laws of software evolution, Proc. IEEE, 68, 9, 1060-1076, (1980) |

[40] | Malabarba, Scott; Pandey, Raju; Gragg, Jeff; Barr, Earl T.; Barnes, J. Fritz, Runtime support for type-safe dynamic Java classes, (Bertino, Elisa, 14th European Conference on Object-Oriented Programming. 14th European Conference on Object-Oriented Programming, ECOOP. 14th European Conference on Object-Oriented Programming. 14th European Conference on Object-Oriented Programming, ECOOP, Lecture Notes in Computer Science, vol. 1850, (2000), Springer), 337-361 |

[41] | Mens, Tom; Demeyer, Serge, Software Evolution, (2008), Springer · Zbl 1153.68358 |

[42] | Mosses, Peter D., A Modular SOS for ML Concurrency Primitives, (1999), BRICS, Dept. of Computer Science, Univ. of Aarhus, Technical Report RS-99-57 |

[43] | Mosses, Peter D., Foundations of modular SOS, (Kutylowski, Miroslaw; Pacholski, Leszek; Wierzbicki, Tomasz, Mathematical Foundations of Computer Science. Mathematical Foundations of Computer Science, MFCS’99. Mathematical Foundations of Computer Science. Mathematical Foundations of Computer Science, MFCS’99, Lecture Notes in Computer Science, vol. 1672, (1999), Springer), 70-80 · Zbl 0955.68075 |

[44] | Mosses, Peter D., Foundations of Modular SOS, (December 1999), Technical Report BRICS RS-99-54, Basic Research in Computer Science |

[45] | Mosses, Peter D., Modular structural operational semantics, J. Log. Algebraic Program., 60-61, 195-228, (2004) · Zbl 1072.68061 |

[46] | Mosses, Peter D.; New, Mark J., Implicit propagation in structural operational semantics, Electron. Notes Theor. Comput. Sci., 229, 4, 49-66, (2009) · Zbl 1339.68159 |

[47] | Mosses, Peter D.; Vesely, Ferdinand, Funkons: component-based semantics in K, (Escobar, Santiago, 10th International Workshop on Rewriting Logic and Its Applications. 10th International Workshop on Rewriting Logic and Its Applications, WRLA. 10th International Workshop on Rewriting Logic and Its Applications. 10th International Workshop on Rewriting Logic and Its Applications, WRLA, Lecture Notes in Computer Science, vol. 8663, (2014), Springer), 213-229 |

[48] | Mousavi, Mohammad Reza; Reniers, Michel A.; Groote, Jan Friso, Notions of bisimulation and congruence formats for SOS with data, Inf. Comput., 200, 1, 107-147, (2005) · Zbl 1082.68075 |

[49] | Mousavi, Mohammad Reza; Reniers, Michel A.; Groote, Jan Friso, SOS formats and meta-theory: 20 years after, Theor. Comput. Sci., 373, 3, 238-272, (2007) · Zbl 1111.68069 |

[50] | Neamtiu, Iulian; Dumitraş, Tudor, Cloud software upgrades: challenges and opportunities, (International Workshop on the Maintenance and Evolution of Service-Oriented and Cloud-Based Systems, (2011)), 1-10 |

[51] | Neamtiu, Iulian; Hicks, Michael W., Safe and timely updates to multi-threaded programs, (Hind, Michael; Diwan, Amer, Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation. Proceedings of the ACM SIGPLAN Conference on Programming Language Design and Implementation, PLDI, (2009), ACM), 13-24 |

[52] | Pierce, Benjamin C., Basic Category Theory for Computer Scientists, (1991), MIT Press · Zbl 0875.18001 |

[53] | Pierce, Benjamin C.; Casinghino, Chris; Greenberg, Michael; Hriţcu, Cătălin; Sjöberg, Vilhelm; Yorgey, Brent, Software foundations, (2012), e-book |

[54] | Pina, Luís; Hicks, Michael, Tedsuto: a general framework for testing dynamic software updates, (IEEE International Conference on Software Testing, Verification and Validation. IEEE International Conference on Software Testing, Verification and Validation, ICST, (2016)), 278-287 |

[55] | Pina, Luís; Veiga, Luís; Hicks, Michael, Rubah: DSU for Java on a stock JVM, (ACM SIGPLAN Notices, vol. 49, (2014), ACM), 103-119 |

[56] | Pratt, Vaughan R., Semantical considerations on floyd-hoare logic, (IEEE Symposium on Foundations of Computer Science. IEEE Symposium on Foundations of Computer Science, FOCS’76, (1976)), 109-121 |

[57] | Prisacariu, Cristian; Owe, Olaf, Dynamic Structural Operational Semantics, (December 2012), Department of Informatics, University of Oslo, Online at |

[58] | Pukall, Mario; Kästner, Christian; Cazzola, Walter; Götz, Sebastian; Grebhahn, Alexander; Schröter, Reimar; Saake, Gunter, Javadaptor: flexible runtime updates of Java applications, Softw. Pract. Exp., 43, 2, 153-185, (2013) |

[59] | Roşu, Grigore; Şerbănuţă, Traian Florin, An overview of the K semantic framework, J. Log. Algebraic Program., 79, 6, 397-434, (2010) · Zbl 1214.68188 |

[60] | Sewell, Peter; Nardelli, Francesco; Owens, Scott; Peskine, Gilles; Ridge, Thomas; Sarkar, Susmit; StrniŠa, Rok, Ott: effective tool support for the working semanticist, J. Funct. Program., 20, 1, 71-122, (2010) · Zbl 1185.68201 |

[61] | Stoyle, Gareth; Hicks, Michael W.; Bierman, Gavin M.; Sewell, Peter; Neamtiu, Iulian, Mutatis Mutandis: safe and predictable dynamic software updating, ACM Trans. Program. Lang. Syst., 29, 4, (2007) · Zbl 1369.68157 |

[62] | Thomas van Binsbergen, L.; Sculthorpe, Neil; Mosses, Peter D., Tool support for component-based semantics, (Fuentes, Lidia; Batory, Don S.; Czarnecki, Krzysztof, 15th International Conference on Modularity, (2016), ACM), 8-11 |

[63] | Wright, Andrew K.; Felleisen, Matthias, A syntactic approach to type soundness, Inf. Comput., 115, 1, 38-94, (1994) · Zbl 0938.68559 |

[64] | Yu, Ingrid Chieh; Broch Johnsen, Einar; Owe, Olaf, Type-safe runtime class upgrades in Creol, (IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems. IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS. IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems. IFIP WG 6.1 International Conference on Formal Methods for Open Object-Based Distributed Systems, FMOODS, LNCS, vol. 4037, (2006), Springer), 202-217 · Zbl 1118.68031 |

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.