2.1. Introduction🔗

In short, Iris is a higher-order concurrent separation logic framework. That is quite a mouthful, so let us break it down.

Firstly, the framework part means that Iris is not tied to any single programming language — it consists of a base logic and can be instantiated with any language one sees fit.

Secondly, a separation logic is a logic used to reason about programs by introducing a notion of resource ownership. The idea is that one must own a resource before one can interact with it. Ownership is generally exclusive but can be transferred. To support this notion, separation logic introduces a new connective called separating conjunction, written P ∗ Q. This asserts ownership of the resources described by propositions P and Q, and, in particular, P and Q describe separate resources. So what is a resource? In Iris, we may define our own notion of resources by creating a so-called resource algebra, which we discuss later. For languages with a heap, a canonical example of a resource is a heap fragment. Owning a resource then amounts to controlling a fragment of the heap, allowing one to read and update the associated locations.

Thirdly, a concurrent separation logic (CSL) extends on the above by adding rules supporting concurrent constructions, such as Fork. As ownership is exclusive, a program that spawns threads must decide how to separate and delegate its resources to its threads, so that they may perform their desired actions.

Finally, higher-order refers to the fact that predicates may depend on other predicates. Being a program logic means that programs are proved correct with respect to some specification — a description of the program's behavior and interaction with resources. As programs are usually composed of other programs, we would want our specifications to be generic so that they may be used in a myriad of contexts. Having support for higher-order predicates means that program specifications can be parametrized by arbitrary propositions. This allows one to write specifications for libraries independently of their clients — the clients will instantiate the propositions to specialize the specification to fit their needs.

In this chapter, we introduce basic separation logic in Iris.