A paper to be presented at ICLP'08, Udine, Italy, December'08. My co-author Tom Schrijvers will give the presentation but here's already a draft of the talk.
If you've followed my previous posts on (software) transactions (in memory aka STM), this paper is more on the theoretical (greek symbol) side, but still worth a read if you seek for a systematic method to improve the efficiency of your STM code.
In the paper, we enrich the Constraint Handling Rules (CHR) calculus with transactions. If you've never heard the name CHR before, think of multi-set rewriting, bounded transactions, or a form of join pattern with guards and propagation. The paper develops a theory of how to (possibly) transform unbounded transactions to bounded transactions. Under optimistic concurrency control, unbounded transactions (e.g. transactions traversing a dynamic data structure such as a linked list) often yield "false" conflicts which means that transactions are executed sequentially instead of in parallel. Bounded transactions (e.g. dining philosphers which grap a bounded, two, number of forks) are generally free of such (in)efficiency problems. Details are in the paper.