EVA-Flo is a research project leaded by Nathalie Revol at the École Normale Supérieure in Lyon and funded by the Agence Nationale de la Recherche. Partners are ELIAUS, LIP, CEA-LIST and INRIA Sophia Antipolis laboratories. The participation of ELIAUS laboratory to this project was established as a part of a collaboration between ELIAUS and LIRMM laboratories.
The most important area of work of the EVA-Flo project in Perpignan was related to formal methods. We were supposed to broaden the use of Gappa tool and to solve a question raised by CEA-LIST during the preparation of the EVA-Flo proposal on the accumulation of small errors on extremely long processes. Such processes occur for example in a 1 kHz numerical integrator used in aircraft operated on a 10 hour flight (approximately 1 billion operations).
We presented one application were we circumvented the limitation induced by constant intervals in Gappa to the price of new theorems on interval arithmetic that cannot be expressed as interval operations (Boldo, Daumas & Giorgi 2008). Meanwhile, we established our first results on stochastic formal methods for long running numerical processes (Daumas & Lester et al. 2008-2009). We showed that we can safely consider that there are still some significant bits in results when worst case analysis considers that no significant bit remains. Our probability of failure is compatible with FAA regulations and below one against a billion. Results still unpublished improve these figures and propose an alternate proof path.
We focused on first order errors during the EVA-Flo project. Yet, we discovered that higher order errors should not be treated stochastically with the semantics developed by CEA-LIST for worst case error analysis. We expect to get significantly tighter results on higher order errors by introducing a new semantics based on conditional integrands.
Perpignan was also supposed to explore the features of graphics processing units for general purpose high performance computing (GPGPU). We carried out many projects on background analysis down to finalized developments (Collange, Daumas, Defour et al. 2007-2009). We also set up a new nationwide action of ASR virtual laboratory.
To sum up, we have achieved many results in the different tasks assigned to Perpignan by the EVA-Flo project and we did significantly contribute to the advances of the knowledge on the use of formal methods and manycore architectures for high performance computing. We also outlined a few difficult and interesting questions that should be explored to efficiently use stochastic formal methods when higher order errors cannot be bounded by worst case analysis. Meanwhile, industry and academic institutions are strongly focusing their attention on general purpose processing on embedded manycore architecture meaning that our expertise on GPGPU should be the key to some future leading edge research.
As a consequence, EVA-Flo in Perpignan is a success for two reasons. First we answered many questions raised in the proposal. Second, we raised new questions that allow us to suggest a follow up on EVA-Flo.
Below is a list of journal and conference publications from ELIAUS laboratory that acknowledged being partly supported by the EVA-Flo project:
Below is a list of other publications and presentations that were also partly supported by the EVA-Flo project: