Esta Dissertação apresenta um modelo de paralelismo de grão fino para utilização em aplicações baseadas em objetos distribuídos. A pesquisa é desenvolvida sobre o modelo de distribuição de objetos da linguagem DPC++, uma extensão de C++ concebida na Universidade Federal do Rio Grande do Sul. A motivação para o desenvolvimento deste modelo é a crescente disponibilidade de arquiteturas multiprocessadas e de tecnologias de comunicação de alto desempenho, o que permite o aproveitamento eficiente de um nível de concorrência de menor granularidade. O objetivo do trabalho é integrar de forma adequada e eficiente a utilização de tal nível de concorrência no modelo original de distribuição de objetos de DPC++, permitindo que as aplicações desenvolvidas com a linguagem possam explorar ao máximo o poder computacional oferecido pelas arquiteturas citadas. Como principais características, o modelo proposto apresenta a capacidade de concorrência entre os métodos de um mesmo objeto distribuído e a introdução de um mecanismo de sincronização baseado na semântica de monitores. Os resultados obtidos com a implementação de uma aplicação de geração de fractais de Mandelbrot demonstram que, em termos de desempenho, o modelo apresentado efetivamente atinge seus objetivos. Além disso, a extinção a sintaxe original de programação de DPC++ revela importante contribuição no sentido de aumentar o poder de expressão da linguagem para o desenvolvimento de aplicações paralelas. / This Thesis presents a fine-grain concurrency model for applications based on distributed objects. The basis for the development of this research is the model of distribution of objects presented by the language DPC++, an extension of C++ conceived at the Federal University of Rio Grande do Sul. The motivation for the development of this model is the growing availability of multiprocessor architectures and high-performance communication technologies, which allows for the efficient use of a finer grain of concurrency. The purpose of this work is to efficiently integrate such level of concurrency into the original model of distribution of objects of DPC++, making it possible for the applications developed with the language to thoroughly explore the computational power offered by the mentioned architectures. As main features the proposed model presents the possibility of concurrency between the methods of a single distributed object and the introduction of a synchronisation mechanism based on the semantics of monitors. The results obtained with the implementation of aMandelbrot fractal generation application showthat, in relation to performance, the presented model effectively reaches its purposes. In addition, the extension to the original programming sintax of DPC++ reveals an important contribution towards a higher expressivity degree in the development of parallel applications.

Sistemas multi-agentes devem oferecer recursos suficientes para que seus agentes possam interagir de maneira satisfatória e atingir seus objetivos. Um exemplo de recurso é um conjunto de dados armazenados em algum tipo de mecanismo de persistência, como um sistema gerenciador de banco de dados. O acesso a dados deve ser possível mesmo que eles estejam distribuídos, fato inclusive que também caracteriza os sistemas multi-agentes. Assim, este trabalho apresenta um sistema chamado DASE cujo objetivo é prover a agentes o acesso a dados distribuídos de forma simples e transparente, ou seja, independentemente da complexidade que o ambiente dos agentes possui e das peculiaridades do Sistema de Banco de Dados Distribuído. O DASE suporta qualquer Sistema Gerenciador de Banco de Dados, seja ele centralizado ou distribuído, desde que o mesmo esteja em conformidade com o JDBC. Além disso, oferece recursos importantes como controle de concorrência, suporte a ambientes de dados simultâneos e uso de sentenças de acesso a dados pré-definidas e parametrizadas. Todos os aspectos mais importantes analisados durante o projeto deste sistema estão descritos neste trabalho, evidenciando e justificando o porquê de cada decisão que certamente refletiram no funcionamento e comportamento do DASE. O sistema foi implementado de acordo com o seu projeto, resultando em uma versão funcional e estável, o que foi comprovado através de seu uso em um projeto que envolvia sistemas multiagentes e controle de tráfego aéreo. Além disso, alguns testes de análise de desempenho considerando cenários variados foram realizados. / Multi-agent systems must offer the needed resources to allow their agents to interact and to reach their goals. An example of resource is a set of data stored in any kind of resource manager, such as a database management system. Data access must be possible even if the data is distributed, characteristic that is also present in multi-agent systems. Thus, this work describes a system whose objective is to provide to agents distributed data access in a simple and transparent way, in other words, hiding the agent environment and complexities related to distributed database systems. DASE supports any database management system, centralized or distributed, in compliance with JDBC (Java Database Connectivity). In addition it offers important features, such as concurrency control, simultaneous data environments and stored SQL sentences. All challenges and important aspects overcome in order to design and implement DASE are described, explaining and justifying every decision that in some way had a participation to form DASE set of functions and behavior. The system was implemented following its design, resulting in a functional and stable version, what could be verified through its adoption in a project based on multiagent systems and air traffic control systems. In addition, a plenty of performance tests were done regarding different scenarios.

