On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk)

Author Ahmed Bouajjani

Thumbnail PDF


  • Filesize: 329 kB
  • 1 pages

Document Identifiers

Author Details

Ahmed Bouajjani
  • Université Paris Cité, CNRS, IRIF, France

Cite AsGet BibTex

Ahmed Bouajjani. On Verifying Concurrent Programs Under Weakly Consistent Models (Invited Talk). In 34th International Conference on Concurrency Theory (CONCUR 2023). Leibniz International Proceedings in Informatics (LIPIcs), Volume 279, p. 2:1, Schloss Dagstuhl – Leibniz-Zentrum für Informatik (2023)


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.

Subject Classification

ACM Subject Classification
  • Theory of computation → Concurrency
  • Concurrent programs
  • weakly consistent models


  • Access Statistics
  • Total Accesses (updated on a weekly basis)
    PDF Downloads
Questions / Remarks / Feedback

Feedback for Dagstuhl Publishing

Thanks for your feedback!

Feedback submitted

Could not send message

Please try again later or send an E-mail