[Iris-Club] Classical version of Iris?

[Joseph Tassarotti]

Ralf, Bob, and I have developed a version of Iris based on linear BI in 
our POPL submission. I mean "linear" in the sense that P * Q does not 
necessarily entail P, in contrast to the "affine" set-up in the original 
Iris (I personally find the "intuitionistic"/"classical" separation 
logic terminology confusing). This is part of an extension to Iris that 
we developed for proving fair termination-preserving refinements between 
a source and target language. We have certain resources that represent 
threads of the source program, and in order to make sure that the 
refinement is termination preserving, we needed to precisely track these 
resources and prevent threads from "throwing them away".

Since we only needed to track these "source-thread" resources so 
carefully and did not care about others, we have an additional modality 
A, which indicates that a proposition is "affine" and can be thrown 
away, i.e. P * A(Q) |- P.

The question arises as to whether knowledge of an invariant should be 
affine. That is, writing [P] for knowledge of invariant P, should we 
have [P] |- A([P])? For various reasons related to other aspects of our 
extensions, we decided the answer should be yes. However, this is 
problematic for exactly the reason Derek alluded to in his second email: 
one could "hide" resources by storing them in an invariant and then 
throw the invariant away! Our work-around for this was to require that 
in order to establish invariant [P] you had to have a proof of A(P). 
Since we did not need to transfer ownership of our source-thread 
resources using invariants in our example proofs, this limitation was 
fine for us.

But, that clearly does not work if the resource you want to track 
precisely is something like memory, in which case you very much want to 
transfer it between threads using invariants. Then, invariants would 
have to be non-affine in general so you could not throw them away.


On 08/14/2016 09:12 AM, Derek Dreyer wrote:
> 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?

-Joe

>
> 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
>>>