Abstract
In the fifth lecture, we studied four extensions of the separating logics of the previous lectures that enable or facilitate the specification and verification of a wider class of programs.
The first extension is the separating implication operator, colloquially known as the "magic wand" because of its shape, which is the adjoint of the separating conjunction, just as the usual implication is the adjoint of the usual conjunction. This "magic wand" facilitates reasoning in separating logic, notably via the branched consequence rule or via a calculation of weaker preconditions.
The second extension enables verification of processes that share data but access it read-only, without modification. This involves associating permissions with memory cells, these permissions being either partial (allowing only reading) or complete (also allowing writing and releasing). Two well-known models of partial permissions are fractional permissions and counted permissions. We have illustrated the use of the latter to verify a multi-reader lock implemented by two semaphores.
Phantom code" is the third technique studied in this session. These are commands that are not executed in the final program, but help to define "ghost variables" that simplify verification. In parallel computing, code and phantom variables keep track of the calculations made by each process and how these individual calculations contribute to the overall execution of the program.
The final extension we have described enables locks and their resource invariants to be stored in memory, along with the data protected by these locks. This makes it possible to specify and verify fine-grained parallel algorithms, as we have illustrated with a simply chained list structure with coupled locking.
As disparate as they may seem, these and many other extensions are special cases of a small number of more general notions, as illustrated by the Iris logical infrastructure.
