Search

International audience; Distributed software built from components has become a mainstay of service-oriented applications, which frequently undergo reconfigurations in order to adapt to changes in their operating environment or their functional requirements. Given the complexity of distributed software and the adverse effects of incorrect reconfigurations, a suitable methodology is needed to ensure the correctness of reconfigurations in component- based systems. This survey gives the reader a global perspective over existing formal techniques that pursue this goal. It distinguishes different ways in which formal methods can improve the reliability of reconfigurations, and lists techniques that contribute to solving each of these particular scientific challenges.

Formal methods provide systematic and rigorous techniques for software development. We strongly believe that they must be taught in computer science curricula. In this paper we present the pedagogic rationale and the concrete implementation of two courses on the use of formal methods, sharing some material. These courses promote the usage of formal verification to ensure safety and security of software, exemplified in the domain of the Internet of Things., Comment: In Proceedings AppFM 2021, arXiv:2111.07538

International audience; An important concern addressed by runtime verification tools for C code is related to detecting memory errors. It requires to monitor some properties of memory locations (e.g., their validity and initialization) along the whole program execution. Static analysis based optimizations have been shown to significantly improve the performances of such tools by reducing the monitoring of irrelevant locations. However, soundness of the verdict of the whole tool strongly depends on the soundness of the underlying static analysis technique. This paper tackles this issue for the dataflow analysis used to optimize the E-ACSL runtime assertion checking tool. We formally define the core dataflow analysis used by E-ACSL and prove its soundness.

International audience; Powerlists are data structures that can be successfully used for defining parallel programs based on divide-and-conquer paradigm. These parallel recursive data structures and their algebraic theories offer both a methodology to design parallel algorithms and parallel programming abstractions to ease the development of parallel applications. The paper presents a technique for speeding up the parallel recursive programs defined based on powerlists. The improvements are achieved by applying transformation rules that introduce tuple functions and prefix operators, for which a more efficient execution model is defined. Together with the execution model, a cost model is also defined in order to allow a proper evaluation. The treated examples emphasise the fact that the transformation leads to important improvements of the programs. The speeding up is achieved by reducing the number of recursive calls, and also by enable the fusion of splitting/combining operations on different data structures. In addition, enhancing the function that has to be computed to other useful functions using a tuple, could improved the cost reduction even more.

International audience

International audience; Parallel programming is much more complex and difficult than sequential programming, and it is therefore more challenging to achieve the same software quality in a parallel context. High-level parallel programming models, if implemented as software frameworks, could increase productivity and reliability. Important requirements such as extensibility and adaptability for different platforms are required for such a framework, and this paper reflects on these requirements and their relation to the software engineering methodologies that could put them in practice. All these are exemplified on a Java framework-JPLF; this is a high-level parallel programming approach being based on the model brought by the PowerLists associated theories, and it respects the analysed requirements. The design of JPLF is analysed by explaining the design choices and highlighting the design patterns and design principles applied.

International audience; Runtime Assertion Checking (RAC) for expressive specification languages is a non-trivial verification task, that becomes even more complex for memory-related properties of imperative languages with dynamic memory allocation. It is important to ensure the soundness of RAC verdicts, in particular when RAC reports the absence of failures for execution traces. This paper presents a formalization of a program transformation technique for RAC of memory properties for a representative language with memory operations. It includes an observation memory model that is essential to record and monitor memory-related properties. We prove the soundness of RAC verdicts with regard to the semantics of this language.

International audience; Parallel programming is more complex than sequential programming. It is therefore more difficult to achieve the same software quality in a parallel context. High-level parallel programming approaches are intermediate approaches where users are offered simplified APIs. There is a trade-off between expressivity and programming productivity, while still offering good performance. By being less error-prone, high-level approaches can improve application quality. From the API user point of view, such approaches should provide ease of programming without hindering performance. From the API implementor point of view, such approaches should be portable across parallel paradigms and extensible. JPLF is a framework for the Java language based on the theory of Powerlists, which are parallel recursive data structures. It is a high-level parallel programming approach that possesses the qualities mentioned above. This paper reflects on the design of JPLF: it explains the design choices and highlights the design patterns and design principles applied to build JPLF.

