MoTH: Practical Verification of High-Level Dataraces in Transactional Memory Programs

MoTH: Practical Verification of High-Level Dataraces in Transactional Memory Programs
Repository URL: 
https://projectos.fct.unl.pt/projects/di-moth/wiki

Transactional Memory (TM) is an approach to concurrency control in general purpose programming languages that inherits the concept of transaction from the database setting. Unlike other language constructs such as locks, TM has an optimistic approach to concurrency control by allowing more than one thread to access simultaneously the same critical section. A transaction always executes as if it is alone in the system, and in the end its effects are undone (rolled back) if it conflicts with another concurrent transactions. In spite of the potential for increasing scalability and performance, TM is a recent and developing programming model and still has a very limited impact in real-world applications.

Designing and developing concurrent software is difficult and error prone. Concurrent programs exhibit concurrency anomalies that originate faults and failures. Despite some claims that TM programs are less error prone, they still exhibit concurrency anomalies such as high-level dataraces, i.e., wrong delimitations of transactions' scope, and stale-value errors, that occur when the value of a shared variable jumps from an atomic block to another.

Programs with this kind of anomalies can exhibit unpredictable and wrong behaviour, not fulfilling the goals for which they were conceived.

This work aims the detection of anomalies through static analysis of transactional Java ByteCode programs that execute in strong atomicity. A extensible and flexible framework is proposed, which can be extended with plugins that detect specific types of anomalies.

With this framework we expect to prove that high-level dataraces and stale-value errors can be detected with reasonable precision through static analysis.

Keywords

Static Analysis; Testing; Verification; Concurrency; Software Transactional Memory

Project Info

Coordinated by: CITI
Project Type: Basic research or R&D projects
Total Funding Amount: Not funded

Start Date: 2010-09-15
End Date: ?

Participants

@ CITI — FCT/UNL
João Lourenço (Principal Investigator)
Ricardo Dias (MSc Student)
Vasco Pessanha (MSc Student)

Recommended Release

Release Package Date
1.0 Download (5.58 MB) Release info Dec 30 2011

Recent Releases

Release Package Date
1.0 Download (5.58 MB) Release info Dec 30 2011