[Iris-Club] Classical version of Iris?

[Derek Dreyer]

Hehe (egg on face)...now I really do need to read your POPL
submission.  Sadly, it's still buried under the ones I actually have
to review. :-)

Sure, if you make the logic linear but restrict invariants to be
affine, then there's no problem.  But indeed I was imagining a
scenario of tracking memory usage where you would want to transfer
ownership of memory in invariants and then, as you said, this would
not be sufficient.

I'm curious to understand why you found linearity necessary to ensure
that resources were not thrown away.  Why is it not sufficient to say
that resource allocation requires some ghost permission, which then
gets returned upon deallocation (or maybe a ghost receipt is
returned).  Then you give the program some permissions to start and
insist that it return them (or the corresponding receipts) after it's
done.  Is strict linearity just more convenient than this, or is it
fundamentally necessary for some reason?

>> In that case, the only way to regain precise
>> tracking of resources would be to explicitly keep track of all known
>> invariants and thread such reasoning through specs, which goes against
>> the use of invariants to model hidden state.  I think that can't
>> possibly work.
>
> I don't understand what you mean here. As long as you can still frame away
> knowledge of invariant assertions, why would it be so bad?

What I meant was that if you can't hide invariants, then you would
have to thread them through the operations of an ADT, and that would
seem to force sequential use of the operations, no?

I'm going to keep shooting from the hip and saying incorrect things
until my students correct me. :-)

Derek


>>
>> On Sun, Aug 14, 2016 at 2:27 PM, Derek Dreyer <dreyer at mpi-sws.org> wrote:
>>>
>>> No one is developing a classical version of Iris, so far as I know.  I
>>> don't know if I've ever thought much about what a classical version
>>> would look like, but I imagine that if it makes sense at all, it would
>>> be very painful to work with because you would lose monotonicity.
>>>
>>> To answer your question about applicability to Rust, this point about
>>> intuitionistic separation logic not being good for explicit storage
>>> deallocation is an oft-repeated myth.  There is no problem with using
>>> intuitionistic separation logic to reason safely about explicit
>>> deallocation -- the only difficulty is in using it to prove absence of
>>> memory leaks.  Indeed, in classical separation logic, if the
>>> postcondition of your program is "emp", then you know all the memory
>>> has been deallocated, whereas you would not know that in
>>> intuitionistic separation logic since the latter collapses the
>>> distinction between emp and true.  However, even in intuitionistic
>>> separation logic, I believe you can use ghost state to effectively
>>> encode the condition that all memory has been deallocated (e.g. by
>>> starting with some tokens that represent the capability to allocate
>>> memory, and then showing in the postcondition that you have regained
>>> ownership of all of them).  This is maybe more cumbersome but I think
>>> it's doable.
>>>
>>> That said, Rust permits memory leaks via reference-counting cycles, so
>>> the point is moot, and I can see no motivation for using classical
>>> rather than intuitionistic separation logic in modeling Rust.
>>>
>>> Cheers,
>>> Derek
>>>
>>> On Sun, Aug 14, 2016 at 2:08 PM, Jeehoon Kang <jeehoon.kang at sf.snu.ac.kr>
>>> wrote:
>>>>
>>>> Dear Iris Club,
>>>>
>>>> In the ICFP 2016 paper is said "Iris is an intuitionistic separation
>>>> logic,
>>>> which gives rise to the monotonicity requirement".  I wonder if someone
>>>> is
>>>> developing a classical version of Iris.
>>>>
>>>> Background: I heard (from some of the Iris authors ;-) that Iris is
>>>> related
>>>> the RustBelt project which aims to verify "unsafe" Rust programs, which
>>>> (I
>>>> guess) involves verification of safe memory disposal.  And I just
>>>> learned
>>>> from a classic textbook (https://www.cs.cmu.edu/~jcr/copenhagen08.pdf)
>>>> that
>>>> verification of safe memory disposal requires classical separation
>>>> logic..
>>>>
>>>> Best,
>>>> Jeehoon
>>>>
>>>> PS. Sorry for cluttering everyone's inbox by sending a lot of emails..
>>>> I
>>>> will at least try to say something useful.  Thank you for answering all
>>>> the
>>>> questions!
>>>>
>>>> --
>>>> Jeehoon Kang (Ph.D. student)
>>>> Software Foundations Laboratory
>>>> Seoul National University
>>>>
>>>> --
>>>> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
>>>> Management: https://lists.mpi-sws.org/listinfo/iris-club
>>>> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org
>>>>
>
>
> --
> iris-club at lists.mpi-sws.org - Mailing List for the Iris Logic
> Management: https://lists.mpi-sws.org/listinfo/iris-club
> Unsubscribe: iris-club-unsubscribe at lists.mpi-sws.org