Publications

Export 30 results:
Sort by: Author Title Type [ Year  (Desc)]
2011
Dias, R. J., J. C. Seco, and J. M. Lourenço, Detection of Snapshot Isolation Anomalies in Software Transactional Memory: A Static Analysis Approach, : Universidade Nova de Lisboa, UNL-DI-5-2011. 2011-dias.pdf
Pessanha, V., R. J. Dias, J. M. Lourenço, E. Farchi, and D. Sousa, "Practical verification of high-level dataraces in transactional memory programs", Proceedings of 9th the Workshop on Parallel and Distributed Systems: Testing, Analysis, and Debugging, New York, NY, USA, ACM, pp. 26–34, July, 2011. Abstract2011-padtad.pdf

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.

Lourenço, J. M., D. Sousa, B. C. Teixeira, and R. J. Dias, "Detecting concurrency anomalies in transactional memory programs", Comput. Sci. Inf. Syst., vol. 8, no. 2, pp. 533–548, 2011. Abstract2011-comsis.pdf

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

Dias, R. J., D. Distefano, J. M. Lourenço, and J. C. Seco, StarTM: Automatic Verification of Snapshot Isolation in Transactional Memory Java Programs, , no. UNL-DI-6-2011, Lisboa, Departamento de Informática FCT/UNL, 2011. Abstractddls11.pdf

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.

Sampaio, P., P. Ferreira, and L. Veiga, "Transparent scalability with clustering for Java e-science applications", Proceedings of the 11th IFIP WG 6.1 international conference on Distributed applications and interoperable systems, Berlin, Heidelberg, Springer-Verlag, pp. 270–277, 2011. Abstract2011-dais-sampaio.pdf

The two-decade long history of events relating object-oriented programming, the development of persistence and transactional support, and the aggregation of multiple nodes in a single-system image cluster, appears to convey the following conclusion: programmers ideally would develop and deploy applications against a single shared global memory space (heap of objects) of mostly unbounded capacity, with implicit support for persistence and concurrency, transparently backed by a possibly large number of clustered physical machines.

In this paper, we propose a new approach to the design of OODB systems for Java applications: (O3)2 (pronounced ozone squared). It aims at providing to developers a single-system image of virtually unbounded object space/heap with support for object persistence, object querying, transactions and concurrency enforcement, backed by a cluster of multi-core machines with Java VMs that is kept transparent to the user/developer. It is based on an existing persistence framework (ozone-db) and the feasibility and performance of our approach has been validated resorting to the OO7 benchmark.

loading