Pascal Fradet and Stéphane Hong Tuan Ha. Aspects of Availability: Enforcing Timed Properties to Prevent Denial of Service. In Science of Computer Programming, SCP, In Press, 2010. (preprint version: )
Key-words: Aspect-oriented programming, resource management, availability, verification, denial of service.

Abstract: We propose a domain-specific aspect language to prevent denial of service caused by resource management. Our aspects specify availability policies by enforcing time limits in the allocation of resources. In our language, aspects can be seen as formal timed properties on execution traces. Programs and aspects are specified as timed automata and the weaving process as an automata product. The benefit of this formal approach is two-fold: the user keeps the semantic impact of weaving under control and (s)he can use a model-checker to optimize the woven program and verify availability properties. This article presents the main approach (programs, aspects, weaving) formally using timed safety automata. The specification of resources, optimizations and verification are sketched in a more intuitive fashion. Even if a concrete implementation remains as future work, we address some high-level implementation issues and illustrate the approach by small examples and a case study.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Classical Coordination Mechanisms in the Chemical Model. In From Semantics to Computer Science: Essays in Honor of Gilles Kahn, Cambridge University Press, pages 29-50, 2009 . (preprint version: )
Key-words: Chemical programming, higher-order conditional multiset rewriting, coordination mechanisms, parallel programming models, Petri nets, Kahn process networks.

Abstract: Originally, the chemical model of computation has been proposed as a simple and elegant parallel programming paradigm. Data is seen as ``molecules'' and computation as ``chemical reactions'': if some molecules satisfy a predefined reaction condition, they are replaced by the ``product'' of the reaction. When no reaction is possible, a normal form is reached and the program terminates. In this paper, we describe classical coordination mechanisms and parallel programming models in the chemical setting. All these examples put forward the simplicity and expressivity of the chemical paradigm. We pay a particular attention to the chemical description of the simple and successful parallel computation model known as Kahn Process Networks.

Simplice Djoko Djoko, Rémi Douence, Pascal Fradet. Aspects Preserving Properties. INRIA Reseach Report nº 7155, December 2009.
Key-words: Aspect-oriented languages, weaving, domain-specific languages, semantics, temporal properties, proofs.

Abstract: Aspect Oriented Programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In this article, we identify categories of aspects that preserve some classes of properties. Specialized aspect languages can be then designed to ensure that aspects belong to a specific category and therefore that woven programs will preserve the corresponding properties. Our categories of aspects, inspired by Katz's, comprise observers, aborters and confiners. Observers introduce new instructions and a new local state but they do not modify the base program's state and control-flow. Aborters are observers which may also abort executions. Confiners only ensure that executions remain in the reachable states of the base program. These categories (along with three other) are defined precisely based on a language independent abstract semantics framework. The classes of preserved properties are defined as subsets of LTL for deterministic programs and CTL* for non-deterministic ones. We can formally prove that, for any program, the weaving of any aspect in a category preserves any property in the related class.We present, for most aspect categories, a specialized aspect language which ensures that any aspect written in that language belongs to the corresponding category. It can be proved that these languages preserve the corresponding classes of properties by construction. The aspect languages share the same expressive pointcut language and are designed wrt a common imperative base language. Each category and language are illustrated by simple examples. The appendix provides semantics and examples of proofs: the proof of preservation of properties by a category and the proof that all aspects written in a language belong to the corresponding category.

Simplice Djoko Djoko, Rémi Douence, Pascal Fradet. Specialized Aspect Languages Preserving Classes of Properties. In Proc. of the Sixth IEEE International Conference on Software Engineering and Formal Methods, SEFM'08, November 2008.
Key-words: Aspect-oriented languages, weaving, domain-specific languages, semantics, temporal properties, proofs.

Abstract: Aspect oriented programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In previous work, we have identified categories of aspects that preserve classes of temporal properties. We have formally proved that, for any program, the weaving of any aspect in a category preserves all properties in the related class. In this article, after a summary of our previous work, we present, for each aspect category, a specialized aspect language which ensures that any aspect written in that language belongs to the corresponding category. It can be proved that these languages preserve the corresponding classes of properties by construction. The aspect languages share the same expressive pointcut language and are designed \wrt a common imperative base language. Each language is illustrated by simple examples. We also prove that all aspects written in one of the languages belong to the corresponding category.

Simplice Djoko Djoko, Rémi Douence, Pascal Fradet. Aspects Preserving Properties. In ACM SIGPLAN Symposium on Partial Evaluation and Semantics-Based Program Manipulation, PEPM'08, pages 135-145, January 2008.
Key-words: Aspect-oriented languages, weaving, semantics, temporal properties, proofs.

