License: 
Creative Commons Attribution 4.0 International license (CC BY 4.0)
When quoting this document, please refer to the following
DOI: 10.4230/LIPIcs.CONCUR.2023.2
URN: urn:nbn:de:0030-drops-189961
URL: http://dagstuhl.sunsite.rwth-aachen.de/volltexte/2023/18996/
Bouajjani, Ahmed
On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk)
Abstract
Developing correct and performant concurrent systems is a major challenge. When programming an application using a memory system, a natural expectation would be that each memory update is immediately visible to all concurrent threads (which corresponds to strong consistency). However, for performance reasons, only weaker guarantees can be ensured by memory systems, defined by what sets of updates can be made visible to each thread at any moment, and by the order in which they are made visible. The conditions on the visibility order guaranteed by a memory system corresponds to its memory consistency model. Weak consistency models admit complex and unintuitive behaviors, which makes the task of application programmers extremely hard. It is therefore important to determine an adequate level of consistency for each given application: a level that is weak enough to ensure performance, but also strong enough to ensure correctness of the application behaviors. This leads to the consideration of several important verification problems:
- the correctness of an application program running over a weak consistency model;
- the robustness of an application program w.r.t. consistency weakening;
- the fact that an implementation of a system (memory, storage system) guarantees a given (weak) consistency model.
The talk gives a broad presentation of these issues and some results in this research area. The talk is based on several joint works with students and colleagues during the last few years.
BibTeX - Entry
@InProceedings{bouajjani:LIPIcs.CONCUR.2023.2,
author = {Bouajjani, Ahmed},
title = {{On Verifying Concurrent Programs Under Weakly Consistent Models}},
booktitle = {34th International Conference on Concurrency Theory (CONCUR 2023)},
pages = {2:1--2:1},
series = {Leibniz International Proceedings in Informatics (LIPIcs)},
ISBN = {978-3-95977-299-0},
ISSN = {1868-8969},
year = {2023},
volume = {279},
editor = {P\'{e}rez, Guillermo A. and Raskin, Jean-Fran\c{c}ois},
publisher = {Schloss Dagstuhl -- Leibniz-Zentrum f{\"u}r Informatik},
address = {Dagstuhl, Germany},
URL = {https://drops.dagstuhl.de/opus/volltexte/2023/18996},
URN = {urn:nbn:de:0030-drops-189961},
doi = {10.4230/LIPIcs.CONCUR.2023.2},
annote = {Keywords: Concurrent programs, weakly consistent models}
}
|
Keywords: |
|
Concurrent programs, weakly consistent models |
|
Collection: |
|
34th International Conference on Concurrency Theory (CONCUR 2023) |
|
Issue Date: |
|
2023 |
|
Date of publication: |
|
07.09.2023 |
