Repository logo

Infoscience

  • English
  • French
Log In
Logo EPFL, École polytechnique fédérale de Lausanne

Infoscience

  • English
  • French
Log In
  1. Home
  2. Academic and Research Output
  3. Conferences, Workshops, Symposiums, and Seminars
  4. Software Transactional Memory on Relaxed Memory Models
 
conference paper

Software Transactional Memory on Relaxed Memory Models

Guerraoui, Rachid  
•
Henzinger, Thomas A.  
•
Singh, Vasu
2009
Proceedings of the 21st International Conference on Computer Aided Verification
21st International Conference on Computer Aided Verification

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.

  • Details
  • Metrics
Type
conference paper
DOI
10.1007/978-3-642-02658-4_26
Web of Science ID

WOS:000270444900022

Author(s)
Guerraoui, Rachid  
Henzinger, Thomas A.  
Singh, Vasu
Date Issued

2009

Publisher

Springer

Publisher place

Berlin

Published in
Proceedings of the 21st International Conference on Computer Aided Verification
Series title/Series vol.

Lecture Notes in Computer Science; 5643

Start page

321

End page

336

Subjects

Transactional memories

•

Relaxed memory models

•

Model checking

URL

URL

http://www-cav2009.imag.fr/
Editorial or Peer reviewed

REVIEWED

Written at

EPFL

EPFL units
DCL  
MTC  
Event nameEvent placeEvent date
21st International Conference on Computer Aided Verification

Grenoble

June 26 - July 2, 2009

Available on Infoscience
May 2, 2009
Use this identifier to reference this record
https://infoscience.epfl.ch/handle/20.500.14299/38241
Logo EPFL, École polytechnique fédérale de Lausanne
  • Contact
  • infoscience@epfl.ch

  • Follow us on Facebook
  • Follow us on Instagram
  • Follow us on LinkedIn
  • Follow us on X
  • Follow us on Youtube
AccessibilityLegal noticePrivacy policyCookie settingsEnd User AgreementGet helpFeedback

Infoscience is a service managed and provided by the Library and IT Services of EPFL. © EPFL, tous droits réservés