João Lourenço

This paper presents an automatic verification technique for transactional memory Java programs executing under snapshot isolation level. We certify which transactions in a program are safe to execute under snapshot isolation without triggering the write-skew anomaly, opening the way to run-time optimizations that may lead to considerable performance enhancements. Our work builds on a novel deep-heap analysis technique based on separation logic to statically approximate the read- and write-sets of a transactional memory Java program. We implement our technique and apply our tool to a set of micro benchmarks and also to one benchmark of the STAMP package. We corroborate known results, certifying some of the examples for safe execution under snapshot isolation by proving the absence of write-skew anomalies. In other cases our analysis has identified transactions that potentially trigger previously unknown write-skew anomalies.>

Software Transactional Memory (STM) algorithms correctness rely on metadata associated with the memory locations accessed during the transaction life-time. STM implementations may store this metadata either in-place, by wrapping the memory cells in a container that includes the memory cell itself and the corresponding metadata, or out-place, by resorting to a mapping function that associates the memory cell address to an external table with the corresponding metadata. The implementation techniques for these two approaches are very different and each STM framework is usually biased towards one of them, only allowing the efficient implementation of algorithms that fall into the appropriate category, and inhibiting the fair comparison with STM algorithms falling into the other. In this paper we introduce a technique that supports the use of in-place metadata without requiring to wrap memory cells, thus providing STM algorithms with direct access to the transactional metadata and overcoming the bias. The proposed technique is available as an extension to the DeuceSTM framework and allows the efficient implementation of a wide range of STM algorithms, thus enabling their fair (unbiased) comparison in a common STM infrastructure. We illustrate the benefits of our approach by analyzing its impact in two popular TM algorithms with two different transactional workloads, TL2 and multi-versioning, which bias to out-place and in-place respectively.

A set of methods defining an API (Application Programming Interface) are to be made thread safe; thus running any subset of these methods in parallel should not create races or deadlocks. Originally, the set of methods were not designed to be thread safe, so races and deadlocks are expected when running them in parallel. The number of possible interleavings when running methods from this API in parallel is huge, and this work focuses on the identification of the high level data races introduced by such interleavings. We propose an analysis that avoids the exhaustive exploration of all possible interleavings. For a concurrent program P, the closure of P, clos(P), is defined. Roughly speaking, we can say that the clos(P) is obtained by adding threads to P in such a way that high level data races resulting from running P in parallel to other programs are exposed statically. A set of methods representing the API is then modeled as a set of concurrent programs and their closure is analysed to identify high level data races. These high level data races are then inspected and removed to make the API thread safe. We illustrate the application of this methodology with a simple use case.

Concurrent programs may suffer from concurrency anomalies that may lead to erroneous and unpredictable program behaviors. To ensure program correctness, these anomalies must be diagnosed and corrected. This paper addresses the detection of both low- and high-level anomalies in the Transactional Memory setting. We propose a static analysis procedure and a framework to address Transactional Memory anomalies. We start by dealing with the classic case of low-level dataraces, identifying concurrent accesses to shared memory cells that are not protected within the scope of a memory transaction. Then, we address the case of high-level dataraces, bringing the programmer's attention to pairs of memory transactions that were misspecified and should have been combined into a single transaction. Our framework was applied to a set of programs, collected form different sources, containing well known low- and high-level anomalies. The framework demonstrated to be accurate, confirming the effectiveness of using static analysis techniques to precisely identify concurrency anomalies in Transactional Memory programs.

In this paper we present MoTh, a tool that uses static analysis to enable the automatic verification of concurrency anomalies in Transactional Memory Java programs. Currently MoTh detects high-level dataraces and stale-value errors, but it is extendable by plugging-in sensors, each sensor implementing an anomaly detecting algorithm. We validate and benchmark MoTh by applying it to a set of well known concurrent buggy programs and by close comparison of the results with other similar tools. The results achieved so far are very promising, yielding good accuracy while triggering only a very limited number of false warnings.

