Rim Abid

Gwen Salaün

Noel De Palma

Soguy Mak

Kare Gueye

Asynchronous Coordination of Stateful Autonomic Managers in the Cloud

Cloud computing is now an omnipresent paradigm in modern programming. Cloud applications usually consist of several software components deployed on remote virtual machines. Managing such applications is a challenging problem because manual administration is no longer realistic for these complex distributed systems. Thus, autonomic computing is a promising solution for monitoring and updating these applications automatically. This is achieved through the automation of administration functions and the use of control loops called autonomic managers. An autonomic manager observes the environment, detects changes, and reconfigures dynamically the application. Multiple autonomic managers can be deployed in the same system and must make consistent decisions. Using them without coordination may lead to inconsistencies and error-prone situations. In this paper, we present our approach for coordinating stateful autonomic managers, which relies on a simple coordination language, new techniques for asynchronous controller synthesis and Java code generation. We used our approach for coordinating real-world cloud applications.

Introduction

Autonomic computing [START_REF] Huebscher | A Survey of Autonomic Computing Degrees, Models and Applications[END_REF] is increasingly used to solve complex systems, since it reduces human errors [START_REF] Kephart | The Vision of Autonomic Computing[END_REF]. It has become popular especially in cloud applications where the management is a crucial feature. Autonomic computing is based on the use of autonomic managers [START_REF] Kephart | Research Challenges of Autonomic Computing[END_REF]. An autonomic manager is built as a control loop. It observes the application execution, ensures a continuous monitoring, and reacts to events and changes by automatically reconfiguring the application. The increasing complexity of cloud applications implies the use of various and heterogeneous autonomic managers, such as self-healing and self-protecting [START_REF] Buyya | Autonomic Cloud Computing: Open Challenges and Architectural Elements[END_REF], with the objective to reconfigure automatically themselves.

When multiple autonomic managers monitor the same system, they should take globally coherent decisions. Hence, a manager should be aware of decisions of other managers before reacting. When it reacts without taking into account decisions of other managers handling the same application, error-prone situations may occur (e.g., removing a server that will be needed). In order to avoid performance degradation and system consistency problems, and also to limit energy consumption it is necessary to coordinate all autonomic managers.

In this paper, we present our approach, whose main goal is to synthesize a controller that monitors and orchestrates the reconfiguration operations of the involved managers. The controller also prevents a manager from violating global objectives of the managers. All participants involved in the application interact asynchronously with the controller and messages are stored/consumed into/from FIFO buffers.

More precisely, an autonomic manager is described using a formal model, namely a Labelled Transition System (LTS). We used reaction rules and regular expressions to specify coordination requirements and interaction constraints. As a consequence, each manager is not only able to manage its internal behaviour but also its relationship with other autonomic managers, which is achieved in accordance with the specification of the coordination requirements. As shown in Figure 1, we propose controller synthesis techniques for asynchronously communicating managers. These techniques rely on an encoding of our inputs (LTS models and coordination requirements) into the LNT process algebra [START_REF] Champelovier | Reference Manual of the LOTOS NT to LOTOS Translator (Version 5.4)[END_REF]. LNT is one of the input languages of the CADP toolbox [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], a state-of-the-art verification toolbox for concurrent systems. CADP compilers and minimization tools are particularly useful for generating a reduced LTS from the LNT specification. The generated LTS corresponds to all possible executions of the controller. It is worth noting that since we rely on formal techniques and tools, all the verification techniques available in the CADP toolbox can be used for validating the generated controller.

Once we have synthesized the controller LTS, Java code is generated using a code generator we developed. This Java code is finally deployed and used for coordinating real applications. We validated our approach on several variants of a N-tier Web application involving several autonomic managers, such as self-sizing or self-repair managers. We emphasize that our approach covers the whole development process from expression of the requirements to the final implementation and deployment of the solution. The rest of this paper is structured as follows. In Section 2, we introduce our formal model for autonomic managers, the coordination language, and our running example (a multi-tier Web application). In Section 3, we present our synthesis techniques that mainly rely on an encoding into process algebra and on LTS manipulations. Section 4 introduces the code generation techniques for obtaining Java code from controller models. We discuss related work in Section 5 and we conclude in Section 6.

Models

In this section, we first present the abstract model used to represent autonomic managers. In a second step, we introduce reaction rules and regular expressions for specifying how the involved managers are supposed to interact together. Manager models and coordination expressions are used as input to our synthesis techniques (Section 3). At the end of this section, we introduce a typical example of distributed cloud application that we use as running example.

Autonomic Manager

Each autonomic manager is modelled as a Labelled Transition System, which is defined as follows: Definition 1. A Labelled Transition System (LTS) is a tuple defined as LT S = (Q, A, T, q 0 ) where Q is a finite set of states, A = A ! ∪ A ? is an alphabet partitioned into a set of send and receive messages, T ⊆ Q × A × Q is the transition relation, and q 0 is the initial state.

We write m! for a send message m ∈ A ! and m? for a receive message m ∈ A ? . A transition is represented as q l -→ q ∈ T where l ∈ A. We assume that managers are deterministic, which can be easily obtained using standard determinization algorithms [START_REF] Hopcroft | Introduction to Automata Theory, Languages and Computation[END_REF]. Given a set of manager LTSs (Q i , A i , T i , q 0 i ), we assume that each message has a unique sender and a unique receiver: ∀i, j ∈ 1..n, i = j, A ! i ∩ A ! j = ∅ and A ? i ∩ A ? j = ∅. Furthermore, each message is exchanged between two different managers: A ! i ∩ A ? i = ∅ for all i. Uniqueness of messages can be achieved via renaming.

Coordination Requirements

In order to coordinate multiple autonomic managers, we use reaction rules and regular expressions with their basic operators (sequence, choice, iteration) to describe the behaviour one expects from the controller. The generated controller aims at orchestrating the execution of the managers. A reaction rule consists of a set of receptions followed by a set of emissions. Basically, it expresses that when the controller receives a set of messages from managers within a certain period of time (left hand part), it must send all the messages specified in the second set (right hand part) once the period is expired. Note that the real period will be chosen during the deployment phase and both sets of actions can be received and emitted in any order. Definition 2. Given a set of managers {M 1 , . . . , M n } with M i = (Q i , A i , T i , q 0 i ), a reaction rule R is defined as a 1 , ..., a m → b 1 , ..., b p where a j ∈ A ?

i and b k ∈ A ! i for 1 j m and 1 k p.

The specification of the behaviour one expects from the controller is expressed using a coordination expression. Definition 3. A coordination expression C is a regular expression over reaction rules R:

C ::= R | C 1 .C 2 | C 1 + C 2 | C * where C 1 .C 2 is a coordination expression C 1 followed by C 2 , C 1 + C 2 is a choice between C 1 and C 2 ,
and C * is a repetition of C zero or several times.

It is worth noting that all participants, namely the autonomic managers and the controller to be generated, communicate asynchronously using message passing via FIFO buffers. Each participant is equipped with one input buffer. Therefore, it consumes messages from its buffer and sends messages to the input buffer of the message recipient. Once generated and added to the system, all managers communicate through the controller, which means that the controller acts as a centralized orchestrator for the whole system.

Running Example

Our running example is a JEE multi-tier application (Fig. 2) composed of an Apache Web server, a set of replicated Tomcat servers, a MySQL proxy server, and a set of replicated MySQL databases. The Apache server receives incoming requests and distributes them to the replicated Tomcat servers. The Tomcat servers access the database through the MySQL proxy server that distributes fairly the SQL queries to a tier of replicated MySQL databases.

Fig. 2. A multi-tier application

