[Iris-Club] Classical version of Iris?

Joseph Tassarotti jtassaro at andrew.cmu.edu
Sun Aug 14 18:55:29 CEST 2016

We used linearity instead of something like what you're proposing 
because we need more than partial correctness. For us, the triple {P} e 
{x. Q} is supposed to ensure that if e diverges (fairly) then the source 
program represented by P also has a fair diverging execution. (There is 
a second extension needed to make this work, beyond the linearity). But, 
the up-shot is this means that it's not good enough to just have the 
post-condition Q stipulate the return of all of the receipts.

Of course, for tracking memory in the setting of partial correctness, 
what you propose seems like it would work (although I cannot speak to 
the convenience). Another advantage of what you suggest is that it is 
easily extended not just to let you track the absence of memory leaks, 
but also to prove an upper bound on space usage. So, I agree with you 
that linearity seems like a red herring when it comes to resource usage, 
at least in the ways it has conventionally been used for that purpose.


On 08/14/2016 11:39 AM, Derek Dreyer wrote:
> 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

More information about the Iris-Club mailing list