Frama-C is a software analysis framework that provides a common infrastructure and a common behavioral specification language to plugins that implement various static and dynamic analyses of C programs. Most plugins do not support concurrency. We have proposed Conc2Seq, a Frama-C plugin based on program transformation, capable to leverage the existing huge code base of plugins and to handle concurrent C programs. In this paper we formalize and sketch the proof of correctness of the program transformation principle behind Conc2Seq, and present an effort towards the full mechanization of both the formalization and proofs with the proof assistant Coq., Comment: In Proceedings VPT 2017, arXiv:1708.06887

To appear; International audience; The BSP model (Bulk Synchronous Parallel) simplifies the constructionand evaluation of parallel algorithms, with its simplifiedsynchronization structure and cost model. Nevertheless, imperativeBSP programs can suffer from synchronization errors.Programs with textually aligned barriers are free from such errors,and this structure eases program comprehension.Replicated synchronization is a sufficient condition for the absence of such errors.We propose a simplified formalization of barrier inference as data flowanalysis, which verifies statically whether an imperative BSP program hasreplicated synchronization, which is a sufficient condition for textual barrier alignment.

International audience; Skeletal parallelism is a model of parallelism where parallel constructs are provided to the programmer as usual patterns of parallel algorithms. High-level skeleton libraries often offer a global view of programs instead of the common Single Program Multiple Data view in parallel programming. A program is written as a sequential program but operates on parallel data structures. Most of the time, skeletons on a parallel data structure have counterparts on a sequential data structure. For example, the map function that applies a given function to all the elements of a sequential collection (e.g., a list) has a map skeleton counterpart that applies a sequential function to all the elements of a distributed collection. Two of the challenges a programmer faces when using a skeleton library that provides a wide variety of skeletons are: which are the skeletons to use, and how to compose them? These design decisions may have a large impact on the performance of the parallel programs. However, skeletons, especially when they do not mutate the data structure they operate on, but are rather implemented as pure functions , possess algebraic properties that allow to transform compositions of skeletons into more efficient compositions of skeletons. In this paper, we present such an automatic transformation framework for the Python skeleton library PySke and evaluate it on several example applications.

International audience; PySke is a library of parallel algorithmic skeletons in Python designed for list and tree data structures. Such algorithmic skeletons are high-order functions implemented in parallel. An application developed with PySke is a composition of skeletons. To ease the write of parallel programs, PySke does not follow the Single Program Multiple Data (SPMD) paradigm but offers a global view of parallel programs to users. This approach aims at writing scalable programs easily. In addition to the library, we present experiments performed on a high-performance computing cluster (distributed memory) on a set of example applications developed with PySke.

Explicit parallel programming for shared and distributed memory architectures is an efficient way to deal with data intensive computations. However approaches such as explicit threads or MPI remain difficult solutions for most programmers. Indeed they have to face different constraints such as explicit inter-processors communications or data distribution.

International audience; While deductive verification is increasingly used on real-life code, making it fully automatic remains difficult. The development of powerful SMT solvers has improved the situation, but some proofs still require interactive theorem provers in order to achieve full formal verification. Auto-active verification relies on additional guiding annotations (assertions, ghost code, lemma functions, etc.) and provides an important step towards a greater automation of the proof. However, the support of this methodology often remains partial and depends on the verification tool. This paper presents an experience report on a complete functional verification of several C programs from the literature and real-life code using auto-active verification with the C software analysis platform Frama-C and its deductive verification plugin . The goal is to use automatic solvers to verify properties that are classically verified with interactive provers. Based on our experience, we discuss the benefits of this methodology and the current limitations of the tool, as well as proposals of new features to overcome them.