The autonomic manager architecture is based on the MAPE-K (Monitor Analyse Plan Execute -Knowledge) reference model [START_REF] Huebscher | A Survey of Autonomic Computing Degrees, Models and Applications[END_REF]. We describe this architecture using several LTS models. First, we model the behaviour of the monitor, analyse, and execute functions of the managers by what we call the application manager (Fig. 3, right), which sends messages when a change occurs in the system and receives messages indicating actual administrative changes to perform on the application. As for the plan functions, we use two models called self-sizing and self-repair managers, resp. The self-sizing manager (Fig. 3, middle) is in charge of adapting dynamically the number of replicated servers by sending the message add! (remove!, resp.) to the system when detecting an overload (underload, resp.). The overload (underload, resp.) is detected when the average of the load exceeds (is under, resp.) a maximum (minimum, resp.) threshold. We associate one instance of the self-sizing manager to the Tomcat servers and another instance to the MySQL databases. The self-repair manager (Fig. 3, left) asks the system to repair a failure by creating a new instance of the failed server. We have four instances of the self-repair manager, one per tier. The absence of coordination between these managers may lead the whole system to some undesired situation such as adding two new servers whereas one was enough as a result of a server failure. More precisely, when the self-repair manager repairs a failure, the other replicated servers receive more requests than before the failure, which causes an overload and therefore the addition of another (unnecessary) server by the self-sizing manager.

We present below an excerpt of the requirements for the controller we want to generate for our running example. These rules ensure that all managers globally satisfy the coordination objectives. Each line presents the actions that can be received by the controller in a period T (left parts of reactions rules). At the end of each period, if the received messages match the left part of one fireable rule, it reacts by emitting the messages appearing in the right part of that rule. All messages are prefixed by the manager name (app stands for the application manager) and suffixed by the name of the tier to which is associated the manager.

( app_failure_apache? -> repair_failure_apache! ()

+ app_overload_tomcat? -> sizing_overload_tomcat! ()
+ app_failure_apache?, app_underload_tomcat?-> repair_failure_apache!() + app_failure_tomcat?, app_overload_tomcat? -> repair_failure_tomcat!()

+ ... ) *
We distinguish two kinds of rules: (1) those where a unique message appears in the left part of the reaction rule (see, e.g., , ). In that case, the corresponding controller immediately transfers that message to the manager; (2) those encoding the coordination we want to impose on managers, e.g., rule permits to generate a controller that can avoid to add two Tomcat servers by forwarding only one of the two received messages on a same period of time. Last, since there is no specific order between all these rules, we use a simple regular expression where all rules can be fired at any time (combination of + and * operators).

Synthesis

In this section, we present our asynchronous controller synthesis techniques, which rely on an encoding of our models and of the coordination requirements into the LNT specification language. From this LNT specification, we can generate the corresponding LTS model using CADP compilers, hiding, and reduction techniques. Validation of the generated controller is also possible using CADP verification tools. This section ends with an illustration of all these techniques on our running example. All the steps presented in this section are fully automated by a tool that we developed in Python. This tool generates the LNT code as well as SVL scripts [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF] that are used for invoking CADP exploration and reduction tools, which finally results in the generation of the controller LTS.

Process Algebra Encoding

The backbone of our solution is an encoding of all managers and of the coordination requirements into the LNT process algebra. The choice of LNT is motivated by several reasons. First, LNT is an expressive behavioural specification language which has a user-friendly syntax and provides expressive operators. Second, LNT is supported by CADP [START_REF] Garavel | CADP 2011: A Toolbox for the Construction and Analysis of Distributed Processes[END_REF], a toolbox that contains optimized state space exploration techniques and verification tools. CADP tools allow to compile the LNT specification into an LTS, which enumerates all the possible executions of the corresponding specification. Third, CADP is a verification toolbox dedicated to asynchronous systems consisting of concurrent processes interacting via message passing. It provides many tools that can be used to make different kinds of analysis, such as model checking.

The behavioural part of the LNT specification language consists of the following constructs: action with input/output parameters, assignment (:=), sequential composition (;), conditional structure (if), loop (loop), parallel composition (par), nondeterministic choice (select), and empty statement (null). Each process defines an alphabet of actions, a list of typed parameters, and a behaviour built using the aforementioned operators. Communication is carried out by rendezvous on actions with bidirectional transmission of multiple values. The parallel composition explicitly declares the set of actions on which processes must synchronize. If the processes evolve independently from one another (interleaving), this set is empty.

In the rest of this section, we successively present the encoding into LNT of the different parts of our system.

Autonomic Manager An LNT process is generated for each state in the manager LTS. Each process is named using the state identifier. The alphabet of the process contains the set of messages appearing on the LTS transitions. The behaviour of the process encodes all the transitions of the LTS going out from the corresponding state. If there is no such transition, the body of the process is the null statement. If there is a single transition, the body of the process corresponds to the message labelling this transition, followed by a call to the process encoding the target state of the transition. If there is more than one transition, we use the select operator. Let us assume that two transitions q l -→ q', q l -→ q'' ∈ T have the same source state q. The behaviour of the process encoding q in LNT is select l; q'[...] [] l'; q'' end select, where the LNT operator select encodes a nondeterministic choice between l and l'.

Since a message name can be used in different autonomic manager LTSs, each message is prefixed with the manager name to avoid further name clashes. We encode emitted messages (received messages, resp.) with a EM ( REC, resp.) suffix. These suffixes are necessary because LNT symbols ! and ? are used for the data transfer only. As an example, m1 ∈ A ! is encoded as m1 EM , and m2 ∈ A ? is encoded as m2 REC.

Coordination Requirements The coordination requirements specified using reaction rules and regular expressions correspond to an abstract version of the controller to be generated. These requirements are encoded into an LNT process called coordination. The process alphabet is composed of all received and emitted messages appearing in the reaction rules. The body of this process encodes the regular expression of reaction rules. Each reaction rule is translated to LNT separating both sides of the rule using the sequential composition construct (;). In order to make explicit in the controller LTS the logical interval of time that will be chosen in the implementation step and during which the controller receives messages, the left hand part of the reaction rule starts with an action TBEGIN and ends with an action TEND. The left hand part is translated using the par operator without synchronization since all messages can be received in any order. After execution of the TEND action, the right hand part of the reaction rule is translated using the parallel composition too, to express that all emissions can be sent in any order. As far as the regular expression is concerned, a sequence (.) of rules is encoded using the sequential composition, a choice (+) between several rules is translated using the select construct and an iteration ( * ) is encoded using the loop operator.

Architecture In this section, we present how all participants (managers and coordination expression) are composed together. The communication between them is achieved asynchronously. The coordination expression represents an abstract description of the future controller, and all messages must go through this controller, which acts as a centralized orchestrator. Each participant is equipped with an input FIFO buffer. When a participant wants to read a message, it reads the oldest message in its buffer. When a participant sends a message to another participant, it sends the message to the input buffer of that participant. LNT functions are used to describe basic operations on these buffers (e.g., adding and retrieving messages). We present below, an example of function that removes a message from a FIFO buffer (i.e., from the beginning).

function remove_MSG (q: TBUFFER): TBUFFER is case q in var hd: TMessage, tl: TBUFFER in nil -> return nil | cons(hd,tl) -> return tl end case end function

It is worth noting that our synthesis techniques allow one to choose buffer bounds. One can either decide to fix an arbitrary bound for buffers or to use unbounded buffers. In the first case, the only constraint is that the same buffer bound should be used when deploying the controller, otherwise unexpected behaviours and erroneous situations may occur. In the second case (unbounded buffers), the risk is to attempt to generate a controller whose corresponding state space is infinite [START_REF] Brand | On Communicating Finite-State Machines[END_REF]. As an intermediate solution, one can use the recent results presented in [START_REF] Basu | Automatic Verification of Interactions in Asynchronous Systems with Unbounded Buffers[END_REF] for identifying whether the interactions between managers with unbounded buffers can be mimicked with bounded buffers. If this is the case, the lower bound returned by these techniques is used as the minimum buffer bound for both synthesis techniques and the deployment of the application.

