Hi, thanks for watching this talk about concurrent seppation logic and template games. First, what's concurrent seppation logic? It's a program logic to prove concurrent programs which n-memory unlocks.

As an extension of Hoare logic, it uses Hoare triples, gamma, p, c, q, which says that if the initial state satisfies the precondition p, after the program c has terminated, the final state satisfies q. Such Hoare triples are proved using derivation trees which are built using inference rules.

In this talk, we'll denote by the letter pi such trees. Given such a proof pi of a Hoare triple in CSL, our approach is to interpret both the program and the proof in two double categories which are induced by templates.

Here, the template CSL for the proof and the template S for the program. We will see that those two templates are related by a forgetful morphism. And also, we can prove that there is always a map from the interpretation of the proof to the interpretation of the program.

It's this map that we will use to express the soundness theorem of the logic which relates the fact that some Hoare triple is provable with some guarantee on the semantics of the program. First, let's look at programs. We will interpret them as state transition systems which are just a set of nodes and a set of transitions between those nodes.

As well as a set of initial nodes which are depicted on the left of the picture and a set of final nodes which are depicted on the right of the picture. A path from an initial node S to a final node S' is just a trace. This will be represented as a cospan in the category of directed graphs.

Here the support C contains the transitions of the codes and Cin and Cout contains the initial and final nodes respectively. Since we are considering an imperative language we want to label each node N of the transition system with a memory state S. And we want to label each transition between two nodes N1 and N2

with a basic instruction M which describes the action on the memory. This is achieved using lambda, a graphomorphism from C, the support of the transition system, to a labeling graph which we write template S of 1. As you can see below, we also want a second labeling graph

for the interfaces Cin and Cout. Now the lower cospan is what we call the template and the whole structure is what we call a cupboardism by analogy with the topological objects. Now I will define the template for programs. The nodes of the graph template 0 and template 1 are the memory states which are either a pair of a heap and a stack

represented as spatial functions or the error state. Here are some examples of basic instructions assigning the result of an expression to a variable, dereferencing a pointer, allocating a new value on the heap or simply doing nothing. The graph template 0 is discrete, meaning it has no transitions

but template 1 has transitions which correspond to the semantics of basic instructions. For example, the instruction x colon equals e replaces the value of x with the result of evaluating e in S. Note that the instructions can be non-deterministic, like allocating a value at an arbitrary fresh location. Now let's see how to compose cupboardisms.

Let's assume we have two cupboardisms, C and D, such that Cout is equal to Din. The way to compose them is to glue them along their common interface. This defines C semicolon D, the support of the composite cupboardism. Note that we perform the corresponding pushouts at the level of templates, defining template 2.

The universal property of the upper pushout gives a map from C D to template 2, and, as I will explain next, there is a map from template 2 to template 1. This gives us a cupboardism whose support is C D. Now, let's understand the structure of the templates which was necessary to define this composition. First, let's look at internal categories which are used in template games.

It is the data of two objects of the ambient category S, the space template 0 of objects, and template 1 of morphisms, with a source and target map from the space of morphisms to the space of objects, and an identity map in the other direction. Given this structure, one can define the space template 2 of composable arrows

as a putback of T and S, which contains intuitively ordered pairs of morphisms with the same target and source. Note that an internal category is the same as a monad in the double category of spans on S. Classical examples of internal categories are that an internal category in the category of sets

is simply a small category, as you would expect, and an internal category in the category of small categories is a double category. The structure that we use for our templates is a dual notion which we call internal op categories. We still have two objects, template 0 and template 1,

but the source and the target maps are reversed. Similarly, composable arrows are now the push-out of T and S, but the composition morphism is in the same direction. Note that this is the same push-out and the same map from template 2 to template 1 as the previous slide. Our getting principle was that, due to an internal category,

an internal op category is the same as a monad in the double category of spans in S. Interestingly, the definition of such a monad forces the three maps, T and S and I, from the space of objects to the space of morphisms, to be equal. First, recall that a double category consists of a class of objects, a category of vertical morphisms,

a weak category of horizontal morphisms, which we denote with crossed arrows, and a class of double cells, which fill squares of this form. Equal morphisms are maps in S which commute with the labeling morphisms, and horizontal morphisms are the cobordisms themselves.