Abstract: Aspect Oriented Programming can arbitrarily distort the semantics of programs. In particular, weaving can invalidate crucial safety and liveness properties of the base program. In this article, we identify categories of aspects that preserve some classes of properties. It is then sufficient to check that an aspect belongs to a specific category to know which properties will remain satisfied by woven programs. Our categories of aspects, inspired by Katz's, comprise observers, aborters and confiners. Observers introduce new instructions and a new local state but they do not modify the base program's state and control-flow. Aborters are observers which may also abort executions. Confiners only ensure that executions remain in the reachable states of the base program. These categories (along with three other) are defined precisely based on a language independent abstract semantics framework. The classes of properties are defined as subsets of LTL for deterministic programs and CTL* for non-deterministic ones. We can formally prove that, for any program, the weaving of any aspect in a category preserves any property in the related class. We give examples to illustrate each category and prove the preservation of one class of properties by one category of aspects in the appendix.

Abstract: We present a formal approach to implement fault-tolerance in real-time embedded systems. The initial fault-intolerant system consists of a set of independent periodic tasks scheduled onto a set of fail-silent processors connected by a reliable communication network. We transform the tasks such that, assuming the availability of an additional spare processor, the system tolerates one failure at a time (transient or permanent). Failure detection is implemented using heartbeating, and failure masking using checkpointing and rollback. These techniques are described and implemented by automatic program transformations on the tasks' programs. The proposed formal approach to fault-tolerance by program transformations highlights the benefits of separation of concerns. It allows us to establish correctness properties and to compute optimal values of parameters to minimize fault-tolerance overhead. We also present an implementation of our method, to demonstrate its feasibility and its efficiency.

Abstract: In this paper, we propose a domain-specific aspect language to prevent the denials of service caused by resource management. Our aspects specify availability policies by enforcing time limits in the allocation of resources. In our language, aspects can be seen as formal timed properties on execution traces. Programs and aspects are specified as timed automata and the weaving process as an automata product. The benefit of this formal approach is two-fold: the user keeps the semantic impact of weaving under control and (s)he can use a model-checker to optimize the woven program and verify availability properties.

Abstract: Building a real-time system from reusable or COTS components introduces several problems, mainly related to compatibility, communication, and QoS issues. We propose an approach to automatically derive adaptors in order to solve black-box integration anomalies, when possible. We consider black-box components equipped with an expressive interface that specifies the interaction behavior with the expected environment, the component clock, as well as latency, duration, and controllability of the component's actions. The principle of adaptor synthesis is to coordinate the interaction behavior of the components in order to avoid possible mismatches, such as deadlocks. Each adaptor models the correct assembly code for a set of components. Our approach is based on labeled transition systems and Petri nets, and is implemented in a tool called SynthesisRT. We illustrate it through a case study concerning a remote medical care system.

Rémi Douence and Pascal Fradet. The next 700 Krivine Machines. In Higher-Order and Symbolic Computation, HOSC, 20(3), 2007.(preliminary version: )
Key-words: Functional programming, Krivine machine, abstract machines, program transformation, compilation, functional language implementations.

Abstract: The Krivine machine is a simple and natural implementation of the normal weak-head reduction strategy for pure lambda-terms. While its original description has remained unpublished, this machine has served as a basis for many variants, extensions and theoretical studies. In this paper, we present the Krivine machine and some well-known variants in a common framework. Our framework consists of a hierarchy of intermediate languages that are subsets of the lambda-calculus. The whole implementation process (compiler + abstract machine) is described via a sequence of transformations all of which express an implementation choice. We characterize the essence of the Krivine machine and locate it in the design space of functional language implementations. We show that, even within the particular class of Krivine machines, hundreds of variants can be designed.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Programming Self-Organizing Systems with the Higher-Order Chemical Language. In International Journal of Unconventional Computing, IJUC, 3(3):161-177, 2007. (preprint version: )
Key-words: Chemical programming, higher-order conditional multiset rewriting, autonomic systems, self-organization, self-protection, self-healing, self-optimization.

Abstract: In a chemical language, computation is viewed as abstract molecules reacting in an abstract chemical solution. Data can be seen as molecules and operations as chemical reactions: if some molecules satisfy a reaction condition, they are replaced by the result of the reaction. When no reaction is possible within the solution, a normal form is reached and the program terminates. In this article, we introduce HOCL, the Higher-Order Chemical Language, where reaction rules are also considered as molecules. We illustrate the application of HOCL to the specification of self-organizing systems. We describe two case studies: an autonomic mail system and the coordination of an image-processing pipeline on a grid.

