Semantics of Remote Direct Memory Access (artifact)

This artifact contains the Coq formalisations of the two operational semantics presented in the paper, and a proof that they are equivalent. While the overall semantics is not presented in the same way as in the paper, the queue pairs follow exactly the definitions given.

Download:

Tarball containing the Coq development (~100 kB) to test the artifact using your local installation of Coq. This was tested on Coq versions 8.15 and 8.16, and can be compiled using the make command.

Organisation of the Coq development:

1. The directory hahn contains a helper library for manipulating lists and binary relations. More information on this library can be found on https://github.com/vafeiadis/hahn.
2. The files RTC.v and ListBefore.v contain general auxiliary Coq definitions and tactics, respectively about the reflexive transitive closure of a relation and the relative ordering of elements in a list.
3. The file FullQP.v contains the definition of the concrete operational semantics (queue pairs with 6 buffers).
4. The file MergedQP.v contains the definition of the simplified operational semantics (queue pairs with 3 buffers).
5. The file EqFullMergedQP.v states and proves the equivalence of the two semantics.