Abstracts

Adnan Bouakaz, Pascal Fradet and Alain Girault. Symbolic Buffer Sizing for Throughput-Optimal Scheduling of Dataflow Graphs. In Proc. of  Real-Time Embedded Technology & Applications Symposium, RTAS'16, April 2016.
Key-words: Dataflow programming, parametric model, symbolic analyses, throughput, buffer size.

Abstract: The synchronous dataflow model is widely used to design real-time streaming applications which must assure a minimum quality-of-service. A benefit of that model is to allow static analyses to predict and guarantee timing (e.g., throughput) and buffering requirements of an application. Performance analyses can either be performed at compile time (for design space exploration) or at run-time (for resource management and reconfigurable systems). However, these algorithms, which often have an exponential time complexity, may cause a huge runtime overhead or make design space exploration unacceptably slow. In this paper, we argue that symbolic analyses are more appropriate since they express the system performance as a function of parameters (i.e., input and output rates, execution times). Such functions can be quickly evaluated for each different configuration or checked w.r.t. many different non-functional requirements. We first provide a symbolic expression of the maximal throughput of acyclic synchronous dataflow graphs. We then perform an analytic and exact study of the minimum buffer sizes needed to achieve this maximal throughput for a single parametric edge graph. Based on these investigations, we define symbolic analyses that approximate the minimum buffer sizes needed to achieve maximal throughput for acyclic graphs. We assess the proposed analyses experimentally on both synthetic and real benchmarks.

Adnan Bouakaz, Pascal Fradet and Alain Girault. Symbolic Analysis of Dataflow Graphs (extended version), INRIA Research Report  nº 8742, January 2016.
Key-words: Dataflow programming, parametric model, symbolic analyses, throughput, buffer size, latency.

Abstract: Synchronous dataflow graphs are widely used to design digital signal processing and real-time streaming applications. A benefit of that model is to allow static analyses to predict and guarantee the performances (e.g., throughput, memory requirements) of an application. Performance analyses can either be performed at compile time (for design space exploration) or at run-time (for resource management and reconfigurable systems). However, these algorithms, which often have an exponential time complexity, may cause a huge run-time overhead or make design space exploration unacceptably slow. In this paper, we argue that symbolic analyses are more appropriate since they express the system performance as a function of parameters (i.e., input and output rates, execution times). Such functions can be quickly evaluated for each different configuration or checked w.r.t. many different non-functional requirements. We first provide a symbolic expression of the maximal throughput of acyclic synchronous dataflow graphs. We then perform an analytic and exact study of the minimum buffer sizes needed to achieve this maximal throughput for a single parametric edge graph. Based on this investigation, we define symbolic analyses that approximate the minimum buffer sizes needed to achieve maximal throughput for acyclic graphs. We assess the proposed analyses experimentally on both synthetic and real benchmarks.

Dmitry Burlyaev and Pascal Fradet.  Formal Verification of Automatic Circuit Transformations for Fault-Tolerance. In Proc. of Formal Methods in Computer-Aided Design, FMCAD'15, September 2015.
Key-words: Fault-tolerance, time redundancy, circuit transformation, semantics, certification, Coq.

Abstract: We present a language-based approach to certify fault-tolerance techniques for digital circuits. Circuits are expressed in a gate-level Hardware Description Language (HDL), fault-tolerance techniques are described as automatic circuit transformations in that language, and fault-models are specified as particular semantics of the HDL. These elements are formalized in the Coq proof assistant and the properties, ensuring that for all circuits their transformed version masks all faults of the considered fault-model, can be expressed and proved. In this article, we consider Single-Event Transients (SETs) and faultmodels of the form “at most 1 SET within k clock cycles”. The primary motivation of this work was to certify the Double-Time Redundant Transformation (DTR), a new technique proposed recently. The DTR transformation combines double-time redundancy, micro-checkpointing, rollback, several execution modes and input/output buffers. That intricacy requested a formal proof to make sure that no single-point of failure existed. The correctness of DTR as well as two other transformations for fault-tolerance (TMR & TTR) have been proved in Coq.

Dmitry Burlyaev, Pascal Fradet and Alain Girault. Time-redundancy transformations for adaptive fault-tolerant circuits. In Proc. of NASA/ESA Conference on Adaptive Hardware and Systems, AHS'15, June 2015.
Key-words: Fault-tolerance, single-event transient, circuit transformation, time redundancy, dynamic redundancy.