Abstract: This SCP special collects articles that make contributions to the foundations of aspect-oriented programming (AOP). Aspects have been developed over the last 10 years to facilitate the modularization of crosscutting concerns, i.e., concerns that crosscut with the primary modularization of a program. This special issue further continues the efforts of the annual FOAL workshop (Foundations of Aspect-Oriented Languages) in so far that it supports and integrates research on firm foundations of AOP. There are 5 contributions addressing the following issues: (i) a fundamental core language for aspects; (ii) subtleties of so-called around advice; (iii) aspects in higher-order languages; (iv) the interaction between aspects and generics; (v) a notion of aspects for reactive systems based on synchronous languages.

Simplice Djoko Djoko, Rémi Douence, Pascal Fradet and Didier Le Botlan. Towards a Common Aspect Semantic Base (CASB). Deliverable 54, EU Network of Excellence in AOSD, 2006.
Key-words: Aspect-oriented languages, AspectJ, Featherweight Java, operational semantics.

Abstract: We gradually introduces formal semantic descriptions of aspect mechanisms. We do our best to describe aspects as independently as possible from the base language. For each aspect feature, we introduce the minimal constructions of the base language necessary to plug aspects in. We consider the weaving of a single aspect, in particular before, after and around aspects. We extend the model with multiple aspects, cflow pointcuts, aspects on exceptions, aspect deployment, aspect instantiation and stateful aspects. Our descriptions could be applied to many different types of programming languages (object-oriented, imperative, functional, logic, assembly, etc.). As an illustration of our technique, we describe the semantics of an AspectJ-like core aspect language (around aspects + cflow + aspect association/instantiation) for a core Java language (Featherweight Java with assignments).

Abstract: We present a formal approach to implement fault-tolerance in real-time embedded systems. The initial fault-intolerant system consists of a set of independent periodic tasks scheduled onto a set of fail-silent processors connected by a reliable communication network. We transform the tasks such that, assuming the availability of an additional spare processor, the system tolerates one failure at a time (transient or permanent). Failure detection is implemented using heartbeating, and failure masking using checkpointing and roll-back. These techniques are described and implemented by automatic program transformations on the tasks' programs. The proposed formal approach to fault-tolerance by program transformation highlights the benefits of separation of concerns and allows us to etablish correctness properties.

Tolga Ayav, Pascal Fradet and Alain Girault. Implementing Fault-Tolerance in Real-Time Systems by Program Transformations. INRIA Reseach Report nº 5919, May 2006
Key-words: Fault-tolerance, real-time systems, heartbeating, checkpointing, program transformations, correctness proofs.

Abstract: We present a formal approach to implement fault-tolerance in real-time embedded systems. The initial fault-intolerant system consists of a set of independent periodic tasks scheduled onto a set of fail-silent processors connected by a reliable communication network. We transform the tasks such that, assuming the availability of an additional spare processor, the system tolerates one failure at a time (transient or permanent). Failure detection is implemented using heartbeating, and failure masking using checkpointing and roll-back. These techniques are described and implemented by automatic program transformations on the tasks' programs. The proposed formal approach to fault-tolerance by program transformation highlights the benefits of separation of concerns and allows us to etablish correctness properties (including the meeting of real-time constraints). We also present an implementation of our method, to demonstrate its feasibility and its efficiency.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Generalized Multisets for Chemical Programming. In Mathematical Structures in Computer Science, MSCS, vol. 16(4), pages 557-580, 2006. (preprint version: )
Key-words: Chemical programming, higher-order conditional multiset rewriting, infinite multisets, negative multiplicities.

Abstract: Gamma is a programming model where computation can be seen as chemical reactions between data represented as molecules floating in a chemical solution. This model can be formalized as associative, commutative, conditional rewritings of multisets where rewrite rules and multisets represent chemical reactions and solutions, respectively. In this article, we generalize the notion of multiset used by Gamma and present applications through various programming examples. First, multisets are generalized to include rewrite rules which become first-class citizen. This extension is formalized by the gamma-calculus, a chemical model that summarizes in a few rules the essence of higher-order chemical programming. By extending the gamma-calculus with constants, operators, types and expressive patterns, we build a higher-order chemical programming language called HOCL. Finally, multisets are further generalized by allowing elements to have infinite and negative multiplicities. Semantics, implementation and applications of this extension are considered.

