Paolo Giarrusso said:
As elegant abstractions go, it's nice that at least one of those uses concurrent separation logic :-)
I see many papers claiming elegance and other good qualities for CSL. Is there any empirical work how this actually works out in practice? I think it would have to go beyond some authors with CSL research grants encoding some definitions/results in both their own framework on someone else's.
For example, Dafny uses "separation predicates" for heap-based reasoning (i.e., not CSL), and was used for the Armada framework for verifying concurrent code: https://github.com/microsoft/Armada -- can it be said a priori or by pointing to some existing results that using a CSL basis for Armada would lead to better abstractions, less code, faster verification, etc.?
The claim of "elegance" is necessarily subjective, but "usefulness in practice" seems born out by an abundance of literature...
I expect the more challenging question is "how much can you automate CSL at scale"
Paolo Giarrusso said:
The claim of "elegance" is necessarily subjective, but "usefulness in practice" seems born out by an abundance of literature...
But isn't the relevant claim that we should all be interested in: "CSL is more useful in practice than competing state-of-the-art approaches"
And I have not seen much in the literature corroborating this, at least not starting from an even playing field.
People have done that for crash-safety proofs (e.g. https://fbinfer.com/docs/separation-logic-and-bi-abduction), but I'm less sure about functional verification
Ah
I'm very far from an expert, but the focus in e.g. Iris has been on doing modular verification of increasingly complicated concurrency patterns
this shows that such proofs can be done in Iris ("exists"), but it doesn't show that doing such proofs in Iris is an "equilibrium" or "maxima"
for example, we regularly get these (in my opinion) useless industry presentations with the title: "using X to do Y", which never explain why using X is a good/optimal choice compared to all other alternatives to accomplishing Y (or why Y is even desirable in the first place, maybe people should instead aim for Z)
I think that’s a good question, except that the metrics on why “X” is good either do not exist, are not measurable, or are not measurable in a meaningful way.
as in, empirically-speaking, we don’t even have good evidence that static types help writing software.
(if you were to go by the evidence standard of medicine or psychology, I’m not sure you have any evidence in software-engineering, but I digress)
well, the domain here is more specific: writing formal correctness proofs about concurrent data structures and systems
back to your question, I expect that everything that can be done in armada can be done in iris, but not viceversa
expressiveness is one measure for sure, but then you can survey whether the additional expressiveness is actually needed in relevant practical work
IIUC, there exist simplifying assumptions that let you avoid separation logic, but they are often nontrivial. But I’d best leave that to the real experts who can defend that better, and based on public evidence :-)
For example, the following papers in my view provide some empirical evidence that formally verified software (whatever exactly that means) is superior to unverified software on some relevant measures: http://www.cs.utah.edu/~regehr/papers/pldi11-preprint.pdf https://unsat.cs.washington.edu/papers/fonseca-dsbugs.pdf
Would be interested in anything reminiscent of this for CSL vs. other verification approaches.
I think to answer this question you have to also take into account automated vs interactive proofs (sadly this is mostly still a strict divide, AFAIK there is not much work on hybrid systems -- some, but not much). I know very little about automated proofs but what people tell me is that for a full CSL, that's very challenging.
For a manual proof, I haven't seen much work that is not CSL-based. I am obviously biased though. ;)
I guess the main exception is the linearizability literature, with lots of trace-based reasoning.
Last updated: Sep 25 2023 at 14:01 UTC