Double cells are the morphisms between the supports of the cobordisms, which makes this diagram commute. To get a taste at how we interpret programs, let's look at how we interpret B and C1 and C2. The idea is to compose a decision union of C1 and of C2 with a cobordism whose purpose is to redirect the flow of control

using NOP instructions to C1 or C2, depending on whether the initial state satisfies B. This yields the following cobordism. But now, what happens if we try to post-compose with the third cobordism, D? The problem is that their interfaces are not compatible. The solution is to fill this gap using a cobordism

which can relate any pair of interfaces, which we call the filling. This phenomenon shows that the set of initial and final nodes of a cobordism are part of its private state, in a way. When we compose them together, the synchronization only happens at the level of templates. This is in contrast with template games, where strategies synchronize on their common game.

This is the reason why we chose to consider a double category of cobordisms instead of a bi-category, like in template games. First, we add new primitives to our language. One to execute programs in parallel, one to create a new log r, which becomes available in C,

and one to acquire and then release a log r. At the level of states, we use machine states, which contain the memory state and a set of available logs at that point. Because we are in a concurrent context, the interpretation of a program must describe any possible interaction between the code and the environment, which abstracts any program that could be running in parallel.

Our solution is to have two kinds of transitions in our transition systems. Code transitions, which describe the action the code performs, and environment transitions, which describe the actions the environment could be doing. Now, our transition systems look like this. The important fact is that a path from an initial state to a final state

can be decomposed into any number of environment transitions, followed by one code transition, followed by any number of environment transitions, and so on. We change the template as follows. Template 1 contains two copies of each transition, one for the code and one for the environment, and template 0 now contains all environment transitions instead of being discrete.

Since this new concurrent template is also an internal op category, we again obtain a double category of cobordisms. To interpret the parallel product, we need to define a monoidal structure on cobordisms. Let's consider the following parallel composition of two programs, C1 and C2. Let's say that C1 does a code transition.

Now, from the point of view of C2, this is an environment transition. The parallel product has more context. It knows that this is a transition from C1. But from the outside, this is just a code transition. The idea of the parallel product is that we want to synchronize such pairs of transitions in C1 and C2.

This is formalized by defining a span of templates whose support has a final notion of polarity, and a map pick which maps a transition in the parallel template to a pair of transitions which should be synchronized. The map pins hides the additional information in the parallel templates. In the case of the template of programs, the parallel template has three polarities, C1, C2, and F,

and it maps a transition with polarity C1 to a transition with code polarity on the left, and environment polarity on the right. The map pins simply maps both C1 and C2 to code, and F to F. Let's see how to define the parallel product of two cobordisms, C1 and C2, using such a span.

First, we pull back the product of C1 and C2 along pick, and then we post-compose with pins to get a normal cobordism. When this span satisfies the right axioms, this handles the double category cob of templates with a monoidal product. There are other operations that are defined in the paper.

In particular, to handle creation of locks and critical sections, we have a family of templates, one for each lock, and there are operations to transport cobordisms between them. We have a monadic treatment of errors by working in the ambient category of algebras of 0 or monads or graphs, instead of the category of graphs itself.

We now have enough structure to interpret concurrent programs, but actually we can also interpret proofs using the same operations if we have the right templates. Let's start with the formulas of CSL. They represent predicates of our logical states, which refine memory states with permissions. Here, real numbers between 0 and 1. A logical state associates each location and each variable not only to a value,

but also permission, which express how much ownership of the location we have, with 1 meaning the complete ownership. There is a partial product and logical states which refines disjoint union. If a location is not in both logical states, then their product behaves the same as a disjoint union.

But if a location is in both logical states, then the product is only defined if they contain the same value, and if the sum of the permissions is not greater than 1. The formulas of CSL are the formulas of first-order logic with new constructions. First, the formula L points to V with permission P,

holds only for the logical state which contains a single location, which is associated to V and P. The separating conjunction, which gives its name to the logic, is defined as follows. A state sigma satisfies P1 star P2 if you can split sigma into two logical states, sigma 1 and sigma 2 using the product above,

in such a way that sigma i satisfies Pi. Finally, the formula empty only holds for the empty state. Now let's look at how triples. In CSL, they also contain a context, gamma, which associate each lock with an invariant, which is a formula which describes the resources that are protected by this lock. The rule for the control composition is just the same as the one for whole logic,