Olivier Michel, Jean-Pierre Banâtre, Pascal Fradet and Jean-Louis Giavitto. Challenging Questions for the Rationale of Non-Classical Programming Languages. In International Journal of Unconventional Computing, IJUC, 2(4):337-347, 2006.(preprint version: )
Key-words: Unconventional programming languages, bio-inspired, DNA, chemical or quantum models.

Abstract: In this position paper, we question the rationale behind the design of unconventional programming languages. Our questions are classified in four categories: the sources of inspiration for new computational models, the process of developing a program, the forms and the theories needed to write and understand non-classical programs and finally the new computing media and the new applications that drive the development of new programming languages.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Towards Grid Chemical Coordination (short paper). In Proc. of the 2006 ACM Symposium on Applied Computing, SAC'06, pages 445-446.
Key-words: Chemical programming, coordination, grid programming.

Abstract: In chemical programming, data is represented by (symbolic) molecules floating in a chemical solution, and computation is performed by reactions between them. In this paper, that model is applied to grid programming. Chemical programs are executed in a grid which is itself specified by the chemical metaphor. Chemical programs or chemical specification self-organise and self-adapt to their environment.

Jean-Pierre Banâtre, Pascal Fradet, and Yann Radenac. Chemical Programming of Self-Organizing Systems. In ERCIM News, Vol. 64, Special Theme: Emergent Computing, Jan 2006
Key-words: Chemical programming, self-organization, self-protection, self-healing, self-optimization.

Abstract:Chemical programming relies on the chemical metaphor: data are seen as molecules and computations as chemical reactions. This programming paradigm exhibits self-organizing properties and allows the description of autonomic systems in an elegant way.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Generalized Multisets for Chemical Programming. Research Report 5743, INRIA, November 2005.
Key-words: Chemical programming, higher-order conditional multiset rewriting, infinite multisets, negative multiplicities.

Abstract: Gamma is a programming model where computation can be seen as chemical reactions between data represented as molecules floating in a chemical solution. This model can be formalized as associative, commutative, conditional rewritings of multisets where rewrite rules and multisets represent chemical reactions and solutions, respectively. In this article, we generalize the notion of multiset used by Gamma and present applications through various programming examples. First, multisets are generalized to include rewrite rules which become first-class citizen. This extension is formalized by the $\gamma$-calculus, a chemical model that summarizes in a few rules the essence of higher-order chemical programming. By extending the $\gamma$-calculus with constants, operators, types and expressive patterns, we build a higher-order chemical programming language called HOCL. Finally, multisets are further generalized by allowing elements to have infinite and negative multiplicities. Semantics, implementation and applications of this extension are considered.

 
Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. A Generalized Higher-Order Chemical Computation Model with Infinite and Hybrid Multisets. In Pre-Proceedings of 1st International Workshop on New Developments in Computational Models, DCM'05, Vol. 135(3) of ENTCS, pages 3-13, March 2006, Elsevier.
Key-words: Chemical programming, higher-order conditional multiset rewriting, infinite multisets.

Abstract: Gamma is a programming model where computation is seen as chemical reactions between data represented as molecules floating in a chemical solution. Formally, this model is represented by the rewriting of a multiset where rewrite rules model the chemical reactions. Recently, we have proposed the $\gamma$-calculus, a higher-order extension, where the rewrite rules are first-class citizen. The work presented in this paper increases further the expressivity of the chemical model with generalized multisets: multiplicities of elements may be infinite and/or negative. Applications of these new notions are illustrated by some programming examples.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Principles of Chemical Programming. In Proceedings of the 5th International Workshop on Rule-Based Programming, RULE'04, volume 124(1) of ENTCS, pages 133--147, June 2005. Elsevier.
Key-words: Chemical programming, higher-order conditional multiset rewriting, chemical metaphor, formal calculi.

Abstract: The chemical reaction metaphor describes computation in terms of a chemical solution in which molecules interact freely according to reaction rules. Chemical models use the multiset as their basic data structure. Computation proceeds by rewritings of the multiset which consume elements according to reaction conditions and produce new elements according to specific transformation rules. Since the introduction of Gamma in the mid-eighties, many other chemical formalisms have been proposed such as the Cham, the P-systems and various higher-order extensions. The main objective of this paper is to identify a basic calculus containing the very essence of the chemical paradigm and from which extensions can be derived and compared to existing chemical models.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Higher-order Chemical Programming Style. In Proceedings of Unconventional Programming Paradigms, pages 84--98, 2005. Springer-Verlag, LNCS, Vol. 3566.
Key-words: Chemical programming, higher-order conditional multiset rewriting, autonomic systems.