Actualmente o mercado residencial de computadores inclui não só multiprocessadores com diversos núcleos (CPUs) como também placas gráficas (GPUs) cuja capacidade de processamento tem evoluído a um ritmo exponencial. Este poder computacional pode ser utilizado para outros fins para além do processamento gráfico, tal como o processamento de algoritmos comuns em computação científica. Neste artigo é apresentada, discutida e avaliada a framework Cheetah, uma framework que distribui programas computacionalmente exigentes sobre uma rede de CPUs e GPUs. Um programador que utilize a Cheetah apenas necessita de especificar o seu programa como um conjunto de kernels OpenCL, relegando para a framework a distribuição destes pelas unidades de processamento disponíveis. O programa pode assim escalar à medida que são adicionados novos recursos computacionais, sem quaisquer esforços adicionais de adaptação ou recompilação. Os testes realizados demonstraram a capacidade de a framework providenciar aceleracçõs até duas ordens de grandeza com um esforço de desenvolvimento reduzido, mesmo quando na presença de recursos computacionais limitados.

Software transactional memory is a promising programming model that adapts many concepts borrowed from the databases world to control concurrent accesses to main memory (RAM). This paper discusses how to support revertible operations, such as memory allocation and release, within software libraries that will be used in software memory transactional contexts. The proposal is based in the extension of the transaction life cycle state diagram with new states associated to the execution of user-defined handlers. The proposed approach is evaluated in terms of functionality and performance by way of a use case study and performance tests. Results demonstrate that the proposal and its current implementation are flexible, generic and efficient

n/a

n/a

n/a

In software, hardware, and embedded system domains, debugging is the process of locating and correcting faults in a system. Depending on the context, the various characteristics of debugging induce different challenges and solutions. Post-silicon hardware debugging, for example, needs to address issues such as limited visibility and controllability, while debugging software entails other issues, such as the handling of distributed or non-deterministic computation. The challenges that accompany such issues are the focus of many current research efforts. Solutions for debugging range from interactive tools to highly analytic techniques. We have seen great advances in debugging technologies in recent years, but bugs continue to occur, and debugging still encompasses significant portions of the life-cycles of many systems. The session covered state-of-the-art approaches as well as promising new research directions in both the hardware and software domains.

This paper presents StarTM , an automatic verification tool for transactional memory Java programs executing under relaxed isolation levels. We certify which transactions in a program are safe to execute under Snapshot Isolation without triggering the write-skew anomaly, opening the way to run-time optimizations that may lead to considerable performance enhancements.
Our tool builds on a novel shape analysis technique based on Separation Logic to statically approximate the read- and write-sets of a transactional memory Java program. This technique is particularly challenging due to the presence of dynamically allocated memory.
We implement our technique and apply our tool to a set of intricate examples. We corroborate known results, certifying some of the examples for safe execution under Snapshot Isolation by proving the absence of write-skew anomalies. In other cases we identify transactions that potentially trigger the write-skew anomaly.

Em caso de falha abrupta de um sistema, é imperativo garantir a consistência do Sistema de Ficheiros (SF). Actualmente existem várias soluções que visam garantir que tanto os dados como os metadados do SF se encontram num estado consistente, mas que não contemplam a garantia de consistência dos dados do ponto de vista das aplicações. Por exemplo, aplicações que pretendam alterar vários ficheiros de configuração terão de encontrar mecanismos para garantir que, ou todos os ficheiros são devidamente alterados, ou nenhum o é, evitando assim que numa situação de falha o conteúdo dos ficheiros fique inconsistente. Do ponto de vista da aplicação, pode não ser simples implementar este comportamento sobre um SF típico; e pode também não ser razoável utilizar um Sistema de Gestão de Bases de Dados (SGBD), que oferece propriedades ACID. Neste artigo propomos, testamos e avaliamos uma integração das propriedades ACID num SF. Partindo do suporte para snapshots do sistema de ficheiros Btrfs, oferece-se uma semântica transaccional às aplicações que operam sobre volumes (sub-árvores) do SF, sem comprometer a semântica POSIX do SF.

Transactional Memory [3] (TM) is a new paradigm for concurrency control that brings the concept of transactions, widely known from the Databases community, into the management of data located in main memory. TM delivers a powerful semantics for constraining concurrency and provides the means for the extensive use of the available parallel hardware. TM uses abstractions that promise to ease the development of scalable parallel applications by achieving performances close to fine-grained locking while maintaining the simplicity of coarse-grained locking.