Abstract: We present a novel logic-level circuit transformation technique for the automatic insertion of fault-tolerance properties. The transformations, based on time-redundancy, allow dynamically changes of the level of redundancy without interrupting the computation. The proposed concept of dynamic time redundancy permits adaptive circuits whose fault-tolerance properties can be ”on-the-fly” traded-off for throughput. The approach is technologically independent and does not require any specific hardware support. Experimental results on the ITC’99 benchmark suite indicate that the benefits of our method grow with the combinational size of the circuit. Dynamic double and triple time redundant transformations generate circuits 1:7 to 2:9 times smaller than full Triple-Modular Redundancy (TMR). This transformation is a good alternative to TMR for logicintensive safety-critical circuits where low hardware overhead or only temporary fault-tolerance guarantees are needed.

Dmitry Burlyaev, Pascal Fradet and Alain Girault.  Automatic Time-Redundancy Transformation for Fault-Tolerant Circuits. In Proc. of International Symposium on Field-Programmable Gate Arrays, FPGA'15, February 2015.
Key-words: Fault-tolerance, single-event transient, circuit transformation, time redundancy, check-pointing.

Abstract: We present a novel logic-level circuit transformation technique for automatic insertion of fault-tolerance properties. Our transformation uses double-time redundancy coupled with micro-checkpointing, rollback and a speedup mode. To the best of our knowledge, our solution is the only technologically independent scheme capable to correct the multiple bit-flips caused by a Single-Event Transient (SET) with double-time redundancy. The approach allows soft-error masking (within the considered fault-model) and keeps the same input/output behavior regardless error occurrences. Our technique trades-o the circuit throughput for a small hardware overhead. Experimental results on the ITC'99 benchmark suite indicate that the bene fits of our methods grow with the combinational size of the circuit. The hardware overhead is 2.7 to 6.1 times smaller than full Triple Modular Redundancy (TMR) with double loss in throughput. We do not consider con figuration memory corruption and our approach is readily applicable to Flash-based FPGAs. Our method does not require any specifi c hardware support and is an interesting alternative to TMR for logic intensive designs.

Vagelis Bebelis, Pascal Fradet and Alain Girault. A framework to schedule parametric dataflow applications on many-core platforms. In Proc. of the Conference on Languages,Compilers and Tools for Embedded Systems, LCTES'14, June 2014.
Key-words: Dataflow programming, parametric model, quasi-static scheduling.

Abstract: Dataflow models, such as SDF, have been effectively used to program streaming applications while ensuring their liveness and boundedness. Yet, industrials are struggling to design the next generation of high definition video applications using these models. Such applications demand new features such as parameters to express dynamic input/output rate and topology modifications. Their implementation on modern many-core platforms is a major challenge. We tackle these problems by proposing a generic and flexible framework to schedule streaming applications designed in a parametric dataflow model of computation. We generate parallel as soon as possible (ASAP) schedules targeted to the new STHORM many-core platform of STMicroelectronics. Furthermore, these schedules can be customized using user-defined ordering and resource constraints. The parametric dataflow graph is associated with generic or user-defined specific constraints aimed at minimizing timing, buffer sizes, power consumption, or other criteria. The scheduling algorithm executes with minimal overhead and can be adapted to different scheduling policies just by adding some constraints. The safety of both the dataflow graph and constraints can be checked statically and all schedules are guaranteed to be bounded and deadlock free. We illustrate the scheduling capabilities of our approach using a real world application: the VC-1 video decoder for high definition video streaming.

Dmitry Burlyaev, Pascal Fradet and Alain Girault. Verification-guided Voter Minimization in Triple-Modular Redundant Circuits. In Proc. of Design, Automation and Test in Europe Conference and Exhibition, DATE’14, 2014.
Key-words: Fault-tolerance, digital circuits, triple modular redundancy, voting, static analysis, optimization.