A buffer in LNT is first encoded using an LNT list and classic operations on it. Then, for the behavioural part, a buffer is encoded using a process with a buffer data type as parameter. This process can receive messages from the other participants, and can synchronize with its own participant when that one wants to read a message. We generate a process encoding each couple (participant, buffer ) that corresponds to a parallel composition (par) of the participant with its buffer. The synchronization set contains messages consumed by the participant from its buffer.

Finally, the whole system (main process in LNT, see below) consists of the parallel composition of all these couples. It is worth noting that since autonomic managers communicate via the controller, they evolve independently from one another and are therefore composed using the par operator without synchronizations. In contrast, the couple (coordination, buffer ) must synchronize with all couples (manager, buffer ) on all emissions from/to the managers, and this is made explicit in the corresponding synchronization set of this parallel composition.

Compilation and Verification

Now that we have encoded our inputs (models and coordination requirements) into LNT, we can use compilers to obtain the LTS corresponding to all behaviours of the LNT specification. In order to keep only the behaviour corresponding to the most permissive controller [START_REF] Wonham | On the Supremal Controllable Sublanguage of a Given Language[END_REF], we need to hide message exchanges corresponding to consumptions of the managers from their buffers and emissions from managers to the coordination expression buffer. All these messages are replaced by internal actions. We use minimization techniques available in CADP for eliminating all internal actions, removing duplicated paths, and determinizing the final LTS. Finally, we preserve only local emissions/receptions from the coordination expression point of view (messages shown in the dashed grey rectangle in Fig. 4). Transitions figuring in the final LTS are labelled with the messages corresponding to the process alphabet of the couple (coordination, buffer ).

Fig. 4. Exchange of messages between the coordination expression and the managers

Last but not least, let us stress that, since the writing of the coordination expression is achieved manually by a designer, this step of our approach may lead to an error-prone expression. However, we can take advantage of the encoding into LNT to check either the controller LTS (and thus the coordination expression) or the LTS corresponding to the composition of all participants. To do so, one can use the CADP model checker, which takes as input an LTS model and a temporal property specified in MCL [START_REF] Mateescu | A Model Checking Language for Concurrent Value-Passing Systems[END_REF]. We distinguish two types of properties: (i) those that depend on the application (e.g., the controller must eventually transmit a specific message to a certain manager), (ii) those that do not depend on the application (e.g., checking the absence of deadlock).

Running Example and Experiments

We present below an example of LNT process encoding the repair manager shown in Figure 3 and its buffer. This manager synchronizes with its buffer on the repair failure REC message when this message is available in the buffer. Note that the buffer process (buffer repair) is equipped with a parameter corresponding to the buffer data type, that is the structure where messages are stored, initialized to nil. From the encoded LNT specification obtained when calling the LNT code generator, we use CADP compilers to generate the LTS describing the whole system for our running example (consisting of 194,026,753 states and 743,878,684 transitions). Then, we use hiding and minimization techniques to generate the LTS of the controller (consisting of 28,992,305 states and 46,761,782 transitions). An excerpt of the controller LTS, which focuses on the failure and overload detection in the same period of time, is shown in Figure 5. We recall that we use specific labels (namely TBEGIN and TEND) for characterizing the messages received during a same period of time. This LTS shows that when the controller receives a failure and an overload message (of a Tomcat server in this example) during a same period, it forwards only the failure message and drops the overload message. In contrast, when the controller receives these two messages in two different periods, it forwards them to the repair and sizing manager, resp.

We show below two examples of liveness properties, the first one is checked on the controller LTS and the second one on the LTS of the whole system:

-The reception of a failure message by the controller is eventually followed by an emission of a repair message -The emission of an overload message by the application manager is eventually followed by an emission of a reparation or addition message by the controller

[true* .app_overload_tomcat_EM] inev (app_repair_tomcat_EM or app_add_tomcat_EM)
This property shows that the overload message is handled by the repair manager when both Tomcat failure and overload occur within a same period of time. Otherwise, it is handled by the sizing manager.

Both properties use the macro inev (M), which indicates that a transition labelled with M eventually occurs. This macro is defined as follows:

macro inev (M) = mu X .( < true > true and [ not (M) ] X ) end macro

Our approach was applied for validation purposes on many illustrative examples of our dataset (managers and coordination requirements). Table 1 summarizes some of our experiments. Each managed application used as input is characterized using the number of managers and the coordination requirements. We give the size of the LTS (states/transitions) of the whole system as well as the controller LTS obtained after minimization (wrt. a strong bisimulation relation). The last column gives the overall time to synthesize the controller. We observe that, for some examples (gray lines), the size of the generated controller LTSs and the time required for generating those LTSs grow importantly when one of the managers exhibit looping behaviours, and particularly cycles with send messages (see, e.g., the 4 th example in Table 1). On a wider scale, we note that LTS sizes and generation times increase with the number of managers in parallel (see, e.g., the last line of Table 1).

Code Generation and Deployment

We present in this section our Java code generation techniques, which allow to deploy controllers in the context of real-world applications. In particular, we show some experimental results for our running example where the autonomic managers are coordinated using a centralized controller generated with our approach.

Java Code Generation Techniques

Our Java code generation techniques are based on the use of object-oriented programming. They take as input the controller LTS synthesized beforehand, and automatically generate all java classes, methods, and types necessary for deploying it. The controller LTS is encoded as an instance of a Java class LTS. This class relies on two classes, namely a class State and a class transition which represents the transitions between the states. The LTS class also defines an attribute cstate representing the current active state in the controller model. This variable is initialized with the LTS initial state. Some Java code is necessary to interface the controller with the running application. We particularly define a method called react that takes as input a list of messages received within a period of time and applies successive moves according to the received messages, the current state of the controller, and the behaviour of the generated controller. This method computes the messages that the controller has to send as reaction to these received messages, and updates the current state of the controller.

Deployment

Our generated Java code can be deployed and applied on concrete applications using the event-based programming paradigm. The period of time described using special actions TBEGIN and TEND in the controller LTS has to be instantiated with a real value. This period is computed using sampling techniques and implemented using the sleep method in Java. The choice of this period cannot be realized during the synthesis phase and is achieved just before deployment. A wrong choice of this period may lead to the reception of these actions in different periods.

The main behaviour of the controller (run method) consists of an infinite reactive loop, which successively receives events from the application, computes reactions (messages to be sent by the controller), and encodes these messages as events too. A part of the Java program is dedicated to converting the events raised by the application into the input format of the react method, and conversely translates the output of the react method into a list of events executed by the system. Each event contains the corresponding message and additional information, for instance a failure event has also as parameter the impacted server and further information (identifier, port, etc.).

Experiments on our Running Example

In this section we present some experiments we performed when deploying and running our controller for the multi-tier application introduced previously. To do so, we used a virtualized experimental platform based on Openstack, which consists of six physical machines on which we instantiate virtual machines.

The JEE multi-tier application is initially configured and deployed with a server at each tier, i.e., an Apache Web server, a Tomcat server, a MySQL proxy, and a MySQL database. The initial deployment phase is automated using a dynamic management protocol allowing to connect and start the involved servers and database in the right order [START_REF] Abid | Verification of a Dynamic Management Protocol for Cloud Applications[END_REF][START_REF] Etchevers | Reliable Selfdeployment of Cloud Applications[END_REF]. In a second step, we use jmeter to inject increasing load on the Apache server and thus to simulate the clients that send HTTP requests on the managed system. Once we have at least two active Tomcat servers and two MySQL databases, we start simulating failures using a failure injector. When we start injecting failures, we stop augmenting the workload on the Apache server and keep the same load for the rest of the execution. The failure injector is flexible and can be used for affecting any active server (Apache, Tomcat, MySQL, etc.), any number of times (single failure or multiple failures of the same or of different servers), and at any time (same period of time, different periods of time, etc.). We conducted our experiments on applications with or without controller. We have considered different scenarios with failures of the Apache server and of the MySQL proxy as well as failures/load variation of the Tomcat servers and of the MySQL databases.

