Abstract
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.
| Original language | English |
|---|---|
| Title of host publication | Formal Methods and Software Engineering. ICFEM 2012 |
| Editors | T. Aoki , K. Taguchi |
| Publisher | Springer Berlin |
| Volume | 7635 |
| ISBN (Electronic) | 9783642342813 |
| ISBN (Print) | 9783642342806 |
| DOIs | |
| Publication status | Published - 2012 |
| Event | Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods - Kyoto, Japan Duration: 12 Nov 2012 → 16 Nov 2012 Conference number: 14 |
Publication series
| Name | Lecture Notes in Computer Science |
|---|---|
| Publisher | Springer Berlin |
| Volume | 7635 |
Conference
| Conference | Formal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods |
|---|---|
| Abbreviated title | ICFEM 2012 |
| Country/Territory | Japan |
| City | Kyoto |
| Period | 12/11/12 → 16/11/12 |