---
_id: '4383'
abstract:
- lang: eng
  text: 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.
acknowledgement: This research was supported by the Swiss National Science Foundation.
alternative_title:
- LNCS
author:
- first_name: Rachid
  full_name: Guerraoui, Rachid
  last_name: Guerraoui
- first_name: Thomas A
  full_name: Thomas Henzinger
  id: 40876CD8-F248-11E8-B48F-1D18A9856A87
  last_name: Henzinger
  orcid: 0000−0002−2985−7724
- first_name: Vasu
  full_name: Vasu Singh
  id: 4DAE2708-F248-11E8-B48F-1D18A9856A87
  last_name: Singh
citation:
  ama: 'Guerraoui R, Henzinger TA, Singh V. Software transactional memory on relaxed
    memory models. In: Vol 5643. Springer; 2009:321-336. doi:<a href="https://doi.org/10.1007/978-3-642-02658-4_26">10.1007/978-3-642-02658-4_26</a>'
  apa: 'Guerraoui, R., Henzinger, T. A., &#38; Singh, V. (2009). Software transactional
    memory on relaxed memory models (Vol. 5643, pp. 321–336). Presented at the CAV:
    Computer Aided Verification, Springer. <a href="https://doi.org/10.1007/978-3-642-02658-4_26">https://doi.org/10.1007/978-3-642-02658-4_26</a>'
  chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Software Transactional
    Memory on Relaxed Memory Models,” 5643:321–36. Springer, 2009. <a href="https://doi.org/10.1007/978-3-642-02658-4_26">https://doi.org/10.1007/978-3-642-02658-4_26</a>.
  ieee: 'R. Guerraoui, T. A. Henzinger, and V. Singh, “Software transactional memory
    on relaxed memory models,” presented at the CAV: Computer Aided Verification,
    2009, vol. 5643, pp. 321–336.'
  ista: 'Guerraoui R, Henzinger TA, Singh V. 2009. Software transactional memory on
    relaxed memory models. CAV: Computer Aided Verification, LNCS, vol. 5643, 321–336.'
  mla: Guerraoui, Rachid, et al. <i>Software Transactional Memory on Relaxed Memory
    Models</i>. Vol. 5643, Springer, 2009, pp. 321–36, doi:<a href="https://doi.org/10.1007/978-3-642-02658-4_26">10.1007/978-3-642-02658-4_26</a>.
  short: R. Guerraoui, T.A. Henzinger, V. Singh, in:, Springer, 2009, pp. 321–336.
conference:
  name: 'CAV: Computer Aided Verification'
date_created: 2018-12-11T12:08:34Z
date_published: 2009-06-19T00:00:00Z
date_updated: 2021-01-12T07:56:34Z
day: '19'
doi: 10.1007/978-3-642-02658-4_26
extern: 1
file:
- access_level: open_access
  checksum: df3c3e6306afd3f630a9146f91642f0a
  content_type: application/pdf
  creator: system
  date_created: 2018-12-12T10:14:50Z
  date_updated: 2020-07-14T12:46:28Z
  file_id: '5105'
  file_name: IST-2012-45-v1+1_Software_transactional_memory_on_relaxed_memory_models.pdf
  file_size: 265763
  relation: main_file
file_date_updated: 2020-07-14T12:46:28Z
intvolume: '      5643'
month: '06'
oa: 1
page: 321 - 336
publication_status: published
publisher: Springer
publist_id: '1074'
pubrep_id: '45'
quality_controlled: 0
status: public
title: Software transactional memory on relaxed memory models
type: conference
volume: 5643
year: '2009'
...