O uso de Web Services tem aberto novas possibilidades de desenvolvimento de software, entre elas a composição de serviços. A composição de serviços apresenta novas questões no ambiente computacional, entre elas a execução integral, garantindo consistência e contemplando o controle de concorrência. O workflow é um conjunto de tarefas e interações organizadas de modo que forneça uma funcionalidade ao sistema, provendo a automatização de processos complexos, através da composição de serviços. Tal composição deve ser executada de forma transacional, processando as operações com consistência. A execução de workflows oriundos de domínios diferentes, faz com que os serviços que estão sendo utilizados, não possuam ciência do contexto da execução, podendo gerar atendimentos que não sejam justos, causando situações de deadlock e de starvation. Este trabalho apresenta estratégias para a execução de workflows em domínios distintos, que requisitam múltiplos serviços de um mesmo conjunto, sem a necessidade de um coordenador central, de forma transacional. O atendimento a requisição contempla uma política justa na utilização do recurso que impede a ocorrência de deadlock ou de starvation para os workflows em execução. Os experimentos realizados neste trabalho mostram que o sistema desenvolvido, aplicando as estratégias propostas, executa as composições de serviços de maneira transacional, atendendo as requisições com justiça, livre de deadlock e starvation, mantendo o sistema independente e autônomo. / Web Services are increasing software development possibilities, among then service composition. Service composition introduces new issues on computational environment, such as the whole service execution, ensuring consistency and concurrency control. Workflow is a set of organized tasks and interactions in order to provide functionality to the system, automating complex process through composition service. Such composition must be performed by transactional support, performing operations consistently. The workflow execution from different domain clients sharing the same composition make these clients ignore the execution context. It may cause inconsistencies, from unfair attendance to deadlock or starvation. This work depicts strategies for workflow execution from different domains, requesting multiple services from the same composition, without a centralized coordinator, in transactional way. The request attendance contains a fair policy for resource usage and consumption to avoid deadlock and starvation. Applying the proposed strategy on the experiments performed in this work, it confirms that the developed system executes service composition with transactional support, avoiding deadlock or starvation, keeping the whole system autonomous and independent.

<p>An embedded system is an application-specific system that is typically dedicated to performing a particular task. Majority of embedded systems are also real-time, implying that timeliness in the system need to be enforced. An embedded system needs to be enforced efficient management of a large amount of data, including maintenance of data freshness in an environment with limited CPU and memory resources. Uniform and efficient data maintenance can be ensured by integrating database management functionality with the system. Furthermore, the resources can be utilized more efficiently if the redundant calculations can be avoided. On-demand updating and active behavior are two solutions that aim at decreasing the number of calculations on data items in embedded systems.</p><p>COMET is a COMponent-based Embedded real-Time database, developed to meet the increasing requirements for efficient data management in embedded real-time systems. The COMET platform has been developed using a novel software engineering technique, AspeCtual COmponent-based Real-time software Development (ACCORD), which enables creating database configurations, using software components and aspects from the library, based on the requirements of an application. Although COMET provides uniform and efficient data management for real-time and embedded systems, it does not provide support for on-demand and active behavior.</p><p>This thesis is focusing on design, implementation, and evaluation of two new COMET configurations, on-demand updating of data and active behavior. The configurations are created by extending the COMET component and aspect library with a set of aspects that implement on-demand and active behavior. The on-demand updating aspect implements the ODDFT algorithm, which traverses the data dependency graph in the depth-first manner, and triggers and schedules on-demand updates based on data freshness in the value domain. The active behavior aspect enables the database to take actions when an event occurs and a condition coupled with that event and action is fulfilled.</p><p>As we show in the performance evaluation, integrating on-demand and active behavior in COMET improves the performance of the database system, gives a better utilization of the CPU, and makes the management of data more efficient.</p>

