A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs

摘要

Most software transactional memories employ optimistic concurrency control. A pessimistic semantics, however, is not without its benefits: its programming model is often much simpler to reason about and supports the execution of irreversible operations. We present a programming model that supports both optimistic and pessimistic concurrency control semantics. Our pessimistic transactions, guaranteed transactions (gatomics), afford a stronger semantics than that typically employed by pessimistic transactions by guaranteeing run once execution and safe encapsulation of the privatisation and publication idioms. We describe our mixed mode transactional programming language by giving a small step operational semantics. Using our semantics and their derived schedules of actions (reads and writes) we show that conflicting transactions (atomics) and gatomics are serialisable. We then go on to define schedules of actions in the form of Java's memory model (JMM) and show that the same properties that held under our restrictive memory model also hold under our modified JMM.