Abstract: The chemical reaction metaphor describes computation in terms of a chemical solution in which molecules interact freely according to reaction rules. Chemical solutions are represented by multisets of elements and computation proceeds by consuming and producing new elements according to reaction conditions and transformation rules. The chemical programming style allows to write many programs in a very elegant way. We go one step further by extending the model so that rewrite rules are themselves molecules. This higher-order extension leads to a programming style where the implementation of new features amounts to adding new active molecules in the solution representing the system.

Pascal Fradet and Stéphane Hong Tuan Ha. Systèmes de gestion de ressources et aspects de disponibilité. In L'Objet, logiciel, bases de données, réseaux, Hermès/Lavoisier. volume 12(2-3), pages 183-210, septembre, 2006. (preprint version: )
Key-words: Programmation par aspects, gestion de ressources, disponibilité, vérification, dénis de service.

Abstract: In this paper, we focus on availability properties and the prevention of denial of services. We propose a domain-specific aspect language to prevent the denials of service caused by resource management. Our aspects specify availability policies by enforcing time limits in the allocation of resources. In our language, an aspect can be seen as a formal temporal property on execution traces. Programs and aspects are specified as timed automata and the weaving process as an automata product. The benefit of this formal approach is two-fold: the user keeps the semantic impact of weaving under control and (s)he can use a model-checker to optimize the woven program and verify availability properties.

Pascal Fradet and Stéphane Hong Tuan Ha. Systèmes de gestion de ressources et aspects de disponibilité. In 2ème Journée Francophone sur le Développement de Logiciels Par Aspects, JFDLPA'05, Lille, France, September 2005.
Key-words: Programmation par aspects, gestion de ressources, disponibilité, vérification, dénis de service.

Abstract: In this paper, we consider resource management in isolation (separation of concerns) and the prevention of denial of service (i.e. availability) as aspects. We concentrate on denials of service caused by resource management (starvations, deadlocks). Our aspects specify time limits or orderings in the allocation of resources. They can be seen as the specification of an availability policy. The approach relies on timed automata to specify services and aspects. It allows us to implement weaving as an automata product and to use model-checking tools to verify that aspects enforce the required availability properties.

Pascal Fradet and Stéphane Hong Tuan Ha. Network Fusion. In Proceedings of Asian Symposium on Programming Languages and Systems, APLAS'04, pages 21-40, november 2004. Springer-Verlag, LNCS, Vol. 3302.
Key-words: Aspect-oriented programming, components, Kahn process networks, fusion, invasive composition, scheduling, synchronisation.

Abstract: Modular programming enjoys many well-known advantages but the composition of modular units may also lead to inefficient programs. In this paper, we propose an invasive composition method which strives to reconcile modularity and efficiency. Our technique, network fusion, automatically merges networks of interacting components into equivalent sequential programs. We provide the user with an expressive language to specify scheduling constraints which can be taken into account during network fusion. Fusion allows to replace internal communications by assignments and alleviates most time overhead. We present our approach in a generic and unified framework based on labeled transition systems, static analysis and transformation techniques.

Rémi Douence, Pascal Fradet and Mario Südholt. Trace-Based Aspects. In Aspect-Oriented Software Development, Mehmet Aksit, Siobhán Clarke, Tzilla Elrad, and Robert Filman, editors, pages 201-217. Addison-Wesley, 2004.
Key-words: Aspect-oriented programming, execution traces, interactions, security.

Abstract: This chapter presents trace-based aspects which take into account the history of program executions in deciding what aspect behavior to invoke. Such aspects are defined in terms of execution traces and may express relations between different events. Weaving is accomplished through an execution monitor which modifies the base program execution as defined by the aspects. We motivate trace-based aspects and explore the trade-off between expressiveness and property enforcement/analysis. More concretely, we first present an expressive model of trace-based aspects enabling proofs of aspect properties by equational reasoning. Using a restriction of the aspect language to regular expressions, we show that it becomes possible to address the difficult problem of interactions between conflicting aspects. Finally, by restricting the actions performed by aspects, we illustrate how to keep the semantic impact of aspects under control and to implement weaving statically.

Rémi Douence, Pascal Fradet and Mario Südholt. Composition, reuse and interaction analysis of stateful aspects. In Proceedings of the 3rd Int' Conf. on Aspect-Oriented Software Development, AOSD'04, pages 141-150, March 2004. ACM Press.
Key-words: Aspect-oriented programming, formal model, static analysis, aspect interactions, aspect composition, reuse of aspects.

