A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs

Granville Barnett , Shengchao Qin

    Research output: Chapter in Book/Report/Conference proceedingConference contribution

    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 languageEnglish
    Title of host publicationFormal Methods and Software Engineering. ICFEM 2012
    EditorsT. Aoki , K. Taguchi
    PublisherSpringer Berlin
    Volume7635
    ISBN (Electronic)9783642342813
    ISBN (Print)9783642342806
    DOIs
    Publication statusPublished - 2012
    EventFormal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods - Kyoto, Japan
    Duration: 12 Nov 201216 Nov 2012
    Conference number: 14

    Publication series

    Name Lecture Notes in Computer Science
    PublisherSpringer Berlin
    Volume7635

    Conference

    ConferenceFormal Methods and Software Engineering - 14th International Conference on Formal Engineering Methods
    Abbreviated titleICFEM 2012
    CountryJapan
    CityKyoto
    Period12/11/1216/11/12

    Fingerprint Dive into the research topics of 'A Composable Mixed Mode Concurrency Control Semantics for Transactional Programs'. Together they form a unique fingerprint.

    Cite this