Moverness for Locks and Transactions

Granville Barnett , Shengchao Qin

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

    Abstract

    Locks are pervasive in multithreaded code. For software transactional memory (STM) to be widely adopted there must be a consensus on a semantics for programs that entail both locks and transactions, particularly for weakly isolated STMs. For instance, in a weakly isolated STM, use of both locks and transactions to access the same data may introduce data races. In response we present a simple and intuitive semantics that guarantees ordered linearisation points for conflicting locks and transactions. Our approach allows us to classify the moverness of locks and transactions, making reasoning about parallel compositions trivial. Under our semantics we show locks to be left movers and transactions right movers, and the serialisability of conflicting locks and transactions.
    Original languageEnglish
    Title of host publication2012 Sixth International Symposium on Theoretical Aspects of Software Engineering
    PublisherIEEE
    ISBN (Print)9781467323536
    DOIs
    Publication statusPublished - 2012
    Event6th International Symposium on Theoretical Aspects of Software Engineering - Beijing, China
    Duration: 4 Jul 20126 Jul 2012
    Conference number: 6

    Conference

    Conference6th International Symposium on Theoretical Aspects of Software Engineering
    Abbreviated titleTASE 2012
    CountryChina
    CityBeijing
    Period4/07/126/07/12

    Fingerprint Dive into the research topics of 'Moverness for Locks and Transactions'. Together they form a unique fingerprint.

  • Cite this

    Barnett , G., & Qin, S. (2012). Moverness for Locks and Transactions. In 2012 Sixth International Symposium on Theoretical Aspects of Software Engineering IEEE. https://doi.org/10.1109/TASE.2012.29