Abstract: We present a formal approach to minimize the number of voters in triple-modular redundant sequential circuits. Our technique actually works on a single copy of the circuit and considers a user-defined fault model (under the form “at most 1 bit-flip every k clock cycles”). Verification-based voter minimization guarantees that the resulting circuit (i) is fault tolerant to the soft-errors defined by the fault model and (ii) is functionally equivalent to the initial one. Our approach operates at the logic level and takes into account the input and output interface specifications of the circuit. Its implementation makes use of graph traversal algorithms, fixed-point iterations, and BDDs. Experimental results on the ITC’99 benchmark suite indicate that our method significantly decreases the number of inserted voters which entails a hardware reduction of up to 55% and a clock frequency increase of up to 35% compared to full TMR. We address scalability issues arising from formal verification with approximations and assess their efficiency and precision.

Vagelis Bebelis, Pascal Fradet, Alain Girault and Bruno Lavigueur. BPDF: A Statically Analyzable Dataflow Model with Integer and Boolean Parameters. In International Conference on Embedded Software, EMSOFT’13, September 2013.
Key-words: Dataflow programming, parametric model, boundedness, liveness, dynamic reconfiguration.

Abstract: Dataflow programming models are well-suited to program many-core streaming applications. However, many streaming applications have a dynamic behavior. To capture this behavior, parametric dataflow models have been introduced over the years. Still, such models do not allow the topology of the dataflow graph to change at runtime, a feature that is also required to program modern streaming applications. To overcome these restrictions, we propose a new model of computation, the Boolean Parametric Data Flow (BPDF) model which combines integer parameters (to express dynamic rates) and boolean parameters (to express the activation and deactivation of communication channels). High dynamism is provided by integer parameters which can change at each basic iteration and boolean parameters which can even change within the iteration. The major challenge with such dynamic models is to guarantee liveness and boundedness. We present static analyses which ensure statically the liveness and the boundedness of BDPF graphs. We also introduce a scheduling methodology to implement our model on highly parallel platforms and demonstrate our approach using a video decoder case study.

Vagelis Bebelis, Pascal Fradet, Alain Girault and Bruno Lavigueur. BPDF: Boolean Parametric Data Flow. INRIA Reseach Report nº 8333, July 2013.
Key-words: Dataflow model of computation, dynamicity, parameters, liveness, boundedness, scheduling.

Abstract: Dataflow programming models are well-suited to program many-core streaming applications. However, many streaming applications have a dynamic behavior. To capture this behavior, parametric dataflow models have been introduced over the years. Still, such models do not allow the topology of the dataflow graph to change at runtime, a feature that is also required to program modern streaming applications. To overcome these restrictions, we propose a new model of computation, the Boolean Parametric Data Flow (BPDF) model which combines integer parameters (to express dynamic rates) and boolean parameters (to express the activation and deactivation of communication channels). High dynamicity is provided by integer parameters which can change at each basic iteration and boolean parameters which can even change within the iteration. The major challenge with such dynamic models is to guarantee liveness and boundedness. We present static analyses which ensure statically the liveness and the boundedness of BDPF graphs. We also introduce a scheduling methodology to implement BPDF graphs on highly parallel platforms. Finally, we demonstrate our approach using a video decoder case study.

Pascal Fradet, Alain Girault and Peter Poplavko. SPDF: A Schedulable Parametric DataFlow MoC. In Proc. of Design, Automation and Test in Europe Conference and Exhibition, DATE’12, March 2012.
Key-words:
dataflow programming, parametric rates, boundedness, liveness, quasi-static scheduling.

Abstract: Dataflow programming models are suitable to express multi-core streaming applications. The design of high quality embedded systems in that context requires static analysis to ensure the liveness and bounded memory of the application. However, many streaming applications have a dynamic behavior. The previously proposed dataflow models for dynamic applications do not provide any static guarantees or only in exchange of significant restrictions in expressive power or automation. To overcome these restrictions, we propose the schedulable parametric dataflow (SPDF) model. We present static analyses and a quasi-static scheduling algorithm. We demonstrate our approach using a video decoder case study.

Simplice Djoko Djoko, Rémi Douence, Pascal Fradet. Aspects preserving properties. In Science of Computer Programming, SCP,  vol. 77, no 3, p. 393-422, July 2012. (preprint version: )
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. Specialized aspect languages are 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, confiners and weak intruders. 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. Weak intruders are confiners between two advice executions. These categories (along with two others) are defined formally 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 w.r.t. a common imperative base language. Each category and language is illustrated by simple examples. The appendix provides semantics and two instances 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

