Skip to content

Implement modular specifications from the HOCAP paper

Dan Frumin requested to merge dfrumin/iris-examples:hocap into master

This branch formalises the specifications for the concurrent bag and concurrent runners from the paper Modular Reasoning about Separation of Concurrent Data Structures Kasper Svendsen, Lars Birkedal, Matthew Parkinson.

Might be interesting for iris-examples, otherwise I can put it in a different repository.

TODO list:

  • Clean up and document the code
  • Explain the differences with the formalisation in the paper
  • Monotone bag specification doesn't make much sense actually
  • Bag with contributions specification (requires gmultiset RA)
Edited by Dan Frumin

Merge request reports