Transactional Memory allows programmers to reduce the number of synchronization errors introduced in concurrent programs, but does not ensures its complete elimination. This paper proposes a pattern matching based approach to the static detection of atomicity violation, based on a path-sensitive symbolic execution method to model four anomalies that may affect Transactional Memory programs. The proposed technique may be used to to bring to programmer's attention pairs of transactions that the programmer has mis-specified, and should have been combined into a single transaction. The algorithm first traverses the AST tree, removing all the non-transactional blocks and generating a trace tree in the path sensitive manner for each thread. The trace tree is a Trie like data structure, where each path from root to a leaf is a list of transactions. For each pair of threads, erroneous patterns involving two consecutive transactions are then checked in the trace tree. Results allow to conclude that the proposed technique, although triggering a moderate number of false positives, can be successfully applied to Java programs, correctly identifying the vast majority of the relevant erroneous patterns.

The recent developments in virtualization change completely the panorama of the Hardware/OS deployment. New bottlenecks arise in the deployment of application stacks, where IT industry will spend most of the time to assure automation. VIRTU tool aims at managing, configuring and testing distributed ground applications of space systems on a virtualized environment, based on open tools and cross virtualization support. This tool is a spin-off of previous activities performed by the European Space Operations Center (ESOC) and thus it covers the original needs from the ground data systems infrastructure division of the European Space Agency. VIRTU is a testing oriented solution. Its ability to group several virtual machines in an assembly provides the means to easily deploy a full testing infrastructure, including the client/server relationships. The possibility of making on-demand request of the testing infrastructure will provide some infrastructure optimizations, specially having in mind that ESA maintains Ground Control software of various missions, and each mission cam potentially have a different set of System baselines and last up to 15 years. The matrix array of supported system combinations is therefore enormous and any improvement on the process provides substantial benefits to ESA, by reducing the effort and schedule of each maintenance activity. The ESOC's case study focuses on the development and validation activities of infrastructure or mission Ground Systems solutions. The Ground Systems solutions are typically composed of distributed systems that could take advantage of virtualized environments for testing purposes. Virtualization is used as way to optimize maintenance for tasks such as testing new releases and patches, test different system's configurations and replicate tests. The main benefits identified are related to deployment test environment and the possibility to have on-demand infrastructure.

n/a

SmART (Smart Application Reconfiguration Tool) is a framework for the automatic configuration of systems and applications. The tool implements an application configuration workflow that resorts to the similarities between configuration files (i.e., patterns such as parameters, comments and blocks) to allow a syntax independent manipulation and transformation of system and application configuration files.Without compromising its generality, SmART targets virtualized IT infrastructures, configuring virtual appliances and its applications. SmART reduces the time required to (re)configure a set of applications by automating time-consuming steps of the process, independently of the nature of the application to be configured. Industrial experimentation and utilization of SmART show that the framework is able to correctly transform a large amount of configuration files into a generic syntax and back to their original syntax. They also show that the elapsed time in that process is adequate to what would be expected of an interactive tool. SmART is currently being integrated into the VIRTU bundle, whose trial version is available for download from the projects web page.

Some performance issues of transactional memory are caused by unnecessary abort situations where non serializable and yet non conflicting transactions are scheduled to execute concurrently. Smartly relaxing the isolation properties of transactions may overcome these issues and attain considerable performance improvements. However, it is known that relaxing isolation restrictions may lead to runtime anomalies. In some situations, like database management systems, developers may choose that compromise, hence avoiding anomalies explicitly. Memory transactions protect the state of the program, therefore execution anomalies may have more severe consequences in the semantics of programs. So, the compromise between a relaxed isolation strategy and enforcing the necessary program correctness is harder to setup. The solution we devise is to statically analyse programs to detect the kind of anomalies that emerge under snapshot isolation. Our approach allows a compiler to either warn the developer about the possible snapshot isolation anomalies in a given program, or possibly inform automatic correctness strategies to ensure Serializability.