Pascal Fradet, Alain Girault and Peter Poplavko. SPDF: A Schedulable Parametric DataFlow MoC (extended version). INRIA Reseach Report nº 7828, December 2011.
Key-words:
dataflow programming, parametric rates, boundedness, liveness, quasi-static scheduling.

Abstract: Dataflow programming models are suitable to express multi-core streaming applications. The design of high-quality embedded systems in that context requires static analysis to ensure the liveness and bounded memory of the application. However, many streaming applications have a dynamic behavior. The previously proposed dataflow models for dynamic applications do not provide any static guarantees or only in exchange of significant restrictions in expressive power or automation. To overcome these restrictions, we propose the schedulable parametric dataflow (SPDF) model of computation. We present static analyses and a quasi-static scheduling algorithm. We demonstrate our approach using a video decoder case study.

Pascal Fradet , Jean-Louis Giavitto and Marnes Hoff. Refinement of Chemical Programs using Strategies. In International Workshop on Strategies in Rewriting, Proving, and Programming, IWS’2010, July 2010.
Key-words: Chemical programming, program refinement.

Abstract: The chemical reaction metaphor describes computation in terms of a chemical solution where molecules interact freely according to reaction rules. Chemical solutions are represented by multisets of elements and reactions by rewrite rules which consume and produce new elements according to conditions. A major drawback is that a reasonably efficient implementation of the language is not straightforward. The sources of inefficiency are the selection of elements and the ordering of reactions which are left completely unspecified. Further, the lack of structured data makes it difficult to specify them. The approach sketched in this abstract aims at refining gamma programs by:

•  structuring the multiset using a data type defining neighborhood relations between elements;
•  describing the selection of elements according to their neighborhood and the previous selection;
•  specifying the evaluation strategy (i.e., the application of rules and termination).

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 and 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 w.r.t. 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 and 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.

Tolga Ayav, Pascal Fradet and Alain Girault. Implementing Fault-Tolerance by Automatic Program Transformations. In ACM Transactions on Embedded Computing Systems, TECS, (to appear). (preprint version: )
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 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.

Pascal Fradet and Stéphane Hong Tuan Ha. Aspects of Availability. In Proc. of the Sixth International Conference on Generative Programming and Component Engineering, GPCE'07, Pages 165-174, Octobre 2007.
Key-words: Aspect-oriented programming, resource management, availability, verification, denial of service.

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.

Massimo Tivoli, Pascal Fradet, Alain Girault and Gregor Goessler. Adaptor Synthesis for Real-Time Components. In Tools and Algorithms for the Construction and Analysis of Systems, 13th International Conference, TACAS'07, Lecture Notes in Computer Science, Volume 4424, Pages 185-200, 2007.
Key-words: Components, real-time, assembly, adaptation, Petri nets.

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.

Pascal Fradet and Ralf Lämmel (editors). Special Issue on Foundations of Aspect-Oriented Programming, Science of Computer Programming, december 2006, Elsevier. (guest editors' introduction )
Key-words: Aspect-oriented programming, foundations, semantics, typing, core aspect languages

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).

Tolga Ayav, Pascal Fradet and Alain Girault. Implementing Fault-Tolerance in Real-Time Systems by Program Transformations. In Proc. of the Sixth ACM & IEEE International Conference on Embedded Software, EMSOFT'06, pages 205-214, 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.

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.

Pascal Fradet. Approches langages pour la conception et la mise en œuvre de programmes. Document d'habilitation à diriger les recherches. Université de Rennes I, 129 pages, novembre 2000.
Mots clés : Langages  (fonctionnels, impératifs, dédiés, d'aspects), compilation, transformation, typage, analyse.

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  :

• comment la compilation des langages fonctionnels peut s'exprimer dans le langage lui-même par transformation de programme. Ce cadre unifié permet de décrire, prouver, comparer et classifier la plupart des mises en œuvre de langages fonctionnels,
• deux optimisations de l'implémentation des langages fonctionnels (une analyse de globalisation et un GC étendu) qui reposent sur la syntaxe et le type des expressions.
Pour les approches qui s'expriment par un langage de programmation, il s'agit de prévenir le problème ou d'assurer une propriété via l'utilisation d'un langage (ou d'une discipline de programmation). Nous illustrons ce style d'approche par trois exemples :
• les types graphes qui permettent de définir et vérifier le partage des structures de données à pointeurs,
• un langage dédié au parallélisme qui garantit une analyse de coût précise et un choix automatique de la meilleure distribution,
• un style de programmation par aspects qui permet d'imposer automatiquement des propriétés aux programmes.

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.