Figure 6 shows an excerpt of the system behaviour after 500 minutes since the application deployment. We observe that, at this moment, the application is composed of five Tomcat servers and three MySQL databases. Figure 6 presents several cases of failure injection. As an example, at minute 508, a failure of a replicated MySQL database causes a workload increase on the other replicated servers. These two actions happen in the same period, but the controller forwards only the failure detection to the repair manager. Accordingly, a single MySQL database is added by the repair manager and the workload returns at once to its average value. We made several experiments in which we varied the number of failures, the Apache load, and the minimum/maximum thresholds of the Tomcat servers and of the MySQL databases. In all these cases, we observe that the controller succeeds in detecting and correcting the problems while avoiding undesired opera-

MySQLs active Tomcats active

Fig. 6. Tomcat and MySQL failure/overload in a coordinated environment tions, that is, the unnecessary addition/removal of VMs. Figure 7 shows experimental results obtained with different number of failures. For instance, we see that when injecting 14 failures to our running application, the controller applies 18 reconfiguration operations on the system (instead of 40 without controller), and thus avoids 22 undesired operations. Controller synthesis for discrete event systems was originally introduced by Ramadge and Wonham [START_REF] Wonham | On the Supremal Controllable Sublanguage of a Given Language[END_REF][START_REF] Ramadge | The Control of Discrete Event Systems[END_REF]. In [START_REF] Wonham | On the Supremal Controllable Sublanguage of a Given Language[END_REF], the authors present a controllable language as a solution for the supervisory of hybrid control systems. This solution generates controllers from a given system called plant and designed as a finite automaton. [START_REF] Ramadge | The Control of Discrete Event Systems[END_REF] proposes a supervisor synthesis algorithm, which allows to automatically generate a controller from a plant modelled as a finite automaton and properties to be ensured by the controller. The generated controller permits all possible legal executions. This synthesis approach is based on a classical two-person game approach. These approaches can be characterized as restrictive because they directly influence and impact the controlled system. In [START_REF] Delaval | Contracts for Modular Discrete Controller Synthesis[END_REF], the authors introduce an approach based on contract enforcement and abstraction of components to apply a modular discrete controller synthesis on synchronous programs. These programs are presented by Synchronous Symbolic Transition Systems. The authors integrate this approach in a high-level programming language combining data-flow and automata. Another decentralized supervisory control approach for synchronous reactive systems is presented in [START_REF] Belhaj Seboui | An Approach for The Synthesis of Decentralised Supervisors for Distributed Adaptive Systems[END_REF]. This work is based on finite state machines and computes local controllers that act on the subsystems to ensure a global property. The local controllers are automatically generated and this approach was applied to several examples for validation purposes. This approach allows decentralized control whereas we generate a centralized controller. Moreover, they rely on synchronous systems and synchronous communication semantics, whereas we assume asynchronous systems and communication, meaning that the controllability hypothesis is impossible in our context.

In [START_REF] De Oliveira | Synchronization of Multiple Autonomic Control Loops: Application to Cloud Computing[END_REF], the authors propose a generic integration model that focuses terms of reciprocal interference. This generic model can be used to manage the synchronization and coordination of multiple control loops, and it was applied to a scenario in the context of cloud computing and evaluated under simulationbased experiments. This paper does not provide any synthesis techniques for coordinating the multiple loops, and coordination is achieved in a rather manual way.

[21] presents a framework for the coordination of multiple autonomic managers in the cloud computing context. These works use a protocol based on synchronous mechanisms and inter-manager events and actions along with synchronization mechanisms for coordinating these managers. The main difference compared with our work is that this paper focuses on quality of service whereas our focus was on behavioural and functional aspects of the system execution.

Other recent works [START_REF] Delaval | Modular Coordination of Multiple Autonomic Managers[END_REF][START_REF] Gueye | Coordinating Multiple Administration Loops Using Discrete Control[END_REF][START_REF] Gueye | Discrete Control for the Coordination of Administration Loops[END_REF] propose some techniques based on synchronous discrete controller synthesis for coordinating autonomic managers, such as selfrepair and self-sizing managers. The communication between the generated controller and the managers is synchronous and uses a synchronous language BZR, which cannot impose a specific order between requirements and contains multiple and complicated operations. This approach uses a background in synchronous systems and languages, whereas our approach assumes that communication is achieved asynchronously. [START_REF] Di Cosmo | Aeolus: A Component Model for the Cloud[END_REF] presents the Aeolus component model and explains how some activities, such as deployment, reconfiguration, and management phases of complex cloud applications, can be automated in this model. Aeolus takes as inputs high-level application designs, user needs, and constraints (e.g., the number of required ports that can be bound to a client port) to provide valid configuration environments. This work presents some similarities with ours, but does not propose solutions for verifying that the constraints are satisfied in the target configurations.

In [START_REF] Brogi | Modelling the Behaviour of Management Operations in Cloud-based Applications[END_REF], the authors present an extension of TOSCA (OASIS Topology and Orchestration Specification for Cloud Applications) in order to model the behaviour of component's management operations. More precisely, they specify the order in which the management operations of an instantiated component must be executed. In this work, the authors explain how management protocols are described as finite state machines, where the states and transitions are associated with a set of conditions on the requirements and capabilities of the components.

In [START_REF] Parashar | AutoMate: Enabling Autonomic Applications on the Grid[END_REF], the authors introduce AutoMate, a framework for coordinating multiple autonomic components hosted on Grid applications, using high-level rules for their dynamic composition. The rules are executed using a decentralized deductive engine, called RUDDER, and composed of distributed specialized agents. RUDDER deploys the rules and coordinates their execution. It assigns priorities to these rules in order to resolve conflicting decisions between them. However, it uses a manual administration to evaluate and update the interaction rules.

Conclusion

In this paper, we propose new controller synthesis techniques to generate a centralized controller that allows to orchestrate a set of autonomic managers. These managers are modelled as LTSs and the set of coordination requirements is specified using reaction rules and regular expressions. The generated controller communicates with the autonomic managers asynchronously using message passing via FIFO buffers. Our solution for controller synthesis relies on an encoding of our models and of the coordination requirements into the LNT process algebra. From this encoding, an LTS can be generated using CADP compilers, and hiding and reduction techniques. This LTS exhibits all the possible executions of the controller. One can also take advantage of this encoding to validate the generated controller with the CADP verification tools, such as the Evaluator model checker. Indeed, since coordination requirements are written by a human being, they can be erroneous, which results in that case in an erroneous controller as well. Finally, we propose code generation techniques to automatically obtain the Java code corresponding to the controller LTS. We validated our approach with many variants of the multi-tier Web application we used as running example in this paper.

It is worth noting that our approach covers all the development steps from the design of the coordination requirements to the actual deployment of the synthesized controller, which helps to coordinate at runtime real-world applications. In addition, these synthesis techniques can be used to control other applications where components are modelled as LTSs and communicate asynchronously. This is the case in application areas such as Web services, multi-agent systems, or hardware protocols.

A first perspective is to generate distributed controllers instead of a centralized controller. This would permit to preserve the degree of parallelism of the system, where the involved participants could exchange messages without systematically passing through a unique controller. Another perspective aims at applying performance evaluation for the whole system using IMC (Interactive Markov Chain) theory [START_REF] Hermanns | Automated Compositional Markov Chain Generation for a Plain-Old Telephone System[END_REF][START_REF] Hermanns | Interactive Markov Chains: And the Quest for Quantified Quality[END_REF].

Fig. 1 .

 1 Fig. 1. Overview of our approach

Fig. 3 .

 3 Fig. 3. (left) Self-repair manager LTS, (middle) Self-sizing manager LTS, (right) Application manager LTS