International audience; Modern verification projects continue to offer new challenges for formal verification. One of them is the linked list module of Contiki, a popular open-source operating system for the Internet of Things. It has a rich API and uses a particular list representation that make it different from the classical linked list implementations. Being widely used in the OS, the list module is critical for reliability and security. A recent work verified the list module using ghost arrays. This article reports on a new verification effort for this module. Realized in the Frama-C/Wp tool, the new approach relies on logic lists. A logic list provides a convenient high-level view of the linked list. The specifications of all functions are now proved faster and almost all automatically, only a small number of auxiliary lemmas and a couple of assertions being proved interactively in Coq. The proposed specifications are validated by proving a few client functions manipulating lists. During the verification, a more efficient implementation for one function was found and verified. We compare the new approach with the previous effort based on ghost arrays, and discuss the benefits and drawbacks of both techniques.

International audience; SyDPaCC is a set of libraries for the Coq interactive theorem prover. It allows to develop correct functional parallel programs on distributed lists based on the transformation of naive sequential programs that are considered as specifications. To offer the parallelization of functions on other data structures, the first step is to implement a parallel version of the considered data structure and to provide parallel implementations of primitive functions manipulating it. This paper presents such a first step: a binary tree extension which includes new map and reduce pure functional algorithmic skeletons for binary trees. Such algorithmic skeletons are templates of parallel algorithms, realized in a functional context as higher-order functions implemented in parallel. The use of these new primitives is illustrated on example applications.

The complexity of modern software systems is continuously growing together with the communication capabilities and computational power of pervasive technology, embodied by a wide range of interacting heterogeneous smart devices.

International audience; Alloy is both a formal language and a tool for software mod-eling. The language is basically first order relational logic. The analyzer is based on instance finding: it tries to refute assertions and if it succeeds it reports a counterexample. It works by translating Alloy models and instance finding into SAT problems. If no instance is found it does not mean the assertion is satisfied. Alloy relies on the small scope hypothesis: examining all small cases is likely to produce interesting counterexamples. This is very valuable when developing a system. However, Alloy cannot show their absence. In this paper, we propose an approach where Alloy can be used as a first step, and then using a tool we develop, Alloy models can be translated to Coq code to be proved correct interactively.

This special issue contains extended versions of selected papers from the 5th International Symposium on Formal Approaches to Parallel and Distributed Systems (4PAD 2018). The symposium was held in Orleans, France on July 19th, 2020 in conjunction with the 2018 International Conference on High Performance Computing & Simulation (HPCS 2018).

International audience; This paper presents the design and implementation of a sequential simulator for the parallel functional language BSML based on the parallel computation model Bulk Synchronous Parallelism (BSP). This simulator is implemented in sequential, runs in any browser, and provides a graphical representation of the parallel executions. Due to the pure functional nature of BSML, the results obtained by this simulator are the same than the results that could be obtained by executing the program in parallel.

International audience; Frequent itemset mining is one pillar of machine learning and is very important for many data mining applications. There are many different algorithms for frequent itemset mining, but to our knowledge no implementation has been proven correct using computer aided verification. Hu et al. derived on paper an efficient algorithm for this problem, starting from an inefficient functional program and by using program calculation derived an efficient version. Based on their work, we propose a formally verified functional implementation for frequent itemset mining developed with the Coq proof assistant. All the proposed programs are evaluated on classical datasets and are compared to a non verified Java implementation of the Apriori algorithm.

Among distributed systems, connected devices and services, also referred to as the Internet of Things (IoT), are becoming more and more widespread. Some of these devices are used in security-critical domains, and even in domains that are not necessarily critical, privacy issues may arise with devices collecting and transmitting a lot of personal information. It is therefore important to provide security guarantees for the software executed by simple devices, which often do not even provide memory protection units. This kind of guarantees can be brought using formal verification. In this tutorial, we focus on the use of Frama-C, a platform for the analysis of C programs, to verify IoT software. We illustrate it on several examples taken from Contiki, a lightweight operating system for Internet of Things.

