Detection of Anomalies in TM Programs

Participant: João Lourenço

Home Institution:
CITI / Universidade Nova de Lisboa

Home Country: Portugal

Host: Dr. Eitan Farchi

Host Institution: IBM Research Labs - Haifa

Host Country: Israel

Start Date:

End Date: 2011-12-19

Transactional Memory (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.
While TM may contribute to the development of concurrent programs with fewer errors, its usage does not imply by itself the full correctness of the program. TM programs may still suffer from both low-level and high-level data races. Low-level data races, commonly called simply by data races, result from the inadequate use of a protection mechanism when accessing a shared memory location, such as forgetting to define a code block as atomic.
Data consistency is violated when two synchronized blocks have a non-synchronized (possibly empty) code block between them, and the programer intended to have those two synchronized code blocks running atomically, but mistakenly believed it was sufficient to ensure their individual atomicity. This anomaly is often referred as atomicity violation or high-level data race (HLDR).
The concept of what in a HLDR in concurrent programs is hard or even impossible to define precisely (sound and complete), I have been collaborating with the group of Dr. Eitan Farchi from IBM Research Labs at Haifa (IBM HRL)in the last 2 years investigating algorithms and techniques for static analysis that, by using a best effort strategy, are able to improve the quality of the HDLR detectors for concurrent (Java) transactional memory programs.

Report: here