Feedback on Concurrent Separation Logic
mdempsky opened this issue · 1 comments
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:
-
Extend the operational semantics with a join operation, like
step (h, l, Par (Return tt) (Return tt)) (h, l, Return tt)
. (Or even changePar
'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 ofstuckJoin
. -
Change
HtPar
's post condition to just[| False |]
. With a slight tweak toinvert_Par
(just dropping/\ Q1 tt * Q2 tt ===> Q tt
) and corresponding simplification topreservation
, 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:
-
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 isReturn v
wherev
and the heap satisfy the Hoare triple post condition. -
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.
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.