and the rule for the parallel product says that in order to prove C1 parallel C2, one needs to be able to split the free and the plus conditions using the separating conjunction, and then prove each program is correct. Note that the context gamma is shared between C1 and C2, which means that they can both use the same shared resources.

One nice thing is that those inference rules are interpreted with the same operations or comorbidisms as sequential and parallel composition of programs. Now let's look at how we can use locks. When we create a lock, we must give part of our precondition to the lock so that it can be shared inside of C.

And when we acquire a lock, the critical section gains access to the resource that the lock protects in its precondition, but has to give it back in its post condition. The template for CSL is based on the notion of separated states. It's a triple of a logical state sigma C, which represents a state which is owned by the code, a logical state sigma F for the environment,

and a vector sigma which associates for each lock either the resources it protects if it is available, or who has acquired it otherwise. Here is a pictorial representation of such a separated state. In this example, both locks are available, and the lighter overlapping areas represent locations

where no one has a full permission. Separated states are the nodes of the underlying graph of the template for CSL, and there are two kinds of transitions, the code transitions, which can only change the part that is owned by the code, and use locks, and similarly, the environment can only use

its part of the state and use locks. The tensor product is defined in a similar way as for the programs, with a parallel template which has three priorities, C1 for the code on the left hand side of the parallel product, C2 for the code on the right hand side, and F for the environment. The main difference is that in this case,

the states themselves are polarized, not just the transitions between them. The parallel template contains separated states with four components, one for C1, one for C2, one for the locks, and one for the environment, and the map pick sends the three-player state sigma1, sigma2, sigma and sigmaF,

to a pair of two-player separated states, such that the state of the other program seems to belong to the environment. So for example, from the point of view of C1, the logical state sigma2, which belongs to C2, is in the third component, which means that it belongs to the environment. And the map pins gives the view from the outside,

where the code owns both sigma1 and sigma2. The case of transitions is exactly the same as for the template of programs. Actually, the template of separated states is an instance of a generalization of internal op-categories, where there is a family of template zeros, one for each formula of the logic.

Template 0P contains all separated states, such that the code component satisfies P, and all environment moves between such states. A proof of a hot-ripple gamma PCQ is then a cobortism whose input interface is above template 0P, and its output interface is above template 0Q.

There is a forgetful map from the template of separated states to the template of programs, which is given by forgetting permissions. This induces a map between the cobortisms of the proof of the program, because they are built using the same operations and cobortisms. This can be visualized with the following drawing. Note that while the image of pi in the interpretation of the program

is closed by code transitions, it's not closed by environmental additions. We are now ready to talk about the Saunet theorem of concurrent separation logic. We first state it somewhat informally, and next we'll see how it is expressed in our setting. It's split in two parts. The first, theorem A, says that given a well-specified program C,

no execution which starts in a state which satisfies a precondition will crash. Moreover, if the program terminates, the final state satisfies a postcondition. When we write that a machine state S satisfies a formula P of CSL, we mean that there exists a separated state which satisfies P,

and which is mapped by L template to the machine state S. Theorem B states that under the same hypothesis, no execution of the program which starts from a state which satisfies a precondition P will encounter a data race. Recall that a data race is a situation where two instructions executing in two different threads try to write the same location, or to read and write the same location.

In this talk, we only talk about how we handle theorem A. In our setting, this theorem states that the map L from the interpretation of the derivation tree of the Hoare triple gamma PCQ to the interpretation of the program is a one-dimensional vibration on code transitions.

The definition is pictured below. This says that if some separated state is mapped by L to some state in the interpretation of C, then for any code transition starting from the state in the interpretation of C, we can find a transition in the interpretation of the proof which is mapped to the transition in C.

The reason this implies the safety of well-specified programs is that since the image of a separated state by L cannot be the error state, no code transition can make the program crash. The way we prove both the existence of the map L between the interpretations and the Sornet theorems is by induction on the derivation trees

using the fact that constructions and chordisms are factorial and that they preserve vibrations. In this paper, we have presented a link between concurrent separation logic and template games with an intriguing duality between spans and cospans and between internal categories and internal op-categories. I think it would be interesting to see if we can learn more about this link

by looking at higher-order separation logics. Also, a proof of Sornet relies on the fact that the ambient category is adhesive and it would be interesting to see how this aspect of the proof evolves if we consider rich variants of the concurrent separation logics like ARIS.

Thank you for your attention, and I would be happy to answer your questions during the conference.