La validation des systèmes critiques réalistes nécessite d'être capable de modéliser et de vérifier formellement des données complexes, du parallélisme asynchrone, et du temps-réel simultanément. Des langages de haut-niveau, comme ceux qui héritent des fondations théoriques des algèbres de processus, ont une syntaxe concise et une grande expressivité pour représenter ces aspects. Cependant, ils disposent de peu d'outils logiciels permettant d'appliquer des algorithmes efficaces du model-checking. Néanmoins, de tels outils existent pour des modèles graphiques, de niveau plus bas, tels que les automates temporisés (par exemple UPPAAL) et les réseaux de Petri temporisés (par exemple TINA). Les modèles intermédiaires sont un moyen pour combler le fossé qui sépare les langages des modèles graphiques. Par exemple, NTIF (New Technology Intermediate Format) a été proposé pour représenter des processus séquentiels non temporisés qui manipulent des données complexes. Dans cette thèse, nous proposons un nouveau modèle nommé ATLANTIF, qui enrichit NTIF de constructions temps-réel et de compositions parallèles de processus séquentiels. Leur synchronisation est exprimée d'une manière simple et intuitive par la nouvelle notion de synchroniseur. Nous montrons qu'ATLANTIF est capable d'exprimer les constructions principales des langages de haut niveau. Nous présentons aussi des traducteurs d'ATLANTIF vers des automates temporisés (pour la vérification avec UPPAAL) et vers des réseaux de Petri temporisés (pour la vérification avec TINA). Ainsi, ATLANTIF étend la classe des systèmes qui peuvent en pratique être vérifiés formellement, ce que nous illustrons par un exemple.

As software systems become larger and more complex, developers require the ability to model abstract concepts while ensuring consistency across the entire project. The internet has changed the nature of software by increasing the desire for software deployment across multiple distributed platforms. Finally, increased dependence on technology requires assurance that designed software will perform its intended function. This thesis introduces the Formal Object Interaction Language (FOIL). FOIL is a new object-oriented modeling language specifically designed to address the cumulative shortcomings of existing modeling techniques. FOIL graphically displays software structure, sequential and concurrent behavior, process, and interaction in a simple unified notation, and has an algebraic representation based on a derivative of the π-calculus. The thesis documents the technique in which FOIL software models can be mathematically verified to anticipate deadlocks, ensure consistency, and determine object state reachability. Scalability is offered through the concept of behavioral inheritance; and, FOIL’s inherent support for modeling concurrent behavior and all known workflow patterns is demonstrated. The concepts of process achievability, process complete achievability, and process determinism are introduced with an algorithm for simulating the execution of a FOIL object model using a FOIL process model. Finally, a technique for using a FOIL process model as a constraint on FOIL object system execution is offered as a method to ensure that object-oriented systems modeled in FOIL will complete their processes based activities. FOIL’s capabilities are compared and contrasted with an extensive array of current software modeling techniques. FOIL is ideally suited for data-aware, behavior based systems such as interactive or process management software.