International audience; With the wide expansion of multiprocessor architectures, the analysis and reasoning for programs under weak memory models has become an important concern. This work presents MMFilter, an original constraint solver for generating program behaviors respecting a particular memory model. It is implemented in Prolog using CHR (Constraint Handling Rules). The CHR formalism provides a convenient generic solution for specifying memory models. It benefits from the existing optimized implementations of CHR and can be easily extended to new models. We present MMFilter design, illustrate the encoding of memory model constraints in CHR and discuss the benefits and limitations of the proposed technique.

International audience; Cloud Computing has known in the past few years a fast development, leading to a spike in the number of companies competing on providing the best Cloud services. This makes it harder for potential Cloud customers to chose the adequate provider. Despite its wide adoption, many are still hesitant due to the security issues Cloud Computing poses. In this paper, we propose a brokerage solution that formalizes security properties under the form of inter-VM relations, and gives the possibility of setting these security requirements to its customers from the first steps. This solution uses formal methods and the finite model finder KodKod to verify the consistency of the customer's requirements, and to find a placement for his deployment model.

Proof assistants such as Coq [1] can be used to develop very high assurance software such as a verified C compiler [2] and verified high performance computing programs [3]. Even when not used for a full system, using such a proof assistant to develop critical parts of a system could be interesting, for example security monitors [4] or the reconfiguration mechanism of a component based system.

International audience; OCaml is a multi-paradigm (functional, imperative,object-oriented) high level sequential language. Types are stati-cally inferred by the compiler and the type system is expressiveand strong. These features make OCaml a very productivelanguage for developing efficient and safe programs. In thistutorial we present three frameworks for using OCaml toprogram scalable parallel architectures: BSML, Multi-ML andSpoc.

With the recent discoveries of widespread vulnerabilities, the use of formal methods in the design of system is more and more important, in particular in the context of Cloud computing which can be used for high performance computing applications [1]. Formal methods range from more lightweight method such as the Alloy [2] formal specification language and analyzer to more heavyweight formal methods based on proof assistants such as Isabelle/HOL or Coq [3].

International audience; Internet of Things (IoT) applications are becoming increasingly critical and require formal verification. Our recent work presented formal verification of the linked list module of Contiki, an OS for IoT. It relies on a parallel view of a linked list via a companion ghost array and uses an inductive predicate to link both views. In this work, a few interactively proved lemmas allow for the automatic verification of the list functions specifications, expressed in the acsl specification language and proved with the Frama-C/Wp tool. In a broader verification context, especially as long as the whole system is not yet formally verified, it would be very useful to use runtime verification , in particular, to test client modules that use the list module. It is not possible with the current specifications, which include an inductive predicate and axiomatically defined functions. In this early-idea paper we show how to define a provably equivalent non-inductive predicate and a provably equivalent non-axiomatic function that belong to the executable subset e-acsl of acsl and can be transformed into executable C code. Finally, we propose an extension of Frama-C to handle both axiomatic specifications for deductive verification and executable specifications for runtime verification.

International audience; Internet of Things (IoT) applications are becoming increasingly critical and require rigorous formal verification. In this paper we target Contiki, a widely used open-source OS for IoT, and present a verification case study of one of its most critical modules: that of linked lists. Its API and list representation differ from the classical linked list implementations, and are particularly challenging for deductive verification. The proposed verification technique relies on a parallel view of a list through a companion ghost array. This approach makes it possible to perform most proofs automatically using the Frama-C/WP tool, only a small number of auxiliary lemmas being proved interactively in the Coq proof assistant. We present an elegant segment-based reasoning over the companion array developed for the proof. Finally, we validate the proposed specification by proving a few functions manipulating lists.

International audience; Parallel programs based on the Divide&Conquer paradigm could be successfully defined in a simple way using powerlists. These parallel recursive data structures and their algebraic theories offer both a methodology to design parallel algorithms and parallel programming abstractions to ease the development of parallel applications. The paper presents how programs based on powerlists can be implemented in Java using the framework we developed. The design of this framework is based on powerlists theory, but in the same time follows the object-oriented design principles that provide flexibility and maintainability. Examples are given and performance experiments are conducted. The results emphasise the utility and the efficiency of the framework.