Programs containing concurrency anomalies will most probably exhibit harmful erroneous and unpredictable behaviors. To ensure program correctness, the sources of those anomalies must be located and corrected. Concurrency anomalies in Transactional Memory (TM) programs should also be diagnosed and fixed. In this paper we propose a framework to deal with two different categories of concurrency anomalies in TM. First, we will address low-level TM anomalies, also called dataraces, which arise from executing programs in weak isolation. Secondly, we will address high-level TM anomalies, also called high-level dataraces, bringing the programmers attention to pairs of transactions that the programmer has misspecified, and should have been combined into a single transaction. Our framework was validated against a set of programs with well known anomalies and demonstrated high accuracy and effectiveness, thus contributing for improving the correctness of TM programs

This document describes a work-in-progress development of NGen-VM, a distributed infrastructure that manages execution environments with run-time and programming language support targeting applications developed in the Java programming language, deployed over clusters of many-core computers. For each running application or suite of related applications, a dedicated single-system image will be provided, regardless of the concurrent threads running on a single machine (on several cores) or scattered on different computers. Such system images rely on a single model for concurrency management (Transactional Shared Memory Model), in order fill the gap between the hardware infrastructure of clusters of many-core nodes and the application runtime that is independent from that hardware infrastructure. Interactions between threads in the same tasks will be supported by a Transactional Memory framework that provides the programming language with Atomic and Isolated code regions. Interactions between thread on different machines will also use the Transactional Memory model, but now resorting to a Distributed Shared Memory abstraction.

Transactional memory is a new trend in concurrency control that was boosted by the advent of multi-core processors and the near to come many-core processors. It promises the performance of finer grain with the simplicity of coarse grain threading. However, there is a clear absence of software development tools oriented to the transactional memory programming model, which is confirmed by the very small number of related scientific works published until now. This paper describes ongoing work. We propose a very low overhead monitoring framework, developed specifically for monitoring TM computations, that collects the transactional events into a single log file, sorted in a global order. This framework is then used by a visualization tool to display different types of charts from two categories: statistical charts and thread-time space diagrams. These last diagrams are interactive, allowing to identify conflicting transactions. We use the visualization tool to analyse the behavior of two different, but similar, testing applications, illustrating how it can be used to better understand the behavior of these transactional memory applications.

Software Transactional Memory is a concurrency control technique gaining increasing popularity, as it provides high-level concurrency control constructs and eases the development of highly multi-threaded applications. But this easiness comes at the expense of restricting the operations that can be executed within a memory transaction, and operations such as terminal and file I/O are either not allowed or incur in serious performance penalties. Database I/O is another example of operations that usually are not allowed within a memory transaction. This paper proposes to combine memory and database transactions in a single unified model, benefiting from the ACID properties of the database transactions and from the speed of main memory data processing. The new unified model covers, without differentiating, both memory and database operations. Thus, the users are allowed to freely intertwine memory and database accesses within the same transaction, knowing that the memory and database contents will always remain consistent and that the transaction will atomically abort or commit the operations in both memory and database. This approach allows to increase the granularity of the in-memory atomic actions and hence, simplifies the reasoning about them.

Database systems are a key component behind many of today's computer systems. As a consequence, it is crucial that database systems provide correct and continuous service despite unpredictable circumstances, such as software bugs or attacks. This paper presents the design of Byzantium, a Byzantine fault-tolerant database replication middleware that provides snapshot isolation (SI) semantics. SI is very popular because it allows increased concurrency when compared to serializability, while providing similar behavior for typical workloads. Thus, Byzantium improves on existing proposals by allowing increased concurrency and not relying on any centralized component. Our middleware can be used with off-the-shelf database systems and it is built on top of an existing BFT library.

Software transactional memory (STM) is a promising programming model that adapts many concepts borrowed from the databases world to control concurrent accesses to memory (RAM) locations. In this paper we propose a new classification for the active states of a transaction; a new memory quiescing algorithm, to allow the safe transition of a memory block form transactional to non-transactional space; we compare word and object transactional grain units; and evaluate the cost of consistent state validation, arguing that this cost can be minimized by performing partial validation on problematic code regions.