×

zbMATH — the first resource for mathematics

Software transactional memory on relaxed memory models. (English) Zbl 1242.68162
Bouajjani, Ahmed (ed.) et al., Computer aided verification. 21st international conference, CAV 2009, Grenoble, France, June 26–July 2, 2009. Proceedings. Berlin: Springer (ISBN 978-3-642-02657-7/pbk). Lecture Notes in Computer Science 5643, 321-336 (2009).
Summary: 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.
For the entire collection see [Zbl 1165.68004].

MSC:
68Q60 Specification and verification (program logics, model checking, etc.)
68N19 Other programming paradigms (object-oriented, sequential, concurrent, automatic, etc.)
Software:
Checkfence
PDF BibTeX XML Cite
Full Text: DOI