--- _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:10.1007/978-3-642-02658-4_26' apa: 'Guerraoui, R., Henzinger, T. A., & Singh, V. (2009). Software transactional memory on relaxed memory models (Vol. 5643, pp. 321–336). Presented at the CAV: Computer Aided Verification, Springer. https://doi.org/10.1007/978-3-642-02658-4_26' chicago: Guerraoui, Rachid, Thomas A Henzinger, and Vasu Singh. “Software Transactional Memory on Relaxed Memory Models,” 5643:321–36. Springer, 2009. https://doi.org/10.1007/978-3-642-02658-4_26. 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. Software Transactional Memory on Relaxed Memory Models. Vol. 5643, Springer, 2009, pp. 321–36, doi:10.1007/978-3-642-02658-4_26. 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' ...