• DocumentCode
    2438142
  • Title

    Model Checking Transactional Memory with Spin

  • Author

    Leary, John O. ; Saha, Bratin ; Tuttle, Mark R.

  • fYear
    2009
  • fDate
    22-26 June 2009
  • Firstpage
    335
  • Lastpage
    342
  • Abstract
    We used the Spin model checker to show that Intel´s implementation of software transactional memory is correct. Transactional memory makes it possible to write properly-synchronized multi-threaded programs without the explicit use of locks. We describe our model of Intel´s implementation, our experience with Spin, what we have shown, and what obstacles remain to showing more.
  • Keywords
    multi-threading; program verification; synchronisation; transaction processing; Spin model checker; software transactional memory; synchronized multithreaded program; Database systems; Distributed computing; Privatization; Read-write memory; Yarn; Spin; Transactional memory; model checking;
  • fLanguage
    English
  • Publisher
    ieee
  • Conference_Titel
    Distributed Computing Systems, 2009. ICDCS '09. 29th IEEE International Conference on
  • Conference_Location
    Montreal, QC
  • ISSN
    1063-6927
  • Print_ISBN
    978-0-7695-3659-0
  • Electronic_ISBN
    1063-6927
  • Type

    conf

  • DOI
    10.1109/ICDCS.2009.72
  • Filename
    5158442
    • Link To Document
    https://search.isc.ac/dl/search/defaultta.aspx?DTC=49&DC=2438142