Participant: Jan Konczak
Home Institution: Poznań University of Technology, Institute of Computing Science
Home Country: Poland
Host: Prof. Rachid Guerraoui
Host Institution: École Polytechnique Fédérale de Lausanne, Distributed Programming Laboratory
Host Country: Switzerland
Start Date: 2013-05-19
End Date: 2013-06-30
Description: Contrary to ACID transactions, transactions that appear in transactional memory and geo- distributed (or geo-replicated) systems cannot be precisely and comprehensively described using only the concepts, models and properties from database and shared memory systems. In recent years, Guerraoui and Kapałka defined a model of transactional memory which can be used to reason about properties and correctness of TM implementations. For this, they introduced a notion of opacity which replaces classical serializability of database transactions, and also discussed the progress (or liveness) properties of lock-based and obstruction-free TMs.
However, the model does not address some aspects of transactional systems, such as irrevo- cable operations and nested transactions. These aspects are notoriously difficult to design and reason about. Many existing TM implementations simply either forbid them which decreases the number of potential applications (e.g. Haskell TM), or they do not give any guarantees which jeopardizes correctness. The use of irrevocable operations (such as I/O or system calls) inside transactions is from pragmatic reasons unavoidable. On the other hand, nested transactions ap- pear naturally whenever a transaction calls a library function that contains some synchronized code.
Thus, there is an urgent need to develop a model in which TM properties will be rethought taking into account irrevocable operations and also nested transactions. The irrevocable opera- tions cause side effects that cannot be rolled back but may be compensated. This means that consistency guarantees should take into account these various additional scenarios. This raises several open research questions: How to model the side effects? What properties can a TM ensure if we assume side effects in addition to memory effects (or memory state)? When is a TM correct then? How to prove the correctness of a TM implementation with side effects and partial rollbacks (due to nesting)? What are the impossibility results (if any)? In the proposed project, we plan to focus on a model which will provide an abstraction to reason about these open problems. During the STSM we would like to begin this work focusing on irrevocable operations, and continue after STSM, possibly including in the model other aspects such as transaction nesting. The project will be done under supervision of Prof. Rachid Guerraoui at EPFL and Dr Paweł Wojciechowski at Poznań University of Technology.
Short Term Scientific Missions Applications > STSM Visits > Analysis and Monitoring of Transactional Memory Programs >