The goal of this dissertation is to present new and improved techniques for fully automatic verification of sequential and concurrent software libraries. In most cases, automatic software verification is plagued by undecidability, while in many others it suffers from prohibitively high computational complexity. Model checking -- a highly successful technique used for verifying finite state hardware circuits against logical specifications -- has been less widely adapted for software, as software verification tends to involve reasoning about potentially infinite state-spaces. Two of the biggest culprits responsible for making software model checking hard are heap-allocated data structures and concurrency. In the first part of this dissertation, we study the problem of verifying shape properties of sequential data structure libraries. Such libraries are implemented as collections of methods that manipulate the underlying data structure. Examples of such methods include: methods to insert, delete, and update data values of nodes in linked lists, binary trees, and directed acyclic graphs; methods to reverse linked lists; and methods to rotate balanced trees. Well-written methods are accompanied by documentation that specifies the observational behavior of these methods in terms of pre/post-conditions. A pre-condition [phi] for a method M characterizes the state of a data structure before the method acts on it, and the post-condition [psi] characterizes the state of the data structure after the method has terminated. In a certain sense, we can view the method as a function that operates on an input data structure, producing an output data structure. Examples of such pre/post-conditions include shape properties such as acyclicity, sorted-ness, tree-ness, reachability of particular data values, and reachability of pointer values, and data structure-specific properties such as: "no red node has a red child'', and "there is no node with data value 'a' in the data structure''. Moreover, methods are often expected not to violate certain safety properties such as the absence of dangling pointers, absence of null pointer dereferences, and absence of memory leaks. We often assume such specifications as implicit, and say that a method is incorrect if it violates such specifications. We model data structures as directed graphs, and use the two terms interchangeably. Verifying correctness of methods operating on graphs is an instance of the parameterized verification problem: for every input graph that satisfies [phi], we wish to ensure that the corresponding output graph satisfies [psi]. Control structures such as loops and recursion allow an arbitrary method to simulate a Turing Machine. Hence, the parameterized verification problem for arbitrary methods is undecidable. One of the main contributions of this dissertation is in identifying mathematical conditions on a programming language fragment for which parameterized verification is not only decidable, but also efficient from a complexity perspective. The decidable fragment we consider can be broadly sub-divided into two categories: the class of iterative methods, or methods which use loops as a control flow construct to traverse a data structure, and the class of recursive methods, or methods that use recursion to traverse the data structure. We show that for an iterative method operating on a directed graph, if we are guaranteed that if the number of destructive updates that a method performs is bounded (by a constant, i.e., O(1)), and is guaranteed to terminate, then the correctness of the method can be checked in time polynomial in the size of the method and its specifications. Further, we provide a well-defined syntactic fragment for recursive methods operating on tree-like data structures, which assures that any method in this fragment can be verified in time polynomial in the size of the method and its specifications. Our approach draws on the theory of tree automata, and we show that parameterized correctness can be reduced to emptiness of finite-state, nondeterministic tree automata that operate on infinite trees. We then leverage efficient algorithms for checking the emptiness of such tree automata to obtain a tractable verification framework. Our prototype tool demonstrates the low theoretical complexity of our technique by efficiently verifying common methods that operate on data structures. In the second part of the dissertation, we tackle another obstacle for tractable software verification: concurrency. In particular, we explore application of a static analysis technique based on interprocedural dataflow analysis to predict and document deadlocks in concurrent libraries, and analyze deadlocks in clients that use such libraries. The kind of deadlocks that we focus result from circular dependencies in the acquisition of shared resources (such as locks). Well-written applications that use several locks implicitly assume a certain partial order in which locks are acquired by threads. A cycle in the lock acquisition order is an indicator of a possible deadlock within the application. Methods in object-oriented concurrent libraries often encapsulate internal synchronization details. As a result of information hiding, clients calling the library methods may cause thread safety violations by invoking methods in a manner that violates the partial ordering between lock acquisitions that is implicit within the library. Given a concurrent library, we present a technique for inferring interface contracts that speciy permissible concurrent method calls and patterns of aliasing among method arguments that guarantee deadlock-free execution for the methods in the library. The contracts also help client developers by documenting required assumptions about the library methods. Alternatively, the contracts can be statically enforced in the client code to detect potential deadlocks in the client. Our technique combines static analysis with a symbolic encoding for tracking lock dependencies, allowing us to synthesize contracts using a satisfiability modulo theories (SMT) solver. Additionally, we investigate extensions of our technique to reason about deadlocks in libraries that employ signalling primitives such as wait-notify for cooperative synchronization. We demonstrate its scalability and efficiency with a prototype tool that analyzed over a million lines of code for some widely-used open-source Java libraries in less than 50 minutes. Furthermore, the contracts inferred by our approach have been able to pinpoint real bugs, i.e. deadlocks that have been reported by users of these libraries. / text

