---
res:
  bibo_abstract:
  - Pseudo-code descriptions of STMs assume sequentially consistent program execution
    and atomicity of high-level STM operations like read, write, and commit. These
    assumptions are often violated in realistic settings, as STM implementations run
    on relaxed memory models, with the atomicity of operations as provided by the
    hardware. This paper presents the first approach to verify STMs under relaxed
    memory models with atomicity of 32 bit loads and stores, and read-modify-write
    operations. We present RML, a new high-level language for expressing concurrent
    algorithms with a hardware-level atomicity of instructions, and whose semantics
    is parametrized by various relaxed memory models. We then present our tool, FOIL,
    which takes as input the RML description of an STM algorithm and the description
    of a memory model, and automatically determines the locations of fences, which
    if inserted, ensure the correctness of the STM algorithm under the given memory
    model. We use FOIL to verify DSTM, TL2, and McRT STM under the memory models of
    sequential consistency, total store order, partial store order, and relaxed memory
    order.@eng
  bibo_authorlist:
  - foaf_Person:
      foaf_givenName: Rachid
      foaf_name: Guerraoui, Rachid
      foaf_surname: Guerraoui
  - foaf_Person:
      foaf_givenName: Thomas A
      foaf_name: Thomas Henzinger
      foaf_surname: Henzinger
      foaf_workInfoHomepage: http://www.librecat.org/personId=40876CD8-F248-11E8-B48F-1D18A9856A87
    orcid: 0000−0002−2985−7724
  - foaf_Person:
      foaf_givenName: Vasu
      foaf_name: Vasu Singh
      foaf_surname: Singh
      foaf_workInfoHomepage: http://www.librecat.org/personId=4DAE2708-F248-11E8-B48F-1D18A9856A87
  bibo_doi: 10.1007/978-3-642-02658-4_26
  bibo_volume: 5643
  dct_date: 2009^xs_gYear
  dct_publisher: Springer@
  dct_title: Software transactional memory on relaxed memory models@
...