Abstract: Aspect-Oriented Programming promises separation of concerns at the implementation level. However, aspects are not always orrthogonal and aspect interaction is a fundamental problem. In this paper, we extend previous work on a generic framework for the formal definition and interaction analysis of stateful aspects. We propose three important extensions which enhance expressivity while preserving static analyzability of interactions. First, we provide support for variables in aspects in order to share information between different execution points. This allows the definition of more precise aspects and to avoid detection of spurious conflicts. Second, we introduce generic composition operators for aspects. This enables us to provide expressive support for the resolution of conflicts among interacting aspects. Finally, we offer a means to define applicability conditions for aspects. This makes interaction analysis more precise and paves the way for reuse of aspects by making explicit requirements on contexts in which aspects must be used.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Chemical Specification of Autonomic Systems. In Proceedings of the 13th International Conference on Intelligent and Adaptive Systems and Software Engineering, IASSE'04, july 2004.
Key-words: Chemical programming, higher-order conditional multiset rewriting, autonomic computing, self-properties (protection, healing, optimization).

Abstract: Autonomic computing provides a vision of information systems allowing self-management of many predefined properties. Such systems take care of their own behavior and of their interactions with other components without any external intervention. One of the major challenges concerns the expression of properties and constraints of autonomic systems. We believe that the {\em chemical programming paradigm} (represented here by the Gamma formalism) is well-suited to the specification of autonomic systems. In Gamma, computation is described in terms of chemical reactions (rewrite rules) in solutions (multisets of elements). It captures the intuition of a collection of cooperative components which evolve freely according to some predefined constraints. In this paper, after a short presentation of a higher-order version of the Gamma formalism, it is shown through the example of a mailing system, how the major properties expected from an autonomic system can be easily expressed as a collection of chemical reactions.

Jean-Pierre Banâtre, Pascal Fradet and Yann Radenac. Higher-order chemistry. In Preproceedings of the Workshop on Membrane Computing, WMC'03, july 2003.
Key-words: Chemical programming, higher-order conditional multiset rewriting.

Abstract: Gamma is a formalism in which programs are expressed in terms of multiset rewriting often referred as the Chemical Reaction Model. In this paper we are concerned with higher-order Gamma programming. First we review three proposals which introduce the notion of membrane and higher order facilities. Finally, we propose a higher-order Gamma which allows the definition of gamma-abstractions (in the same sense as $\lambda$-abstractions in the lambda-calculus) which are considered as first class citizens.

Rémi Douence, Pascal Fradet and Mario Südholt. A framework for the detection and resolution of aspect interactions. In Proceedings of Conference on Generative Programming and Component Engineering, GPCE'02, 2002. Springer-Verlag, LNCS, Vol. 2487.
Key-words: Aspect-oriented programming, formal model, static analysis, aspect interactions, aspect composition.

Abstract: Aspect-Oriented Programming (AOP) promises separation of concerns at the implementation level. However, aspects are not always orthogonal and aspect interaction is an important problem. Currently there is almost no support for the detection and resolution of such interactions. The programmer is responsible for identifying interactions between conflicting aspects and implementing conflict resolution code. In this paper, we propose a solution to this problem based on a generic framework for AOP. The contributions are threefold: we present a formal and expressive crosscut language, two static conflict analyses and some linguistic support for conflict resolution.

Jean-Pierre Banâtre, Pascal Fradet and Daniel Le Métayer. Gamma and the chemical reaction model: fifteen years after. In Multiset Processing. Springer-Verlag, LNCS, Vol. 2235, 2001.
Key-words: Chemical programming, survey, applications.

Abstract: Gamma was originally proposed in 1986 as a formalism for the definition of programs without artificial sequentiality. The basic idea underlying the formalism is to describe computation as a form of {\em chemical reaction} on a collection of individual pieces of data. Due to the very minimal nature of the language, and its absence of sequential bias, it has been possible to exploit this initial paradigm in various directions. This paper reviews most of the work around Gamma considered as a programming or as a specification language. A special emphasis is placed on unexpected applications of the chemical reaction model, showing that this paradigm has been a source of inspiration in various research areas.

Résumé : Par "approche langage" on entend désigner une approche qui s'exprime, soit dans un langage de programmation, soit par un langage de programmation.

Les approches qui s'expriment dans le langage ne font appel à aucun formalisme éloigné (e.g. sémantique). Le langage de programmation est l'unique cadre de travail pour exprimer le problème, le résoudre et appliquer la solution. Nous montrons  :

Thomas Colcombet and Pascal Fradet. Enforcing Trace Properties by Program Transformation. In Proc. of  Principles of Programming Languages, POPL'00, ACM Press, pp. 54-66, Boston, January 2000.
Key-words: Aspect-oriented programming, security policies, program transformation, static analysis, dynamic enforcement.

