We use Cosmo, a modern concurrent separation logic, to formally specify and verify an implementation of a multiple-producer multiple-consumer concurrent queue in the setting of the Multicore OCaml weak memory model. We view this result as a demonstration and experimental verification of the manner in which Cosmo allows modular and formal reasoning about advanced concurrent data structures. In particular, we show how the joint use of logically atomic triples and of Cosmo's views makes it possible to describe precisely in the specification the interaction between the queue library and the weak memory model.

@article{paperbot1115,
  title = {Formal verification of a concurrent bounded queue in a weak memory model},
  author = {Glen Mével and Jacques-Henri Jourdan},
  journal = {Proceedings of the ACM on Programming Languages},
  volume = {5},
  number = {ICFP},
  year = {2021},
  doi = {10.1145/3473571}
}