Seminar details
Abstract: Handling concurrency using a shared memory and locks can be tedious and
error-prone. One solution is to use message-passing instead. We study here
a particular flavor that makes the ownership transfer of messages explicit.
In this case, ownership of the heap region representing the content of a
message is lost upon sending, which can lead to efficient implementations.
We have defined a proof system for a concurrent imperative programming
language implementing this idea and inspired by the Singularity operating
system research project. The proof system, which we have proved sound, is
an extension of separation logic, a logic that has already been used
successfully to study various ownership-oriented paradigms.
In this talk, I will present the programming language, the properties
we can prove using our logic, and give some insights about the
semantics of our objects.
This is joint work with Étienne Lozes (LSV) and Cristiano Calcagno
(Imperial College).