International audience; Skeletal parallelism offers a good trade-off between programming productivity and execution efficiency. In this style of parallelism, an application is a composition of algorithmic skeletons. An algorithmic skeleton captures a pattern of parallel algorithm on a distributed data structure, and is also often associated with a sequential algorithm on a sequential data structure that is the counterpart of the parallel data structure. The algorithmic skeleton approach has been inspired by functional programming. It is therefore very natural to embed algorithmic skeletons in a functional programming language. In this paper we present a new algorithmic skeleton library for the statically typed functional language OCaml, and illustrate its use on some applications. This functional skeletal parallel programming library is implemented using the Bulk Synchronous Parallel ML parallel programming library for OCaml.

International audience; This paper presents an extension of a library for the Coq interactive theorem prover that enables the development of correct functional parallel programs based on sequential program transformation and automatic parallelization using an algorithmic skeleton named accumulate. Such an algorithmic skeleton is a pattern of a parallel algorithm that is provided as a high-order function implemented in parallel. The use of this framework is illustrated with the bracket matching problem, including experiments on a parallel machine.

International audience; Bulk synchronous parallelism (BSP) offers an abstract and simple model of parallelism yet allows to take realistically into account the communication costs of parallel algorithms. BSP has been used in many application domains. BSPlib and its variants are programming libraries for the C language that support the BSP style. Bulk Synchronous Parallel ML (BSML) is a library for BSP programming with the functional language OCaml. It offers parallel operations on a data structure named parallel vector. BSML provides a global view of programs, i.e. BSML programs can be seen as sequential programs working on a parallel data structure (seq of par) while a BSPlib program is written in the SPMD style and understood as a parallel composition of communicating sequential programs (par of seq). The communication styles of BSML and BSPlib are also quite different. The contribution of this paper is a BSPlib-style communication API implemented on top of BSML. It has been designed without extending BSML, but only using the imperative features of the underlying function language OCaml. Programs implemented using this API are very close to programs implemented using a BSPlib library for the C language. It therefore shows that BSML is universal for the BSP model.

