Karl Palmskog (Aug 06 2020 at 20:36): Karl Palmskog (Aug 06 2020 at 20:36):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.
Karl Palmskog (Aug 06 2020 at 20:40):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.?
Paolo Giarrusso (Aug 06 2020 at 20:42):The claim of "elegance" is necessarily subjective, but "usefulness in practice" seems born out by an abundance of literature...
Paolo Giarrusso (Aug 06 2020 at 20:42):I expect the more challenging question is "how much can you automate CSL at scale"
Karl Palmskog (Aug 06 2020 at 20:46):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.
Paolo Giarrusso (Aug 06 2020 at 20:46):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
Paolo Giarrusso (Aug 06 2020 at 20:46):Ah
Paolo Giarrusso (Aug 06 2020 at 20:48):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
Karl Palmskog (Aug 06 2020 at 20:49):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"
Karl Palmskog (Aug 06 2020 at 20:51):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)
Paolo Giarrusso (Aug 06 2020 at 20:53):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.
Paolo Giarrusso (Aug 06 2020 at 20:54):as in, empirically-speaking, we don’t even have good evidence that static types help writing software.
Paolo Giarrusso (Aug 06 2020 at 20:55):(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)
Karl Palmskog (Aug 06 2020 at 20:55):well, the domain here is more specific: writing formal correctness proofs about concurrent data structures and systems
Paolo Giarrusso (Aug 06 2020 at 20:56):back to your question, I expect that everything that can be done in armada can be done in iris, but not viceversa
Karl Palmskog (Aug 06 2020 at 20:58):expressiveness is one measure for sure, but then you can survey whether the additional expressiveness is actually needed in relevant practical work
Paolo Giarrusso (Aug 06 2020 at 21:05):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 :-)
Karl Palmskog (Aug 06 2020 at 21:15):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.
Ralf Jung (Aug 18 2020 at 06:36):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.
Ralf Jung (Aug 18 2020 at 06:39):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: Jun 01 2023 at 13:01 UTC