§ Regular Plain Separation Logic

• Have the separating conjuction * and the magic wand operator -*.
• We use what's called as the 'update pattern' (?) when trying to reason about thing like linked lists.
• For example, consider the program that returns the pointer to the nth element on the linked list.

using LinkedList = ptr[(int, LinkedList)]def nth(x : ptr, i : int) -> ptr:  match i:    case 0: return x    case succ i': return nth(x.next, i')

§ Concurrent Separation Logic Without Higher Order Nonsense

§ Invariants

• An invariant is a proposition that's drawn as if it's in a box (I assume it's a modality?)
• Firstly an invaraiant is duplicable, and is thus not substructral.
• Secondly, an invariant can be 'opened', as long as can re-prove the invariant after closing it.
• I can't remember where ''atomically?'' was important.

Consider a program that adds 2 and 2 to a variable x.

def progi(_i : thread_id, x : int):   x += 2   return xx = 0; progi(0, x) || progi(0, x);

• If we just have invariants, then we can keep an invariant that x is even, and we can prove that both threads maintain this invariant.
• However, we cannot prove that the value of x is 4.
• So, we invent some more machinery to allow us to prove that x is 4.

§ Resource Algebras

• Resource algebra is a commutative monoid that has a predicate valid on it.
• For example, for fractional ownership, we use $\mathbb Q \cap [0, \infty)$, where valid(x) is true if $x \in [0, 1]$. We use $0$ as the unit, and $x \cdot y = x + y$.
• This generalizes heaps, because a heap is a RA with finite maps and a bottom element, with valid(h) is true if h is a finite map, and h1 * h2 = h1 \cup h2 if dom(h1) \cap dom(h2) = \emptyset, and bottom otherwise. The unit is the empty heap.
• More interestingly, we can have an RA that has frac(a) or botha(a) or full(a) or empty(a) or bottom.
• We say that frac(a) <> full(a) = both(a), and empty(a) <> x = x, and anything else is bottom.

x = 0; progi(0, x) || progi(0, x);

• We start with the precondition that x = p1 + p2 and ....

§ Atomically

I can't remmber where this played a role.