Formal methods offer a way to deal with the complexity of information systems. They are adapted to a variety of domains like design, verification, model-checking, test and supervision. But information systems are also more and more often distributed, first because of the generalization of information networks, but also because inside a single device, like a computer, the numerous components run concurrently. The problem is that concurrency is known to be a major difficulty for the use of formal methods because it causes a combinatorial explosion of the state space of the systems. This difficulty comes sometimes with another one due to time when it plays an important role in the behaviour of the systems, for instance when the execution time is a critical parameter. These two difficulties, concurrency and real-time, have guided my research works. Sometimes I have tackled one of these two aspects separately, but in many of my works, I have dealt with the problems that arise when one studies systems that are both concurrent and real-time. In my habilitation thesis, I give an overview of my recent research works on dependencies between events in real-time distributed systems and on implementability issues for these systems.

This thesis aims to present solutions to improve the performance of SQLite library on mobile systems. In particular, two approaches are presented to add lightweight locking mechanisms to the SQLite library and improve concurrency of the SQLite library on Android operating system. The impact on performance is discussed after each section. Many applications on the Android operating system rely on the SQLite library to store ordered data. However, due to heavy synchronization primitives used by the library, it becomes a performance bottleneck for applications which push large amount of data into the database. Related work in this area also points to SQLite database as one of the factors for limiting performance. With increasing network speeds, the storage system can become a performance bottleneck, as applications download larger amounts of data. The following work in this thesis addresses these issues by providing approaches to increase concurrency and add light-weight locking mechanisms. The factors determining the performance of Application Programming Interfaces provided by SQLite are first gathered from IO traces of common database operations. By analyzing these traces, opportunities for improvements are noticed. An alternative locking mechanism is added to the database file using byte-range locks for fine-grained locking. Its impact on performance is measured using SQLite benchmarks as well as real applications. A multi-threaded benchmark is designed to measure the performance of fine grained locking in multi-threaded applications using common database operations. Recent versions of SQLite use write ahead logs for journaling. We see that writes to this sequential log can occur concurrently, especially in flash drives. By adding a sequencing mechanism for the write ahead log, the writes can proceed simultaneously. The performance of this method is also analyzed using the synthetic benchmarks and multi-threaded benchmarks. By using these mechanisms, the library is observed to gain significant performance for concurrent writes.

Concurrence est concernée par les systèmes informatiques des agents multiples qui interagissent les uns avec les autres. Bisimilarité est l'un des principales représentantes de ces derniers. Programmation concurrente par contraintes (ccp) est un formalisme qui combine le point de vue traditionnel des formules algébriques et opérationnelles des calculs de processus avec une notion déclarative basée sur logique. La définition standard de bisimilarité n'est pas complètement satisfaisante pour ccp car il donne une équivalence qui est trop à grain fin. Nous introduisons une sémantique de transitions étiquetées et une notion de bisimilarité totalement abstraite à l'équivalence observationnelle en ccp. Lorsque l'espace d'état d'un système est fini, la notion ordinaire de bisimilarité peut être calculé par l'algorithme de partition de raffinement, mais, cet algorithme ne fonctionne pas pour la bisimilarité de ccp. Par conséquent, nous fournissons un algorithme que nous permet de vérifier bisimilarité forte pour ccp, en utilisant un pré-raffinement et une fonction de partition basée sur la bisimilarité irredondante. Bisimilarité faible est une équivalence comportementale obtenue en prenant en compte uniquement les actions qui sont observables dans le système. Typiquement, le raffinement de partition standard peut être utilisé pour décider bisimilarité faible simplement en utilisant la réduction de Milner allant de faible à forte. Nous démontrons que, en raison de ses impliquées transitions étiquetées, la technique mentionnée ci-dessus ne fonctionne pas pour ccp. Nous donnons une réduction qui nous permet d'utiliser cet algorithme pour ccp pour décider cette équivalence.