RGSep is a program logic that combines rely-guarantee reasoning and separation
logic. It has been used, both manually and automatically, to prove the
correctness of several fine-grained concurrent algorithms.
Material
Tool support
- SmallfootRG: a
memory safety checker for fine-grained concurrent singly linked list programs.
- CAVE: a more powerful tool that can infer
the rely and guarantee relations and can prove linearizability of concurrent libraries.
Related program logics
- SAGL: a similar logic for assembly code.
- Local rely-guarantee:
variant of RGSep supporting an interference hiding rule at the expense of
additional precision requirements.
- Deny-guarantee: an
extension of rely-guarantee that supports unstructured thread creation and
join.
- Concurrent abstract predicates:
adapts deny-guarantee to heaps and adds abstract predicates.
- Iris:
a generic framework for encoding concurrent program logics