Search

This paper presents the formalisation of an object calculus in Isabelle/HOL highlighting the binder technique called locally nameless1. This techniques has its origins already in a note at the end of de Bruijn’s paper [5] introducing the classical de Bruijn indices. In the last few years, with the advent of mechanized proofs in the domain of programming languages, e.g. [1], this technique attracted new attention. The most recent work on locally nameless technique [2] provides cofinite quantification, necessary for proving non-trivial properties. Indeed the de Bruijn indices are often criticised, as being too technical, that is why alternative techniques are investigated. The de Bruijn indices method, however, is known to be reliable, and is often chosen in order to focus on aspects of programming languages unrelated to variable bindings. With locally nameless techniques, one expects to spend less time proving auxiliary lemmas dealing with variable bind- ings, but also to obtain theorems that are more convincing because closer to the paper version. Our contributions are a formalisation in Isabelle/HOL of ς-calculus; and an in depth comparison of both locally nameless and de Bruijn complete mechanisations including specification and proofs.

International audience; We study deadlock detection in an actor model with wait-by-necessity synchronizations, a lightweight technique that synchronizes invocations when the corresponding values are strictly needed. This approach relies on the use of futures that are not given an explicit " Future " type. The approach we adopt allow the implicit synchronization on the availability of some value (where the producer of the value might be decided at runtime), whereas previous work allowed only explicit synchronization on the termination of a well-identified request. This way we are able to analyse the data-flow synchronization inherent to languages that feature wait-by-necessity. We provide a type-system and a solver inferring the type of a program so that deadlocks can be identified statically. As a consequence we can automatically verify the absence of deadlocks in actor programs with wait-by-necessity synchronizations.

This thesis is related to the dynamic adaptation problem in the context ofcomponent-based applications. Dynamic adaptation, in this context, is the ability to change a component system at runtime without stopping it completely. Many real component systems are critica! and can not indeed be really stopped, and their maintenance is very costly. For example, there are applications for which their adaptation must be realized with mínimum perturbation, like banking applications, or like routing Internet applications. There are various reasons for adapting a system, for example:• The behaviour of the system is not correct, then it is necessary to identify and change the components which are defectives for a new version ofthose components. The new version of the components must ha ve the same functionalities ofthe old version, but with a corrected behaviour.• The behaviour is correct but the original environment or rules have changed, then the system must be adapted to the new execution environment. Thesystem changes the components needed so that the application can behavewell under the new conditions.• The system needs new functionalities that were not considered in the conception of the system. The system must add the extensions associated to thosefunctionalities, it can add new components or change old components into new components with new functionalities.• The behaviour is correct, but the performance ofthe system is poor. Then the system needs to be optimized for improving its performance.It is very difficult to know at conception time all the problems that a system can have during its lifetime. Adaptation of a system is, thus, an essential point to consider if the system must run for a long time. The very general context ofthis thesis is components models. Indeed, the OASIStcam is highly involved in the design of a Grid Component Model (GCM), whichconsists in a Grid-oriented extension of the Fractal component model. The OASIS team is developing a distributed implementation of Fractal (overProActive- a Java library for distributed computing), together with model checkingtools adapted to those components systems. ProActive/Fractal implementationmerges the notions of active objects and Fractal components, yielding to a distributed component framework having a single thread for each component.Component models provide a structured programming paradigm, and ensure abetter re-usability of programs. Indeed application dependencies are defined togcther with provided functionalities by the mean of provided/required ports; thisimproves the program specification and thus its re-usability. In distributed systems, this takes even more importance as the structure of components can also be used at runtime to discover services or adapt component behaviour. Several effective distributed component models have been specified, developed, and implemented in the last years [27; 90; 10; 6] ensuring different kinds ofproperties to their users. To beable to prove such properties, one must rely on sorne well defined semantics for the underlying programming language or middleware. We rely here on a model for distributed components. This model is based on one key principie: Components are the unit of concurrency. More precisely, components only communicate by sending requests or results for those requests. We say that this model is asynchronous because requests can be treated in an asynchronous manner thanks to the introduction offutures (place-holders for request results). Inorder to prevent other communications or concurrency to occur, we require thatcomponents do not share memory, which ensures that components really are theconcurrency unit. From a computational point ofview, components are loosely coupled: the only strong synchronisation consists in waiting for the result of a request, and can be performed only when and where this result is really needed thanks to the use of futures. Such componcnts can then provide a convenient abstraction for distribution:each component can be placed on a different (virtual) machine. Indeed, the abstractions suggested above imply that each memory location is only accessible by one component, and thus it is easy to place each component on a different independent location. This makes our component model adapted to distribution.In general for component programming, but even more specifically in distributedand Grid environments, components need to be highly adaptative. A great part ofadaptativeness relies on dynamic reconfiguration of component systems. Fractal predefines basic controllers that should be present in most of Fractal components. We are interested here in binding, life-cycle, and content controllers. The primitivesproposed in Fractal are expressive enough for encoding any reconfiguration,but they are situated ata rather low-level and they were done for non distributed systems. Reconfigurations and all other aspects defined by component controllers are called non-functional. Doctor en Ciencias TERMINADA PFCHA-Becas 144p. PFCHA-Becas

International audience; This article presents an extension of the Fractal component model targeted at programming applications to be run on computing grids: the Grid Component Model (GCM). First, to address the problem of deployment of components on the Grid, deployment strategies have been defined. Then, as Grid applications often result from the composition of a lot of parallel (sometimes identical) components, composition mechanisms to support collective communications on a set of components are introduced. Finally, because of the constantly evolving environment and requirements for Grid applications, the GCM defines a set of features intended to support component autonomicity. All these aspects are developed in this paper with the challenging objective to ease the programming of Grid applications, while allowing GCM components to also be the unit of deployment and management.