Pascal Fradet, Valérie Issarny, and Siegfried Rouvrais. Analyzing non-functional properties of mobile agents. In Proc. of Fundamental Approaches to Software Engineering, FASE'00, LNCS, Mars 2000.
Key-words: Mobile agents, RPC, performance, security.

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.

Pascal Fradet and Julien Mallet. Compilation of a Specialized Functional Language for Massively Parallel Computers. In Journal of Functional Programming, JFP, 10(6), pp. 561-605, 2000.
Key-words: Skeletons, polytopes, data parallelism, cost analysis, program transformation.

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.

Pascal Fradet, Daniel Le Métayer and Michaël Périn. Consistency checking for multiple view software architectures. In Proc. of the Joint European Software Engineering Conference and Symp. on Foundations of Software Engineering, ESEC/FSE'99,  Software Engineering Notes 24 (6) or LNCS Vol 1687 pp. 410-428, 1999.
Key-words: Software architecture, multiple views, consistency, UML diagrams.

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.

Pascal Fradet and Mario Südholt. An aspect language for robust programming,  In Int. Workshop on Aspect-Oriented Programming, ECOOP, June 1999.
Key-words: Aspect-oriented programming, robustness, exceptions, program transformation, program analysis.

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.

Rémi Douence and Pascal Fradet. A systematic study of functional language implementations. In ACM Transactions on Programming Languages and Systems, TOPLAS, 20(2), pp. 344-387, 1998.   [ACM library version]
Key-words: Compilation, optimizations, program transformation, abstract machines, lambda-calculus, combinators.

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.

Pascal Fradet and Daniel Le Métayer. Structured Gamma. In Science of Computer Programming, SCP, 31(2-3), pp. 263-289, 1998.
Key-words: Multiset rewriting, graph types, type checking, refinement.

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.

Pascal Fradet and Mario Südholt, Towards a Generic Framework for Aspect-Oriented Programming. In Third AOP Workshop, ECOOP'98 Workshop Reader, LNCS, Vol. 1543, pp. 394-397, July 1998.
Key-words: Aspect-oriented programming, program transformation, program analysis.

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.

Pascal Fradet and Daniel Le Métayer , Shape Types. In Proc. of Principles of Programming Languages, POPL'97, ACM Press, pp. 27-39, Paris, January 1997.
Key-words: Pointer data structures, pointer manipulation, graph grammars, type checking, program robustness, C.

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.

Ronan Gaugne , Pascal Fradet and Daniel Le Métayer , Static Detection of Pointer Errors: an Axiomatisation and a Checking Algorithm. In Proc. European Symposium on Programming, ESOP'96, LNCS, 1996.
Key-words: Debugging tool, alias analysis, Hoare's logic.

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.

Pascal Fradet, Collecting More Garbage. In Proc. of ACM Conf. on Lisp and Functional Programming, LISP'94, ACM Press, pp. 24-33, Orlando, FL, USA, June 1994.
Key-words: Garbage collection, space leaks, typing, parametricity.

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.

Pascal Fradet, Compilation of Head and Strong Reduction. In Proc of the 5th European Symposium on Programming , ESOP'94, LNCS Vol 788, pp. 211-224, Edinburgh, UK, April 1994.
Key-words: Lambda-calculus, continuations, strong reduction, head reduction, compilation.

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.

Pascal Fradet, Syntactic Detection of Single-Threading Using Continuations. In Proc. of the 5th ACM Conf. on Functional Prog. Lang. and Comp. Arch., FPCA'91,  LNCS VOL. 523, pp. 241-258, Cambridge, MA, USA, August 1991.
Key-words: Globalization, single-threading, in-place update, CPS conversion.

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.

P. Fradet and Daniel Le Métayer. Compilation of functional languages by program transformation. In ACM Transactions on Programming Languages and Systems, TOPLAS, 13(1), pp. 21-51, 1991.
Key-words: Functional programming, compilation, continuations, program transformation, lambda-calculus, combinators.
[ACM library version]

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.

Disclaimer:

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.