Proving Copyless Message-Passing
Intervenant(s) : Etienne Lozes, LSV, ENS de Cachan
We present an extension of Separation Logic, a program logic in the tradition of the Hoare-Floyd logic. Separation Logic is natively motivated by the proof of heap-manipulating and concurrent programs. Our extension is dedicated to copyless message passing, a form of message passing that takes advantage of a shared memory to reduce the amount of copies involved along message exchanges. Inspired by the Sing# operating system, our extension introduces channel contracts, which specify for each communication channel the protocol that should be followed on that channel. The theory of these communication contracts is exposed, in particular its connection to half-duplex communicating finite state machines. The proof system is shown to enforce several properties on provable programs, some of which are rather standard in Separation Logic, like memory safety, or race-freedom, and others that are possibly less expected, like some special forms of deadlock-freedom, or the confluence of computations.
This is a joint work with Jules Villard.