Feedback on Concurrent Separation Logic about frap HOT 1 CLOSED

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.

from frap.