Computer Science – Logic in Computer Science
Scientific paper
2006-10-24
Computer Science
Logic in Computer Science
29 pages
Scientific paper
The Software Transactional Memory (STM) model is an original approach for controlling concurrent accesses to ressources without the need for explicit lock-based synchronization mechanisms. A key feature of STM is to provide a way to group sequences of read and write actions inside atomic blocks, similar to database transactions, whose whole effect should occur atomically. In this paper, we investigate STM from a process algebra perspective and define an extension of asynchronous CCS with atomic blocks of actions. Our goal is not only to set a formal ground for reasoning on STM implementations but also to understand how this model fits with other concurrency control mechanisms. We also view this calculus as a test bed for extending process calculi with atomic transactions. This is an interesting direction for investigation since, for the most part, actual works that mix transactions with process calculi consider compensating transactions, a model that lacks all the well-known ACID properties. We show that the addition of atomic transactions results in a very expressive calculus, enough to easily encode other concurrent primitives such as guarded choice and multiset-synchronization (\`{a} la join-calculus). The correctness of our encodings is proved using a suitable notion of bisimulation equivalence. The equivalence is then applied to prove interesting ``laws of transactions'' and to obtain a simple normal form for transactions.
Acciai Lucia
Boreale Michele
Zilio Silvano Dal
No associations
LandOfFree
A Concurrent Calculus with Atomic Transactions does not yet have a rating. At this time, there are no reviews or comments for this scientific paper.
If you have personal experience with A Concurrent Calculus with Atomic Transactions, we encourage you to share that experience with our LandOfFree.com community. Your opinion is very important and A Concurrent Calculus with Atomic Transactions will most certainly appreciate the feedback.
Profile ID: LFWR-SCP-O-343699