Abstract: We propose an automatic method to enforce trace properties on programs. The programmer specifies the property separately from the program; a program transformer takes the program and the property and automatically produces another ``equivalent'' program satisfying the property. This separation of concerns makes the program easier to develop and maintain. Our approach is both static and dynamic. It integrates static analyses in order to avoid useless transformations. On the other hand, it never rejects programs but adds dynamic checks when necessary. An important challenge is to make this dynamic enforcement as inexpensive as possible. The most obvious application domain is the enforcement of security policies. In particular, a potential use of the method is the securization of mobile code upon receipt.

Abstract: The mobile agent technology is emerging as a useful new way of building large distributed systems. The advantages of mobile agents over the traditional client-server model are mainly non-functional. We believe that one of the reasons preventing the wide-spread use of mobile agents is that non-functional properties are not easily grasped by system designers. Selecting the right interactions to implement complex services is therefore a tricky task. In this paper, we tackle this problem by considering efficiency and security criteria. We propose a language-based framework for the specification and implementation of complex services built from interactions with primitive services. Mobile agents, Rpc, remote evaluation, or any combination of these forms of interaction can be expressed in this framework. We show how to analyze (i.e. assess and compare) complex service implementations with respect to efficiency and security properties. This analysis provides guidelines to service designers, enabling them to systematically select and combine different types of protocols for the effective realization of interactions with primitive services.

Abstract: We propose a parallel specialized language that ensures portable and cost-predictable implementations on parallel computers. The language is basically a first-order, recursion-less, strict functional language equipped with a collection of higher-order functions or skeletons. These skeletons apply on (nested) vectors and can be grouped in four classes: computation, reorganization, communication, and mask skeletons. The compilation process is described as a series of transformations and analyses leading to SPMD-like functional programs which can be directly translated into real parallel code. The language restrictions enforce a programming discipline whose benefit is to allow a static, symbolic, and accurate cost analysis. The parallel cost takes into account both load balancing and communications, and can be statically evaluated even when the actual size of vectors or the number of processors are unknown. It is used to automatically select the best data distribution among a set of standard distributions. Interestingly, this work can be seen as a cross fertilization between techniques developed within the FORTRAN parallelization, skeleton, and functional programming communities.

Abstract: Consistency is a major issue that must be properly addressed when considering multiple view architectures. In this paper, we provide a formal definition of views expressed graphically using diagrams with multiplicities and propose a simple algorithm to check the consistency of diagrams. We also put forward a simple language of constraints to express more precise (intra-view and inter-view) consistency requirements. We sketch a complete decision procedure to decide whether diagrams satisfy a given constraint expressed in this language. Our framework is illustrated with excerpts of a case study: the specification of the architecture of a train control system. 

Abstract: In this position paper, we advocate the use of an aspect language for robust programming. AOP is particularly appealing for this task because robustness crosscuts traditional structuring means. Consider, for instance, the problem of ensuring that a global index remains in a given range. The code needed to check such an invariant is typically scattered all over the program. The paper presents an example-driven introduction of the proposed aspect language for program robustness; it then discusses its semantics and implementation and suggests extensions.

Abstract: We introduce a unified framework to describe, relate, compare and classify functional language implementations. The compilation process is expressed as a succession of program transformations in the common framework. At each step, different transformations model fundamental choices. A benefit of this approach is to structure and decompose the implementation process. The correctness proofs can be tackled independently for each step and amount to proving program transformations in the functional world. This approach also paves the way to formal comparisons by making it possible to estimate the complexity of individual transformations or compositions of them. Our study aims at covering the whole known design space of sequential functional languages implementations. In particular, we consider call-by-value, call-by-name and call-by-need reduction strategies as well as environment and graph-based implementations. We describe for each compilation step the diverse alternatives as program transformations. In some cases, we illustrate how to compare or relate compilation techniques, express global optimizations or hybrid implementations. We also provide a classification of well-known abstract machines.

Abstract: The Gamma language is based on the chemical reaction metaphor which has a number of benefits with respect to parallelism and program derivation. But the original definition of Gamma does not provide any facility for data structuring or for specifying particular control strategies. We address this issue by introducing a notion of structured multiset which is a set of addresses satisfying specific relations. The relations can be seen as a form of neighborhood between the molecules of the solution; they can be used in the reaction condition of a program or transformed by the action. A type is defined by a context-free graph grammar and a structured multiset belongs to a type T if its underlying set of addresses satisfies the invariant expressed by the grammar defining T. We define a type checking algorithm that allows us to prove mechanically that a program maintains its data structure invariant. We illustrate the significance of the approach for program refinement and we describe its application to coordination.