[Fig. 5 .

 5 Fig. 5. Excerpt of the controller LTS for the running example

Fig. 7 .

 7 Fig. 7. Number of reconfiguration operations with/without coordination and number of undesired operations avoided by coordination

  process main [message1:any, ..., messagen:any] is par messagep, ..., message k in

	couple_buffer_coordination [...]
	||
	par
	couple_buffer_manager1 [...]
	|| . . . ||
	couple_buffer_managern [...]
	end par
	end par
	end process

Table 1 .

 1 Experimental results: LTSs size and synthesis time

	|Managers| Whole system LTS Controller LTS Time
		|states| |transitions| |states| |transitions| (m:s)
	2	2,307	6,284	118	157	0:10
	3	103,725	365,845	1,360	2,107	1:15
	4	145	267	38	44	0:06
	5	10,063,873 39,117,110 17,662	28,003	43:59
	6	1,900	4,945	186	285	0:08
	10	300,000	1,686,450	1,786	3,471	6:54

Acknowledgements. This work has been supported by the OpenCloudware project (2012-2015), which is funded by the French Fonds national pour la Société Numérique (FSN), and is supported by Pôles Minalogic, Systematic, and SCS.


Eric Guiot Independent
email: guiot.eric_1@yahoo.fr

A classical Force of Gravitation as an alternative to MOND?

Keywords: Central force, conic, dark matter, force of gravitation, galaxies, modified gravitation, PACS Number:04.70.Kd

published or not. The documents may come

A classical Force of Gravitation as an alternative to

MOND?

Introduction

It is well known that an important problem of the contemporary physics is to describe the celestial mechanics for large distances. For example, it appears that the classical laws of gravitation failed to describe the "flat" curves of rotation of the spirals galaxies without add, inside these galaxies, an important amount of a mysterious matter, called "dark matter" (1)(2)(3). Another important problem of the celestial mechanics is to explain the expansion, at an increasing rate, of the universe [4]. Indeed, classical theories of gravitation are always attractive. To solve this contradiction, physicians have to suggest, that another mysterious energy, called this time "dark energy", exists inside the Universe [START_REF]Patantonopoulos The Invisible Universe, Dark Matter and Dark Energy Springer[END_REF][START_REF] Huterer | [END_REF]. Problem is that there is no proof of the reality of the "dark matter" and the "dark energy" despite several important experiments on the Earth [7]. Moreover the most accurate study to try to detect them in the space seems also have failed [8]. Consequently, an important contemporary way of research is to modify the classical laws of Gravitation. Several alternative theories are in competition as for example, the ) (R f theories of gravity [9], the scalar-tensor gravity theories [10,11] or the Modified Newtonian dynamics (MOND) theory [12]. But it appears today that no one of these theories does unanimity. In particular in the case of MOND the laws of classical physics are not respected. This point is the reason for what we are looking for such a law. In two previously papers, we presented a possible way to obtain an alternative and non relativistic force of gravitation [13,14] with respect for classical physics. This work can be considered as an alternative to MOND and possesses common points with this theory. In particular we introduced an acceleration which is a constant of the Universe. Therefore as distinguished from MOND our original hypothesis is that trajectories of celestial bodies are always conics. This assumption led us to study with a mathematical point of view the family of forces which leads to conic trajectories and we present here a part of our results. Indeed it appears that at the 19 th century a theorem has been written about this problem, the Bertrand's theorem [15]. This work proved that there are only two central forces for which all orbits radially bounded are closed, the force of Newton and the Hooke's. These forces leads to conic trajectories with the difference that the Newton's is directed towards one of the foci and the Hooke's towards the geometrical centre of the conic. The proof of this theorem has continued to draw attention and several different demonstrations has been recently published [16,17].

Our own attempt to obtain a force of gravitation different from the Newton's in the case of large distances led us to study this theorem and to compare our results with its predictions. It is the reason for what in this paper we will present in a first part our mathematical results about the conics by comparison with this theorem. In a second part we will present the force of gravitation we obtained. At end we will purpose an experiment in order to valid or invalid our model.

Mathematical study of the forces which leads to conic trajectories

Theory

To obtain these forces we use the equation of the acceleration in polar coordinate. Therefore as distinguished from the Binet's equation we consider not only the radial acceleration but also the tangential acceleration. This original method (at our knowledge) allows obtaining all the forces which lead to conic trajectories and not only the central forces. We present here this method which has been published elsewhere [13,14].

As usual in celestial mechanics we will use the polar system of coordinate

) ; ; (  e e F R  
where F (foci of the conic) is the origin of the repair, r is the radial distance to the origin with the relation

R e r M F   . 
And the angle  is measured from the periapsis of the orbit. In this repair the acceleration is given by the classical relations

    e r r e r r a R           ) 2 ( ) ( 2    
But the orbital shape is more concisely described by the reciprocal r u 1  as a function of  .

And by using the relations " . ' ' ' .

1 2 2 u u d d dt d u dt d u u u d du dt d u dt d u u u u dt d r dt d r                      
We obtain a generalization of the Binet's equation.

       e u u u u e u u u u u u u u a R            4 3 2 2 4 2 2 2 2 3 2 2 ' 2 ' ' 2 "        
Our method to obtain conic trajectories is to solve by substitution the system of equation

            ) ( ) ( ' ) ( ' " 4 2 3 2 2 u Z a u Z u u u Y a u u u u u u a R       Where 4 3 2 2 ' 2 ) ( u u u u u Z         And 4 2 3 2 2 " ) ( u u u u u Y        We introduce a function ) (u f definite by ) ( . ) ( u f A u Y  

Where

Ais constant. To obtain ) ( r as a conic, we have to solve a differential equation as

B u u   "
Where B is a second constant. Consequently we have now to introduce a relation between ) (u Y and   . This relation is

) (u f Cu   

Where

C is a constant of the motion. Consequently

) ( " 2 2 2 u f Au u u        And 2 " C A B u u   
This differential equation leads now to the classical solution

  eCos p r   1 ) ( The parameter p of the conic is A C e a p 2 2 ) 1 (   
Where e is the eccentricity and a the semi major axis. Thus we obtain We have now to determine the tangential component of the acceleration and by using

        f r f f r r C ' 2 1 . 2     Where ) ( ' r f dr d f  We obtain f r r C f r Cf r r a           ' 2 1 2   
Consequently our family of force (per unit mass) is with respect for the Newton's law of dynamics

 e r f f f r C e r f f r e Af F R R       . 1 ' 2 1 1 ' 2 1 . 2                   Or, more simply    e r f f d dr r e r f f r e Af F R R       . 1 ' 2 1 1 ' 2 1 . 2 2                   (2)
Where A and C are two constants. Their physical dimensions depend on the choice of ) (r f . It is also interesting to determine the magnitude of the total speed

) ( ) 2 ( ) ( 2 2 r f a r r a A r r V        (3)

Nature of the force

The force given by equation ( 2) can be decomposed in two forces: the first part given by

R A e Af F   .  
Is naturally always directed to F , foci of the conic. The second part of this force given by

   e r f f d dr r e r f f r F R B      . 1 ' 2 1 1 ' 2 1 2                
Is tangent to the trajectory. Indeed, if we consider that the direction vector of tangent line to a curve is given, in polar coordinate, by

    e r e d dr V R D    ) ( ) (  
And if we do the vector product which is tangential to the trajectory.

D B V F    we obtain 0 1 ' 2 1 1 ' 2 1 2 2 2                              d dr r f f r d dr r r f f d dr V F D B    

Thus we prove that

The force is directed to F : the force of Newton

If the force is directed to the foci F of the conic then the tangential part

B F 
of the force has to be a null vector. Consequently we write

0 . 1 ' 2 1 1 ' 2 1 2                           e r f f d dr r e r f f r F R B
The only solution is given by the relation

0 1 ' 2 1   r f f
The solving of this differential equation is In the case of a point particle which orbits around a center of mass the constant is simply given by GM A  Where G is the universal constant of gravity and M the mass of the center of mass.

Consequently we prove here that it is only one possible force which is always directed to F . This point is in agreement with the Bertrand's theorem but can be considered complementary. Note that our way to obtain this result seems original.

The force is directed to O : the force of Hooke

To determine the family of forces which are directed to O we introduce a point, called I which is located between O and F . This distance FI is called  . If the force is directed to

I then the vector product 0 *     F M I
By noticing that, in our repair

 e e F R   the vector M I  is given by   Sin r Cos M I      We obtain 0 ). ( .         F r Cos F Sin R
With the relations specific to the conics

 eCos e a r    1 ) 1 ( 2 and f r e a eCSin r ) 1 ( 2     (4)
We obtain

f a r f rf f ae 2 ) ( ' ) ' 2 (     
To respect our condition, and by noticing that the distance ea FO  we write that ea   Consequently we have to solve the differential equation

1 2 ) ( ' ) ' 2 (     f a r f rf f
The equation becomes 0 '  f Consequently the function ) (r f has to be constant. We called this one k and by using

k r f  ) (
We obtain the expression of our force

  e keSin e a r e r a kA F R    . 1 ) 1 ( 2            
Its magnitude is given by

ar a r e a a k A F 2 ) 1 ( 2 2 2 2      
By noticing that the distance OM , where M is the point-particle and O the center of the conic, is given by

ar a r e a OM 2 ) 1 ( 2 2 2 2      We obtain OM a k A F  
This force is consequently a force of Hooke and its constant factor is

A a k K 
We have proved here that it is only one central force which is located at O and which leads to a conic trajectory. As previously this mathematical demonstration is in agreement with the Bertrand's theorem but the demonstration seems original. Moreover note that the force of Hooke can lead to parabolic or hyperbolic trajectories, and not only circular or elliptic trajectories.

We present these results on the Figure 1

. 1 F 
is the force of Newton, 2 F  the Hooke's.

Central forces which lead to conic trajectories

To obtain a central force we are looking for the family of functions ) (r f which leads to  as a constant. Consequently we write the equation

0   dr d This relation leads to 0 ) 2 ) ( ' ( ) ' 3 " 2 ( 2 2 2     f a r f f ff ea
And the solving is

 e Sin C r C eC A e C r C ar r e a C rC C ar A F R    . ) ( ) ( ) ) 1 ( ( ) ( 3 2 1 2 3 2 1 2 2 2 2 1 2        
We can distinguish two limiting cases: we obtain the force of Newton.

Secondly, if 0 1  C : In this case ea  
and the center is of the force is located at O , center of the conic. The force is given by

  e Sin C e A e arC r e a ar A F R    . ) 1 ( 2 2 2 2 2 2 2     
This force is the Hooke's.

We can also determine a constant angular momentum at I . In order to study it, we begin to determine the angular momentum at F , foci of the conic. We use the relation

Z R R F e r e r e r e r L         . ) . . ( * . 2      
And by using equations (4) we obtain

Z F e C r C Cr L   .
IF   ) . . ( *   e r e r O I L L R F I           By noticing that ) . . (    e Sin e Cos O I R       I L  becomes   Z F I e Sin r Cos r L L             .
And

  Z I e Sin r Cos r aC C e aC C r C Cr L             . 1 2 2 2 1
By using the relations specific to the conics (4) we obtain

Z I e aC C aC L   1 2   ) ( 1 2  s m
Consequently, the angular momentum is constant for all the forces and the trajectory is plane. Moreover we verify that our force is well central.

We can also giving the equation of time of the motion. As usual, we write this equation by using the eccentric anomaly E . Indeed, we have the relation

eCosE e E    1 1 2    But we saw that ) (r f r C    Consequently we obtain 2 1 2 1 1 1 C r C r C eCosE e E      With the relation ) 1 ( eCosE a r   We obtain   a A e a C C eCosE a C E      2 2 1 1 ) 1 (



And by integration

t a A E C eSinE E a C    2 1 ) ( Consequently t a A aSinE eC C a C E    1 2 1 ) ( By a factorization t a A SinE C a C a C e E C a C           2 1 1 2 1 ) ( And wt t a A C a C SinE C a C a C e E      ) (



Consequently we see that the equation of time and the angular momentum can be described with simple expressions. Note that more generally these mathematical results seem original. Therefore it appears with respect for the Bertrand's theorem that the trajectories can't be closed. In this paper we won't study this point which will be the subject of another paper.

Alternative classical force of gravitation

Our assumptions

We will use now our mathematical results to try to build a possible force of gravitation. This one is building with respect for several assumptions. We list them here.

First of all we suppose that the classical physics can describe with a good approximation the motion of the stars and the actual dynamics of the universe. Indeed, if it is well known that the classical physics leads only to an approximation of the reality, it appears that this physics can in certain cases describe with a great precision the motion of celestial bodies, in particular when the speeds and the density of mass are low. It appears that these conditions are met at the periphery of the galaxies, and inside the clusters of galaxies.

Secondly, as we wrote it previously our fundamental idea is that the first law of Kepler is respected whatever the gravitational system (solar systems, galaxies, clusters of galaxies,..): if a pointparticle interacts with a center of mass its trajectory is always a conic (circle, ellipse, parabola or hyperbola).

At end we suppose that the force of gravitation is central. Indeed, this kind of force, well known in classical physics is generally used to describe action-at-a-distance. This point makes different from our previously work. Indeed it appears that with this condition the choice of possible force is drastically reduced. In fact only one mathematical form is possible.

By taking into consideration these three assumptions and our mathematical results we will explore the possibility that the force of Hooke is the force of gravitation in the case of large distances. Indeed it appears that the only force which is directed toward the foci of the conic is the Newton's and we suppose that the force we are looking for is central. Moreover, our work has shown that we can link these two forces with a gradual evolution.

To explore this possibility we study two limiting cases of motion: firstly, the circular motion, in order to determine the curve of rotation of this force. Secondly, the parabolic motion, in order to determine the dynamics of the universe we expect.

Curve of rotation of the galaxies: determination of K

If our idea is correct, we should obtain a flat curve of rotation by a correct choice of the constant factor K . In order to determine it we study as usual the circular motion. Indeed, this motion describes with a good approximation the motion of the stars around the center of galaxies. In this particular motion, the eccentricity of the conic is given by 0  e and r a  . Consequently, the force given by relation (2) becomes simply

R e kA F    
The curve of rotation is obtained by written the equality of the acceleration and the force

kA r V    2 Where
V is the speed of the point-particle. We obtain kAr V  And consequently kAa V  In order to obtain a flat curve of rotation, and with respect for the physical dimension of k ( 2  m ) we see that this factor has to be dependant of the semi-major axis, as

a r k 0 1  (5)
Where 0 r is constant ( m ). Moreover, we can determine this constant, because we have to respect the Tully Fisher law [18]. Indeed, this empirical relation suggests a correspondence between the visible mass of galaxies and the velocity as

) ( 4 M V  
Where M is the total mass of the galaxy and  V the constant speed of the stars. We saw that A has to be proportional to the mass thus a is an acceleration. This acceleration has to be constant in the entire universe, and can be linked with the Milgrom's acceleration used in MOND [12]. With this relation V is constant for all the stars at the periphery of one galaxy and is in agreement with the Tully-Fisher law. We see that by using a constant acceleration, which has been introduced in another theory, we can describe the curve of rotation of galaxies without dark matter hypothesis. Note that unlike several other alternative theories our model is in agreement with classical physics. By using relation [START_REF]Patantonopoulos The Invisible Universe, Dark Matter and Dark Energy Springer[END_REF] the force can be written

F R    . 1 ) 1 ( 0 2 0            
We can now use this expression to study the parabolic motion.

Consequence on the parabolic motion: dynamics of the Universe

We see here the predictions of our model about the dynamics of the universe. To do it we study the limiting case of parabolic motion. The eccentricity is given by

A F            1 0
We can see that the sign of this force can be positive or negative, and is depending on the ratio a r . Indeed, if a r  the force is repulsive. However, it also appears that this force can be attractive if a r  .

With this result we try to build a simple model about the dynamics of the Universe. We consider, for example, the interaction of two clusters of galaxies between themselves. We approximate their motion with a parabolic motion, and the force of gravitation is the force we present here.

If the clusters move away from one another it is possible that this force is repulsive. Consequently, their relative speed will increase, at least for a time. It appears that if our idea is correct this kind of interactions is actually majority inside the Universe. However when the distance between the clusters progresses this force becomes a day attractive. Consequently, we can easily describe the actual expansion of the Universe at an increasing rate, and simultaneously build a model of the expansion of the Universe compatible with the classical idea of "Big Bang / Big Crunch". This simple model doesn't need naturally a "dark energy" hypothesis, because the Universe is considerate as a kind of harmonic oscillator.

A general force of gravitation?

We saw that our model allows explaining the "flat" curve of rotation of the galaxies without dark matter. Moreover, it allows explaining the expansion of the Universe without dark energy.

Consequently it seems that our hypothesis could describe these two different problems unlike majority of other alternative theories. However, it is certain that the force of Hooke can't be the dominant force in the case of small distance, as solar systems for example. Consequently, the nature of force has to change gradually when the acceleration decreases.

To describe this evolution, we use our previously work about the central forces. We saw that the forces given by the relation

A possible experiment inside the solar system: a test on the free fall motion

Our model indicates that in our solar system, a part of the force of gravitation should be due to the force of Hooke. Naturally, this part should be a tiny amount of the force of gravitation, because the Newton's law is well verified. Moreover, this part should increases with the distance to the sun, and be more important at the periphery of the system than at its center. At end, this part won't modify the trajectories of celestial bodies, because these trajectories are always conic.

We can use this reasoning to purpose an experiment inside our solar system or perhaps at the surface of the Earth. Indeed if trajectories are not modified, it isn't the case of the equation of time.

Consequently it appears that a classical experiment, the study of the free fall motion, could help to valid or invalid our model. We will now try to prove it by using our equations about the conics.

Equation of the free fall motion

We saw in part 2. that the radial acceleration is given by We obtain, after simplification

          r f f r Af a R 1 ' 2
)) 2 ) 1 ( )( ( ' ) ) 1 ( )( ( 2 ( 2 1 2 3 2 2 2 2 2 a r r e ra r f ar r e a r f ar A a R         
And, in the case of free fall motion ( 1  e ) the radial acceleration becomes

)) 2 )( ( ' ) )( ( 2 ( 2 1 2 ra r r f a r r f a A r        (5)
If we consider that the Newton's force is the correct force of gravitation, valid in all the cases, then the radial acceleration has to be given by

2 r A r    
Consequently we can write a differential equation

)) 2 )( ( ' ) )( ( 2 ( 2 1 2 2 ra r r f a r r f a A r A       And after simplification )) 2 )( ( ' ) )( ( 2 ( 2 1 1 2 2 ra r r f a r r f a r      
The solving of this equation is With this expression of ) (r f the force is the Newton's. Consequently, we can't obtain a force different from this force which leads to the same acceleration, in the case of the free fall motion. This point indicates that if a force of gravitation different from the Newton's is valuable for large distances we should detect an anomaly around this law. As we wrote it previously, this anomaly should be a tiny proportion of it but it is possible to think that with a contemporary precision, we could detect it. Note that this test is only a modern version of the experiments of Galilee. Moreover note that it should detect all variations around the Newton's law and not only our model. At end it appears that this kind of anomaly has been suspected in the past [19].

           r a r C a r r f 2 2

Our prediction

If our model is correct we should obtain in the case of free fall motion a radial acceleration given by  . Note also that if a r 2  this term becomes negative. At end if our model is correct we should detect a small modification around the Newton's law given by the previously relation.

Discussion

Physical interpretation

In this paper, we tried to show that the force of Hooke can describe several astronomical observations. However we can try to discuss this assumption with a physical point of view.

Firstly, we can say that the force of Hooke exist already in the gravitation. It is the force which interacts with a point-particle inside a sphere where the density of mass is uniform. This is the consequence of the theorem of Gauss and this result is well known since centuries. For example, in a sphere the acceleration is given by

 

We see that the expressions are proximate. With this analogy we can suggest a physical interpretation of our force: progressively, when the distance to the center of force increases, the point particle which orbits around the center of mass "considers" that this mass is progressively «diluted" inside a closed volume. This volume is depending on the semi major axis of its trajectory and on the constant 0 r

. At the end of this evolution the density of mass inside this closed volume is uniform and the force becomes entirely the Hooke's.



  which is directed to the foci and a force B F 

1 C

 1 is constant. But this one does duplication with our previously constant Aand consequently

and 2 Ca

 2 Figure 1. Representation of the forces



  of the force is the foci of the conic. By choosing 1 1  C

Figure 2 .

 2 Figure 2. Representation of the central force



  If the force is the Newton's we obtain the equation of time of Kepler

  This condition, with respect for physical dimensions, leads to write the relation

  And, in the simplest case, the angular  is determined by 0

  We can determine the constants for our limiting cases: if 0 r r  the force is the Newton'Indeed, by using this relation we obtain a graduation between our two limiting cases. Moreover the distance FI becomes of force I is well located between O and F (Figure2.).

1 2 

 12 And, by using the relations specifics to the conics 

1 C 2 (

 12 is constant. With this relation and by using (3) the total speed becomes However this speed has to be equal to zero if a r Case of the free fall motion without initial speed). Thus we have to write that 1

D

  The first term is naturally the Newton's. The additive term we should obtain is Note that this term is equal to zero at the beginning of the free fall motion. Indeed at this point we have the relation a r 2

MC

  is the total mass contained inside the sphere of radius r . If the point particle is dropped out from a distance a of the center and if the mass density is uniform we obtain is constant. We can compare this with the acceleration we obtained in a comparable motion with our force

Conclusion

In this paper we present our results about an alternative and classical force of gravitation. This force allows describing the "flat" curve of rotation of the spiral galaxies and the expansion at an increasing rate of the Universe. This model is building by using an acceleration which is constant inside the Universe, and which is comparable to the acceleration used in MOND. Moreover we present an experiment on the Earth to valid or invalid our model. At end we present a mathematical study of the forces which leads to conic trajectories.

Note that this kind of interpretation was already used in another action-at-a-distance, for example to build the model of the atom of Thomson at the 19 th century.

A way to build a relativistic theory?

The theory we are trying to build is classical, and consequently can't describe exactly the gravitation. But if this theory is correct it has to be a limiting case of a relativistic theory. This point is a theorist test for this model. Indeed without experiment we can't prove that this model is correct. But we can notice that the solution is simple and seems in agreement with the astronomical observations. The test we suggested in this paper is naturally difficult to implement but it is perhaps possible, with contemporary precision, to do it. At end, building a relativistic theory should be naturally very difficult but, if the force is always central, as we suggested it in this paper, perhaps a simple solution exists.

Is this idea so surprising?

We want discuss this last point. Effectively it can be surprising that a so simple force could be the force of gravitation in the case of large distances. Naturally the last word will be for the experiments, for example if dark matter is discovered or perhaps if our own experiment is done a day. But if we compare this idea with other perhaps it isn't worth. I think especially to the idea of "dark energy" which seems really problematic. All things considered this idea of "the force of Hooke" has perhaps the virtue of simplicity.


Fabrice Le Fessant
email: fabrice.lefessant@inria.fr

Pierre Chambart
email: pierre.chambart@ocamlpro.com

Towards A Debugger for Native-Code OCaml Applications

In this talk, we will present a starting project at OCamlPro, the development of a debugging framework for OCaml native-code applications, based on the LLDB Debugger, a debugger built on top of the LLVM framework. We implemented a complete binding of LLDB C++ API for OCaml, and then used it to build several tools, one "generic" debugger, and two small utilities to monitor the memory behavior of OCaml applications.

Introduction

The OCaml distribution provides a debugger, ocamldebug, but only for bytecode applications. This limitation is unfortunate, as most users, today, only work with native-code applications. Moreover, the bytecode debugger is limited to OCaml code, and cannot debug interactions between OCaml and C.

Recent work has been done by Mark Shinwell at OCamllabs [START_REF] Shinwell | Emission of dwarf debugging information[END_REF] to extend gdb to debug OCaml native applications. It is a complex task, as not only the OCaml compiler itself must be modified to emit DWARF information [START_REF] Eager | Introduction to the DWARF Debugging Format[END_REF], but gdb itself must be extended to deal with OCaml specifics. Unfortunately, extending gdb is not a simple task, it must be done in a combination of C and Python, and requires an expertise of gdb internals that are not very well documented. Finally, the system integration of gdb is not very good on Windows and Mac OS X platforms, two major targets for OCaml applications in the future.

Recently, a new tool appeared in the LLVM project, a framework to build compilers and associated tools: the new tool, LLDB, uses LLVM capabilities to assemble/disassemble machine-code and object files, and extends LLVM with debugging facilities (managing code and data breakpoints, etc.). LLDB is now the standard tool within Apple's Xcode to debug Mac OS X applications, and is now being ported under Windows. Moreover, LLDB has been designed from the beginning to be more a framework than a tool, providing a clean C++ API to build advanced debugging tools and scripts.

Thus, we decided to explore the capabilities to use LLDB API to build a debugger for native-code OCaml applications. We started by creating an OCaml binding for LLDB C++ API, that allowed us to program our young debugger completely in OCaml. We then tried several approaches: first, we built some little tools using the new OCaml API to monitor the memory behavior of some OCaml applications, using breakpoints and memory introspection; then, we develop a standalone debugger for TypeRex, that takes benefit from some extensions available in our version of OCaml for memory-profiling. We think the result is promising.

LLDB-OCaml Binding

LLDB comes both with a clean C++ API and a Python binding, generated in SWIG [START_REF] Beazley | Swig: an easy to use tool for integrating scripting languages with c and c++[END_REF]. After a short look at the C++ API, we decided it was clean enough to automate the generation of a complete OCaml binding: it tooks us a few minutes to manually write working stubs for a few methods, then a few hours to write a stub generator taking the C++ header files as input, and then a few days to test and polish the binding. The stub generator is less than a thousand lines of OCaml, mostly a simple parser for C++ header files (based on top of Genlex...), and two pretty-printers for C++ and OCaml parts of the binding. Of course, we used our experience of developing such binding generators, in particular for the wxWidgets library [START_REF] Fessant | The design of the wxocaml library[END_REF].

The binding itself covers 97% of LLDB C++ API (1065 methods are available in OCaml over 1090 in the complete API), and it works now both with the version of LLDB available in Debian and with the trunk version. We used a purely functional syntax for the binding, i.e. C++ methods are OCaml functions, taking the object as first argument.

Applications

We first tried the new born OCaml binding to build a few small tools, to check how it behaved for OCaml applications:

First, we developed gc stats, a tool that sets a breakpoint on caml sys exit on the target application, and then explores the memory of the target application to recover and print garbage collection counters. With only 150 lines of OCaml, we were able to monitor the final memory usage of any OCaml application, without instrumenting its code.

Then, we developed alloc prof, a tool that sets a breakpoint on caml garbage collection, and then outputs the complete stack (including C functions) at every such garbage collection. With only 130 lines of code, this is close to what our previous allocation profiler would do, but again, without using a specific compiler or runtime.

Finally, we started to develop ocp-lldb, an interactive debugger for OCaml native applications. For that, we used the interactive debugger already available in LLDB C++ API, but we customized it be adding a new ocaml sub-command with facilities to debug OCaml specific features:

ocaml modules prints the list of OCaml modules in the executable ocaml target MODULE prints function symbols in module MODULE ocaml break MOD.FUN set a breakpoint on the corresponding function ocaml args NARGS print NARGS registers, corresponding to the arguments in the current OCaml calling ABI ocaml global MOD.VAL print the value of a fully-qualified global value ocaml heap print heap information (size of heap, heap segments and minor heap, gc stats) ocaml print ADDR print the value at address ADDR Currently, when debugging a standard OCaml application, we print OCaml values as simple blocks, using only header information (size) and our capacity to know if a value is in the heap. However, when debugging a TypeRex application (i.e. compiled using ocp-memprof OCaml compiler, we are able to use the additionnal typing information present in the header of every OCaml value to correctly display most values depending on their types, as in the OCaml toplevel.

Discussion

In the future, we plan to extend this work in several directions:

• Add a graphical interface on top of the debugger to offer visual debugging with variable monitoring;

• Modify the compiler to allow breakpoints to be set in any OCaml expression (currently, breakpoints can only be set on functions), and to provide information on local variables (using a specific format, while waiting for DWARF support to be available);


Pierre Chambart

Michael Laporte

Vincent Bernardoff

Fabrice Le Fessant

Operf: Benchmarking the OCaml Compiler

We present operf, a set of tools to benchmark the OCaml compiler, with both microbenchmarks, for fast feedback during development, and macro-benchmarks, for results on a larger set of benchmarks.

Introduction

Adding optimisations to the compiler is not risk-free. A compiler is a complicated beast and adding some code can introduce complex bugs and increase the maintenance burden. Before considering an optimisation for inclusion, the risk/reward ratio must be carefully evaluated. Currently, there is no way to simply assert the improvement or regression of a change. This is the problem that operf intend to solve.

Use cases

Benchmarking a compiler means benchmarking programs built with a given compiler. There is nothing really specific to compilers benchmarking compared to a library or a program, but it represents a lot more bookeeping and maintainance. In particular there is a need for a common an automatable way to compile and execute lot of different applications, recover the results in a similar fashion and compare them, sometimes over a long period of time. For that, operf is composed of two packages: operf-micro and operf-macro.

The operf-macro Package

The operf-macro package is designed to benchmark real applications and accurately account for their running time. It is the part of operf that is expected to be used to evaluate compiler changes before integration. The package provides tools to measure the running time, CPU counters (like number of intructions executed), and GC statistics. To recover GC information, we propose a simple standard. If a program does not comply with it, it is still possible to extract some GC information with another tool (cf. our submitted article on lldb for OCaml, and the ocp-gcstats tool).

Since the evaluation of the compiler needs a representative set of applications, operf-macro has been designed to allow developers to easily add new benchmarks, by recording benchmarks in a simple database. We expect that this will allow a majority of open-source released OPAM packages to declare their own benchmarks, and thus, to be automatically tested for performance and correctness when a new version of OCaml will be released.

operf-macro leverages OPAM to simplify automated bulk testing. It is not strongly tied, but good practices and a few command-line tools makes it as easy as typing one command to test a new compiler version on the world.

The operf-micro Package

The operf-micro package is intended to be used in quick iterations of modification/evaluation of the compiler. A developer can typically add the operf-micro command to its makefile invocation to evaluate its changes after every build. The operf-micro tool was designed to simply test some small patterns, or algorithms and demonstrate in which cases some optimisation should or should not be triggered. To allow immediate use after the compilation of the compiler, operf-micro has as few dependencies as possible. Benchmarks built using its simple API can report their running time, but also the GC statistics and CPU cycles, in a format usable by operf-macro.

Conclusion

Currently, operf-micro and operf-macro are distributed with a set of benchmarks, which are used to develop the new flambda inliner for OCaml. Those benchmarks were also useful to uncover early bugs during the developement of the 4.03.0 branch. Maintaining a test and benchmark suite for a lot of applications on the developement branch of OCaml represents quite a lot of work. We think that this work is valuable, and can improve the the confidence of compiler developers in their changes and their impact on real world software. Of course, we hope the original authors will take over the work of maintaining benchmarks for their applications, and we designed the tools with this goal in mind. We wish that operf will have a success comparable with OPAM for package developers.

Authors' addresses: pierre.chambart at ocamlpro.com, fabrice.le fessant at inria.fr, vincent.bernardoff at ocamlpro.com