We now live surrounded by sensors, we create information continuously and we leave constantly computer traces of our activities. The processing and analysis of this huge volume data, so called Big Data, offer innumerable and still largely unexplored: health (epidemiology, genomics complex energy networks, intelligent cities, forecasting and management of environmental risks, etc. Big Data has, and will increasingly, a very significant impact at the societal economic and commercial levels. Many interesting Big Data problems can be modeled as problems on graphs/networks.

Information technologies have allowed for the rapid growth of both data acquisition and data storage. With this growth comes the challenge of extracting useful information. One piece of information that is interesting to academics and industry is the relationships between items in a large data set. One approach is to find the relationships between items by calculating how frequently the items appear together in a subset. This is known as the frequent itemset mining problem. The problem goes as follows, given a database with sets of items, find the items that occur frequently together in a subset.

From smartphones to supercomputers, parallel architectures are nowadays pervasive. However parallel programming is still reserved to experienced and trained programmers. The trend is towards the increase of cores in processors and the number of processors in multiprocessor machines: The need for scalable computing is everywhere. But parallel and distributed programming is still dominated by low-level techniques such as send/receive message passing and POSIX threads. Thus high-level approaches should play a key role in the shift to scalable computing in every computer and device. Algorithmic skeletons (Google MapReduce being the most well-known skeletal parallelism approach), parallel extensions of functional languages such as Haskell and ML, parallel logic and constraint programming, parallel execution of declarative programs such as SQL queries, meta-programming in object-oriented languages, etc. have produced methods and tools that improve the price/performance ratio of parallel software, and broaden the range of target applications. Also, high level languages offer a high degree of abstraction which ease the development of complex systems. Moreover, being based on formal semantics, it is possible to certify the correctness of critical parts of the applications. The aim of all these languages and tools is to improve and ease the development of applications. The paper presented in this special issue are extended versions of papers presented at the Practical Aspects of High-Level Parallel Programming (PAPP) workshop that was affiliated to the International Conference on Computational Science (ICCS) from 2004 to 2012, and the Practical Aspects of High-Level Parallel Programming (PAPP) track of the ACM Symposium on Applied Computing (SAC). It also features a paper written specifically for this special issue. While a lot of work in high-level approaches focus on regular data structures such as arrays and multi-dimensional arrays, the papers of this issue consider more irregular data structures, in particular trees and graphs. Kaheki, Matsuzaki and Emoto present a new approach for parallel reduction on trees in a distributed memory setting. Their algorithm is based on a suitable serialization of trees and its efficiency is shown for the Bulk Synchronous Parallel (BSP) model. Matzusaki proposes a set of efficient skeletons on distributed trees: their efficient implementation relies on the segmentation of trees based on the idea of m-bridges that ensures high locality, and allows to represent local segments as serialized arrays for high sequential performance. Dazzi, Carlini, Lulli and Ricci propose Telos, a high-level approach for large graphs processing based on overlay networks, and an implementation on top of Apache Spark. Hajibaba, Gorgin, and Sharifi present a sequence similarity parallelization technique in the context of another Apache project: Storm a stream processing framework. I wish to thank Anne Benoit and Frederic Gava, co-chairs of some the previous PAPP workshops and the program committee members of the PAPP workshops and the PAPP ACM SAC track who reviewed the initial papers and the revised versions of this special issue.

International audience; SyDPaCC is a set of libraries for the Coq proof assistant. It allows to write naive functional programs (i.e. with high complexity) that are considered as specifications, and to transform them into more efficient versions. These more efficient versions can then be automatically parallelised before being extracted from Coq into source code for the functional language OCaml together with calls to the Bulk Synchronous Parallel ML (BSML) library. In this paper we present a new core version of SyDPaCC for the development of parallel programs correct-by-contruction using the theory of list homomorphisms and algorithmic skeletons implemented and verified in Coq. The framework is illustrated on the the maximum prefix sum problem.

Exception handling is a traditional and natural mechanism to manage errors and events that disrupt the normal flow of program instructions. In most concurrent or parallel systems, exception handling is done locally or sequentially, and cannot guarantee the global coherence of the system after an exception is caught. Working with a structured parallel model is an advantage in this respect. Algorithmic skeletons, that are patterns of parallel algorithms on distributed data structures, offer such a structured model. However very few algorithmic skeleton libraries provide a specific parallel exception mechanism, and no C++-based library. In this paper we propose the design of an exception mechanism for the C++ Orleans Skeleton Library that ensures the global coherence of the system after exceptions are caught. We explain our design choices, experiment on the performance penalty of its use, and we illustrate how to purposefully use this mechanism to extract the results in the course of some algorithms.

International audience; It is difficult for customers to select the adequate cloud providers which fit their needs, as the number of cloud offerings increases rapidly. Many works thus focus on the design of cloud brokers. Unfortunately, most of them do not consider precise security requirements of customers. In this paper, we propose a methodology defined to place services in a multi-provider cloud environment, based on functional and non-functional requirements, including security requirements. To eliminate inner conflicts within customers requirements, and to match the cloud providers offers with these customers requirements, we use a formal analysis tool: Alloy. The broker uses a matching algorithm to place the required services in the adequate cloud providers, in a way that fulfills all customer requirements. We finally present a prototype implementation of the proposed broker.

For the sake of modularity, programming languages with atomic sections should offer nesting and inner parallelism in such sections. The possible escape of a thread created inside a section makes these languages also more expressive. In this paper we address the compilation of such a language towards a language with threads and locks. The design decisions of this compilation pass and of the target language were made with respect to the ultimate goal of a mechanised proof of semantic preservation.

International audience; For the sake of modularity, programming languages with atomic sections should offer nesting and inner parallelism in such sections. The possible escape of a thread created inside a section makes these languages also more expressive. In this paper we address the compilation of such a language towards a language with threads and locks. The design decisions of this compilation pass and of the target language were made with respect to the ultimate goal of a mechanised proof of semantic preservation.

Many applications of computing require performance levels attainable only on parallel architectures. Such systems are now readily available as their price/performance ratio continues to improve. Despite this, corresponding software has not developed to the same levels of capability, price, and flexibility as those of sequential software. There are deep technical reasons for this, which research has been addressing for two decades. Sequential programming has long benefited from high-level programming techniques and tools that have made today's immense range of software economically viable. Research into high-level parallel programming is producing methods and tools that improve the price/performance ratio of parallel software, and broaden the range of target applications. This special issue of Parallel Processing Letters presents recent work of researchers in this field. One promising approach to developing portable parallel programs lies in the use of algorithmic skeletons templates for common patterns of parallel computation. Jocelyn SEROT demonstrates the use of dataflow techniques for efficient implementation of nested dynamic skeletons. Andrea ZAVANELLA applies the BSP cost model to data-parallel skeletons, allowing architecture-independent optimizations. The BSP computation model is also the subject of contributions by Alexandre TISKIN, who shows how threads may be used to allow divide-and-conquer algorithms to be expressed in BSP. Frederic LOULERGUE, who presents a functional calculus of BSP programs ; and Yifeng CHEN & J. W. SANDERS who define a refinement calculus for deriving BSP programs from specifications. Paul H. J. KELLY, Olav BECKMANN, Tony FIELD & Scott B. BADEN present the THEMIS model for dynamic optimizations of run-time parallel program behavior. Hans-Wolfgang LOIDL, Philip W. TRINDER & Carsten BUTZ introduce a way of improving task granularity and data locality in parallel Haskell programs based on systematic transformations of a data class. Zineb H ABB AS, Michael KRAJECKI & Daniel SINGER show a simple decomposition strategy for distributing a constraint satisfaction problem among machines. These papers were first presented at the International Workshop on High-Level Parallel Programming and Applications in Orleans in March 2001. This special

Bulk-Synchronous Parallel (BSP) is a bridging model between abstract execution and concrete parallel architectures that retains enough information to model performance scalability. In order to model BSP program executions, Hains adapted the theory of finite automata to the BSP paradigm by introducing BSP automata [12]. In the initial description of the theory, BSP automata had to be explicitly defined as structured sets of states and transitions. The lack of a clean and efficient algorithm for generating them from regular expressions would have prevented this theory from being used in practice. To alleviate this problem we introduce in this paper an algorithm that generates a BSP automaton recognizing a BSP language defined by a BSP regular expression. The main practical use of BSP automata developed in this paper is the parallelization of finite state automata with an explicit distribution and a performance model, that enable parallel matching of regular expressions. Secondarily, BSP regular expressions provide a convenient structure for automatic code generation of imperative BSP programs that is also developed in this paper.

International audience; The latest developments of the computation systems impose using tools and methodologies able to simplify the development process of parallel software, but also to assure a high level of performance and robustness. Powerlists and their variants are data structures that can be successfully used in a simple, provably correct, functional description of parallel programs, which are divide and conquer in nature. They represent one of the high-level algebraic theories which are appropriate to be used as fundamentals for a model of parallel computation that assures correctness proving. The paper presents how programs defined based on powerlists could be transformed to real code in the functional language OCaml plus calls to the parallel functional programming library Bulk Synchronous Parallel ML. BSML functions follow the BSP model requirements, and so its advantages are introduced in OCaml parallel code. The transformations are based on a framework that assures: simple, correct, efficient implementation. Examples are given and concrete experiments for their executions are conducted. The results emphasise the utility and the efficiency of the framework.

International audience; For over a decade, MapReduce has become a prominent programming model to handle vast amounts of raw data in large scale systems. This model ensures scalability, reliability and availability aspects with reasonable query processing time. However these large scale systems still face some challenges: data skew, task imbalance, high disk I/O and redistribution costs can have disastrous effects on performance. In this paper, we introduce MRFA-Join algorithm: a new frequency adaptive algorithm based on MapReduce programming model and a randomised key redistribution approach for join processing of large-scale datasets. A cost analysis of this algorithm shows that our approach is insensitive to data skew and ensures perfect balancing properties during all stages of join computation. These performances have been confirmed by a series of experimentations.