Abstract: What exactly are aspects? How to weave? What are the join points used to anchor aspects into the component program? Is there a general purpose aspect language? In this position paper, we address these questions for a particular class of aspects: aspects expressible as static, source-to-source program transformations. An aspect is defined as a collection of program transformations acting on the abstract syntax tree of the component program. We discuss the design of a generic framework to express these transformations as well as a generic weaver. The coupling of component and aspect definitions can be defined formally using operators matching subtrees of the component program. The aspect weaver is simply a fixpoint operator taking as parameters the component program and a set of program transformations. In many cases, program transformations based solely on syntactic criteria are not satisfactory and one would like to be able to use semantic criteria in aspect definitions. We show how this can be done using properties expressed on the semantics of the component program and implemented using static analysis techniques. One of our main concerns is to keep weaving predictable. This raises several questions about the semantics (termination, convergence) of weaving.

Abstract: Type systems currently available for imperative languages are too weak to detect a significant class of programming errors. For example, they cannot express the property that a list is doubly-linked or circular. We propose a solution to this problem based on a notion of shape types defined as context-free graph grammars. We define graphs in set-theoretic terms, and graph modifications as multiset rewrite rules. These rules can be checked statically to ensure that they preserve the structure of the graph specified by the grammar. We provide a syntax for a smooth integration of shape types in C. The programmer can still express pointer manipulations with the expected constant time execution and benefits from the additional guarantee that the property specified by the shape type is an invariant of the program. 

Abstract: The incorrect use of pointers is one of the most common source of bugs. As a consequence, any kind of static code checking capable of detecting potential bugs at compile time is welcome. This paper presents a static analysis for the detection of incorrect accesses to memory (dereferences of invalid pointers). A pointer may be invalid because it has not been initialized or because it refers to a memory location which has been deallocated. The analyzer is derived from an axiomatisation of alias and connectivity properties which is shown to be sound with respect to the natural semantics of the language. It deals with dynamically allocated data structures and it is accurate enough to handle circular structures.

Abstract: We present a method, adapted to polymorphically typed functional languages, to detect and collect more garbage than existing GCs. It can be applied to strict or lazy higher order languages and to several garbage collection schemes. Our GC exploits the information on utility of arguments provided by polymorphic types of functions. It is able to detect garbage that is still referenced from the stack and may collect useless parts of otherwise useful data structures. We show how to partially collect shared data structures and to extend the type system to infer more precise information. We also present how this technique can plug several common forms of space leaks.

Abstract: Functional language compilers implement only weak-head reduction. However, there are cases where head normal forms or full normal forms are needed. Here, we study how to use cps conversion for the compilation of head and strong reductions. We apply cps expressions to a special continuation so that their head or strong normal form can be obtained by the usual weak-head reduction. We remain within the functional framework and no special abstract machine is needed. Used as a preliminary step our method allows a standard compiler to evaluate under lambda's.

Abstract: We tackle the problem of detecting global variables in functional programs. We present syntactic criteria for single-threading which improves upon previous solutions (both syntactic and semantics-based) in that it applies to higher-order languages and to most sequential evaluation strategies. The main idea of our approach lies in the use of continuations. One advantage of continuation expressions is that evaluation ordering is made explicit in the syntax of expressions. So, syntactic detection of single-threading is simpler and more powerful on continuation expressions. We present the application of the analysis to the compilation of functional languages, semantics-directed compiler generation and globalization-directed transformations (i.e. transforming non-single-threaded expressions into single-threaded ones). Our results can also be turned to account to get single-threading criteria on regular lambda-expressions for different sequential evaluation orders.

Abstract: One of the most important issues concerning functional languages is the efficiency and the correctness of their implementation. We focus on sequential implementations for conventional von Neumann computers. The compilation process is described in terms of program transformations in the functional framework. The original functional expression is transformed into a functional term that can be seen as a traditional machine code. The two main steps are the compilation of the computation rule by the introduction of continuation functions and the compilation of the environment management using combinators. The advantage of this approach is that we do not have to introduce an abstract machine, which makes correctness proofs much simpler. As far as efficiency is concerned, this approach is promising since many optimizations can be described and formally justified in the functional framework.

These documents are provided by the contributing authors as a means to ensure timely dissemination of scholarly and technical work on a non-commercial basis. Copyright and all rights therein are maintained by the authors and by other copyright holders, notwithstanding that they have offered their works here electronically. It is understood that all persons copying this information will adhere to the terms and constraints invoked by each author's copyright. These works may not be reposted without the explicit permission of the copyright holder.