Feedback on Concurrent Separation Logic

[mdempsky]

In our study group session today, we discussed FRAP chapter 18. We spent a while discussing the HtPar rule, because we were wondering about "r" in the book's rendition vs tt in the Coq code. What occurred to us is because there's no way for Return tt || Return tt to take a step, the post condition for c1 || c2 doesn't end up mattering.

For example, a program like:

Example stuckJoin : cmd unit :=
  _ <- (Return tt; Return tt);
  Fail.

gets stuck without ever reaching Fail. It's possible to prove that notAboutToFail is an invariant of this program, but not with hoare_triple_sound because HtPar is too restrictive (it requires you to prove tt = tt -> False).

Two reasonable options we saw:

1. Extend the operational semantics with a join operation, like step (h, l, Par (Return tt) (Return tt)) (h, l, Return tt). (Or even change Par's type and make it return a tuple of the results from its two subcommands.)

   Note: With this option, notAboutToFail is no longer an invariant of stuckJoin.

2. Change HtPar's post condition to just [| False |]. With a slight tweak to invert_Par (just dropping /\ Q1 tt * Q2 tt ===> Q tt) and corresponding simplification to preservation, I was able to still prove the same final results.

However, this also got us wondering about notAboutToFail more broadly. Most of us initially assumed it served a role similar to the unstuck predicate from chapter 12 used for proving progress. But upon closer inspection, realized it's more limited than we thought. For example, it doesn't prevent reading/writing bad memory addresses, or unlocking locks that are already unlocked.

Again, two reasonable options:

1. If a step rule is added for Par (Return v1) (Return v2), then use an unstuck invariant like in previous chapters. That is, prove there's always a step to take, or the command is Return v where v and the heap satisfy the Hoare triple post condition.

2. Add Fail transitions for cases that shouldn't happen. For example:

   | StepUnlockFail : forall h l a,
     ~a \in l
     -> step (h, l, Unlock a) (h, l, Fail)
   

   These transitions might be interesting to add anyway. I imagine a bunch would just make the proofs tedious, but even one would probably be edifying.

[achlipala]

Thanks for the thoughts. I had indeed considered a change along these lines before, but inertia kept me from going for it. I've switched to assigning contradictory postconditions to parallel compositions.

I also agree that notAboutToFail doesn't give the perfect characterization of safety, but note that unstuckness isn't obviously right either, because we might have two threads, one in an infinite loop and the other trying to dereference a null pointer. That program isn't stuck, but it's also ready to crash. I held back on making any changes you suggested in the operational semantics because I feel like they make the story more complicated without paying back enough in cool consequences we can explore.