Adaptive Structural Operational Semantics (Video, SLE 2023)
Gwendal Jouneaux, Damian Frölich, Olivier Barais, Benoit Combemale, Gurvan Le Guernic, Gunter Mussbacher, and L. Thomas van Binsbergen
(University of Rennes, France / Inria, France / IRISA, France; University of Amsterdam, Netherlands; University of Rennes, France / Inria, France / CNRS, France / IRISA, France; University of Rennes, France / Inria, France / IRISA, France; DGA Maîtrise de l’Information, France / University of Rennes, France / Inria, France / IRISA, France; McGill University, Canada / Inria, France; University of Amsterdam, Netherlands)
Abstract: Software systems evolve more and more in complex and changing environments, often requiring runtime adaptation
to best deliver their services. When self-adaptation is the main concern of the system, a manual implementation of the underlying feedback loop and trade-off analysis may be desirable. However, the required expertise and substantial development effort make such implementations prohibitively difficult when it is only a secondary concern for the given domain. In this paper, we present ASOS, a metalanguage abstracting the runtime adaptation concern of a given domain in the behavioral semantics of a domain-specific language (DSL), freeing the language user from implementing it from scratch for each system in the domain. We demonstrate our approach on RobLANG, a procedural DSL for robotics, where we abstract a recurrent energy-saving behavior depending on the context. We provide formal semantics for ASOS and pave the way for checking properties such as determinism, completeness, and termination of the resulting self-adaptable language. We provide first results on the performance of our approach compared to a manual implementation of this self-adaptable behavior. We demonstrate, for RobLANG, that our approach provides suitable abstractions for specifying sound adaptive operational semantics while being more efficient.
Article: https://doi.org/10.1145/3623476.3623517
ORCID: https://orcid.org/0000-0003-1158-9335, https://orcid.org/0000-0003-1016-5303, https://orcid.org/0000-0002-4551-8562, https://orcid.org/0000-0002-7104-7848, https://orcid.org/0000-0003-0387-9738, https://orcid.org/0009-0006-8070-9184, https://orcid.org/0000-0001-8113-2221
Video Tags: DSL, Operational Semantics, Self-Adaptation, sle23main-p29-p, doi:10.1145/3623476.3623517, orcid:0000-0003-1158-9335, orcid:0000-0003-1016-5303, orcid:0000-0002-4551-8562, orcid:0000-0002-7104-7848, orcid:0000-0003-0387-9738, orcid:0009-0006-8070-9184, orcid:0000-0001-8113-2221
Presentation at the SLE 2023 conference, October 23–24, 2023, https://2023.splashcon.org/home/sle-2023
Sponsored by ACM SIGPLAN,
Okay so hello everyone my name is gend Junu and uh I will present you uh my last paper adaptive structural operational semantics to join work between uh the divers team in Ren um people from University of Amsterdam and Mill um so before talking about uh languages first I want to introduce a
Bit um about the software that we build with um so nowaday software evolve in complex and changing environments such as iot um or embedded systems and we see more and more the need for dynamic adaptation uh to best deliver the services um so for example Netflix adapt the quality of the
Video they send you depending on Among Us are you bandwidth um and so what we argue is that as a consequence there is a need to provide abstractions uh for self adaptation uh not for when it’s primary concern like Netflix where you want tailor everything by hand but when it’s a
Secondary uh but nevertheless an important concern so the abstraction for self- adaptation is a problem studied in other communities in basically in the self adaptive system Community um and solution have been proposed so for example there are multiple AR architectural solution such as the mekal loop the architecture or the morph uh AR
Ure and they also provide um Frameworks such as DCL uh execu Time mega models and P 2 which even have a DSL to Define uh your s adaptive system um but the problem is that if you want or have uh already a DSL to um capitalize uh your domain uh knowledge
Um it can be difficult uh to uh integrate those architectural solution of Frameworks so as we know dsls are tool for experts with the appropriate constrict for the given domain but uh if your domain does um does not have as a primary concern uh self adaptation uh
You have to um basically Implement in the programs or in the systems uh your own self adaptation which if you want to use Frameworks or architectural solution is uh it require reimplementation for example for Frameworks which can be tuse or even uh impossible in some case when
You don’t have The Primitives in the dsls um and that also require expertise in self- adaptation uh from the language user um which is not always the case if it’s not primary concern of the DSL um so as an example I will talk about the small language uh named robling
Which is a procedural DSL to program robot missions um which provide abstraction for robot sensor and actuator and for instance in this kind of DSL what we want what we might want to do is to adapt for example the the motor the the robot speed to save energy
It’s classical uh tradeoff that we may want to perform and so if we have difficulties to use a framework or have to uh C that by hand we fall back to kind of method programming where we have um implementation of a kind of tradeoff reasoning at the at the top and
After that you have the the effects of this tradeoff reasoning uh with different condition which can be uh error prone and tuse and for each system you have to manually design adaptation um that requires expertise to design um manual implementation of the tradeoff proning like I said and uh to be
Correctly integrated within the code base uh which is uh often uh not really easy so the question is the end of course if I’m giving a talk it’s the answer is no uh so we did previous work on that with the seales framework uh published ATD two years ago uh the idea
Of the seals framework is a framework to implement dsls with self ad self adaptive operational semantics what we mean by self adaptive operation semantics is that your operational semantics will change at R time based on the result of a feedback loop that will drive some adaptations of uh the
Semantic rules basically and in addition this framework also provide modularity for uh designing this adaptation so you can just decorrelate the creation of the self adaptive DSL and the creation of the adaptation in thems El so the way the sales framework work um basically you you free the DSL user
From implementing the feedback loop and Associated tradeoff resoning and integrate execution viant which are the adaptation and for the GSL designer you have um modeling capacities for modeling domain concept and also to specialize um The figb Loop and the adaptation process in general um but the problem is that
It’s mainly an implementation framework so we cannot specify our our DSL with that and particularly uh it’s really it became hard to reason about because basically a Java implementation um so what we want and what I want to present today is uh Asos so adaptive structural personal
Semantics which is a meta language to specify and reason about such self- adaptable operational semantics so uh Asos is defined as an extension of msos so modular structural operational semantics uh so we based on msos because it’s a metal language to Define operational semantics which is
The domain that we want to Target uh as a modular definition of semantics rule which fits what we what we want to do with uh modular adaptation and uh provide the ability to verify some properties uh such as determinism completeness or determinism in in some case um so we extended msos with
Um uh by providing additional uh adaptation uh rules and uh or to introduce them in um in the in the semantics of the language and uh from this definition we generate uh an implementation with seals that use the SE framework so our approach is um around the
Definition of the DSL so the language definition using Asos um you have to Define mainly three thing so the abstract syntax with metam um GE semantics rule with with the Asos uh metal language and you have also to configure the feedback loop by giving some properties of interest for the trade-off and
Resources and basically the operational semantics that you that you uncode with Asos is defined as a default semantic which is the usual semantics for your DSL uh adaptation semantics which is uh additional rules to adapt this uh default behavior and uh Point cuts to uh to express when and where to weave these
Adaptation uh semantics so um let’s talk a bit about the code right now uh so this is an Asos definition of some rules of semantics uh so the first instruction is um basically the model uh or where to import the abstract syntax so the idea is the our
Syntax is uh is presented as a meta model that we merge with another meta model that represent the dynamic information uh that we merge to have an execution meta model uh on which we can operate and in addition to that this uh semantic definition uh is composed of a set of
Semantic rules so you have for example here the rule program that is the the root rule uh for our GSL uh which Define uh a conclusion as a transition between terms so here you have the term program with a subterm command and uh this rule um result in another program with new
Command that has been partially evaluated uh well and that has meant progress uh in addition to do um so yeah in addition to this uh conclusion you can provide some premises that uh help you either compute subterms or Define a condition to uh to um call those rules
So for example uh the resolve keyword uh here is the defining the section of the premise and here we have a premise that said that if the command can progress to a new command then the program is Advance also so the idea said that if we can execute
The command to a new state then the pro the world program has advaned to New State um we have two kinds of uh transition premise so the first one which is the classic one which we also have termination uh premise so so the termination keyword is to deal with abup termination in
The in the semantics so for example if you want to implement a break a return or exceptions uh you might want you you want to stop the uh the execution of the current uh control flow and just fold back to some rules and so to do to do so
You have the termination keyword which given as an output of uh of the conclusion rule will just throw um uh um emit a signal of termination with uh some Dynamic values so here for example we have we took about runtime errors and in your um premises you can just catch
That to uh manage and continue and um fall back to another Behavior so for example if you get the a return uh you can just get the value and say that the function written this value uh so in addition to transition premise we uh provide bindings that’s uh the
Bind section is uh related to Computing values and storing values B basically so in this case you have a self. value so this value is coming from the dynamic affirmation that we’re weaved with the Met model and the self refer to the assignment that is uh in the input of
The rules so basically what we say here is that the current value of the uh of the variable um uh which is assigned is the integer uh that has been computed from from the expression basically and finally we have the the Wear close uh where you can express
First ofic conditions uh allowing for example to uh to know if you have to go into the then Branch or the else branch of a of a if um uh concept for example and so in addition to do uh semantics rules and so the semantics rules provided the semantics for the
Default semantics but we can also Express adaptations on top of those rules so here is for example the definition of um uh an adaptation module which is approximate dble uh um where we have mainly two kind of things inside those modules uh first uh matching definition which is the the point cut of
Our adaptation where we have a structural matching of our nodes saying that we want to uh apply some rules at some point if uh we are uh in a subtree from an assignment uh which has a VF for example and we can also Express additional constraints uh through the
Where close so for example we here we target an assignment where the the value that is assigned is assigned to a variable of type float um after this uh matching definition we also can express adaptation rules so adaptation rules are um Extended uh semantic rules so the
First thing that you specify here is the kind of adaptation you have three kind of adapation before after and um specialize that will uh make that will weave the the new rules uh inside the sematics before after the specified rules um or in place of the specify R so for example here the
Before B up right hand side specified that the rule bin up left hand side to float uh that is defined after uh should be called uh before calling the bin up right hand side um rule basically so if we take a look uh step back and look at the meta model uh what
I showed you is that we have a definition of adaptive operational semantics which is for the default semantics composed of rules those rules uh contain at least one transion that represent the conclusion and the effect of the rules and potentially uh some premises that uh Express the the
Continuation of the computation to child of the node in the as for example we have also uh the different Clauses so the bindings the condition but also uh I did not show but we also have input and output that allow you to communicate with the outside of the
Language so for example input is for uh user input in the console or an output for for example printing uh in the terminal for example and the second part of the Adaptive operational semantics is the adaptation modules uh that are composed of a match uh one or more match
Closes that def Define when to uh introduce the adaptation rules and adaptation rules that can be uh before Specialized or after rules uh kind of adaptation that Target one rules and Define another rule so now that we know a bit more about the syntax of the metal language
Uh we provided some formal semantics I will not go too much into the detail of uh that uh but the core idea is that we have to to decide if we apply an adaptation or apply the default semantics and so the translation of this rule is basically saying that Um if you uh if you uh first you get the set of uh possible adaptation or activated adaptation uh that you might want uh to apply uh and if you uh select uh the correct one given the the matching that you have if you have uh at
Some point one rule that ex one ADT one adaptation rule that uh that can be executed you call it and if you cannot here uh then you fall back to the default semantics which is basically how we proceed but if you want to have uh
More detail we can you can take a look at the paper where it’s more clearly more clearly explained um so on top of that we provide uh a trans a translation semantics from Asos to seals to be able to execute um the semantics uh so the
Idea is the the same structure of rule uh from Asos we first generate uh guards which correspond to verifying that the current term is corresponding to the pattern uh the input pattern the in the conclusion of the rule so that’s the the little one after that we check some
Conditions so the condition that were expressed in the in the b in the um in the work close and uh we resolve premise to check if the output of the premise is corresponding to the term so for example you’ve seen uh before the um the output termination runtime here so we’ll check
Uh if it’s correctly a runtime error or not if it’s not we don’t call this rule but another and if all those checks um are passed we then enter the the effect part so so it’s really applying the rule so we just call uh we basically translate the input uh and get the
Information from the outside uh compute um compute the different bindings um that we can have um then we uh we actually compute uh the term um the output term which can be done in different way uh so for example you can just update the current
Node or you can return a value um same here if you want more detail on how we exactly proceed uh you can take a look at the paper and finally we manage some the some of the output so for example print statement and inside uh this generated effect you have the input
Point for the different code for the adaptations so now we generate this code but all that is executed um so the first part when you call uh a rule on a node is to uh perform the feedback loop to know if there is some adaptation so you will first monitor
Analyze plan and execute by selecting the different modules that can be applied uh with respect to the trade-off and the current context and based on that you will have uh the second part of the of the process which is basically matching those uh activated adaptation modules to the
Current node to see if the if the node matches those adaptation uh to sort out the applicable uh adaptation rules and then after we want we enter the process of just checking if the rule exist and call uh the the adaptation rules uh one after another and select in the case of
Specialize because we replace uh and not add just uh a new rule so to evaluate this work we provide some proof on top of the of the formal model that we provided in the paper uh so basically we check determinism and completeness of uh the semantics that we
Define using Asos and uh about non-termination uh what we can do currently is that we can detect patterns that we know will provide uh will will cause um um for example race condition and cycle between adaptations uh but we currently overestimate because for example the the feedback loop the concrete Fe the
Feedback loop step are are not yet model um modeled in the in the formal model so for example we cannot detect if um two adaptation rules would create a race condition but they will never because they matching uh is uh they the feedback loop made them never appear together for
Example in addition on the on the more execut execut execute executable Port uh we check the applicability on the robling DSL by uh providing adaptation um to a program uh to slow the the the motor speeds uh to save energy and we observe uh correct uh adaptation behavior and uh we also uh
Observe that when changing the tradeoff and dynamically we uh are able to adapt to the change in in this context so that is okay and on the second um experiment we wanted to check the performance of that so compared to a man implementing the the adaptation process inside the the
The robling program so we made a um an experimental setup with a a machine when we uh executed a 30 time the experiment with three time uh with reboot um to mitigate the effect of initial state to try to have a a proper setup and the
Results are a bit well at first were were strange because we we gain actually speed uh but our our Theory right now is that probably from jvm optimization because uh the feedback loop in our case so using Asos is defined using Java while in robang it’s in robang and so
Probably um some jvm uh optimization uh help us in in the performance here so as a conclusion the Asus metal language uh provides abstraction for defining operational semantics and their adaptations uh we also provide mechanism for composing adaptation with the defa semantics uh at R time so basically
Calling them and we also um Provide support for verifying properties on do semantics uh on the technical aspect we provide uh the ID tool support uh for Asos in an eclipse environment uh generator targeting the sees framework and we are also fully compatible with exex which means that you can Define
Your DSL INX Tex and just provide semantics as as as an Asos C itics and uh it will it should work and the perspective of this work is that first evaluate to uh evaluate the complexity of using Asos because it’s declarative and Rule based language it’s
Not the same as uh expressing that as let’s say a visitor um pattern for implementing the um the semantics so we have to assess the the complexity of that um we also want to rify uh the the correctness envelope so the the way that we we uh constraints what are the possible
Adaptation that were present in seal that that we do not make in Asos because we don’t really know how to constrain uh rules right now in the way that we want and we also want to extend Asos to uh configure the feedback loops which is basically what I said earlier when we uh
When I was talking about uh disambiguating uh some detection in the n termination and non-termination and we also want to use asos’s declarative nature to uh support cell composition and make uh language composition uh self adaptable language composition thanks for attention and if you have any question thank you do we have question
Thank you very much for the talk and also thank you for your interest in modular SOS which a very popular framework um the beginning of section four in the paper you say um you motivate these adaptation rules and the extension to the msos framework by saying that um it allows to express
Struct structural patterns that are not possible to express using the typical msos rule format have you proved that um and uh no um okay uh that’s maybe not the right way to put it um the idea was uh when when we were writing this is that if you
Want to have some property like uh the simulation as a congruence uh your pattern just you you cannot Nest so much pattern while uh our matching uh pattern can be arbitrary deep so that that was the idea around that um by allo uh this matching uh deeper it’s it cannot be
Represented using msos without bre breaking this property and that’s that’s we that’s what we we we said another question yes yes maybe one brief question first thank you for the part very interesting um I have one question regarding the uh checking of the validity what you can translate and
What um I mean we just heard about the structural features but um just from a behavioral point of view as Java is to incomplete I would hope that well you can translate nearly everything which is feasible can you give an example what absolutely makes no sense to translate
And how would you deal with that you mean translate from java to Asos no no uh I think the other way around the other way um so you have your Asos rules and translate Java or did I get that wrong yeah that’s basically what we do in the generator in fact
And no I don’t see really any problem of generation uh okay um but why is then this uh checking St step if you can uh whether you can translate something um by checking step you mean the generated gu uh it was a slide or two before I
Think yeah uh there’s no valid uh adaptation uh transition maybe that wrong uh no Val transition is that uh for example you have some adaptations that are active and that’s are for for example for the assignment but you have an assignment if we take for example the the previous
Example which is well so long ago uh so for example here we target assignment data tab FL so you have module that uh is activated but is not matching so we do not provide these rules so we have to check if those rules are available when we are executing basically so so that
That’s what’s thank you okay thank you